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?

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:

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.