Type equalities, extending to type constructors

Learning
1

Hi all,

I want to have a value that allows me to identify two apparently distinct types:

type (_,_) ty_eq = Ty_eq : ('a,'a) ty_eq


module M(X: sig
    type a
    val x : a
    val e: (a,int list) ty_eq
end) = struct
  open X

  let f =
    match e with
    | (Ty_eq : (a,int list) ty_eq) -> 
      (x:a) = [1]  (* type a is known to be equal to int list *)      
end

This seems to work OK. So I wonder about whether this extends to type constructors like list:

module N(S:sig
    type 'a t
    val x: int t
    val e: ('a t,'a list) ty_eq
end) = struct
  open S

  let f = 
    match e with
    | (Ty_eq : (int S.t, int list)ty_eq) ->
      (* it seems that the type system doesn't know that int S.t = int
         list here, ie, that type equalities don't extend to type
         constructors *)
      x=([]:int list)

end

Unfortunately it seems it doesn’t. My guess is that there is some well-known way to achieve want I want. Can someone help me?

Thanks

2

One technique is to define a function conv : ('a, 'b) ty_eq -> 'a -> 'b:

let conv (type a b) (te : (a, b) ty_eq) (x : a) : b =
  match te with Ty_eq -> x

module N (S : sig
    type 'a t

    val x : int t
    val e : ('a t, 'a list) ty_eq
  end) =
struct
  open S

  let f =
    conv e x = ([] : int list)
  ;;
end

This technique is employed in Base.Type_equal, which is where I learned about it. I don’t know why it works, other than this comment:

    In a program that has [t : (a, b) t] where one has a value of type [a] that one wants
    to treat as a value of type [b], it is often sufficient to pattern match on
    [Type_equal.T] rather than use [conv].  However, there are situations where OCaml's
    type checker will not use the type equality [a = b], and one must use [conv].  For
    example:
1 Like
3

Thanks! That is a useful link. Still, would be nice to understand what the type checker is doing on a slightly deeper level…

4

The short answer is that pattern matching on GADT can only refine abstract types. In the definition of conv, this works due to the locally abstract types:

let conv (type a b) (Ty_eq: (a,b) ty_eq) (x:a) = (x:b)

Your first example also works fine because X.a is abstract. But in your second example S.t is no longer an abstract type but a type constructor which means that you cannot refine it anymore. Using conv is a way to circumvent this issue.

1 Like