[Caml-list] Covariant GADTs

[Markus Mottl <markus.mottl@gmail.com>]

Hi,

GADTs currently do not allow for variance annotations so I wondered
whether there are any workarounds for what I want:

-----
type +_ t =
  | Z : [ `z ] t
  | S : [ `z | `s ] t -> [ `s ] t

let get_next (s : [ `s ] t) =
  match s with
  | S next -> next
-----

The above compiles without the variance annotation, but then you
cannot express "S Z", because there is no way to coerce Z to be of
type [`z | `s] t.

Another approach I tried is the following:

-----
type _ t =
  | Z : [ `z ] t
  | S : [< `z | `s ] t -> [ `s ] t

let get_next (s : [ `s ] t) : [< `z | `s ] t =
  match s with
  | S next -> next
-----

The above gives the confusing error:

-----
Error: This expression has type [< `s | `z ] t
       but an expression was expected of type [< `s | `z ] t
       The type constructor $S would escape its scope
-----

There are apparently two type variables associated with [< `s | `z ]
t: the locally existential one introduced by matching the GADT, and
the one in the type restriction of the function, but the compiler
cannot figure out that these can be safely unified.  There is
currently no way of specifying locally abstract types that have type
constraints, which could possibly also help here.

Are there workarounds to achieve the above?  Are there any plans to
add variance annotations for GADTs?

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com