Unexpected warning with GADT and empty types

Learning
1

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?

1 Like
2

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

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.

4 Likes
3

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

type b = a = |

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

4

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

module M = struct
  type t = A | B
end

then the following

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

raises an error

Error: Unbound constructor N.A

whereas

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.

5

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

6

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.