GADTs and match cases

Learning
1

When using GADTs with pattern matching it seems like OCaml cannot always infer that certain match cases are impossible. For instance, consider:

type _ t =
| Indexed : Ident.t * index -> index t
| Leveled : Ident.t * level -> level t

let equal (type a) (x: a t) (y: a t) : bool = match x, y with
| Indexed (id, i), Indexed (id', i') -> Ident.equal id id' && Index.equal i i'
| Indexed _, _ -> false
| Leveled (id, l), Leveled (id', l') -> Ident.equal id id' && Level.equal l l'
| Leveled _, _ -> false

In the equal function, the second and fourth cases are impossible, because x: a t and y: a t, so the combinations Indexed _, Leveled _ and Leveled _, Indexed _ are impossible. Is there any way to get OCaml to see this?

2

Can you show us the definitions of the types index and level?
The compiler can deduce that the combinations Indexed _, Leveled _ and Leveled _, Indexed _ are impossible only if it can ensure that the types index and level are distinct.
If index and level are type aliases for the same type or, most probably, if they are both abstract, the compiler cannot ensure that they are distinct (see for instance, this previous discussion here: Unexpected GADT behavior when wrapping a type into a module).

Most probably, you do not rely on the fact that the type parameter of 'a t is either the type index or level themselves. Therefore, a solution can be to use another types to parameterize the result types of the constructors, for instance polymorphic variant types that are known to be distinct:

type _ t =
| Indexed : Ident.t * index -> [`index] t
| Leveled : Ident.t * level -> [`level] t
3

This happens when OCaml can’t tell that the types index and level are different, and thus you could have a = index = level which requires the cross cases. This crops up when your type are equal, or when they are opaque, the common case being hidden behind an interface:

module Index : sig type t end = struct type t = int end
module Level : sig type t end = struct type t = string end

type index = Index.t
type level = Level.t

If you want the compiler to tell them apart, you need to make your types transparent:

module Index : sig type t = int end = struct type t = int end
module Level : sig type t = string end = struct type t = string end

type index = Index.t
type level = Level.t

Another solution is to create special types just for your GADT cases:

type gadt_index = I
type gadt_level = J (* types with the same constructors are equal, so chose a different one *)

type _ t =
| Indexed : Ident.t * index -> gadt_index t
| Leveled : Ident.t * level -> gadt_level t
4

The compiler can’t refute these cases because it appears that with GADT two distinct abstract types can be proved equal in some circumstances:

type (_,_) eq = Refl : ('a,'a) eq

module type S = sig
  type t
  val e : t
  val eq : (int, t) eq
end

 module A : S = struct
  type t = int
  let e = 1
  let eq = Refl
end

module B : S = struct
  type t = int
  let e = 2
  let eq = Refl
end

(* type error *)
A.e = B.e;;
Error: This expression has type B.t but an expression was expected of type A.t

(* we're breaking type abstraction *)
 match A.eq, B.eq with Refl, Refl -> A.e = B.e;;
- : bool = false