Merge branch 'type-equations' into 'master'

Add a notion of type equality in the client

See merge request !44

client/F.ml

@@ -4,11 +4,20 @@
 
 (* Types. *)
 
-(* We include recursive types [FTyMu] in the target calculus, not only because
+(* We include recursive types [TyMu] in the target calculus, not only because
    we might wish to support them, but also because even if we disallow them,
    they can still arise during unification (the occurs check is run late), so
    we must be able to display them as part of a type error message. *)
 
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+   equality checking, we do not allow ∀ under μ.
+   For instance :
+           ∀ a. μ t. a -> t is allowed
+           μ t . ∀ a . (a -> t) is not allowed
+           μ t . (∀ a . a) -> t is not allowed *)
+
+(* We also include a type equality witness [TyEq]. *)
+
 (* Nominal or de Bruijn representation of type variables and binders. The
    nominal representation is more convenient when translating from ML to F,
    while the de Bruijn representation is more convenient when type-checking
@@ -27,6 +36,7 @@ type ('a, 'b) typ =
   | TyForall of 'b * ('a, 'b) typ
   | TyMu of 'b * ('a, 'b) typ
   | TyConstr of ('a, 'b) datatype
+  | TyEq of ('a, 'b) typ * ('a, 'b) typ
 
 and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
 
@@ -53,7 +63,27 @@ type debruijn_datatype_env =
 
 (* Nominal representation of term variables and binders. *)
 
-type tevar = string
+(* Nominal or de Bruijn representation of type variables and binders. *)
+
+(* We include a term [Refl] that represents a type equality witness.
+   Note that it has only one type argument but is typed as a witness for
+   an equality between two possibly distinct types (see [TyEq] above).
+
+   [Use] is a construct that "opens" a type equality. That is, it allows us to
+   reason in a context where two types are assumed to be equals.
+   It is supposed to be used with a type equality witness as a left-hand side :
+
+           use (eq : TyEq (ty1, ty2)) in
+           ... (* here ty1 and ty2 are assumed to be equal *)
+
+   Doing this might introduce inconsistent assumptions about types (this can
+   occur for example inside a pattern matching). That is why we introduce
+   a construct [Absurd], that can be used as a placeholder in pieces of code
+   with inconsistent equations in the environment and that are thus
+   unreachable. *)
+
+type tevar =
+  string
 
 type ('a, 'b) term =
   | Var of range *  tevar
@@ -69,6 +99,9 @@ type ('a, 'b) term =
   | LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
   | Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
   | Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
+  | Absurd of range * ('a,'b) typ
+  | Refl of range * ('a,'b) typ
+  | Use of range * ('a,'b) term * ('a,'b) term
 
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
@@ -149,7 +182,10 @@ module TypeInType : DeBruijn.TRAVERSE
         let env, x = extend env x in
         let ty1' = trav env ty1 in
         TyMu (x, ty1')
-
+    | TyEq (ty1, ty2) ->
+        let ty1' = trav env ty1 in
+        let ty2' = trav env ty2 in
+        TyEq (ty1', ty2')
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -219,6 +255,16 @@ module TypeInTerm : DeBruijn.TRAVERSE
         let t' = trav env t
         and brs' = List.map (traverse_branch lookup extend env) brs in
         Match (pos, ty', t', brs')
+    | Absurd (pos, ty) ->
+        let ty' = TypeInType.traverse lookup extend env ty in
+        Absurd (pos, ty')
+    | Refl (pos, ty) ->
+        let ty' = TypeInType.traverse lookup extend env ty in
+        Refl (pos, ty')
+    | Use (pos, t, u) ->
+        let t' = trav env t in
+        let u' = trav env u in
+        Use (pos, t', u')
 
   and traverse_datatype lookup extend env (tid, tyargs) =
     (tid, List.map (TypeInType.traverse lookup extend env) tyargs)

client/F.mli

@@ -4,11 +4,20 @@
 
 (* Types. *)
 
-(* We include recursive types [FTyMu] in the target calculus, not only because
+(* We include recursive types [TyMu] in the target calculus, not only because
    we might wish to support them, but also because even if we disallow them,
    they can still arise during unification (the occurs check is run late), so
    we must be able to display them as part of a type error message. *)
 
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+   equality checking, we do not allow ∀ under μ.
+   For instance :
+           ∀ a. μ t. a -> t is allowed
+           μ t . ∀ a . (a -> t) is not allowed
+           μ t . (∀ a . a) -> t is not allowed *)
+
+(* We also include a type equality witness [TyEq]. *)
+
 (* Nominal or de Bruijn representation of type variables and binders. The
    nominal representation is more convenient when translating from ML to F,
    while the de Bruijn representation is more convenient when type-checking
@@ -26,6 +35,7 @@ type ('a, 'b) typ =
   | TyForall of 'b * ('a, 'b) typ
   | TyMu of 'b * ('a, 'b) typ
   | TyConstr of ('a, 'b) datatype
+  | TyEq of ('a, 'b) typ * ('a, 'b) typ
 
 and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
 
@@ -55,6 +65,23 @@ type debruijn_datatype_env =
 
 (* Nominal or de Bruijn representation of type variables and binders. *)
 
+(* We include a term [Refl] that represents a type equality witness.
+   Note that it has only one type argument but is typed as a witness for
+   an equality between two possibly distinct types (see [TyEq] above).
+
+   [Use] is a construct that "opens" a type equality. That is, it allows us to
+   reason in a context where two types are assumed to be equals.
+   It is supposed to be used with a type equality witness as a left-hand side :
+
+           use (eq : TyEq (ty1, ty2)) in
+           ... (* here ty1 and ty2 are assumed to be equal *)
+
+   Doing this might introduce inconsistent assumptions about types (this can
+   occur for example inside a pattern matching). That is why we introduce
+   a construct [Absurd], that can be used as a placeholder in pieces of code
+   with inconsistent equations in the environment and that are thus
+   unreachable. *)
+
 type tevar =
     string
 
@@ -72,6 +99,9 @@ type ('a, 'b) term =
   | LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
   | Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
   | Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
+  | Absurd of range * ('a,'b) typ
+  | Refl of range * ('a,'b) typ
+  | Use of range * ('a,'b) term * ('a,'b) term
 
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 

client/FPrinter.ml

@@ -40,6 +40,8 @@ let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) :
       P.TyMu (alpha, self ((x, alpha) :: env) ty)
   | F.TyConstr (constr, tys) ->
       P.TyConstr (constr, List.map (self env) tys)
+  | F.TyEq (ty1, ty2) ->
+      P.TyEq (self env ty1, self env ty2)
 
 let print_type ty =
   Printer.print_type (translate_type [] ty)
@@ -84,6 +86,14 @@ let rec translate_term env (t : F.nominal_term) : P.term =
         self env t,
         List.map (translate_branch env) brs
       )
+  | F.Absurd (_, ty) ->
+      P.Absurd (translate_type env ty)
+  | F.Refl (_, ty) ->
+      P.Refl (translate_type env ty)
+  | F.Use (_, t, u) ->
+      let t' = self env t in
+      let u' = self env u in
+      P.Use (t', u')
 
 and translate_branch env (pat, t) =
   (translate_pattern env pat, translate_term env t)
@@ -155,6 +165,8 @@ let rec translate_db_type (env : P.tyvar list) (ty : F.debruijn_type) : P.typ =
       P.TyMu (alpha, self (alpha :: env) ty)
   | F.TyConstr (constr, tys) ->
       P.TyConstr (constr, List.map (self env) tys)
+  | F.TyEq (ty1, ty2) ->
+      P.TyEq (self env ty1, self env ty2)
 
 let print_db_type ty =
   Printer.print_type (translate_db_type [] ty)
@@ -190,9 +202,19 @@ let print_type_error e =
       str "Type error." ++
       str "This type should be a universal type:" ++
       print_db_type ty
+  | NotAnEqual ty ->
+      str "Type error." ++
+      str "This type should be an equality type:" ++
+      print_db_type ty
   | UnboundTermVariable x ->
       str "Scope error." ++
       str "The variable %s is unbound." x
+  | UnboundTypeVariable x ->
+      str "Scope error." ++
+      str "The type variable %d is unbound." x
   | TwoOccurencesOfSameVariable x ->
       str "Scope error." ++
       str "The variable %s is bound twice in a pattern." x
+  | ContextNotAbsurd ->
+       str "Type error." ++
+       str "The type equations in the typing environment are not contradictory."

client/FTypeChecker.mli

@@ -8,8 +8,11 @@ type type_error =
   | NotAnArrow of debruijn_type
   | NotAProduct of debruijn_type
   | NotAForall of debruijn_type
+  | NotAnEqual of debruijn_type
   | UnboundTermVariable of tevar
+  | UnboundTypeVariable of tyvar
   | TwoOccurencesOfSameVariable of string
+  | ContextNotAbsurd
 
 (* An arity-related requirement on a certain (sum or product) type
    arising during type-checking:

client/Infer.ml

@@ -39,6 +39,8 @@ module O = struct
         F.TyProduct ts
     | S.TyConstr (tyconstr, ts) ->
         F.TyConstr(tyconstr, ts)
+    | S.TyEq (t1, t2) ->
+        F.TyEq (t1, t2)
 
   let mu x t =
     F.TyMu (x, 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
 
@@ -33,6 +34,9 @@ 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
+  | Absurd of typ
+  | Refl of typ
+  | Use of term * term
 
 and branch = pattern * term
 

client/Printer.ml

@@ -38,6 +38,10 @@ and print_type_arrow ty =
       print_type_tyconstr ty1
       ^^ space ^^ string "->"
       ^//^ print_type_arrow ty2
+  | TyEq (ty1, ty2) ->
+      print_type_tyconstr ty1
+      ^^ space ^^ string "="
+      ^//^ print_type_arrow ty2
   | ty ->
       print_type_tyconstr ty
 
@@ -55,7 +59,7 @@ and print_type_atom ty =
   | TyProduct tys ->
       surround_separate_map 2 0 (lbrace ^^ rbrace)
         lbrace star rbrace print_type tys
-  | TyMu _ | TyForall _ | TyArrow _ | TyConstr _ as ty ->
+  | TyMu _ | TyForall _ | TyArrow _ | TyConstr _ | TyEq _ as ty ->
       parens (print_type ty)
 
 and print_datatype (Datatype.Type tyconstr, tyargs) =
@@ -143,7 +147,7 @@ let print_annot print_elem (rigidity, tyvars, typ) =
                 "for"
   in
   surround 2 0 lparen (
-    print_elem ^^ space ^^ string ":"
+    print_elem ^^ break 1 ^^ string ":"
     ^^ (if tyvars = [] then empty
         else prefix 2 1 empty
                (rigidity_kwd ^^ space ^^
@@ -167,6 +171,11 @@ and print_term_abs t =
   | Abs _ ->
       let (ps, t) = flatten_abs t in
       print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
+  | Use (t, u) ->
+      string "use" ^^ space
+      ^^ print_term t
+      ^^ space ^^ string "in" ^^ hardline
+      ^^ print_term u
   | t ->
       print_term_app t
 
@@ -183,6 +192,11 @@ and print_term_app t =
       ^^ space ^^ print_term_atom t
   | Variant (lbl, dty, t) ->
       print_variant lbl dty print_term_atom t
+  | Refl ty ->
+     group (
+       string "Refl"
+       ^^ print_angle_type ty
+     )
   | t ->
       print_term_atom t
 
@@ -200,8 +214,10 @@ and print_term_atom t =
       print_match ty t brs
   | Annot (t, tyannot) ->
       print_annot (print_term t) tyannot
-  | TyAbs _ | Let _ | Abs _
-  | TyApp _ | App _ | Proj _ | Inj _ | Variant _ as t ->
+  | Absurd _ ->
+      dot
+  | TyAbs _ | Let _ | Abs _ | Use _
+  | TyApp _ | App _ | Proj _ | Inj _ | Variant _  | Refl _ as t ->
       parens (print_term t)
 
 and print_match ty scrutinee brs =

client/Structure.ml

@@ -6,6 +6,7 @@ type 'a structure =
   | TyArrow of 'a * 'a
   | TyProduct of 'a list
   | TyConstr of Datatype.tyconstr_id * 'a list
+  | TyEq of 'a * 'a
 
 (* -------------------------------------------------------------------------- *)
 
@@ -16,7 +17,8 @@ type 'a structure =
 
 let iter f t =
   match t with
-  | TyArrow (t1, t2) ->
+  | TyArrow (t1, t2)
+  | TyEq (t1, t2) ->
       f t1; f t2
   | TyProduct ts
   | TyConstr (_, ts) ->
@@ -24,7 +26,8 @@ let iter f t =
 
 let fold f t accu =
   match t with
-  | TyArrow (t1, t2) ->
+  | TyArrow (t1, t2)
+  | TyEq (t1, t2) ->
       let accu = f t1 accu in
       let accu = f t2 accu in
       accu
@@ -34,7 +37,8 @@ let fold f t accu =
 
 let map f t =
   match t with
-  | TyArrow (t1, t2) ->
+  | TyArrow (t1, t2)
+  | TyEq (t1, t2) ->
       let t1 = f t1 in
       let t2 = f t2 in
       TyArrow (t1, t2)
@@ -57,7 +61,8 @@ let list_iter2 f ts us =
 
 let iter2 f t u =
   match t, u with
-  | TyArrow (t1, t2), TyArrow (u1, u2) ->
+  | TyArrow (t1, t2), TyArrow (u1, u2)
+  | TyEq (t1, t2), TyEq (u1, u2) ->
       f t1 u1;
       f t2 u2
   | TyProduct ts1, TyProduct ts2 ->
@@ -67,7 +72,8 @@ let iter2 f t u =
       list_iter2 f ts1 ts2
   | TyArrow _, _
   | TyProduct _, _
-  | TyConstr _, _ ->
+  | TyConstr _, _
+  | TyEq _, _->
       raise Iter2
 
 (* The function [conjunction] that is expected by the solver is essentially
@@ -89,8 +95,10 @@ open PPrint
 let pprint leaf s =
   match s with
   | TyArrow (t1, t2) ->
-      leaf t1 ^^ string " -> " ^^ leaf t2
+      parens (leaf t1) ^^ string " -> " ^^ leaf t2
   | TyProduct ts ->
       braces (separate_map (string " * ") leaf ts)
   | TyConstr (Datatype.Type c, ts) ->
       string c ^^ parens (separate_map (string ", ") leaf ts)
+  | TyEq (t1, t2) ->
+      parens (leaf t1 ^^ string " = " ^^ leaf t2)

client/test/CheckF.ml

 open Client
 
-let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
+(* Typecheck a System F term after a bunch of debugging printing.
+   FTypechecker returns a [result] that is treated by the user-supplied
+   [on_error] and [on_ok] functions. *)
+let check (env : F.nominal_datatype_env) (t : F.nominal_term)
+  : (F.debruijn_type, FTypeChecker.type_error) result
+  =
   Printf.printf "Formatting the System F term...\n%!";
   let doc = FPrinter.print_term t in
   Printf.printf "Pretty-printing the System F term...\n%!";
@@ -11,8 +16,21 @@ let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
   let t : F.debruijn_term =
     F.Term.translate t in
   print_string "Type-checking the System F term...\n";
-  match FTypeChecker.typeof_result env t with
+  FTypeChecker.typeof_result env t
+
+(* Test a term that is expected to pass type checking. *)
+let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
+  match check env t with
+  | Ok _ ->
+     ()
   | Error e ->
-    Utils.emit_endline (FPrinter.print_type_error e);
+     Utils.emit_endline (FPrinter.print_type_error e);
+     failwith "Type-checking error."
+
+(* Test a term that is expected to fail type checking. *)
+let test_error (env : F.nominal_datatype_env) (t : F.nominal_term) =
+  match check env t with
+  | Error _ ->
+     ()
+  | Ok _ ->
     failwith "Type-checking error."
-  | Ok _v -> ()

client/test/TestF.ml

 open Client
 
+(* -------------------------------------------------------------------------- *)
+
+(* AST helper functions *)
+
+let (-->) ty1 ty2 =
+  F.TyArrow (ty1, ty2)
+
+let unit =
+  F.Tuple (F.dummy_range, [])
+
+let unit_type =
+  F.TyProduct []
+
+let unit_pattern =
+  F.PTuple (F.dummy_range, [])
+
+let var x =
+  F.(Var (dummy_range, x))
+
+let annot ty t =
+  F.(Annot (dummy_range, ty, t))
+
+let abs x ty t =
+  F.(Abs (dummy_range, x, ty, t))
+
+let app t u =
+  F.(App (dummy_range, t, u))
+
+let tyabs x t =
+  F.(TyAbs (dummy_range, x, t))
+
+let tyapp t ty =
+  F.(TyApp (dummy_range, t, ty))
+
+let tuple ts =
+  F.(Tuple (dummy_range, ts))
+
+let letprod xs t u =
+  F.(LetProd (dummy_range, xs, t, u))
+
+let variant lbl datatype t =
+  F.(Variant (dummy_range, lbl, datatype, t))
+
+let match_ ty scrutinee branches =
+  F.(Match (dummy_range, ty, scrutinee, branches))
+
+let absurd ty =
+  F.(Absurd (dummy_range, ty))
+
+let refl ty =
+  F.(Refl (dummy_range, ty))
+
+let use t u =
+  F.(Use (dummy_range, t, u))
+
+let pvar x =
+  F.(PVar (dummy_range, x))
+
+let pwildcard =
+  F.(PWildcard dummy_range)
+
+let ptuple ps =
+  F.(PTuple (dummy_range, ps))
+
+let pvariant lbl datatype t =
+  F.(PVariant (dummy_range, lbl, datatype, t))
+
+(* -------------------------------------------------------------------------- *)
+
 (* ∀a b. ({} -> (a * (a -> b))) -> b
    Λa b. fun (p : {} -> (a * (a -> b))) ->
      let (x, f) = p () in f x
 *)
 let let_prod =
-  let open F in
   let alpha, beta = 0, 1 in
   let p, f, x = "p", "f", "x" in
-  TyAbs (dummy_range, alpha, TyAbs (dummy_range, beta,
-    Abs (dummy_range, p, TyArrow (TyProduct [],
-           TyProduct [TyVar alpha; TyArrow (TyVar alpha, TyVar beta)]),
-         LetProd (dummy_range, [x; f],
-                  App (dummy_range,
-                       Var (dummy_range, p),
-                       Tuple (dummy_range, [])),
-        App (dummy_range, Var (dummy_range, f), Var (dummy_range, x))))))
+  tyabs alpha @@
+  tyabs beta @@
+  abs p (unit_type --> F.(TyProduct [TyVar alpha; TyVar alpha --> TyVar beta])) @@
+  letprod [x; f]
+    (app (var p) (tuple []))
+    (app (var f) (var x))
 
 (* Λαβ. λ(x:{α*β}. match x with (_, y) -> y end *)
 let match_with_prod =
   let alpha, beta = 1, 0 in
-  F.(
-    TyAbs(dummy_range, alpha,
-      TyAbs(dummy_range, beta,
-        Abs(dummy_range, "x",
-          TyProduct [ TyVar alpha ; TyVar beta ],
-          Match(dummy_range, TyVar beta,
-                Var (dummy_range, "x"),
-                [
-                  (PTuple (dummy_range,
-                           [ PWildcard dummy_range ; PVar (dummy_range, "y") ]) ,
-                   Var (dummy_range, "y"))
-                ]
-            )
-          )
-        )
-      )
-  )
+    tyabs alpha @@
+    tyabs beta @@
+    abs "x" (F.TyProduct [ F.TyVar alpha ; F.TyVar beta ]) @@
+    match_ (F.TyVar beta) (var "x") [
+        (ptuple [ pwildcard ; pvar "y" ]) , var"y"
+      ]
 
 (* option *)
 let option_env =
   let option_typedecl =
     let open Datatype in {
-        name = Type "option";
-        type_params = [ 0 ];
-        data_kind = Variant;
-        labels_descr = [
-          {
-            label_name = Label "None";
-            type_name = Type "option";
-            arg_type = F.TyProduct [];
-          } ; {
-            label_name = Label "Some";
-            type_name = Type "option";
-            arg_type = F.TyVar 0;
-          }
-        ];
-      }
+      name = Type "option";
+      type_params = [ 0 ];
+      data_kind = Variant;
+      labels_descr = [
+        {
+          label_name = Label "None";
+          type_name = Type "option";
+          arg_type = F.TyProduct [];
+        } ; {
+          label_name = Label "Some";
+          type_name = Type "option";
+          arg_type = F.TyVar 0;
+        }
+      ];
+    }
   in
   Datatype.Env.add_decl Datatype.Env.empty option_typedecl
 
-let unit = F.Tuple (F.dummy_range, [])
-let unit_pattern = F.PTuple (F.dummy_range, [])
-
 (* None *)
 let none =
   let alpha = 0 in
-  F.(
-    Variant (dummy_range,
-             Datatype.Label "None", (Datatype.Type "option", [TyForall (alpha, TyVar alpha)]), unit)
-  )
+  let label = Datatype.Label "None" in
+  let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
+  variant label datatype unit
 
 let none_pattern =
   let alpha = 0 in
-  F.(
-    PVariant (dummy_range,
-      Datatype.Label "None",
-      (Datatype.Type "option", [TyForall (alpha, TyVar alpha)]),
-      unit_pattern
-    )
-  )
+  let label = Datatype.Label "None" in
+  let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
+  pvariant label datatype unit_pattern
 
 (* Some Λα.λx:α.x *)
 let some =
   let alpha = 0 in
-  F.(
-    Variant (dummy_range,
-      Datatype.Label "Some",
-      (Datatype.Type "option", [ TyForall (alpha, TyArrow (TyVar alpha, TyVar alpha)) ]),
-      TyAbs (dummy_range, alpha, Abs (dummy_range, "x", TyVar alpha, Var (dummy_range, "x")))
-    )
-  )
+  let label = Datatype.Label "Some" in
+  let datatype = Datatype.Type "option",
+                 [ F.TyForall (alpha, F.TyVar alpha --> F.TyVar alpha) ] in
+  variant label datatype @@
+  tyabs alpha @@
+  abs "x" (F.TyVar alpha) @@
+  var "x"
 
 let some_pattern =
   let alpha = 0 in
-  F.(
-    PVariant (dummy_range,
-      Datatype.Label "Some",
-      (Datatype.Type "option", [ TyForall (alpha, TyVar alpha) ]),
-      PWildcard dummy_range
-    )
-  )
+  let label = Datatype.Label "Some" in
+  let datatype = Datatype.Type "option", [ F.TyForall (alpha, F.TyVar alpha) ] in
+  pvariant label datatype pwildcard
 
 (* Λα. match None with
        | None     -> ()
        | Some (_) -> ()
  *)
-let match_none = F.(
+let match_none =
   let alpha = 0 in
-  TyAbs(dummy_range, alpha,
-    Match (dummy_range,
-      TyProduct [] ,
-      none,
-      [
-        (none_pattern , unit)
-      ;
-        (some_pattern , unit)
+  tyabs alpha @@
+  match_ unit_type none @@ [
+    (none_pattern , unit);
+    (some_pattern , unit);
+  ]
+
+(* ( refl_{} : Eq(∀α.{} , {}) ) *)
+let type_eq =
+  let alpha = 0 in
+  annot (refl unit_type) @@
+  F.TyEq (F.TyForall (alpha, unit_type),
+          unit_type)
+
+(* Λ α. use (Refl_α : eq (α,α)) in λ (x:α). x *)
+let introduce_type_eq =
+  let alpha = 0 in
+  let x = "x" in
+  tyabs alpha @@
+  use
+    (annot (refl (F.TyVar alpha)) (F.TyEq (F.TyVar alpha, F.TyVar alpha))) @@
+    abs x (F.TyVar alpha) (var x)
+
+(* Λ αβ. λ (x : eq (α,β)). use x in (Refl_β : eq (β,α))
+ * ∀ αβ. eq (α,β) -> eq (β,α) *)
+let sym =
+  let alpha = 1 in
+  let beta = 0 in
+  let x = "x" in
+  annot
+    (tyabs alpha @@
+     tyabs beta @@
+     abs x (F.TyEq (F.TyVar alpha, F.TyVar beta)) @@
+     use (var x) @@
+     annot (refl (F.TyVar beta)) (F.TyEq (F.TyVar beta, F.TyVar alpha)))
+    @@
+    F.TyForall (alpha,
+    F.TyForall (beta,
+    F.TyEq (F.TyVar alpha, F.TyVar beta)
+    --> F.TyEq (F.TyVar beta, F.TyVar alpha)))
+
+
+(* Λ αβγ.
+   λ (x : eq (α,β)).
+   λ (y : eq (β,γ)).
+   use x in
+   use y in
+   (Refl_γ : eq (α,γ))
+
+   ∀αβγ. eq (α,β) -> eq (β,γ) -> eq (α,γ) *)
+let trans =
+  let alpha = 2 in
+  let beta = 1 in
+  let gamma = 0 in
+  let x = "x" in
+  let y = "y" in
+  annot
+    (tyabs alpha @@
+     tyabs beta @@
+     tyabs gamma @@
+     abs x (F.TyEq (F.TyVar alpha, F.TyVar beta)) @@
+     abs y (F.TyEq (F.TyVar beta, F.TyVar gamma)) @@
+     use (var x) @@
+     use (var y) @@
+     annot (refl (F.TyVar gamma)) (F.TyEq (F.TyVar alpha, F.TyVar gamma)))
+
+     @@
+     F.TyForall (alpha,
+     F.TyForall (beta,
+     F.TyForall (gamma,
+     F.TyEq (F.TyVar alpha, F.TyVar beta)
+     --> (F.TyEq (F.TyVar beta, F.TyVar gamma)
+         --> F.TyEq (F.TyVar alpha, F.TyVar gamma)))))
+
+let bool_env =
+  let bool_typedecl =
+    let open Datatype in {
+      name = Type "bool";
+      type_params = [];
+      data_kind = Variant;
+      labels_descr = [
+        {
+          label_name = Label "True";
+          type_name = Type "bool";
+          arg_type = F.TyProduct [];
+        } ; {
+          label_name = Label "False";
+          type_name = Type "bool";
+          arg_type = F.TyProduct [];
+        }
       ]
-      )
-    )
-  )
+    }
+  in
+  Datatype.Env.add_decl option_env bool_typedecl
 
-let test_ok_from_ast datatype_env t () =
-  Alcotest.(check unit) "type inference" (Test.CheckF.test datatype_env t) ()
+let bool_datatype =
+  Datatype.Type "bool", []
 
-let test_case msg datatype_env t =
-  Alcotest.(test_case msg `Quick (test_ok_from_ast datatype_env t))
+let nat_env =
+  let nat_typedecl =
+    let open Datatype in {
+      name = Type "nat";
+      type_params = [];
+      data_kind = Variant;
+      labels_descr = [
+        {
+          label_name = Label "O";
+          type_name = Type "nat";
+          arg_type = F.TyProduct [];
+        } ; {
+          label_name = Label "S";
+          type_name = Type "nat";
+          arg_type = F.TyConstr (Type "nat", []);
+        }
+      ]
+    }
+  in
+  Datatype.Env.add_decl bool_env nat_typedecl
+
+let nat_datatype =
+  Datatype.Type "nat", []
+
+(* small gadt *)
+let small_gadt_env =
+  let small_gadt_typedecl =
+    let alpha = 0 in
+    let open Datatype in {
+      name = Type "ty";
+      type_params = [ alpha ];
+      data_kind = Variant;
+      labels_descr = [
+        {
+          label_name = Label "Nat";
+          type_name = Type "ty";
+          arg_type = F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype);
+        } ; {
+          label_name = Label "Bool";
+          type_name = Type "ty";
+          arg_type = F.TyEq (F.TyVar alpha, F.TyConstr bool_datatype);
+        }
+      ];
+    }
+  in
+  Datatype.Env.add_decl nat_env small_gadt_typedecl
+
+let nat_pattern arg_type pat =
+  pvariant
+    (Datatype.Label "Nat")
+    (Datatype.Type "ty", arg_type)
+    pat
+
+let bool_pattern arg_type pat =
+  pvariant
+    (Datatype.Label "Bool")
+    (Datatype.Type "ty", arg_type)
+    pat
+
+(*
+Λα.
+  λ(x : μβ. {} * β).
+  x
+ *)
+let mu_under_forall =
+  let alpha = 1 in
+  let beta = 0 in
+  let x = "x" in
+  tyabs alpha @@
+  abs x (F.TyMu (beta, F.TyProduct [unit_type ; F.TyVar beta])) @@
+  var x
+
+(*
+Λα.
+  λ(w : Eq(α,nat)).
+    use w in
+    ( O : α )
+ *)
+let cast =
+  let alpha = 0 in
+  tyabs alpha @@
+  abs "w" (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype)) @@
+  use (var "w") @@
+  annot (variant (Datatype.Label "O") nat_datatype unit) (F.TyVar alpha)
+
+(*
+Λα.
+  λ(n : α ty).
+    match_α n with
+    | Nat p ->
+        use (p : Eq(α,nat)) in (O : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True : α)
+ *)
+let match_gadt_default =
+  let alpha = 0 in
+
+  let nat_pat =
+    nat_pattern [F.TyVar alpha] (pvar "p")
+  in
+
+  let nat_payoff =
+    use
+      (annot
+         (var "p")
+         (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype)))
+      (annot
+         (variant
+            (Datatype.Label "O")
+            nat_datatype
+            unit)
+         (F.TyVar alpha))
+  in
+
+  let bool_pat =
+    bool_pattern [F.TyVar alpha] (pvar "p")
+  in
+
+  let bool_payoff =
+    use
+      (annot
+         (var "p")
+         (F.TyEq (F.TyVar alpha, F.TyConstr bool_datatype)))
+      (annot
+         (variant
+            (Datatype.Label "True")
+            bool_datatype
+            unit)
+         (F.TyVar alpha))
+  in
+  tyabs alpha @@
+  abs "n" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
+  match_ (F.TyVar alpha) (var "n") [
+    (nat_pat , nat_payoff);
+    (bool_pat , bool_payoff)
+  ]
+
+(*
+(Λα.
+  λ(n : α ty).
+    match_α n with
+    | Nat p ->
+        use (p : Eq(α,nat)) in (O : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True : α))
+nat
+(Nat (refl_nat))
+ *)
+let default_nat =
+  app
+    (tyapp match_gadt_default (F.TyConstr nat_datatype))
+    (variant
+       (Datatype.Label "Nat")
+       (Datatype.Type "ty", [F.TyConstr nat_datatype])
+       (refl (F.TyConstr nat_datatype)))
+
+(*
+(Λα.
+  λ(n : α ty).
+    match_α n with
+    | Nat p ->
+        use (p : Eq(α,nat)) in (O : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True : α))
+bool
+(Bool (refl_bool))
+ *)
+let default_bool =
+    app
+      (tyapp match_gadt_default (F.TyConstr bool_datatype))
+      (variant
+         (Datatype.Label "Bool")
+         (Datatype.Type "ty", [F.TyConstr bool_datatype])
+         (refl (F.TyConstr bool_datatype)))
+
+(*
+Λα.
+  λ(n : α ty).
+    match_α n with
+    | Nat p ->
+        use (p : Eq(α,nat)) in (O (. : unit) : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True (. : unit) : α)
+ *)
+let default_absurd_wrong =
+  let alpha = 0 in
+
+  let nat_pat =
+    nat_pattern [F.TyVar alpha] (pvar "p")
+  in
+
+  let nat_payoff =
+    use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype))) @@
+    annot
+      (variant
+         (Datatype.Label "O")
+         nat_datatype
+         (absurd unit_type))
+      (F.TyVar alpha)
+  in
+
+  let bool_pat =
+    bool_pattern [F.TyVar alpha] (pvar "p")
+  in
+
+  let bool_payoff =
+    use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr bool_datatype))) @@
+    annot
+      (variant
+         (Datatype.Label "True")
+         bool_datatype
+         (absurd unit_type))
+      (F.TyVar alpha)
+  in
+
+  tyabs alpha @@
+  abs "n" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
+  match_ (F.TyVar alpha) (var "n") [
+    (nat_pat , nat_payoff);
+    (bool_pat , bool_payoff)
+  ]
+
+(*
+Λα.
+  λ(x : α ty).
+    λ(y : α ty).
+      match (x, y) with
+      | (Nat p1, Nat p2) ->
+          payoff1
+      | (Bool p1, Bool p2) ->
+          payoff2
+      | (Nat p1, Bool p2) ->
+          payoff3
+      | (Bool p1, Nat p2) ->
+          payoff4
+*)
+let test_absurd payoff1 payoff2 payoff3 payoff4 =
+    let alpha = 0 in
+
+    let variant_ty lbl pat =
+      pvariant
+          (Datatype.Label lbl)
+          (Datatype.Type "ty", [F.TyVar alpha])
+          pat
+    in
+
+    (* Helper functions for payoff *)
+
+    (* use (p1 : Eq(α,dt1)) in use (p2 : Eq(α,dt2)) in payoff *)
+    let double_use datatype1 datatype2 payoff=
+      use (annot (var "p1") (F.TyEq (F.TyVar alpha, F.TyConstr datatype1))) @@
+      use (annot (var "p2") (F.TyEq (F.TyVar alpha, F.TyConstr datatype2))) @@
+      payoff
+    in
+
+    (*
+      (Nat p1, Nat p2) ->
+          use (p1 : Eq(α,nat)) in use (p2 : Eq(α,nat)) in payoff1
+     *)
+    let nat_nat_branch =
+      ptuple [
+          (variant_ty "Nat" (pvar "p1"));
+          (variant_ty "Nat" (pvar "p2"));
+      ] ,
+      double_use nat_datatype nat_datatype payoff1
+
+    (*
+      (Bool p1, Bool p2) ->
+          use (p1 : Eq(α,bool)) in use (p2 : Eq(α,bool)) in payoff2
+     *)
+    and bool_bool_branch =
+      ptuple [
+          (variant_ty "Bool" (pvar "p1"));
+          (variant_ty "Bool" (pvar "p2"));
+      ] ,
+      double_use bool_datatype bool_datatype payoff2
+
+    (*
+      (Nat p1, Bool p2) ->
+          use (p1 : Eq(α,nat)) in use (p2 : Eq(α,bool)) in payoff3
+     *)
+    and nat_bool_branch =
+      ptuple [
+          (variant_ty "Nat" (pvar "p1"));
+          (variant_ty "Bool" (pvar "p2"));
+      ] ,
+      double_use nat_datatype bool_datatype payoff3
+
+    (*
+      (Bool p1, Nat p2) ->
+          use (p1 : Eq(α,bool)) in use (p2 : Eq(α,nat)) in payoff4
+     *)
+    and bool_nat_branch =
+      ptuple [
+          (variant_ty "Bool" (pvar "p1"));
+          (variant_ty "Nat" (pvar "p2"));
+      ] ,
+      double_use bool_datatype nat_datatype payoff4
+    in
+
+    tyabs alpha @@
+    abs "x" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
+    abs "y" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
+    match_ unit_type (tuple [ var "x"; var "y" ]) [
+      nat_nat_branch ;
+      bool_bool_branch;
+      nat_bool_branch;
+      bool_nat_branch;
+    ]
+
+(*
+Λα.
+  λ(x : α ty).
+    λ(y : α ty).
+      match (x, y) with
+      | (Nat p1, Nat p2) ->
+          ()
+      | (Bool p1, Bool p2) ->
+          ()
+      | (Nat p1, Bool p2) ->
+          .
+      | (Bool p1, Nat p2) ->
+          .
+*)
+(* This example is ok : the two last branches are unreachable. *)
+let test_absurd_ok =
+  test_absurd
+    unit
+    unit
+    (absurd unit_type)
+    (absurd unit_type)
+
+
+(*
+Λα.
+  λ(x : α ty).
+    λ(y : α ty).
+      match (x, y) with
+      | (Nat p1, Nat p2) ->
+          ()
+      | (Bool p1, Bool p2) ->
+          ()
+      | (Nat p1, Bool p2) ->
+          ()
+      | (Bool p1, Nat p2) ->
+          ()
+*)
+(* This example is ok : the two last branches are unreachable, but it is not
+   mandatory to declare them as such. *)
+let test_absurd_ok2 =
+  test_absurd
+    unit
+    unit
+    unit
+    unit
+
+(*
+Λα.
+  λ(x : α ty).
+    λ(y : α ty).
+      match (x, y) with
+      | (Nat p1, Nat p2) ->
+          .
+      | (Bool p1, Bool p2) ->
+          .
+      | (Nat p1, Bool p2) ->
+          .
+      | (Bool p1, Nat p2) ->
+          .
+*)
+(* This example is wrong : the first two branches are reachable, i.e. they
+   don't introduce type inconsistencies in the environment *)
+let test_absurd_wrong =
+  test_absurd
+    (absurd unit_type)
+    (absurd unit_type)
+    (absurd unit_type)
+    (absurd unit_type)
+
+let test_ok_from_ast msg datatype_env t =
+  let test_ok () =
+    Alcotest.(check unit) "type inference" (Test.CheckF.test datatype_env t) ()
+  in
+  Alcotest.(test_case msg `Quick test_ok)
+
+let test_type_error msg datatype_env t =
+  let test_error () =
+    Alcotest.(check unit) "type inference"
+      (Test.CheckF.test_error datatype_env t) ()
+  in
+  Alcotest.(test_case msg `Quick test_error)
 
 let test_suite =
   [(
     "test F ast",
-    [ test_case "let prod" Datatype.Env.empty let_prod;
-      test_case "match with prod" Datatype.Env.empty match_with_prod;
-      test_case "unit" option_env unit;
-      test_case "none" option_env none;
-      test_case "some" option_env some;
-      test_case "match none" option_env match_none;
+    [ test_ok_from_ast "let prod" Datatype.Env.empty let_prod;
+      test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
+      test_ok_from_ast "unit" option_env unit;
+      test_ok_from_ast "none" option_env none;
+      test_ok_from_ast "some" option_env some;
+      test_ok_from_ast "match none" option_env match_none;
+      test_type_error "type equality" Datatype.Env.empty type_eq;
+      test_ok_from_ast "introduce type equality" Datatype.Env.empty introduce_type_eq;
+      test_ok_from_ast "symmetry" Datatype.Env.empty sym;
+      test_ok_from_ast "transitivity" Datatype.Env.empty trans;
+      test_ok_from_ast "mu under forall" Datatype.Env.empty mu_under_forall;
+      test_ok_from_ast "cast" nat_env cast;
+      test_ok_from_ast "default" small_gadt_env match_gadt_default;
+      test_ok_from_ast "default nat" small_gadt_env default_nat;
+      test_ok_from_ast "default bool" small_gadt_env default_bool;
+      test_type_error "default absurd wrong" small_gadt_env default_absurd_wrong;
+      test_ok_from_ast "pair of gadt" small_gadt_env test_absurd_ok;
+      test_ok_from_ast "pair of gadt" small_gadt_env test_absurd_ok2;
+      test_type_error "pair of gadt" small_gadt_env test_absurd_wrong;
     ]
   )]