Remove unused equality check and change comments.

The term Refl is a proof of a type equality TyEq(ty1,ty2) and Use is a construct that introduce a type equality in the typing context.

client/F.ml

@@ -27,6 +27,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
 
@@ -69,6 +70,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 +153,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 +226,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

@@ -26,6 +26,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
 
@@ -72,6 +73,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,16 @@ 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
   | TwoOccurencesOfSameVariable x ->
       str "Scope error." ++
       str "The variable %s is bound twice in a pattern." x
+  | ContextNotAbsurd ->
+      str "Type error." ++
+      str "The context is not absurd"

client/FTypeChecker.ml

@@ -6,8 +6,10 @@ type type_error =
   | NotAnArrow of debruijn_type
   | NotAProduct of debruijn_type
   | NotAForall of debruijn_type
+  | NotAnEqual of debruijn_type
   | UnboundTermVariable of tevar
   | TwoOccurencesOfSameVariable of string
+  | ContextNotAbsurd
 
 and arity_requirement = Index of int | Total of int
 
@@ -37,19 +39,59 @@ module TermVarMap =
 module N2DB =
   DeBruijn.Nominal2deBruijn(TermVar)
 
+(* We use a union-find to represent equalities between rigid variables
+   and types. We need the ability to snapshot and rollback changes, to
+   "un-do" 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
+   only possible 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
+
 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;
+  (* The global store of the union-find. *)
+  store: structure option UF.store;
+  (* A mapping from rigid variables to union-find vertices. *)
+  tyvars: structure option UF.elem list;
+  (* Is set to false when an inconsistent equation is introduced in the
+     environment. It is useful while typechecking pattern-matching. *)
+  consistent: bool;
 }
 
-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;
+  store = UF.new_store();
+  tyvars = [];
+  consistent = true;
+}
 
-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 +104,47 @@ 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; store; tyvars; consistent } 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 } =
+    names = N2DB.slide names x;
+    store;
+    tyvars;
+    consistent; }
+
+let extend_with_tyvar { types; names; store; tyvars; consistent } =
+  (* 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. *)
-  { types; names = N2DB.bump names }
+  let names = N2DB.bump names in
+  { types; names ; store; tyvars; consistent }
 
 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
+  let store = (assert (env1.store == env2.store); env1.store) in
+  let tyvars = env2.tyvars @ env1.tyvars in
+  let consistent = env1.consistent && env2.consistent in
+  { types; names; store; tyvars; consistent }
 
 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
+    let store = (assert (env1.store == env2.store); env1.store) in
+    let tyvars = env2.tyvars @ env1.tyvars in
+    let consistent = env1.consistent && env2.consistent in
+    Ok { types; names; store; tyvars; consistent }
   with Conflict x -> Error x
 
 (* -------------------------------------------------------------------------- *)
@@ -130,202 +187,133 @@ 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 that no occurence of forall quantification
+   appear under a mu-type. *)
+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))
+      List.nth env x
 
   | 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) ->
+      if inside_mu then raise Clash;
+     (* 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))))
 
-and translate_list env tys =
-  List.map (translate env) tys
+  | 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 ~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 =
+(* When we try to perform an equality check, the [mode] tells us if
+   one should unify rigid variables with structure (Input mode), that
+   is add new equalities in the typing context, or if it is not allowed
+   (Check mode). *)
+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 equal mode env ty1 ty2 =
+  not env.consistent ||
+  try
+    let v1 = translate ~inside_mu:false env.store env.tyvars ty1
+    and v2 = translate ~inside_mu:false env.store env.tyvars ty2 in
+    unify mode env.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
+let (--) ty1 ty2 env : unit =
+  if not (equal Check env ty1 ty2) then
     raise (TypeError (TypeMismatch (ty1, ty2)))
 
 (* -------------------------------------------------------------------------- *)
@@ -349,14 +337,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;
+      (typeof env t -- ty) env;
       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;
+      (typeof env u -- ty1) env;
       ty2
   | Let (_, x, t, u) ->
       let env = extend_with_tevar env x (typeof env t) in
@@ -375,7 +363,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;
+      (ty -- arg_type) env;
       TyConstr dty
   | LetProd (_, xs, t, u) ->
       let ty = typeof env t in
@@ -387,8 +375,30 @@ 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 -> (--) ty ty2 env) tys;
       ty
+  | Absurd (_, ty) ->
+      if env.consistent then
+        raise (TypeError (ContextNotAbsurd))
+      else
+        ty
+  | Refl (_, ty) ->
+      TyEq (ty, ty)
+  | Use (_, t, u) ->
+      let store_copy = UF.copy env.store in
+      let env = { env with store = store_copy } in
+      begin
+        match typeof env t with
+        | TyEq (ty1, ty2) ->
+           if equal Input env ty1 ty2 then
+             (* typecheck [u] in a context containing equalities introduced by
+                the equality ty1 = ty2 *)
+             typeof env u
+           else
+             typeof { env with consistent = false } 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 +417,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;
+      (scrutinee_ty -- ty) env;
       binding_pattern ty pat
   | PTuple (_, ps) ->
       let tys = as_product scrutinee_ty in
@@ -432,7 +442,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;
+      (scrutinee_ty -- TyConstr dty) env;
       binding_pattern arg_type pat
 
 let typeof datatype_env t =

client/FTypeChecker.mli

@@ -8,8 +8,10 @@ type type_error =
   | NotAnArrow of debruijn_type
   | NotAProduct of debruijn_type
   | NotAForall of debruijn_type
+  | NotAnEqual of debruijn_type
   | UnboundTermVariable of tevar
   | 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) =
@@ -119,7 +123,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 ^^
@@ -147,6 +151,11 @@ and print_term_abs t =
       ^^ print_pattern p ^^ space
       ^^ string "->"
       ^//^ 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
 
@@ -163,6 +172,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
 
@@ -180,8 +194,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

@@ -16,3 +16,20 @@ let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
     Utils.emit_endline (FPrinter.print_type_error e);
     failwith "Type-checking error."
   | Ok _v -> ()
+
+let test_error (env : F.nominal_datatype_env) (t : F.nominal_term) =
+  Printf.printf "Formatting the System F term...\n%!";
+  let doc = FPrinter.print_term t in
+  Printf.printf "Pretty-printing the System F term...\n%!";
+  Utils.emit_endline doc;
+  let env : F.debruijn_datatype_env =
+    F.translate_env env in
+  print_string "Converting the System F term to de Bruijn style...\n";
+  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
+  | Error _ ->
+     ()
+  | Ok _v ->
+     failwith "Type-checking error."

client/test/TestF.ml

@@ -1,141 +1,669 @@
 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 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))