[WIP] change the semantics of absurd.

We use the search function that maintains a maximum scope during traversal.
The other search function is removed.

.gitlab-ci.yml

@@ -1,10 +0,0 @@
-include: 'https://gitlab.com/gasche/gitlab-ocaml-ci-example/-/raw/11c1d7e/.gitlab-ci.yml'
-
-
-.build-matrix:
-  parallel:
-    matrix:
-    - OCAML_COMPILER: "4.12.0"
-
-variables:
-  DUNE_DOC_TARGETS: ""

CHANGES.md

@@ -2,6 +2,16 @@
 
 ## 2022/06/03
 
+* **Incompatible** changes to the Solver error-handling logic: instead of
+  raising several different exceptions, the solver now raises a single Error
+  exception carrying a datatype indicating the error case.
+
+  All errors now consistently report the source location when
+  available (if it was provided when building the constraint). This
+  improves in particular the error-reporting behavior of our
+  demonstration client, which is now able to show source locations on
+  type-checking errors.
+
 * Support for rigid variables, that is, variables that cannot be unified with
   other rigid variables or with older flexible variables. These variables are
   introduced by the new combinators `letr1` and `letrn`. The exception

client/Datatype.ml

@@ -1,5 +1,5 @@
-(* tyconstr_id is the name of an datatype constructor.
-   label_id is the name of a field label or data constructor. *)
+(* [tyconstr_id] is the name of an datatype constructor.
+   [label_id] is the name of a field label or data constructor. *)
 type tyconstr_id = Type of string
 type label_id = Label of string
 
@@ -46,6 +46,8 @@ module Env = struct
     }
 
   exception UnexpectedRecord
+  exception DeclarationNotFound of tyconstr_id
+  exception LabelNotFound of label_id
 
   let empty = {
       datatypes = TyConstrMap.empty;
@@ -64,19 +66,17 @@ module Env = struct
       labels = add_labels e.labels tdescr.labels_descr;
     }
 
-  let find_label { labels ; _ } (Label l) =
-    LabelMap.find (Label l) labels
-
-  let find_decl { datatypes ; _ } (Type tid) =
-    TyConstrMap.find (Type tid) datatypes
-
-  let label_index { labels_descr ; _ } l =
-    let combine i ldescr = (i, ldescr.label_name) in
-    List.mapi combine labels_descr
-    |> List.find (fun (_, l') -> l = l')
-    |> fst
-
-  let () = ignore label_index
+  let find_label { labels ; _ } label =
+    try
+      LabelMap.find label labels
+    with Not_found ->
+       raise (LabelNotFound label)
+
+  let find_decl { datatypes ; _ } tid =
+    try
+      TyConstrMap.find tid datatypes
+    with Not_found ->
+       raise (DeclarationNotFound tid)
 
   let map (type b1 b2 t1 t2)
     (f : (b1, t1) decl -> (b2, t2) decl)

client/Datatype.mli

@@ -1,5 +1,5 @@
-(* tyconstr_id is the name of an datatype constructor.
-   label_id is the name of a field label or data constructor. *)
+(* [tyconstr_id] is the name of an datatype constructor.
+   [label_id] is the name of a field label or data constructor. *)
 type tyconstr_id = Type of string
 type label_id = Label of string
 
@@ -34,6 +34,8 @@ module Env : sig
   type ('b, 't) t
 
   exception UnexpectedRecord
+  exception DeclarationNotFound of tyconstr_id
+  exception LabelNotFound of label_id
 
   val empty: ('b, 't) t
   val add_decl: ('b, 't) t -> ('b, 't) decl -> ('b, 't) t

client/DeBruijn.ml

@@ -79,21 +79,6 @@ module Nominal2deBruijn (N : Map.OrderedType) = struct
     let current = current + 1 in
     { map; current }
 
-  (* [concat env1 env2] extends [env1] with all the bindings of [env2];
-     bindings of [env2] shadow any binding of the same variable in [env1]. *)
-
-  let concat env1 env2 =
-    (* We need to shift the de Bruijn levels of [env2] (and its
-       [current] value) by as many bindings as there are in [env1]. *)
-    let shift _x in1 in2 =
-      match in2 with
-      | None -> in1
-      | Some lvl -> Some (env1.current + lvl)
-    in
-    {
-      current = env1.current + env2.current;
-      map = M.merge shift env1.map env2.map;
-    }
 end
 
 (* -------------------------------------------------------------------------- *)

client/DeBruijn.mli

@@ -49,11 +49,6 @@ module Nominal2deBruijn (N : Map.OrderedType) : sig
      to [slide (bump env) x]. *)
 
   val bump: env -> env
-
-  (* [concat env1 env2] extends [env1] with all the bindings of [env2];
-     bindings of [env2] shadow any binding of the same variable in [env1]. *)
-
-  val concat: env -> env -> env
 end
 
 (* -------------------------------------------------------------------------- *)

client/F.ml

@@ -4,21 +4,26 @@
 
 (* 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
    F. *)
 
-type range =
-  Lexing.position * Lexing.position
-
-let dummy_range : range =
-  Lexing.(dummy_pos, dummy_pos)
+type loc = Utils.loc
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -27,10 +32,12 @@ 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
 
-type tyvar = int
+type tyvar =
+    string * int
 
 type nominal_type =
     (tyvar, tyvar) typ
@@ -53,31 +60,56 @@ 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
-  | Hole of range * ('a, 'b) typ * ('a, 'b) term list
-  | Annot of range * ('a, 'b) term * ('a, 'b) typ
-  | Abs of range * tevar * ('a, 'b) typ * ('a, 'b) term
-  | App of range * ('a, 'b) term * ('a, 'b) term
-  | Let of range * tevar * ('a, 'b) term * ('a, 'b) term
-  | TyAbs of range * 'b * ('a, 'b) term
-  | TyApp of range * ('a, 'b) term * ('a, 'b) typ
-  | Tuple of range * ('a, 'b) term list
-  | Proj of range * int * ('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
+  | Var of loc *  tevar
+  | Hole of loc * ('a, 'b) typ * ('a, 'b) term list
+  | Annot of loc * ('a, 'b) term * ('a, 'b) typ
+  | Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
+  | App of loc * ('a, 'b) term * ('a, 'b) term
+  | Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
+  | TyAbs of loc * 'b * ('a, 'b) term
+  | TyApp of loc * ('a, 'b) term * ('a, 'b) typ
+  | Tuple of loc * ('a, 'b) term list
+  | Proj of loc * int * ('a, 'b) term
+  | LetProd of loc * tevar list * ('a, 'b) term * ('a, 'b) term
+  | Variant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
+  | Match of loc * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
+  | Absurd of loc * ('a,'b) typ
+  | Refl of loc * ('a,'b) typ
+  | Use of loc * ('a,'b) term * ('a,'b) typ * ('a,'b) typ * ('a,'b) term
+
+and rec_status = Recursive | Non_recursive
 
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
 and ('a,'b) pattern =
-  | PVar of range * tevar
-  | PAnnot of range * ('a, 'b) pattern * ('a, 'b) typ
-  | PWildcard of range
-  | PTuple of range * ('a,'b) pattern list
-  | PVariant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
+  | PVar of loc * tevar
+  | PAnnot of loc * ('a, 'b) pattern * ('a, 'b) typ
+  | PWildcard of loc
+  | PTuple of loc * ('a,'b) pattern list
+  | PVariant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
 
 type nominal_term = (tyvar, tyvar) term
 type nominal_pattern = (tyvar, tyvar) pattern
@@ -90,10 +122,10 @@ type debruijn_term =
 
 (* Constructors. *)
 
-let ftyabs vs t =
-  List.fold_right (fun v t -> TyAbs (dummy_range, v, t)) vs t
-let ftyapp t tys =
-  List.fold_left (fun t ty -> TyApp (dummy_range, t, ty)) t tys
+let ftyabs ~loc vs t =
+  List.fold_right (fun v t -> TyAbs (loc, v, t)) vs t
+let ftyapp ~loc t tys =
+  List.fold_left (fun t ty -> TyApp (loc, t, ty)) t tys
 
 (* -------------------------------------------------------------------------- *)
 
@@ -149,7 +181,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
 
 (* -------------------------------------------------------------------------- *)
@@ -169,36 +204,39 @@ module TypeInTerm : DeBruijn.TRAVERSE
 
   let rec traverse lookup extend env t =
     let trav env = traverse lookup extend env in
+    let trav_ty env ty =
+      TypeInType.traverse lookup extend env ty in
     match t with
     | Var (pos, x) ->
         Var (pos, x)
     | Hole (pos, ty, ts) ->
-      let ty' = TypeInType.traverse lookup extend env ty in
+      let ty' = trav_ty env ty in
       let ts' = List.map (trav env) ts in
       Hole (pos, ty', ts')
     | Annot (pos, t, ty) ->
         let t' = trav env t
-        and ty' = TypeInType.traverse lookup extend env ty in
+        and ty' = trav_ty env ty in
         Annot (pos, t', ty')
     | Abs (pos, x, ty, t) ->
-        let ty' = TypeInType.traverse lookup extend env ty
+        let ty' = trav_ty env ty
         and t' = trav env t in
         Abs (pos, x, ty', t')
     | App (pos, t1, t2) ->
         let t1' = trav env t1
         and t2' = trav env t2 in
         App (pos, t1', t2')
-    | Let (pos, x, t1, t2) ->
+    | Let (pos, rec_, x, ty, t1, t2) ->
+        let ty' = trav_ty env ty in
         let t1' = trav env t1
         and t2' = trav env t2 in
-        Let (pos, x, t1', t2')
+        Let (pos, rec_, x, ty', t1', t2')
     | TyAbs (pos, x, t) ->
         let env, x = extend env x in
         let t' = trav env t in
         TyAbs (pos, x, t')
     | TyApp (pos, t, ty) ->
         let t' = trav env t
-        and ty' = TypeInType.traverse lookup extend env ty in
+        and ty' = trav_ty env ty in
         TyApp (pos, t', ty')
     | Tuple (pos, ts) ->
         let ts' = List.map (trav env) ts in
@@ -215,10 +253,22 @@ module TypeInTerm : DeBruijn.TRAVERSE
         and t' = trav env t in
         Variant (pos, lbl, dty', t')
     | Match (pos, ty, t, brs) ->
-        let ty' = TypeInType.traverse lookup extend env ty in
+        let ty' = trav_ty env ty in
         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' = trav_ty env ty in
+        Absurd (pos, ty')
+    | Refl (pos, ty) ->
+        let ty' = trav_ty env ty in
+        Refl (pos, ty')
+    | Use (pos, t, ty1, ty2, u) ->
+        let t' = trav env t in
+        let ty1' = trav_ty env ty1 in
+        let ty2' = trav_ty env ty2 in
+        let u' = trav env u in
+        Use (pos, t', ty1', ty2', u')
 
   and traverse_datatype lookup extend env (tid, tyargs) =
     (tid, List.map (TypeInType.traverse lookup extend env) tyargs)
@@ -250,6 +300,11 @@ end
 
 (* -------------------------------------------------------------------------- *)
 
+module TyVar = struct
+  type t = tyvar
+  let compare = Stdlib.compare
+end
+
 (* Type-in-type weakening and substitution. *)
 
 module Type = struct
@@ -257,7 +312,7 @@ module Type = struct
 
   include DeBruijn.MakeSubst(TypeVar)(TypeInType)(TypeInType)
 
-  include DeBruijn.MakeTranslate(TypeVar)(TypeInType)(Int)
+  include DeBruijn.MakeTranslate(TypeVar)(TypeInType)(TyVar)
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -265,11 +320,11 @@ end
 (* Translation of nominal terms to de Bruijn terms. *)
 
 module Term = struct
-  include DeBruijn.MakeTranslate(TypeVar)(TypeInTerm)(Int)
+  include DeBruijn.MakeTranslate(TypeVar)(TypeInTerm)(TyVar)
 end
 
 
-module N2DB = DeBruijn.Nominal2deBruijn(Int)
+module N2DB = DeBruijn.Nominal2deBruijn(TyVar)
 
 (* Translate a nominal-F datatype description into a De Bruijn version *)
 let translate_datatype tdescr =

client/F.mli

@@ -4,20 +4,26 @@
 
 (* 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
    F. *)
 
-type range =
-  Lexing.position * Lexing.position
-
-val dummy_range: range
+type loc = Utils.loc
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -26,12 +32,12 @@ 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
 
 type tyvar =
-    int
-
+    string * int
 type nominal_type =
     (tyvar, tyvar) typ
 
@@ -55,32 +61,54 @@ 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
 
 type ('a, 'b) term =
-  | Var of range * tevar
-  | Hole of range * ('a, 'b) typ * ('a, 'b) term list
-  | Annot of range * ('a, 'b) term * ('a, 'b) typ
-  | Abs of range * tevar * ('a, 'b) typ * ('a, 'b) term
-  | App of range * ('a, 'b) term * ('a, 'b) term
-  | Let of range * tevar * ('a, 'b) term * ('a, 'b) term
-  | TyAbs of range * 'b * ('a, 'b) term
-  | TyApp of range * ('a, 'b) term * ('a, 'b) typ
-  | Tuple of range * ('a, 'b) term list
-  | Proj of range * int * ('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
+  | Var of loc * tevar
+  | Hole of loc * ('a, 'b) typ * ('a, 'b) term list
+  | Annot of loc * ('a, 'b) term * ('a, 'b) typ
+  | Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
+  | App of loc * ('a, 'b) term * ('a, 'b) term
+  | Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
+  | TyAbs of loc * 'b * ('a, 'b) term
+  | TyApp of loc * ('a, 'b) term * ('a, 'b) typ
+  | Tuple of loc * ('a, 'b) term list
+  | Proj of loc * int * ('a, 'b) term
+  | LetProd of loc * tevar list * ('a, 'b) term * ('a, 'b) term
+  | Variant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
+  | Match of loc * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
+  | Absurd of loc * ('a,'b) typ
+  | Refl of loc * ('a,'b) typ
+  | Use of loc * ('a,'b) term * ('a,'b) typ * ('a,'b) typ * ('a,'b) term
+
+and rec_status = Recursive | Non_recursive
 
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
 and ('a,'b) pattern =
-  | PVar of range * tevar
-  | PAnnot of range * ('a, 'b) pattern * ('a, 'b) typ
-  | PWildcard of range
-  | PTuple of range * ('a,'b) pattern list
-  | PVariant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
+  | PVar of loc * tevar
+  | PAnnot of loc * ('a, 'b) pattern * ('a, 'b) typ
+  | PWildcard of loc
+  | PTuple of loc * ('a,'b) pattern list
+  | PVariant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
 
 type nominal_term =
     (tyvar, tyvar) term
@@ -98,11 +126,13 @@ type debruijn_term =
 
 (* Constructors. *)
 
-val ftyabs: 'b list -> ('a, 'b) term -> ('a, 'b) term
-val ftyapp: ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
+val ftyabs: loc:loc -> 'b list -> ('a, 'b) term -> ('a, 'b) term
+val ftyapp: loc:loc -> ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
 
 (* -------------------------------------------------------------------------- *)
 
+module TyVar : Map.OrderedType with type t = tyvar
+
 module Type : sig
   (* Type-in-type weakening and substitution. *)
 
@@ -116,7 +146,7 @@ module Type : sig
 
   (* Translation of nominal types to de Bruijn types. *)
   val translate: nominal_type -> debruijn_type
-  val translate_open: DeBruijn.Nominal2deBruijn(Int).env -> nominal_type -> debruijn_type
+  val translate_open: DeBruijn.Nominal2deBruijn(TyVar).env -> nominal_type -> debruijn_type
 end
 
 (* -------------------------------------------------------------------------- *)

client/FPrinter.ml

@@ -2,14 +2,11 @@
 
 (* We translate from System F to P and then print the P term (resp. type). *)
 
-let new_id : unit -> int =
-  Inferno.Utils.gensym()
-
-let new_tyvar () =
-  Printf.sprintf "a%d" (new_id())
+let new_tyvar (s,x) =
+  Printf.sprintf "%s%d" s x
 
-let translate_old_var (x : F.tyvar) =
-  Printf.sprintf "r%d" x
+let translate_old_var ((s,x) : F.tyvar) =
+  Printf.sprintf "?%s%d" s x
 
 let translate_tyvar env x =
   try
@@ -33,13 +30,15 @@ let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) :
   | F.TyProduct tys ->
       P.TyProduct (List.map (self env) tys)
   | F.TyForall (x, ty) ->
-      let alpha = new_tyvar () in
+      let alpha = new_tyvar x in
       P.TyForall (alpha, self ((x, alpha) :: env) ty)
   | F.TyMu (x, ty) ->
-      let alpha = new_tyvar () in
+      let alpha = new_tyvar x in
       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)
@@ -52,16 +51,21 @@ let rec translate_term env (t : F.nominal_term) : P.term =
   | F.Hole (_, ty, ts) ->
       P.Hole (Some (translate_type env ty), List.map (self env) ts)
   | F.Annot (_, t, ty) ->
-      P.Annot (self env t, (P.Flexible, [], translate_type env ty))
+      P.Annot (self env t, translate_type env ty)
   | F.Abs (_, x, ty, t) ->
-      let annot = P.PAnnot (P.PVar x, (P.Flexible, [], translate_type env ty)) in
-      P.Abs (annot, self env t)
+      let x_annot = P.PAnnot (P.PVar x, translate_type env ty) in
+      P.Abs (x_annot, self env t)
   | F.App (_, t1, t2) ->
       P.App (self env t1, self env t2)
-  | F.Let (_, x, t, u) ->
-      P.Let (P.PVar x, self env t, self env u)
+  | F.Let (_, rec_, x, ty, t, u) ->
+      let rec_ = match rec_ with
+      | F.Recursive -> P.Recursive
+      | F.Non_recursive -> P.Non_recursive
+      in
+      let x_annot = P.PAnnot (P.PVar x, translate_type env ty) in
+      P.Let (rec_, x_annot, self env t, self env u)
   | F.TyAbs (_, x, t) ->
-      let alpha = new_tyvar () in
+      let alpha = new_tyvar x in
       P.TyAbs (alpha, self ((x, alpha) :: env) t)
   | F.TyApp (_, t, ty) ->
       P.TyApp (self env t, translate_type env ty)
@@ -71,7 +75,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
       P.Proj (i, self env t)
   | F.LetProd (_, xs, t, u) ->
       let pat = P.PTuple (List.map (fun x -> P.PVar x) xs) in
-      P.Let (pat , self env t, self env u)
+      P.Let (P.Non_recursive, pat, self env t, self env u)
   | F.Variant (_, lbl, (tid, tys) , t) ->
       P.Variant (
           lbl,
@@ -84,6 +88,16 @@ 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 (Some (translate_type env ty))
+  | F.Refl (_, ty) ->
+      P.Refl (Some (translate_type env ty))
+  | F.Use (_, t, ty1, ty2, u) ->
+      let t' = self env t in
+      let ty1' = translate_type env ty1 in
+      let ty2' = translate_type env ty2 in
+      let u' = self env u in
+      P.Use (t', ty1', ty2', u')
 
 and translate_branch env (pat, t) =
   (translate_pattern env pat, translate_term env t)
@@ -96,7 +110,7 @@ and translate_pattern env pat =
   | F.PWildcard _ ->
       P.PWildcard
   | F.PAnnot (_, p, ty) ->
-      P.PAnnot (self env p, (P.Flexible, [], translate_type env ty))
+      P.PAnnot (self env p, translate_type env ty)
   | F.PTuple (_, ps) ->
       P.PTuple (List.map (self env) ps)
   | F.PVariant (_, lbl, (tid, tys), p) ->
@@ -118,7 +132,7 @@ let str =
 let (++) d1 d2 =
   d1 ^^ hardline ^^ d2
 
-let new_id : unit -> F.tyvar =
+let new_id : unit -> int =
   Inferno.Utils.gensym()
 
 let new_tyvar () : P.tyvar =
@@ -155,6 +169,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 +206,28 @@ 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."
+  | UnexpectedRecord ->
+      str "Type error." ++
+      str "A record was expected."
+  | DeclarationNotFound (Datatype.Type tid) ->
+      str "Scope error." ++
+      str "Unknown type declaration : %s." tid
+  | LabelNotFound (Datatype.Label lid) ->
+      str "Scope error." ++
+      str "Unknown variant constructor : %s." lid

client/FTypeChecker.ml

@@ -6,12 +6,19 @@ type type_error =
   | NotAnArrow of debruijn_type
   | NotAProduct of debruijn_type
   | NotAForall of debruijn_type
+  | NotAnEqual of debruijn_type
   | UnboundTermVariable of tevar
+  | UnboundTypeVariable of int
   | TwoOccurencesOfSameVariable of string
+  | ContextNotAbsurd
+  | UnexpectedRecord
+  | DeclarationNotFound of Datatype.tyconstr_id
+  | LabelNotFound of Datatype.label_id
+
 
 and arity_requirement = Index of int | Total of int
 
-exception TypeError of type_error
+exception TypeError of loc * type_error
 
 (* -------------------------------------------------------------------------- *)
 
@@ -37,58 +44,99 @@ 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 =
-  try
-    (* Obtain the type associated with [x]. *)
-    let ty = TermVarMap.find x types in
+let lookup ~loc { types; names; _ } x =
+  (* Obtain the type associated with [x]. *)
+  match TermVarMap.find x types with
+  | exception Not_found ->
+    raise (TypeError (loc, UnboundTermVariable x))
+  | ty ->
     (* Find how long ago [x] was bound. *)
     let w = N2DB.lookup names x in
     (* Shift the type [ty] by this amount, so that it makes sense in the
        current scope. *)
     Type.lift w 0 ty
-  with Not_found ->
-    (* 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 }
-
-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 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; }
-  with Conflict x -> Error x
+    names = N2DB.slide names x;
+    equations; }
+
+let extend_with_tevar_no_dup ~loc ({ types; _ } as env) x ty =
+  if TermVarMap.mem x types then
+    raise (TypeError (loc, TwoOccurencesOfSameVariable x));
+  extend_with_tevar env x ty
+
+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 } }
 
 (* -------------------------------------------------------------------------- *)
 
@@ -101,95 +149,32 @@ let unfold ty =
   | _ ->
       assert false
 
-let rec as_arrow ty =
+let rec as_arrow ~loc ty =
   match ty with
   | TyArrow (ty1, ty2) ->
       ty1, ty2
   | TyMu _ ->
-      as_arrow (unfold ty)
+      as_arrow ~loc (unfold ty)
   | _ ->
-      raise (TypeError (NotAnArrow ty))
+      raise (TypeError (loc, NotAnArrow ty))
 
-let rec as_product ty =
+let rec as_product ~loc ty =
   match ty with
   | TyProduct tys ->
       tys
   | TyMu _ ->
-      as_product (unfold ty)
+      as_product ~loc (unfold ty)
   | _ ->
-      raise (TypeError (NotAProduct ty))
+      raise (TypeError (loc, NotAProduct ty))
 
-let rec as_forall ty =
+let rec as_forall ~loc ty =
   match ty with
   | TyForall ((), ty) ->
       ty
   | TyMu _ ->
-      as_forall (unfold ty)
+      as_forall ~loc (unfold ty)
   | _ ->
-      raise (TypeError (NotAForall 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
+      raise (TypeError (loc, NotAForall ty))
 
 (* -------------------------------------------------------------------------- *)
 
@@ -197,204 +182,279 @@ let _unsound_equal ty1 ty2 =
 
 (* 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. *)