Re: [Caml-list] Strange interaction between recursive modules, GADT exhaustiveness checking and type-checking?

["Grégoire Henry" <gregoire.henry@ocamlpro.com>]

Hi,

  I believe the presence of recursive module has nothing to do with
this particular warning. But, in general, the exhaustiveness-check
can't assume that two abstract types are distinct, as they may be
equal in some other typing context. In your code example, there is no
such typing context. But, for instance, imagine the following program:

  module rec W : sig

    type a
    type b

    type (_, _) t =
      | AA : (a, a) t
      | AB : (a, b) t
      | BB : (b, b) t

    type 'a w =
      | W : ('a, 'b) W.t * 'b -> 'a w

    val x : a w

  end = struct

    type a = unit
    type b = unit

    type (_, _) t =
      | AA : (a, a) t
      | AB : (a, b) t
      | BB : (b, b) t

    type 'a w =
      | W : ('a, 'b) W.t * 'b -> 'a w

    let x : a w = W (BB, ())

  end

  open W

  type s =
    | A of a
    | B of b

  let f : a w -> s = function
    | W (AA, a) -> A a
    | W (AB, b) -> B b
    (* Warning *)

  let _ = f x (* Match_failure *)

In general, it is rather difficult to decide if there exists a typing
context where two abstract types may be considered as equal. And even
more complex with separate compilation.

As a consequence, while testing the exhaustiveness of a pattern-matching,
the type-checker has to assume that 'W.a' and 'W.b' might be equal.

  let f3 : a w -> s = function
    | W (AA, a) -> A a
    | W (AB, b) -> B b
    | W (BB, b) -> B b

In particular, while type-checking the third branch of [f3], the
type-checker assumes that 'W.a = W.b'. This is safe, as the existence
of a value 'W (BB, b)' of type 'a w' can be seen as a proof of this
equality: in the typing context where the value was built, the two
types have to be equals.

Your first example is a particular case where we could assume that
'W.a' and 'W.b' are distinct. They are 'fully abstract types', they
have no inhabitants. They were introduced in current typing context
(and not imported from the signature of another module) and we known
they are distinct.

HTH,
Grégoire