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

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

[Nicolas Trangez]

All,

I was working on some code lately (admittedly, pushing some boundaries
w.r.t. recursive modules & GADTs), and got some confusing results.

All of this using OCaml 4.01.0, using `-w +A -warn-error +A`.

I tried to break it down to a small test-case, which you can find at
https://gist.github.com/NicolasT/3a6ef50d5607b744206b

The first case, implemented in module `W`, works as expected. No
warnings about a pattern match for `W (BB, _)` missing in `W.f`. Jay!

When doing something fairly similar in a couple of recursive modules
below, things become confusing. The compiler warns about a missing case
for `W (T.BB, _)` in `S.f`, as noted above it, whilst I think that
pattern shouldn't even type-check... I validated this by adding some
code at the end (in the `demo` function), trying to call `S.f` with a
`B.b S.w` argument, and this fails (as expected & desired). So why would
I be forced, or even allowed, to match on this case in `S.f` at all?

Nicolas

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

[Grégoire Henry]

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

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

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 737 bytes --]

On 29 June 2014 15:49, Grégoire Henry <gregoire.henry@ocamlpro.com> wrote:

> 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.
>

This has bitten me before as well. It seems to me that whether or not a
type is abstract and whether or not it has any values should be essentially
independent characteristics, but it seems impossible to state in a
signature that a type has no constructors. So there's this property of
types that you can't preserve across module boundaries.

[-- Attachment #2: Type: text/html, Size: 1098 bytes --]