# GADTs and match cases

**URL:** <https://discuss.ocaml.org/t/gadts-and-match-cases/13773>\
**Category:** Learning\
**Created:** [January 3, 2024, 4:25pm UTC](https://discuss.ocaml.org/t/gadts-and-match-cases/13773 "2024-01-03T16:25:19Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![jordydickinson](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/jordydickinson/32/4983_2.png) [@jordydickinson](https://discuss.ocaml.org/u/jordydickinson)\
**Post date:** [January 3, 2024, 4:25pm UTC](https://discuss.ocaml.org/t/gadts-and-match-cases/13773/1 "2024-01-03T16:25:19Z")

</div>

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

```auto
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?

---

<div class="post-metadata">

**Author:** ![thierry-martinez](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/thierry-martinez/32/1481_2.png) [@thierry-martinez](https://discuss.ocaml.org/u/thierry-martinez)\
**Post date:** [January 3, 2024, 4:38pm UTC](https://discuss.ocaml.org/t/gadts-and-match-cases/13773/2 "2024-01-03T16:38:55Z")

</div>

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](https://discuss.ocaml.org/t/unexpected-gadt-behavior-when-wrapping-a-type-into-a-module/5707)).

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:

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

```

---

<div class="post-metadata">

**Author:** ![dlesbre](https://avatars.discourse-cdn.com/v4/letter/d/bbce88/32.png) [@dlesbre](https://discuss.ocaml.org/u/dlesbre)\
**Post date:** [January 3, 2024, 4:45pm UTC](https://discuss.ocaml.org/t/gadts-and-match-cases/13773/3 "2024-01-03T16:45:26Z")

</div>

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:

```ocaml
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:

```ocaml
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:

```auto
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

```

---

<div class="post-metadata">

**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\
**Post date:** [January 3, 2024, 4:46pm UTC](https://discuss.ocaml.org/t/gadts-and-match-cases/13773/4 "2024-01-03T16:46:15Z")

</div>

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

```ocaml
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

```