GADTs with actual type parameters need an intensional type

[brandonzstride]

We would like to encode GADTs using dependent type parameters, where we can intensionally refine the type.

Here is one such GADT encoding.

type term = Mu term. 
  {: a : type (* dependent record here *)
   ; v = 
    | `T_Lift of a
    | `T_Int of { int | fun _ -> a = int } (* refine a to be int by comparing types *)
    | `T_Bool of { bool | fun _ -> a = bool }
    | `T_Add of { r : { left : term ; right : term } | a = int && r.left.a = int && r.right.a = int }
    | `T_Pair of { r : { left : term ; right : term } | is_product a && r.left.a = a.leftt && r.right.a = a.rightt }

let rec eval (x : term) : x.a =
  match x.v with
  | `T_Lift y -> y
  | `T_Int n -> n
  | `T_Bool b -> b
  | `T_Add r -> eval r.left + eval r.right
  | `T_Pair r -> { left = eval r.left ; right = eval r.right }

We would simply refine x.a if we wanted to only handle some cases in eval.

Since Bluejay only supports so many types, and any type-as-expression can be encoded with nondeterminism, we can generate any intensional type (called itype for example), and we structurally compare on it. This would be slow in practice, but it theoretically, it would work. So in the above example, we would have a : itype instead of a : type.