The way GADTs are handled is that local constraints are generated when patterns are typed and then those constraints are used in the body of the associated clause. To generate the constraints, we need to propagate typing information. From my understanding, we can't do this with polymorphic variants because it would change the typing algorithm. In other words, with polymorphic variants the type of the pattern is infered independently of the context.
>From my understanding, Jacques Garrigue has good reasons to reject propagation in such a case. Personally, I'd like to see a flag, say -unsafepropagation, to let people use polymorphic variants and GADTs at their own risk, knowing that the behaviour of the typing algorithm may not satisfy some expected theoretical properties. On Tue, Dec 13, 2011 at 9:35 AM, Dario Teixeira <[email protected]> wrote: > Hi, > I wonder, is there any theoretical reason why GADTs cannot be associated with > polymorphic variants? As an example, consider the two type declarations > below. > The first is your run-of-the-mill GADT, supported by the current SVN trunk. > The > second is a PV-GADT, which is not accepted. But is this just a present > limitation > or a fundamental one? > > type _ t1 = Foo: int t1 | Bar: float t1 > > type _ t2 = [ `Foo: int t2 | `Bar: float t2 ] > > > Thanks in advance for your input! > Cheers, > Dario Teixeira > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
