# Unexpected warning with GADT and empty types

**URL:** <https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724>\
**Category:** Learning\
**Created:** [October 15, 2018, 3:31pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724 "2018-10-15T15:31:30Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![n47](https://avatars.discourse-cdn.com/v4/letter/n/7feea3/32.png) [@n47](https://discuss.ocaml.org/u/n47)\
**Post date:** [October 15, 2018, 3:31pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724/1 "2018-10-15T15:31:30Z")

</div>

Hi, I came across an unexpected warning while playing with GADTs.

Here is the code.

```
module G : sig
  type t_foo = |
  type t_bar = |
end = struct
  type t_foo = |
  type t_bar = |
end

type _ t_gadt =
  | Foo : G.t_foo t_gadt
  | Bar : G.t_bar t_gadt

let to_string (x:G.t_foo t_gadt) : string =
  match x with
  | Foo -> "foo"

File "test.ml", line 54, characters 2-31:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Bar

```

Here, since G.t\_foo and G.t\_bar are different types, I would expect the compiler to detect that Foo is the only possible constructor for x. And it does detect it if I get rid of the module G.

Am I missing something? Is is a known limitation?

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [October 15, 2018, 3:58pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724/2 "2018-10-15T15:58:22Z")

</div>

This is a classical problem with type inequalities. Outside of the definition of `G`, the typechecker does not have enough information to know for sure that `t_foo` ≠ `t_bar` because `G` could have been implemented as

```auto
type (_,_) eq = Eq: ('a,'a) eq
module G: sig
  type a = |
  type b = |
  val eq: (a,b) eq
end = struct
   type a = |
   type b = a = |
   let eq = Eq
end

```

The problem does not exist inside of the definition of the module defining `a` and `b` because the typechecker can know for sure if the two type are independent or not.  
Note that a possible workaround is to add an unique private constructor to `t_foo` and `t_bar`.

---

<div class="post-metadata">

**Author:** ![n47](https://avatars.discourse-cdn.com/v4/letter/n/7feea3/32.png) [@n47](https://discuss.ocaml.org/u/n47)\
**Post date:** [October 15, 2018, 4:23pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724/3 "2018-10-15T16:23:09Z")

</div>

Ok, thank you.  
I thought exposing the type definitions in the signature was enough.  
And also I didn’t know one can write

```auto
type b = a = |

```

In what kind of situation is this construct (type a = b = something) useful?

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [October 15, 2018, 4:31pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724/4 "2018-10-15T16:31:53Z")

</div>

For more classical variant type, it can be useful to re-export the constructors.  
For instance, if I have a type

```OCaml
module M = struct
  type t = A | B
end

```

then the following

```OCaml
module N = struct type t = M.t end
let x = N.A

```

raises an error

> Error: Unbound constructor N.A

whereas

```OCaml
module N = struct type t = M.t = A | B end
let x = N.A

```

is fine.

For instance, it can occur that you need to define a type earlier than its main module (to avoid some circular dependencies for instance). In this case, it might make sense to completely reexport the type in this main module.

---

<div class="post-metadata">

**Author:** ![n47](https://avatars.discourse-cdn.com/v4/letter/n/7feea3/32.png) [@n47](https://discuss.ocaml.org/u/n47)\
**Post date:** [October 15, 2018, 6:49pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724/5 "2018-10-15T18:49:29Z")

</div>

Yes I see how re-exporting might be useful. Thanks again.

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [January 21, 2022, 10:33pm UTC](https://discuss.ocaml.org/t/unexpected-warning-with-gadt-and-empty-types/2724/6 "2022-01-21T22:33:55Z")

</div>

I just thought I would point out, for the benefit of future readers of this thread, that for the suggested workaround (adding a unique private constructor to `t_foo` and `t_bar`) to work, the two constructors added to `t_foo` and `t_bar` must have _different names_. This was not obvious to me, although in hindsight I can see why the same issue would arise.