Type identifiers with phantom types

Learning
1

I use type identifiers in a pretty standard way, i.e.

type _ id = .. 
  
module type S = sig
  type t
  type _ id += K : t id 
end

type 'a t = (module S with type t = 'a)

let make (type a) () = (module struct
    type t = a
    type _ id += K : t id
  end : S with type t = a)

However, these aren’t polymorphic when used with phantom types:

# type 'a ex = Int : int ex ;;
type 'a ex = Int : int ex
# let ex_id : 'a ex t = make () ;;
val ex_id : '_a ex t = <module>

ex_id is weakly polymorphic, and gets concretized when used.

I tried using explicit polymorphic notation with abstract types, but that also (predictably) fails with the following error:

# let ex_id : type a. a ex t = make () ;;
Line 1, characters 4-36:
Error: This definition has type 'a ex t which is less general than 'a0. 'a0 ex t

Is it possible to construct an identifier for 'a t for all 'a in this instance?

2

You can only resort to

let ex_id () : _ ex t = male ()

since with a GADT you cannot rely on the relaxed value restriction.

3

Bummer. That’s not an ideal solution, since every call to ex_id creates a new K and thus a new identifier, making tasks like constructing equality witnesses impossible.

Thanks again, @octachron

4

If it were possible to construct ex_id : type a. a ex t, then the following function would type-check:

let cast (type a b) (x : a) : b =
  let module A = (val (ex_id : a ex t)) in
  let module B = (val (ex_id : b ex t)) in
  match A.K with
  | B.K -> x
  | _ -> assert false

I don’t know what would be a type-safe form for identifiers of type families.

(EDIT: I first wrote cast : 'a 'b. 'a ex -> 'b ex, but it is even more convincing with cast : 'a 'b. 'a -> 'b)

5

Yeah, this is why I initially assumed it wasn’t possible, as proving equality between two instances of 'a ex was my initial intent. The way I kind of solved this was by wrapping ex in an existential (sorry, in hindsight maybe ex was a bad choice) and using some other ID’s.

type exist = E : 'a ex -> exist

let exist_id : exist t = make ()

let int_id : int t = make ()

let inner_id : type a. a ex -> a t = function
  | Int -> int_id

Using these you can pack ex inside the existential and use the inner ID’s to recover the inner type.