WIP

client/Infer.ml

@@ -219,6 +219,9 @@ let rec convert_deep (env : ML.datatype_env) (params : (string * variable) list)
   | ML.TyConstr (_, tid, tys) ->
      DeepStructure (S.TyConstr(tid, List.map conv tys))
 
+  | ML.TyEq (_, _ty1, _ty2) ->
+     failwith "todo"
+
 let convert env params ty =
   let deep_ty = convert_deep env params ty in
   deep deep_ty
@@ -375,6 +378,9 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
         and+ ty = decode w
         in F.Match (pos, ty, t, branches')
 
+    | ML.Eq _ ->
+        
+
     | ML.Hole (pos, ts) ->
       (* A hole ...[t1, t2, .., tn] has any type, and its subterms
          [t1, .., tn] can themselves have any type; our return type

client/ML.ml

@@ -22,6 +22,7 @@ type typ =
   | TyArrow of range * typ * typ
   | TyProduct of range * typ list
   | TyConstr of range * Datatype.TyConstrId.t * typ list
+  | TyEq of range * typ * typ
  [@@deriving compare]
 
 type type_annotation = tyvar list * typ [@@deriving compare]
@@ -38,6 +39,8 @@ type term =
   | LetProd of range * tevar list * term * term
   | Variant of range * Datatype.LabelId.t * term Option.t
   | Match of range * term * branch list
+  | Eq of range
+  | Use of range * term * typ * term
 
 and branch = pattern * term
 

client/ML2F.ml

@@ -22,6 +22,8 @@ let rec translate_type (translate_tyvar : ML.tyvar -> F.nominal_type) (ty : ML.t
       F.TyProduct (List.map trans tys)
   | ML.TyConstr (_, tyconstr, tys) ->
       F.TyConstr (tyconstr, List.map trans tys)
+  | ML.TyEq (_, _ty1, _ty2) ->
+      failwith "todo"
 
 (* Translate a ML datatype description into a nominal System F version *)
 let translate_datatype tdescr =

client/MLPrinter.ml

@@ -13,6 +13,8 @@ let rec translate_type (ty : ML.typ) : P.typ =
       P.TyProduct (List.map self tys)
   | ML.TyConstr (_, lbl, tys) ->
       P.TyConstr (lbl, List.map self tys)
+  | ML.TyEq (_, ty1, ty2) ->
+      P.TyEq (self ty1, self ty2)
 
 let print_type (ty : ML.typ) =
   Printer.print_type (translate_type ty)
@@ -44,6 +46,10 @@ let rec translate_term (t : ML.term) : P.term =
       P.Variant (lbl, None, Option.map self t)
   | ML.Match (_, t, brs) ->
       P.Match (None, self t, List.map translate_branch brs)
+  | ML.Eq _ ->
+      P.Eq
+  | ML.Use (_, t1, ty1, t2) ->
+      P.Use (self t1, translate_type ty1, self t2)
 
 and translate_branch (pat, t) =
   (translate_pattern pat, translate_term t)

client/P.ml

@@ -9,6 +9,7 @@ type typ =
   | TyForall of tyvar * typ
   | TyMu of tyvar * typ
   | TyConstr of datatype
+  | TyEq of typ * typ
 
 and datatype = Datatype.tyconstr_id * typ list
 
@@ -31,6 +32,8 @@ type term =
   | Inj of (typ list) option * int * term
   | Variant of Datatype.label_id * datatype option * term option
   | Match of typ option * term * branch list
+  | Eq
+  | Use of term * typ * term
 
 and branch = pattern * term
 

client/Printer.ml

@@ -55,6 +55,11 @@ and print_type_atom ty =
   | TyProduct tys ->
       surround_separate_map 2 0 (lbrace ^^ rbrace)
         lbrace star rbrace print_type tys
+  | TyEq (ty1, ty2) ->
+      string "eq " ^^ lparen ^^
+      print_type ty1 ^^ comma ^^
+      print_type ty2 ^^
+      rparen
   | TyMu _ | TyForall _ | TyArrow _ | TyConstr _ as ty ->
       parens (print_type ty)
 
@@ -168,6 +173,12 @@ and print_term_atom t =
       print_tuple print_term ts
   | Match (ty, t, brs) ->
       print_match ty t brs
+  | Eq ->
+      string "Eq"
+  | Use (t1, ty1, t2) ->
+      string "use " ^^
+      print_term t1 ^^ colon ^^ print_type ty1 ^^ string "in" ^^
+      print_term t2
   | Annot (t, tyannot) ->
       print_annot (print_term t) tyannot
   | TyAbs _ | Let _ | Abs _