Problem with subtyping in polymorphic variant in gadt

Learning
,
1

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
2

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:

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