Re: [Caml-list] Covariant GADTs

["Petter A. Urkedal" <paurkedal@gmail.com>]

Hi Markus,

On 17 September 2016 at 19:38, Markus Mottl <markus.mottl@gmail.com> wrote:
> 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.

In this case, you can supply the needed type information to `get_next`
with structural type matching:

  type _ t = Z : [`z] t | S : 'a t -> [`s of 'a] t
  let get_next : [`s of 'a] t -> 'a t = function S next -> next

This gives you a richer type which also allows defining get_next_pair, etc.

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

I had a similar problem myself and found a paper [1] explaining the
issue and a possible solution.  Haven't really studied it, but as I
understand the issue is that the current GADTs only introduce type
equality, which is too strict to verify variance.  What is needed is
more like (my ASCIIfication)

  type +'a t =
    | Z when 'a >= [`z]
    | S when 'a >= [`s] of [< `z | `s] t

allowing 'a in each case to be a supertype rather than equal to the
specified type.  In that spirit, I tried

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

but that does not check for variance either.

Best,
Petter

[1] https://arxiv.org/abs/1301.2903