Hello! I’ve been playing with GADTs and I found a very interesting problem. I seem to be getting `Warning 8: this pattern-matching is not exhaustive.`, when the pattern-matching should be exhaustive.

Here is my minimal example:

``````module FailsWithWarning = struct
module Nat = struct
type zero

type positive

type 'n s = S : 'n -> 'n s

type ('m, 'n, 'typ) t =
| Z : ('m, 'm, zero) t
| S : ('m, 'n, 'any) t -> ('m, 'n s, positive) t
end

type ('a, 'length) hlist =
| [] : ('b, ('m, 'm, Nat.zero) Nat.t) hlist
| ( :: ) :
'a * ('b, ('m, 'l, 'typ) Nat.t) hlist
-> ('a -> 'b, ('m, 'l Nat.s, Nat.positive) Nat.t) hlist

type a. (a -> 'b, ('m, 'l Nat.s, Nat.positive) Nat.t) hlist -> a = function
| x :: _ -> x
end

module NoWarning = struct
type zero

type positive

type 'n s = S : 'n -> 'n s

type ('m, 'n, 'typ) t =
| Z : ('m, 'm, zero) t
| S : ('m, 'n, 'any) t -> ('m, 'n s, positive) t

type ('a, 'length) hlist =
| [] : ('b, ('m, 'm, zero) t) hlist
| ( :: ) :
'a * ('b, ('m, 'l, 'typ) t) hlist
-> ('a -> 'b, ('m, 'l s, positive) t) hlist

type a. (a -> 'b, ('m, 'l s, positive) t) hlist -> a = function
| x :: _ -> x
end
``````

I’m guessing that the type unification must have some module bounds. It can infer it correctly when all types are in the same module but not across modules.

Any idea what could be causing the issue?

1 Like

In brief, when defining type-level tags, you should always define them with a private constructor:

``````type zero = private Zero_tag
type positive = private Positive_tag
``````

Otherwise the typechecker cannot prove their inequalities. Indeed, without those incompatible constructors, the typechecker cannot rule out this situation:

``````type (_,_) eq = Refl: ('a,'a) eq
module M: sig
type a
type b
val eq_or_not: (a,b) eq option
end = struct
type a
type b = a
let eq_or_not = Some Refl
end
``````

Unfortunately, there is a special rule in the typechecker for abstract types defined in the current module
that makes it possible to write

``````type a
type b
let nevert: 'f . (a,b) eq -> 'f = function _ -> .
``````

But this special cases breaks as soon as one leaves the current module or move the definition to a submodule as you have experimented.

4 Likes

That makes sense. Thanks a lot for the explanation!