Hi,

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

Thanks for the clarification.  Mind you, my question did not stem from any
actual need for PV-GADTS; it was pure curiosity...

Cheers,
Dario


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

Reply via email to