# Problem with subtyping in polymorphic variant in gadt

**URL:** <https://discuss.ocaml.org/t/problem-with-subtyping-in-polymorphic-variant-in-gadt/6650>\
**Category:** Learning\
**Tags:** polymorphism, gadt\
**Created:** [October 24, 2020, 5:02am UTC](https://discuss.ocaml.org/t/problem-with-subtyping-in-polymorphic-variant-in-gadt/6650 "2020-10-24T05:02:52Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![bn-d](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bn-d/32/6471_2.png) [@bn-d](https://discuss.ocaml.org/u/bn-d)\
**Post date:** [October 24, 2020, 5:02am UTC](https://discuss.ocaml.org/t/problem-with-subtyping-in-polymorphic-variant-in-gadt/6650/1 "2020-10-24T05:02:52Z")

</div>

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

i.e I have type

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

```

With list, I can do

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

```

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

```ocaml
# 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.

---

<div class="post-metadata">

**Author:** ![CraigFe](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/craigfe/32/1989_2.png) [@CraigFe](https://discuss.ocaml.org/u/CraigFe)\
**Post date:** [October 24, 2020, 9:40am UTC](https://discuss.ocaml.org/t/problem-with-subtyping-in-polymorphic-variant-in-gadt/6650/2 "2020-10-24T09:40:36Z")

</div>

Hi @bn-d,

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:

```ocaml
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):

```ocaml
(* 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:

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

```