Re: [Caml-list] PV-GADTs

[Dario Teixeira <darioteixeira@yahoo.com>]

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