# Problem with subtyping in polymorphic variant in gadt

Hello, I was playing around with polymorphic variant in gadt. And I get some problem with subtyping.

i.e I have type

``````# type int_ = [ `Int ];;
# type real = [ `Int | `Float ];;
``````

With list, I can do

``````# let int_list : int_ list = [];;
# (int_list :> real list);;
- : real list = []
``````

But I am unable to achieve the same thing with gadt.

``````# type _ t = | Int : int_ t | Real : real t;;
# (Int :> real t);;
Error: Type int_ t is not a subtype of real t
The first variant type does not allow tag(s) `Float
``````

I know if I replace `Int : int_ t` with something like `Int : [> `Int] t`, it will work. But if want to abstract the type, OCaml does not allow me to do `type int_ = [> `Int ]`. Is there a way for me to get around this? Thank you.

1 Like

Hi @erebuxy,

Broadly speaking, your problem is that β even if `int_` is a subtype of `real` β itβs not the case that `int_ t` is a subtype of `real t` for an arbitrary type `t`, and your example demonstrates this. In particular, since the `Int` and `Real` cases of the GADT have provably non-equal type parameters, I can use this to force a choice of one or the other:

``````type _ t =
| Int  : [ `Int ] t
| Real : [ `Int | `Float ] t

(* No exhaustivity warnings β these functions are total *)
let get_int  : [ `Int ]          t -> unit = fun Int -> ()  ;;
let get_real : [ `Int | `Float ] t -> unit = fun Real -> () ;;
``````

This hopefully sheds some light on why itβs not possible to coerce a `int_ t` into a `real t`: `int_ t` is a type containing exactly one term `Int`, and `real t` contains exactly one term `Real`. As you suggest, you probably want to keep the polymorphic variants open (to leave the possibility that the terms `Int` and `Real` can be given the same type):

``````(* option 1 β keep type params on type tags *)
type 'a int_ = [> `Int ] as 'a
type 'a real = [> `Int | `Float ] as 'a

type _ t =
| Int : _ int_ t
| Real : _ real t

(* option 2 β reopen type tags inside GADT *)
type int_ = [ `Int ]
type real = [ `Int | `Float ]

type _ t =
| Int : [> int_ ] t
| Real : [> real ] t
``````

These options are equivalent, so itβs up to you. Either way, our new definitions allow the coercion you want:

``````# (Int :> [> real ] t);;
- : [> real ] t = Int
``````
3 Likes