RE: [Caml-list] Match error with abstract types in modules

[David Allsopp <dra-news@metastack.com>]

Leo White wrote:
> > Please could someone remind me what it is about types in modules which
> > means that
> >
> >   module Foo = struct
> >     type 'a foo
> >   end
> >
> >   type _ t = A : int Foo.foo t
> >            | B : float Foo.foo t
> >
> >   let foo A = ()
> >
> > is non-exhaustive pattern matching, but:
> >
> >   type 'a bar
> >
> >   type _ u = C : int bar u
> >            | D : float bar u
> >
> >   let bar C = ()
> >
> > is exhaustive? Or is it actually a bug (given that foo B is a type
> error)?
> >
> 
> If Foo is replaced with:
> 
>     module Foo : sig
>       type 'a foo
>     end = struct
>       type 'a foo = unit
>     end
> 
> so that `int foo` is equal to `float foo`, then your match isn't really
> exhaustive.

How so? What's (very) confusing to me is that it seems to permit nonsensical matches without warning. In both the unconstrained and constrained versions of Foo, the resulting type of the function [foo] is [int Foo.foo t -> unit] so [foo B] is always rejected. But you get no warning about an unusable match case with:

let foo = function A -> () | B -> ()

although 

let foo = function A | B -> ()

unsurprisingly does not type.

> In the second version, the compiler cheats. Since `bar` is definied in the
> same module, it knows that the abstract `bar` type it can see is actually
> the definition, not just an abstraction of a type defined elsewhere, so it
> knows that `int bar` cannot equal `float bar`.
> 
> Personally, I dislike this behaviour and would prefer both cases to give
> an error.

What's to dislike? It's rather useful - the constructors of a GADT are partionable by type. What caught me out was that two constructors with distinct types (in my actual use with different instantiations of 'a BatSet.t) were being regarded as equal in terms of pattern matching. I'd be quite happy if a type annotation were necessary to make it explicit that I meant to do it:

let foo (key : int Foo.foo t) =
  match key with A -> ()

Especially with that explicit type, I find it very odd to get a warning about a constructor whose type is not permitted in this context and so cannot be matched.

Ta for the explanation behind the difference in behaviour, regardless!


David