GADT pattern matching exhaustiveness

Community
,
1

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

  let safe_head :
    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

  let safe_head :
    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
2

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
3

That makes sense. Thanks a lot for the explanation!