Re: [Caml-list] Question on the covariance of a GADT (polymorphic

[Oleg <oleg@okmij.org>]

> type 'a t =
>    | Wine: [> `Wine ] t
>    | Food: [> `Food ] t
>    | Box : 'a t * 'a t -> 'a t
>    | Fridge: [< `Wine | `Food ] t -> [> `Fridge ] t
>
> In this definition, the type parameter 'a is a phantom parameter. It is not
> used to describe the type of a value; it is used only to restrict the set of
> values of type "t" that can be constructed.
>
> The goal here is to allow storing wine and food (and boxes containing
> boxes containing wine and food) in a fridge, but forbid storing a
> fridge in a fridge (or a fridge in a box in a fridge, etc.).

This is indeed a very `popular' problem. On June 21 this year Josh
Berdine posed almost the same question (without wine and food, alas).
On 28 June 2020 I sent the reply with three solutions. Perhaps it
would be easier to point to the code, which also has many comments and
explanations:

        http://okmij.org/ftp/tagless-final/subtyping.ml

The gist of the first two solutions is to exploit the fact that
tagless-final is sort of isomorphic to GADTs. That is, lots of things
that can be done with GADTs can be done without (or with GADTs hidden
away). That hiding has benefit of no longer bringing the problems with
variance. No GADTs (at least, not in the part facing the user), no
variance problems, at least, not for the end user. The library author
may use regular ADT, which are also non-problematic. A regular ADT
doesn't have the same typing guarantees -- but the typing is enforced
by the signature (at the module level), so there is no loss.

I was going to write an article for my web site explaining this and a
few earlier answers to the similar problems. Maybe I will eventually
get to it.