Problem with subtyping in polymorphic variant in gadt

Learning
,
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