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

[Ashish Agarwal <agarwal1975@gmail.com>]

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

Thanks for the link to the Mantis issue.

On Fri, Nov 21, 2014 at 4:04 PM, Leo White <lpw25@cam.ac.uk> wrote:

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

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