diff --git a/client/test/CheckF.ml b/client/test/CheckF.ml
index e51d35388fcd4fb81feacafd3365cd0844ea3fef..8a5c68684af3015a68bd249526505753b2e78008 100644
--- a/client/test/CheckF.ml
+++ b/client/test/CheckF.ml
@@ -1,6 +1,11 @@
 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 -> ()
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index 851fc5b15d0456f7234778dfe94beada564deadc..f5ab3108bfaf2f0a5df89f00ad02be6f735534d4 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -19,7 +19,7 @@ let unit_pattern =
 let var x =
   F.(Var (dummy_range, x))
 
-let _annot ty t =
+let annot ty t =
   F.(Annot (dummy_range, ty, t))
 
 let abs x ty t =
@@ -31,7 +31,7 @@ let app t u =
 let tyabs x t =
   F.(TyAbs (dummy_range, x, t))
 
-let _tyapp t ty =
+let tyapp t ty =
   F.(TyApp (dummy_range, t, ty))
 
 let tuple ts =
@@ -46,6 +46,15 @@ let variant 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))
 
@@ -148,21 +157,513 @@ let match_none =
     (some_pattern , unit);
   ]
 
-let test_ok_from_ast datatype_env t () =
-  Alcotest.(check unit) "type inference" (Test.CheckF.test datatype_env t) ()
+(* ( 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 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 int_env =
+  let int_typedecl =
+    let open Datatype in {
+      name = Type "int";
+      type_params = [];
+      data_kind = Variant;
+      labels_descr = [
+        {
+          label_name = Label "O";
+          type_name = Type "int";
+          arg_type = F.TyProduct [];
+        } ; {
+          label_name = Label "S";
+          type_name = Type "int";
+          arg_type = F.TyConstr (Type "int", []);
+        }
+      ]
+    }
+  in
+  Datatype.Env.add_decl bool_env int_typedecl
+
+let int_datatype =
+  Datatype.Type "int", []
+
+(* 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 "Int";
+          type_name = Type "ty";
+          arg_type = F.TyEq (F.TyVar alpha, F.TyConstr int_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 int_env small_gadt_typedecl
+
+let int_pattern arg_type pat =
+  pvariant
+    (Datatype.Label "Int")
+    (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(α,int)).
+    use w in
+    ( O : α )
+ *)
+let cast =
+  let alpha = 0 in
+  tyabs alpha @@
+  abs "w" (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype)) @@
+  use (var "w") @@
+  annot (variant (Datatype.Label "O") int_datatype unit) (F.TyVar alpha)
+
+(*
+Λα.
+  λ(n : α ty).
+    match_α n with
+    | Int p ->
+        use (p : Eq(α,int)) in (O : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True : α)
+ *)
+let match_gadt_default =
+  let alpha = 0 in
+
+  let int_pat =
+    int_pattern [F.TyVar alpha] (pvar "p")
+  in
+
+  let int_payoff =
+    use
+      (annot
+         (var "p")
+         (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype)))
+      (annot
+         (variant
+            (Datatype.Label "O")
+            int_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") [
+    (int_pat , int_payoff);
+    (bool_pat , bool_payoff)
+  ]
+
+(*
+(Λα.
+  λ(n : α ty).
+    match_α n with
+    | Int p ->
+        use (p : Eq(α,int)) in (O : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True : α))
+int
+(Int (refl_int))
+ *)
+let default_int =
+  app
+    (tyapp match_gadt_default (F.TyConstr int_datatype))
+    (variant
+       (Datatype.Label "Int")
+       (Datatype.Type "ty", [F.TyConstr int_datatype])
+       (refl (F.TyConstr int_datatype)))
+
+(*
+(Λα.
+  λ(n : α ty).
+    match_α n with
+    | Int p ->
+        use (p : Eq(α,int)) 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
+    | Int p ->
+        use (p : Eq(α,int)) in (O : α)
+    | Bool p ->
+        use (p : Eq(α,bool)) in (True : α))
+bool
+(Bool (refl_bool))
+ *)
+let default_absurd_wrong =
+  let alpha = 0 in
+
+  let int_pat =
+    int_pattern [F.TyVar alpha] (pvar "p")
+  in
+
+  let int_payoff =
+    use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype))) @@
+    annot
+      (variant
+         (Datatype.Label "O")
+         int_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") [
+    (int_pat , int_payoff);
+    (bool_pat , bool_payoff)
+  ]
+
+(*
+Λα.
+  λ(x : α ty).
+    λ(y : α ty).
+      match (x, y) with
+      | (Int p1, Int p2) ->
+          payoff1
+      | (Bool p1, Bool p2) ->
+          payoff2
+      | (Int p1, Bool p2) ->
+          payoff3
+      | (Bool p1, Int 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
+
+    (*
+      (Int p1, Int p2) ->
+          use (p1 : Eq(α,int)) in use (p2 : Eq(α,int)) in payoff1
+     *)
+    let int_int_branch =
+      ptuple [
+          (variant_ty "Int" (pvar "p1"));
+          (variant_ty "Int" (pvar "p2"));
+      ] ,
+      double_use int_datatype int_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
+
+    (*
+      (Int p1, Bool p2) ->
+          use (p1 : Eq(α,int)) in use (p2 : Eq(α,bool)) in payoff3
+     *)
+    and int_bool_branch =
+      ptuple [
+          (variant_ty "Int" (pvar "p1"));
+          (variant_ty "Bool" (pvar "p2"));
+      ] ,
+      double_use int_datatype bool_datatype payoff3
+
+    (*
+      (Bool p1, Int p2) ->
+          use (p1 : Eq(α,bool)) in use (p2 : Eq(α,int)) in payoff4
+     *)
+    and bool_int_branch =
+      ptuple [
+          (variant_ty "Bool" (pvar "p1"));
+          (variant_ty "Int" (pvar "p2"));
+      ] ,
+      double_use bool_datatype int_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" ]) [
+      int_int_branch ;
+      bool_bool_branch;
+      int_bool_branch;
+      bool_int_branch;
+    ]
+
+(*
+Λα.
+  λ(x : α ty).
+    λ(y : α ty).
+      match (x, y) with
+      | (Int p1, Int p2) ->
+          ()
+      | (Bool p1, Bool p2) ->
+          ()
+      | (Int p1, Bool p2) ->
+          .
+      | (Bool p1, Int 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
+      | (Int p1, Int p2) ->
+          ()
+      | (Bool p1, Bool p2) ->
+          ()
+      | (Int p1, Bool p2) ->
+          ()
+      | (Bool p1, Int 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
+      | (Int p1, Int p2) ->
+          .
+      | (Bool p1, Bool p2) ->
+          .
+      | (Int p1, Bool p2) ->
+          .
+      | (Bool p1, Int 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" int_env cast;
+      test_ok_from_ast "default" small_gadt_env match_gadt_default;
+      test_ok_from_ast "default int" small_gadt_env default_int;
+      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;
     ]
   )]