Re: [Caml-list] GADTs and parsers

[Dario Teixeira <darioteixeira@yahoo.com>]

Hi,

And thanks for the prompt reply!

> I suspect the problem may be one of variance: you are using

> polymorphic variants, but implicitly assuming that ([ `Nolink ]
> inline_t) is a subtype of ([ `Nolink | `Link ] inline_t), which means
> that "inline_t" is covariant in its first parameter. However, variance
> of GADTs is currently very strict, and your inline_t definition is in
> fact considered invariant (to check that, replace "type _ inline_t" by
> "type (+'a) inline_t" and watch the error), so this conversion does
> not pass. On the contrary, with a phantom type definition, the
> parameter is inferred to be irrelevant (any variance is accepted), so
> you can do whatever you want inside the abstraction boundary.

Ah, indeed.  And on a related note: is there a way to get the compiler
to spill out the variance it infers?  I'm assuming that 'ocamlc -i' does
not include inferred variance because it is generally "obvious" and
not something you usually have to worry about unless you want to
make a type abstract.  However, in a case like this it would help.
(Or does the compiler *always* assume invariance with GADTs?)


> (For more information on GADTs and variance, see the previous thread
> on this on the mailing-list; the summary is that it's complicated, but
> I still hope we could get something finer in the future. It would
> probably not work with polymorphic variant instances, anyway.)

In this case the use of polymorphic variants for the type parameter comes
in handy because there is a subtyping relation and the [> ] declaration
allows for useful mixing:

# let x1 = Text "ola";;
val x1 : [> `Nonlink ] inline_t = Text "ola"

# let x2 = Link "lnk";;
val x2 : [> `Link ] inline_t = Link "lnk"

# let xs = [x1; x2];;
val xs : [> `Link | `Nonlink ] inline_t list = [Text "ola"; Link "lnk"]

Cheers,
Dario