[WIP] equations environment using a union-find.

These comments should appear in F.mli too, but I'm waiting for feedbacks before I copy-paste them.

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.ml

@@ -6,8 +6,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
 
 and arity_requirement = Index of int | Total of int
 
@@ -37,19 +40,64 @@ module TermVarMap =
 module N2DB =
   DeBruijn.Nominal2deBruijn(TermVar)
 
+(* We use a union-find data structure to represent equalities between rigid
+   variables and types. We need the ability to snapshot and rollback changes, to
+   undo the addition of an equality to the environment. *)
+module UF = struct
+  include UnionFind.Make(UnionFind.StoreVector)
+  type 'a elem = 'a rref
+end
+
+module S =
+  Structure
+
+(* We translate types into union-find graphs to check equality.
+   μ-types create cyclic graphs. Each vertex represents a type expression.
+   GADTs can add type equalities in the context and we represent
+   this by unifying their vertices in the union-find graph. This is
+   possible only when they have compatible structures (or one of the
+   side has no structure), otherwise the equality is inconsistent. *)
+type vertex =
+  structure option UF.elem
+
+and structure =
+  (* Corresponds to types from the source language (arrow, product, ...). *)
+  | SStruct of vertex S.structure
+  (* Represents ∀α.τ. We use De Bruijn levels, so we don't need to name
+     explicitly the bound variable α. *)
+  | SForall of vertex
+  (* A De Bruijn level corresponding to a ∀-bound variable. Using levels
+     instead of indices makes the equality test easier. *)
+  | SForallLevel of int
+
+(* The global store of the union-find. *)
+type uf_store = structure option UF.store
+
+(* A mapping from rigid variables to union-find vertices. *)
+type uf_tyvars = structure option UF.elem list
+
+(* If the type equations introduced are inconsistent, then no need for
+   [store] and [tyvars] *)
+type equations_env =
+  | Equations of { store: uf_store ; tyvars: uf_tyvars }
+  | Inconsistent
+
 type env = {
   (* A mapping of term variables to types. *)
   types: debruijn_type TermVarMap.t;
   (* A translation environment of TERM variables to TYPE indices. *)
   names: N2DB.env;
+  (* We keep trace of whether or not the typing equations is consistent *)
+  equations: equations_env;
 }
 
-type _datatype_env = (unit, debruijn_type) Datatype.Env.t
-
-let empty =
-  { types = TermVarMap.empty; names = N2DB.empty }
+let empty = {
+  types = TermVarMap.empty;
+  names = N2DB.empty;
+  equations = Equations { store = UF.new_store() ; tyvars = [] };
+}
 
-let lookup { types; names } x =
+let lookup { types; names; _ } x =
   try
     (* Obtain the type associated with [x]. *)
     let ty = TermVarMap.find x types in
@@ -62,32 +110,59 @@ let lookup { types; names } x =
     (* must have been raised by [TermVarMap.find] *)
     raise (TypeError (UnboundTermVariable x))
 
-let extend_with_tevar { types; names } x ty =
+let extend_with_tevar { types; names; equations } x ty =
   (* Map the name [x] to [ty], and record when it was bound, without
      incrementing the time. *)
   { types = TermVarMap.add x ty types;
-    names = N2DB.slide names x }
-
-let extend_with_tyvar { types; names } =
-  (* Increment the time. *)
-  { types; names = N2DB.bump names }
+    names = N2DB.slide names x;
+    equations; }
+
+let extend_with_tyvar { types; names; equations } =
+  match equations with
+  | Inconsistent ->
+     { types; names; equations }
+  | Equations { store; tyvars } ->
+     (* Create a fresh vertex for the new type variable *)
+     let v = UF.make store None in
+     (* Extend the environment of type variables *)
+     let tyvars = v :: tyvars in
+     (* Increment the time. *)
+     let names = N2DB.bump names in
+     { types; names ; equations = Equations { store ; tyvars } }
 
 let singleton x ty =
   extend_with_tevar empty x ty
 
 let concat env1 env2 =
   let combine _ _ ty2 = Some ty2 in
-  { types = TermVarMap.union combine env1.types env2.types ;
-    names = N2DB.concat env1.names env2.names }
+  let types = TermVarMap.union combine env1.types env2.types in
+  let names = N2DB.concat env1.names env2.names in
+  match (env1.equations, env2.equations) with
+  | Inconsistent,_ | _, Inconsistent ->
+     { types; names; equations = Inconsistent }
+  | Equations { store = store1; tyvars = tyvars1 },
+    Equations { store = store2; tyvars = tyvars2 } ->
+     assert (store1 == store2);
+     let store = store1 in
+     let tyvars = tyvars1 @ tyvars2 in
+     { types; names; equations = Equations { store; tyvars} }
 
 let concat_disjoint env1 env2 =
   let exception Conflict of TermVarMap.key in
   try
     let combine x _ _ =
       raise (Conflict x) in
-    let types = TermVarMap.union combine env1.types env2.types
-    and names = N2DB.concat env1.names env2.names in
-    Ok { types; names; }
+    let types = TermVarMap.union combine env1.types env2.types in
+    let names = N2DB.concat env1.names env2.names in
+    match (env1.equations, env2.equations) with
+    | Inconsistent,_ | _, Inconsistent ->
+       Ok { types; names; equations = Inconsistent }
+    | Equations { store = store1; tyvars = tyvars1 },
+      Equations { store = store2; tyvars = tyvars2 } ->
+       assert (store1 == store2);
+       let store = store1 in
+       let tyvars = tyvars1 @ tyvars2 in
+       Ok { types; names; equations = Equations { store; tyvars } }
   with Conflict x -> Error x
 
 (* -------------------------------------------------------------------------- *)
@@ -130,204 +205,182 @@ let rec as_forall ty =
 
 (* -------------------------------------------------------------------------- *)
 
-(* [equal1] groups the easy cases of the type equality test. It does not
-   accept arguments of the form [TyMu]. It expects a self parameter [equal]
-   that is used to compare the children of the two root nodes. *)
-
-let pointwise equal tys1 tys2 =
-  try
-    List.for_all2 equal tys1 tys2
-  with Invalid_argument _ ->
-    (* Catching [Invalid_argument] is bad style, but saves a couple calls
-       to [List.length]. A cleaner approach would be to use arrays instead
-       of lists. *)
-    false
-
-let equal1 equal ty1 ty2 =
-  match ty1, ty2 with
-  | TyMu _, _
-  | _, TyMu _ ->
-      assert false
-  | TyVar x1, TyVar x2 ->
-      Int.equal x1 x2
-  | TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b) ->
-      equal ty1a ty2a && equal ty1b ty2b
-  | TyForall ((), ty1), TyForall ((), ty2) ->
-      equal ty1 ty2
-  | TyProduct tys1, TyProduct tys2 ->
-      pointwise equal tys1 tys2
-  | TyConstr (Datatype.Type tyconstr1, tys1),
-    TyConstr (Datatype.Type tyconstr2, tys2) ->
-      String.equal tyconstr1 tyconstr2 &&
-      pointwise equal tys1 tys2
-  | (TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _),
-    _ ->
-      false
-
-(* -------------------------------------------------------------------------- *)
-
-(* An unsound approximation of the equality test. (Now unused.) *)
-
-(* Comparing two [TyMu] types simply by comparing their bodies would be
-   correct, but incomplete: some types that are equal would be considered
-   different. *)
-
-(* Naively unfolding every [TyMu] type is sound and complete, but leads to
-   potential non-termination. The following code avoids non-termination by
-   imposing a budget limit. This makes this equality test unsound: two types
-   may be considered equal when they are in fact different. *)
-
-let rec equal budget ty1 ty2 =
-  match ty1, ty2 with
-  | (TyMu _ as ty1), ty2
-  | ty2, (TyMu _ as ty1) ->
-      budget = 0 || equal (budget - 1) (unfold ty1) ty2
-  | _, _ ->
-      equal1 (equal budget) ty1 ty2
-
-let budget =
-  4
-
-let _unsound_equal ty1 ty2 =
-  equal budget ty1 ty2
-
-(* -------------------------------------------------------------------------- *)
-
 (* A sound approximation of the equality test. *)
 
 (* The System F types produced by an ML type inference algorithm cannot
    contain [TyForall] under [TyMu]. In this restricted setting, deciding
-   type equality is relatively easy. We proceed in two layers, as follows:
-
-   - Initially, we perform a normal (structural) equality test, going
-     down under [TyForall] constructors if necessary. As soon as we
-     hit a [TyMu] constructor on either side, we switch to the lower
-     layer:
-
-   - In the lower layer, we know that we cannot hit a [TyForall]
-     constructor (if we do, we report that the types differ). We
-     map each type (separately) to a graph of unification variables
-     (where every variable has rigid structure), then we check that
-     the two graphs can be unified. *)
+   type equality is relatively easy. We map each type to a graph of
+   unification variables (where every variable has rigid structure),
+   then we check that the two graphs can be unified. *)
 
 exception Clash =
   Structure.Iter2
 
-module S =
-  Structure
-
-type vertex =
-  structure UnionFind.elem
-
-and structure =
-  | SRigidVar of DeBruijn.index
-  | SStruct of vertex S.structure
-
-let rec translate (env : vertex list) (ty : F.debruijn_type) : vertex =
-  match ty with
+(* This function assumes no universal quantification inside a μ-type, because
+   it would be difficult to check type equality otherwise. The boolean
+   [inside_mu] tracks whether we are already under a μ quantifier. *)
+let rec translate ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
+  : vertex
+  = match ty with
 
   | TyVar x ->
-      (* If [x] is bound in [env], then [x] is bound by μ, and we
-         already have a vertex that represents it. Otherwise, [x]
-         is bound by ∀, and it is regarded as a rigid variable. *)
-      let n = List.length env in
-      if x < n then
-        List.nth env x
-      else
-        UnionFind.make (SRigidVar (x - n))
+      begin
+        (* If the type is closed, then [x] was bound by a quantifier before and
+           was added to the environment. *)
+        try
+          List.nth env x
+        with Not_found ->
+          raise (TypeError (UnboundTypeVariable x))
+      end
 
   | TyMu ((), ty) ->
       (* Extend the environment with a mapping of this μ-bound variable
          to a fresh vertex. *)
-      let dummy : structure = SRigidVar 0 in
-      let v1 = UnionFind.make dummy in
+      let v1 = UF.make store None in
       let env = v1 :: env in
       (* Translate the body. *)
-      let v2 = translate env ty in
+      let v2 = translate ~inside_mu:true store env ty in
       (* Unify the vertices [v1] and [v2], keeping [v2]'s structure. *)
-      let v = UnionFind.merge (fun _ s2 -> s2) v1 v2 in
+      let v = UF.merge store (fun _ s2 -> s2) v1 v2 in
       v
 
-  | TyForall _ ->
-      (* Either we have found a ∀ under a μ, which is unexpected, or one
-         of the types that we are comparing has more ∀ quantifiers than
-         the other. Either way, we report that the types differ. *)
-      raise Clash
+  | TyForall ((), ty) ->
+      assert (not inside_mu);
+      (* Extend the environment with a mapping of this forall-bound variable
+         to a fresh vertex. *)
+      let v1 = UF.make store (Some (SForallLevel (List.length env))) in
+      let env = v1 :: env in
+      (* Translate the body. *)
+      let v2 = translate ~inside_mu store env ty in
+      UF.make store (Some (SForall v2))
 
   | TyArrow (ty1, ty2) ->
-      let v1 = translate env ty1
-      and v2 = translate env ty2 in
-      UnionFind.make (SStruct (S.TyArrow (v1, v2)))
+      let v1 = translate ~inside_mu store env ty1
+      and v2 = translate ~inside_mu store env ty2 in
+      UF.make store (Some (SStruct (S.TyArrow (v1, v2))))
 
   | TyProduct tys ->
-      let vs = translate_list env tys in
-      UnionFind.make (SStruct (S.TyProduct vs))
+      let vs = translate_list ~inside_mu store env tys in
+      UF.make store (Some (SStruct (S.TyProduct vs)))
 
   | TyConstr (id, tys) ->
-      let vs = translate_list env tys in
-      UnionFind.make (SStruct (S.TyConstr (id, vs)))
+      let vs = translate_list ~inside_mu store env tys in
+      UF.make store (Some (SStruct (S.TyConstr (id, vs))))
+
+  | TyEq (ty1, ty2) ->
+      let v1 = translate ~inside_mu store env ty1
+      and v2 = translate ~inside_mu store env ty2 in
+      UF.make store (Some (SStruct (S.TyEq (v1, v2))))
 
-and translate_list env tys =
-  List.map (translate env) tys
+and translate_list ~inside_mu store env tys =
+  List.map (translate ~inside_mu store env) tys
 
 let insert q v1 v2 =
   Stack.push (v1, v2) q
 
 let unify_struct q s1 s2 =
   match s1, s2 with
-  | SRigidVar x1, SRigidVar x2 ->
+  | SForallLevel x1, SForallLevel x2 ->
       if x1 <> x2 then raise Clash
   | SStruct s1, SStruct s2 ->
       Structure.iter2 (insert q) s1 s2
-  | SRigidVar _, SStruct _
-  | SStruct _, SRigidVar _ ->
+  | SForall s1, SForall s2 ->
+      insert q s1 s2
+  | SForallLevel _, _
+  | SStruct _, _
+  | SForall _, _ ->
       raise Clash
 
-let merge_struct q s1 s2 =
-  unify_struct q s1 s2;
-  s1
-
-let rec unify q (v1 : vertex) (v2 : vertex) =
-  let (_ : vertex) = UnionFind.merge (merge_struct q) v1 v2 in
-  unify_pending q
 
-and unify_pending q =
+(* We need two operations on equalities between types:
+   - add an equality to the equations in the environment
+   - check if a given equality holds modulo the equations in the environment *)
+
+(* Both operations can be described as first decomposing a given equality
+   "ty1 = ty2" into "simple equalities" between a rigid variable and a type.
+   In fact, the union-find data structure that we use to represent an
+   environment of equations store exactly those simple equalities. *)
+
+(* Then:
+   - to add an equality, we modify our environment by unifying the type
+     variables with the equated type
+   - to check an equality, we check that the simple equalities are already
+     valid in the equations of the environment, and fail otherwise *)
+
+(* The decomposition process does not produce simple equalities if the
+   provided equality is absurd ("int * int = int * bool").
+   Then:
+   - if we are adding this equality to the environment, we record that the
+     environment is now Inconsistent
+   - if we are checking the equality (in a consistent environment), we fail *)
+
+(* The functions below implement a unification procedure that implements both
+   these operations, depending on a [mode] parameter:
+   - in [Input] mode, they add an equality to the environment
+   - in [Check] mode, they check that the equality holds modulo the equations
+   in the environment *)
+
+type mode = Input | Check
+
+let merge_struct mode q so1 so2 : structure option =
+  match so1, so2 with
+  | Some s1, Some s2 ->
+     unify_struct q s1 s2;
+     so1
+  | None, so | so, None ->
+     match mode with
+     | Input ->
+        so
+     | Check ->
+        raise Clash
+
+let rec unify mode store q (v1 : vertex) (v2 : vertex) =
+  let (_ : vertex) = UF.merge store (merge_struct mode q) v1 v2 in
+  unify_pending mode store q
+
+and unify_pending mode store q =
   match Stack.pop q with
   | v1, v2 ->
-      unify q v1 v2
+      unify mode store q v1 v2
   | exception Stack.Empty ->
       ()
 
-let unify v1 v2 =
+let unify mode store v1 v2 =
   let q = Stack.create() in
-  unify q v1 v2
-
-let rec equal ty1 ty2 =
-  match ty1, ty2 with
-  | (TyMu _ as ty1), ty2
-  | ty2, (TyMu _ as ty1) ->
-      (* We have hit a μ binder on one side. Switch to layer-1 mode. *)
-      begin try
-        let env = [] in
-        let v1 = translate env ty1
-        and v2 = translate env ty2 in
-        unify v1 v2;
-        true
-      with Clash ->
-        false
-      end
-  | _, _ ->
-      (* Otherwise, continue in layer-2 mode. *)
-      equal1 equal ty1 ty2
+  unify mode store q v1 v2
+
+let unify_types mode env ty1 ty2 =
+  match env.equations with
+  | Inconsistent ->
+     true
+  | Equations { store ; tyvars } ->
+     try
+       let v1 = translate ~inside_mu:false store tyvars ty1
+       and v2 = translate ~inside_mu:false store tyvars ty2 in
+       unify mode store v1 v2;
+       true
+     with Clash ->
+       false
 
 (* -------------------------------------------------------------------------- *)
 
-(* Re-package the type equality test as a type equality check. *)
-
-let (--) ty1 ty2 : unit =
-  if not (equal ty1 ty2) then
+(* Re-package the type unification as a type equality check. *)
+let enforce_equal env ty1 ty2 : unit =
+  if not (unify_types Check env ty1 ty2) then
     raise (TypeError (TypeMismatch (ty1, ty2)))
 
+(* Re-package the type unification as an addition in the environment. *)
+let add_equation env ty1 ty2 : env =
+  if unify_types Input env ty1 ty2 then
+    env
+  else
+    { env with equations = Inconsistent }
+
+let copy_env env store tyvars =
+  let store_copy = UF.copy store in
+  let equations = Equations { store = store_copy; tyvars } in
+  { env with equations }
+
 (* -------------------------------------------------------------------------- *)
 
 (* The type-checker. *)
@@ -349,14 +402,14 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
       List.iter on_subterm ts;
       ty
   | Annot (_, t, ty) ->
-      typeof env t -- ty;
+      enforce_equal env (typeof env t) ty;
       ty
   | Abs (_, x, ty1, t) ->
       let ty2 = typeof (extend_with_tevar env x ty1) t in
       TyArrow (ty1, ty2)
   | App (_, t, u) ->
       let ty1, ty2 = as_arrow (typeof env t) in
-      typeof env u -- ty1;
+      enforce_equal env (typeof env u) ty1;
       ty2
   | Let (_, x, t, u) ->
       let env = extend_with_tevar env x (typeof env t) in
@@ -375,7 +428,7 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
   | Variant (_, lbl, dty, t) ->
       let arg_type = typeof_variant datatype_env lbl dty in
       let ty = typeof env t in
-      ty -- arg_type;
+      enforce_equal env ty arg_type;
       TyConstr dty
   | LetProd (_, xs, t, u) ->
       let ty = typeof env t in
@@ -387,8 +440,32 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
   | Match (_, ty, t, brs) ->
       let scrutinee_ty = typeof env t in
       let tys = List.map (typeof_branch datatype_env env scrutinee_ty) brs in
-      List.iter ((--) ty) tys;
+      List.iter (fun ty2 -> enforce_equal env ty ty2) tys;
       ty
+  | Absurd (_, ty) ->
+      begin
+        match env.equations with
+        | Inconsistent ->
+           ty
+        | Equations _ ->
+           raise (TypeError (ContextNotAbsurd))
+      end
+  | Refl (_, ty) ->
+      TyEq (ty, ty)
+  | Use (_, t, u) ->
+     begin
+       match env.equations with
+       | Inconsistent ->
+          typeof env u
+       | Equations { store ; tyvars } ->
+          let env = copy_env env store tyvars in
+          match typeof env t with
+          | TyEq (ty1, ty2) ->
+             let env = add_equation env ty1 ty2 in
+             typeof env u
+          | ty ->
+             raise (TypeError (NotAnEqual ty))
+     end
 
 and typeof_variant datatype_env lbl (tid, tyargs) =
   let Datatype.{ data_kind ; type_params ; labels_descr; _ } =
@@ -407,19 +484,19 @@ and typeof_variant datatype_env lbl (tid, tyargs) =
   ) tyargs type_params arg_type
 
 and typeof_branch datatype_env env scrutinee_ty (pat, rhs) =
-  let new_bindings = binding_pattern datatype_env scrutinee_ty pat in
+  let new_bindings = binding_pattern datatype_env env scrutinee_ty pat in
   let new_env = concat env new_bindings in
   typeof datatype_env new_env rhs
 
-and binding_pattern datatype_env scrutinee_ty pat =
-  let binding_pattern = binding_pattern datatype_env in
+and binding_pattern datatype_env env scrutinee_ty pat =
+  let binding_pattern = binding_pattern datatype_env env in
   match pat with
   | PVar (_, x) ->
       singleton x scrutinee_ty
   | PWildcard _ ->
       empty
   | PAnnot (_, pat, ty) ->
-      scrutinee_ty -- ty;
+      enforce_equal env scrutinee_ty ty;
       binding_pattern ty pat
   | PTuple (_, ps) ->
       let tys = as_product scrutinee_ty in
@@ -432,7 +509,7 @@ and binding_pattern datatype_env scrutinee_ty pat =
       List.fold_left f empty envs
   | PVariant (_, lbl, dty, pat) ->
       let arg_type = typeof_variant datatype_env lbl dty in
-      scrutinee_ty -- TyConstr dty;
+      enforce_equal env scrutinee_ty (TyConstr dty);
       binding_pattern arg_type pat
 
 let typeof datatype_env t =

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)
@@ -239,7 +241,10 @@ let rec map_co (f : 'a -> 'b co) : 'a list -> 'b list co
       and+ ys = map_co f xs
       in y :: ys
 
-let rec convert_deep (env : ML.datatype_env) (params : (ML.tyvar * variable) list) (ty : ML.typ) : deep_ty =
+let rec convert_deep
+  (env : ML.datatype_env) (params : (ML.tyvar * variable) list) (ty : ML.typ)
+  : deep_ty
+  =
   let conv ty = convert_deep env params ty in
   match ty with
   | ML.TyVar (_, tx) ->

client/Infer.mli

@@ -2,7 +2,7 @@ type range = Lexing.position * Lexing.position
 exception Unbound of range * ML.tevar
 exception Unify of range * F.nominal_type * F.nominal_type
 exception Cycle of range * F.nominal_type
-exception VariableScopeEscape of range
+exception VariableScopeEscape of range * int * int
 
 (* Contraint generation, constraint solving and elaboration, combined. *)
 val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term

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

@@ -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 -> ()

client/test/CheckML.ml

@@ -37,7 +37,7 @@ let translate ~verbose ~rectypes e t =
         Printf.fprintf stdout "%!";
       end;
       None
-  | Infer.VariableScopeEscape range ->
+  | Infer.VariableScopeEscape (range, _, _) ->
       if verbose then begin
           Printf.fprintf stdout
             "%sA rigid variable escapes its scope.\n%!"

client/test/TestF.ml

@@ -1,141 +1,667 @@
 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.(