Re: [Caml-list] OR-patterns with GADTs

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

Ashish Agarwal <agarwal1975@gmail.com> writes:

> The following works fine:
>
> type foo
> type bar
> type _ t =
> | Foo : string -> foo t
> | Bar : string -> bar t
>
> let to_string : type a . a t -> string = function
>   | Foo x -> x
>   | Bar x -> x
>
> However, if you try to avoid the redundant code of the two branches, you get a compile error:
>
> let to_string : type a . a t -> string = function
>   | Foo x
>   | Bar x -> x
>
> Error: This pattern matches values of type foo t
>        but a pattern was expected which matches values of type a t
>        Type foo is not compatible with type a
>
> Is there a real reason for this?

I think the reason is that full support for or-patterns with GADTs is
difficult. Matching on one GADT pattern generates one set of equations
and matching on the other generates a different set of equations and you
then need to check the body under the (parts of the) equations that are
in both patterns. There might be something simpler than full support
which wouldn't be that hard, but its not clear what that would be, so at
the moment things just fail if you use GADTs in an or-pattern.

There is a Mantis issue for it
(http://caml.inria.fr/mantis/view.php?id=5736), so hopefully it will be
resolved one day.

Regards,

Leo