[Caml-list] Subtyping of phantom GADT indices?

[Josh Berdine <josh@berdine.net>]

I wonder if anyone has any suggestions on approaches to use GADTs with a type parameter that is phantom and allows subtyping.

(My understanding is that the approach described in 
"Gabriel Scherer, Didier Rémy. GADTs meet subtyping. ESOP 2013"
hasn't entirely been settled on as something that ought to be implemented in the compiler. Right? Is there anything more recent describing alternatives, concerns or limitations, etc.?)

As a concrete example, consider something like:
```
type _ exp =
  | Integer : int -> [> `Integer] exp
  | Float : float -> [> `Float] exp
  | Add : ([< `Integer | `Float] as 'n) exp * 'n exp -> 'n exp
  | String : string -> [> `String] exp
```
The intent here is to use polymorphic variants to represent a small (upper semi-) lattice, where basically each point corresponds to a subset of the constructors. The type definition above is admitted, but while the index types allow subtyping:
```
let widen_index x = (x : [`Integer] :> [> `Integer | `Float])
```
this does not extend to the base type:
```
# let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
Line 1, characters 18-67:
1 | let widen_exp x = (x : [`Integer] exp :> [> `Integer | `Float] exp);;
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Type [ `Integer ] exp is not a subtype of
         ([> `Float | `Integer ] as 'a) exp 
       The first variant type does not allow tag(s) `Float

```
This makes sense since `type _ exp` is not covariant. But trying to declare it to be covariant doesn't fly, yielding:
```
Error: In this GADT definition, the variance of some parameter
       cannot be checked
```

I'm not wedded to using polymorphic variants here, but I have essentially the same trouble using a hierarchy of class types (with different sets of `unit` methods to induce the intended subtype relation) to express the index lattice. Are there other options?

I also tried using trunk's injectivity annotations (`type +!_ exp = ...`) on a lark since I'm not confident that I fully understand what happens to the anonymous type variables for the rows in the polymorphic variants. But that doesn't seem to change things.

Is this sort of use case something for which there are known encodings? In a way I'm trying to benefit from some of the advantages of polymorphic variants (subtyping) without the drawbacks such as weaker exhaustiveness and less compact memory representation by keeping the polymorphic variants in a phantom index. Is this approach doomed?

Cheers, Josh