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

[Leo White <lpw25@cam.ac.uk>]

>> so that `int foo` is equal to `float foo`, then your match isn't really
>> exhaustive.
>
> How so?

Both constructors would then have the same type. Since it is possible
they both have the same type, you need to match on both of them.

> 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 -> ()
>

This is because `foo B` may not always be rejected. Consider the
following code:

    module F (Foo : sig type 'a foo end) = struct

      type _ t = A : int Foo.foo t
           | B : float Foo.foo t

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

      (* [foo B] would be an error here *)

    end

    module M = F(struct type 'a foo = unit end)

    (* But out here it is fine *)
    let () = M.foo M.B

> although
>
> let foo = function A | B -> ()
>
> unsurprisingly does not type.

That's due to GADTs not currently being compatible with or-patterns, it
is not related to the injectivity issues you are having.

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

Giving different behviour based on whether something is defined in the
same module is anti-modular, and confuses people when they try to split
their code across different modules.

> It's rather useful - the constructors of a GADT are
> partionable by type.

That is indeed useful, but only really works in OCaml if you expose the
definitions of these types, so that OCaml can see that they are
definitely not the same type. This is why you see people use:

    type z = Z

    type 'a s = S

when doing type-level arithmetic. By giving types with incompatible
definitions, rather than abstract types, OCaml can safely conclude they
are not the same 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.

The problem is that OCaml has no way to know that `int Foo.foo` is not
equal to `float Foo.foo` so it must insist that you include a case for
it. OCaml also doesn't know that `int Foo.foo` does equal `float
Foo.foo` so it can't let you call `foo Foo.B` either.

Regards,

Leo