From 22dde290e53a71a0474f37b7ca24547b0d1627aa Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sat, 11 Feb 2023 22:01:30 +0100
Subject: [PATCH 1/5] include location ranges in FTypeChecker error messages

---
 client/FTypeChecker.ml       | 161 +++++++++++++++++------------------
 client/FTypeChecker.mli      |   4 +-
 client/Utils.ml              |   6 ++
 client/Utils.mli             |   6 ++
 client/test/BenchMLRandom.ml |   4 +-
 client/test/CheckF.ml        |   6 +-
 6 files changed, 99 insertions(+), 88 deletions(-)

diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index d5079d2..7a12b7e 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -18,7 +18,7 @@ type type_error =
 
 and arity_requirement = Index of int | Total of int
 
-exception TypeError of type_error
+exception TypeError of range * type_error
 
 (* -------------------------------------------------------------------------- *)
 
@@ -101,18 +101,17 @@ let 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; equations } x ty =
   (* Map the name [x] to [ty], and record when it was bound, without
@@ -121,9 +120,9 @@ let extend_with_tevar { types; names; equations } x ty =
     names = N2DB.slide names x;
     equations; }
 
-let extend_with_tevar_no_dup ({ types; _ } as env) x ty =
+let extend_with_tevar_no_dup ~loc ({ types; _ } as env) x ty =
   if TermVarMap.mem x types then
-    raise (TypeError (TwoOccurencesOfSameVariable x));
+    raise (TypeError (loc, TwoOccurencesOfSameVariable x));
   extend_with_tevar env x ty
 
 let extend_with_tyvar { types; names; equations } =
@@ -150,32 +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))
+      raise (TypeError (loc, NotAForall ty))
 
 (* -------------------------------------------------------------------------- *)
 
@@ -193,7 +192,7 @@ exception Clash =
 (* 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)
+let rec translate ~loc ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
   : vertex
   = match ty with
 
@@ -204,7 +203,7 @@ let rec translate ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
         try
           List.nth env x
         with Not_found ->
-          raise (TypeError (UnboundTypeVariable x))
+          raise (TypeError (loc, UnboundTypeVariable x))
       end
 
   | TyMu ((), ty) ->
@@ -213,7 +212,7 @@ let rec translate ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
       let v1 = UF.make store None in
       let env = v1 :: env in
       (* Translate the body. *)
-      let v2 = translate ~inside_mu:true store env ty in
+      let v2 = translate ~loc ~inside_mu:true store env ty in
       (* Unify the vertices [v1] and [v2], keeping [v2]'s structure. *)
       let v = UF.merge store (fun _ s2 -> s2) v1 v2 in
       v
@@ -225,29 +224,29 @@ let rec translate ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
       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
+      let v2 = translate ~loc ~inside_mu store env ty in
       UF.make store (Some (SForall v2))
 
   | TyArrow (ty1, ty2) ->
-      let v1 = translate ~inside_mu store env ty1
-      and v2 = translate ~inside_mu store env ty2 in
+      let v1 = translate ~loc ~inside_mu store env ty1
+      and v2 = translate ~loc ~inside_mu store env ty2 in
       UF.make store (Some (SStruct (S.TyArrow (v1, v2))))
 
   | TyProduct tys ->
-      let vs = translate_list ~inside_mu store env tys in
+      let vs = translate_list ~loc ~inside_mu store env tys in
       UF.make store (Some (SStruct (S.TyProduct vs)))
 
   | TyConstr (id, tys) ->
-      let vs = translate_list ~inside_mu store env tys in
+      let vs = translate_list ~loc ~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
+      let v1 = translate ~loc ~inside_mu store env ty1
+      and v2 = translate ~loc ~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
+and translate_list ~loc ~inside_mu store env tys =
+  List.map (translate ~loc ~inside_mu store env) tys
 
 let insert q v1 v2 =
   Stack.push (v1, v2) q
@@ -323,14 +322,14 @@ let unify mode store v1 v2 =
   let q = Stack.create() in
   unify mode store q v1 v2
 
-let unify_types mode env ty1 ty2 =
+let unify_types ~loc 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
+       let v1 = translate ~loc ~inside_mu:false store tyvars ty1
+       and v2 = translate ~loc ~inside_mu:false store tyvars ty2 in
        unify mode store v1 v2;
        true
      with Clash ->
@@ -339,13 +338,13 @@ let unify_types mode env ty1 ty2 =
 (* -------------------------------------------------------------------------- *)
 
 (* 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)))
+let enforce_equal ~loc env ty1 ty2 : unit =
+  if not (unify_types ~loc Check env ty1 ty2) then
+    raise (TypeError (loc, 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
+let add_equation ~loc env ty1 ty2 : env =
+  if unify_types ~loc Input env ty1 ty2 then
     env
   else
     { env with equations = Inconsistent }
@@ -359,74 +358,74 @@ let copy_env env store tyvars =
 
 (* The type-checker. *)
 
-let nth_type ty tys i =
+let nth_type ~loc ty tys i =
   if i < 0 || i >= List.length tys then
-    raise (TypeError (ArityMismatch (Index i, ty)))
+    raise (TypeError (loc, ArityMismatch (Index i, ty)))
   else
     List.nth tys i
 
 let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
   let typeof = typeof datatype_env in
   match t with
-  | Var (_, x) ->
-      lookup env x
+  | Var (loc, x) ->
+      lookup ~loc env x
   | Hole (_, ty, ts) ->
       let on_subterm t =
         ignore (typeof env t) in
       List.iter on_subterm ts;
       ty
-  | Annot (_, t, ty) ->
-      enforce_equal env (typeof env t) ty;
+  | Annot (loc, t, ty) ->
+      enforce_equal ~loc 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
-      enforce_equal env (typeof env u) ty1;
+  | App (loc, t, u) ->
+      let ty1, ty2 = as_arrow ~loc (typeof env t) in
+      enforce_equal ~loc env (typeof env u) ty1;
       ty2
   | Let (_, x, t, u) ->
       let env = extend_with_tevar env x (typeof env t) in
       typeof env u
   | TyAbs (_, (), t) ->
       TyForall ((), typeof (extend_with_tyvar env) t)
-  | TyApp (_, t, ty2) ->
-      Type.subst ty2 0 (as_forall (typeof env t))
+  | TyApp (loc, t, ty2) ->
+      Type.subst ty2 0 (as_forall ~loc (typeof env t))
   | Tuple (_, ts) ->
       let tys = List.map (typeof env) ts in
       TyProduct tys
-  | Proj (_, i, t) ->
+  | Proj (loc, i, t) ->
       let ty = typeof env t in
-      let tys = as_product ty in
-      nth_type ty tys i
-  | Variant (_, lbl, dty, t) ->
-      let arg_type = typeof_variant datatype_env lbl dty in
+      let tys = as_product ~loc ty in
+      nth_type ~loc ty tys i
+  | Variant (loc, lbl, dty, t) ->
+      let arg_type = typeof_variant datatype_env ~loc lbl dty in
       let ty = typeof env t in
-      enforce_equal env ty arg_type;
+      enforce_equal ~loc env ty arg_type;
       TyConstr dty
-  | LetProd (_, xs, t, u) ->
+  | LetProd (loc, xs, t, u) ->
       let ty = typeof env t in
-      let tys = as_product ty in
+      let tys = as_product ~loc ty in
       if List.length xs <> List.length tys then
-        raise (TypeError (ArityMismatch (Total (List.length xs), ty)));
+        raise (TypeError (loc, ArityMismatch (Total (List.length xs), ty)));
       let env = List.fold_left2 extend_with_tevar env xs tys in
       typeof env u
-  | Match (_, ty, t, brs) ->
+  | Match (loc, 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 (fun ty2 -> enforce_equal env ty ty2) tys;
+      List.iter (fun ty2 -> enforce_equal ~loc env ty ty2) tys;
       ty
-  | Absurd (_, ty) ->
+  | Absurd (loc, ty) ->
       begin
         match env.equations with
         | Inconsistent ->
            ty
         | Equations _ ->
-           raise (TypeError (ContextNotAbsurd))
+           raise (TypeError (loc, ContextNotAbsurd))
       end
   | Refl (_, ty) ->
       TyEq (ty, ty)
-  | Use (_, t, u) ->
+  | Use (loc, t, u) ->
      begin
        match env.equations with
        | Inconsistent ->
@@ -435,24 +434,24 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
           let env = copy_env env store tyvars in
           match typeof env t with
           | TyEq (ty1, ty2) ->
-             let env = add_equation env ty1 ty2 in
+             let env = add_equation ~loc env ty1 ty2 in
              typeof env u
           | ty ->
-             raise (TypeError (NotAnEqual ty))
+             raise (TypeError (loc, NotAnEqual ty))
      end
 
-and typeof_variant datatype_env lbl (tid, tyargs) =
+and typeof_variant datatype_env ~loc lbl (tid, tyargs) =
   let Datatype.{ data_kind ; type_params ; labels_descr; _ } =
     try
       Datatype.Env.find_decl datatype_env tid
     with Datatype.Env.DeclarationNotFound _ ->
-      raise (TypeError (DeclarationNotFound tid))
+      raise (TypeError (loc, DeclarationNotFound tid))
   in
   let Datatype.{ arg_type; _ } =
     try
       List.find (fun l -> l.Datatype.label_name = lbl) labels_descr
     with Datatype.Env.LabelNotFound _ ->
-      raise (TypeError (LabelNotFound lbl))
+      raise (TypeError (loc, LabelNotFound lbl))
   in
   begin
     match data_kind with
@@ -472,22 +471,22 @@ and typeof_branch datatype_env env scrutinee_ty (pat, rhs) : debruijn_type =
 and binding_pattern datatype_env env scrutinee_ty pat : env =
   let binding_pattern = binding_pattern datatype_env in
   match pat with
-  | PVar (_, x) ->
-      extend_with_tevar_no_dup env x scrutinee_ty
+  | PVar (loc, x) ->
+      extend_with_tevar_no_dup ~loc env x scrutinee_ty
   | PWildcard _ ->
       env
-  | PAnnot (_, pat, ty) ->
-      enforce_equal env scrutinee_ty ty;
+  | PAnnot (loc, pat, ty) ->
+      enforce_equal ~loc env scrutinee_ty ty;
       binding_pattern env ty pat
-  | PTuple (_, ps) ->
-      let tys = as_product scrutinee_ty in
+  | PTuple (loc, ps) ->
+      let tys = as_product ~loc scrutinee_ty in
       if List.length ps <> List.length tys then
         raise
-          (TypeError (ArityMismatch (Total (List.length ps), scrutinee_ty)));
+          (TypeError (loc, ArityMismatch (Total (List.length ps), scrutinee_ty)));
       List.fold_left2 binding_pattern env tys ps
-  | PVariant (_, lbl, dty, pat) ->
-      let arg_type = typeof_variant datatype_env lbl dty in
-      enforce_equal env scrutinee_ty (TyConstr dty);
+  | PVariant (loc, lbl, dty, pat) ->
+      let arg_type = typeof_variant datatype_env ~loc lbl dty in
+      enforce_equal ~loc env scrutinee_ty (TyConstr dty);
       binding_pattern env arg_type pat
 
 let typeof datatype_env t =
@@ -497,5 +496,5 @@ let typeof_result datatype_env u =
   match typeof datatype_env u with
   | v ->
       Ok v
-  | exception TypeError e ->
-      Error e
+  | exception TypeError (loc, e) ->
+      Error (loc, e)
diff --git a/client/FTypeChecker.mli b/client/FTypeChecker.mli
index 92324a9..8aa3866 100644
--- a/client/FTypeChecker.mli
+++ b/client/FTypeChecker.mli
@@ -24,7 +24,7 @@ type type_error =
 *)
 and arity_requirement = Index of int | Total of int
 
-exception TypeError of type_error
+exception TypeError of range * type_error
 
 (* [typeof env t] type-checks the closed term [t] in datatype environment [env]
    and constructs its type.
@@ -34,4 +34,4 @@ val typeof: debruijn_datatype_env -> debruijn_term -> debruijn_type
 
 (* Similar to {!typeof}, but returns a [result] type instead of raising an exception. *)
 val typeof_result:
-  debruijn_datatype_env -> debruijn_term -> (debruijn_type, type_error) result
+  debruijn_datatype_env -> debruijn_term -> (debruijn_type, range * type_error) result
diff --git a/client/Utils.ml b/client/Utils.ml
index f05e064..0b2a32c 100644
--- a/client/Utils.ml
+++ b/client/Utils.ml
@@ -15,3 +15,9 @@ let emit doc =
 let emit_endline doc =
   emit PPrint.(doc ^^ hardline);
   flush stdout
+
+type range = Lexing.position * Lexing.position
+
+let emit_error range doc =
+  print_string (MenhirLib.LexerUtil.range range);
+  emit_endline doc
diff --git a/client/Utils.mli b/client/Utils.mli
index cab144e..70338aa 100644
--- a/client/Utils.mli
+++ b/client/Utils.mli
@@ -15,3 +15,9 @@ val emit : PPrint.document -> unit
 (* Similar to {!emit}; [emit_endline] also includes a newline at the
    end and flushes [stdout]. *)
 val emit_endline : PPrint.document -> unit
+
+type range = Lexing.position * Lexing.position
+
+(* Similar to {!emit_endline}, but starts by printing
+   a source location range. *)
+val emit_error : range -> PPrint.document -> unit
diff --git a/client/test/BenchMLRandom.ml b/client/test/BenchMLRandom.ml
index 28c94d0..8c08856 100644
--- a/client/test/BenchMLRandom.ml
+++ b/client/test/BenchMLRandom.ml
@@ -62,8 +62,8 @@ let () =
   let time, () =
     Measure.time ~repetitions @@ fun () ->
     match FTypeChecker.typeof_result env v with
-    | Error e ->
-      Utils.emit_endline (FPrinter.print_type_error e);
+    | Error (range, e) ->
+      Utils.emit_error range (FPrinter.print_type_error e);
       failwith "Sanity check failed."
     | Ok _v -> ()
   in
diff --git a/client/test/CheckF.ml b/client/test/CheckF.ml
index 8a5c686..0614a89 100644
--- a/client/test/CheckF.ml
+++ b/client/test/CheckF.ml
@@ -4,7 +4,7 @@ open Client
    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
+  : (F.debruijn_type, F.range * FTypeChecker.type_error) result
   =
   Printf.printf "Formatting the System F term...\n%!";
   let doc = FPrinter.print_term t in
@@ -23,8 +23,8 @@ 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);
+  | Error (range, e) ->
+     Utils.emit_error range (FPrinter.print_type_error e);
      failwith "Type-checking error."
 
 (* Test a term that is expected to fail type checking. *)
-- 
GitLab


From e31e8032fa697818fb43c2584a5ba8745fdda707 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sun, 12 Feb 2023 08:24:49 +0100
Subject: [PATCH 2/5] consistently emit error locations in Infer error messages

---
 client/F.ml               |  14 +-
 client/F.mli              |   9 +-
 client/Infer.ml           | 432 +++++++++++++++++++++-----------------
 client/Infer.mli          |  15 +-
 client/ML.ml              |   5 +-
 client/Utils.ml           |   8 +-
 client/Utils.mli          |   2 +
 client/test/CheckML.ml    |  42 +---
 client/test/TestF.ml      |   6 +-
 client/test/suite.t/run.t |   2 -
 10 files changed, 274 insertions(+), 261 deletions(-)

diff --git a/client/F.ml b/client/F.ml
index 72891b5..f72903d 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -23,11 +23,7 @@
    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 range = Utils.range
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -123,10 +119,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
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/client/F.mli b/client/F.mli
index ee46f38..7c062de 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -23,10 +23,7 @@
    while the de Bruijn representation is more convenient when type-checking
    F. *)
 
-type range =
-  Lexing.position * Lexing.position
-
-val dummy_range: range
+type range = Utils.range
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -128,8 +125,8 @@ 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:Utils.range -> 'b list -> ('a, 'b) term -> ('a, 'b) term
+val ftyapp: loc:Utils.range -> ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/client/Infer.ml b/client/Infer.ml
index 96e0f2d..485c796 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -96,6 +96,17 @@ end
 module Solver = Inferno.Solver.Make(X)(S)(O)
 open Solver
 
+(* Errors *)
+
+type error =
+  | Unbound of ML.tevar
+  | Unify of F.nominal_type * F.nominal_type
+  | Cycle of F.nominal_type
+  | VariableConflict of ML.tevar
+  | VariableScopeEscape
+
+exception Error of range * error
+
 (* -------------------------------------------------------------------------- *)
 
 let arrow x y =
@@ -113,12 +124,12 @@ let constr c xs =
 let smart =
   true
 
-let flet (x, t, u) =
+let flet ~loc (x, t, u) =
   match t with
   | F.Var (_, y) when smart && x = y ->
       u
   | t ->
-      F.Let (F.dummy_range, x, t, u)
+      F.Let (loc, x, t, u)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -143,23 +154,23 @@ let bottom : F.nominal_type =
    coercion clutter in the common case where the coercion actually has no
    effect. *)
 
-let ftyabs1 v t =
+let ftyabs1 ~loc v t =
   match t with
   | F.TyApp (_, t, F.TyVar w) when smart && v = w ->
       t
   | t ->
-      F.TyAbs (F.dummy_range, v, t)
+      F.TyAbs (loc, v, t)
 
 (* TEMPORARY find a better name for [coerce] *)
 
-let coerce (vs1 : O.tyvar list) (vs2 : O.tyvar list) : coercion =
+let coerce ~loc (vs1 : O.tyvar list) (vs2 : O.tyvar list) : coercion =
   (* Assume the term [t] has type [forall vs1, _]. *)
   fun t ->
     (* Introduce the desired quantifiers. *)
-    List.fold_right ftyabs1 vs2 (
+    List.fold_right (ftyabs1 ~loc) vs2 (
       (* Now, specialize the term [t]. For each member of [vs1],
          we must provide a suitable instantiation. *)
-      F.ftyapp t (
+      F.ftyapp ~loc t (
         (* [vs1] is a superset of [vs2]. For each member of [vs1], if it is a
            member of [vs2], then we keep it (by instantiating it with itself),
            otherwise we get rid of it (by instantiating it with an arbitrary
@@ -261,8 +272,6 @@ let convert env params ty =
   let deep_ty = convert_deep env params ty in
   deep deep_ty
 
-exception VariableConflict of ML.tevar
-
 (* -------------------------------------------------------------------------- *)
 
 (* [get_range t] returns the range of [t]. *)
@@ -296,80 +305,80 @@ type type_env = (ML.tevar * variable) list
 let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.nominal_term co
   =
   let rec hastype t w =
-    let pos = get_range t in
-    correlate pos @@
+    let loc = get_range t in
+    correlate loc @@
     match t with
-      (* Variable. *)
-    | ML.Var (pos, x) ->
-
-        (* [w] must be an instance of the type scheme associated with [x]. *)
-        let+ tys = instance (X.Var x) w in
-        (* The translation makes the type application explicit. *)
-        F.ftyapp (F.Var (pos, x)) tys
-
-      (* Abstraction. *)
-    | ML.Abs (pos, x, u) ->
-
-        (* We do not know a priori what the domain and codomain of this function
-           are, so we must infer them. We introduce two type variables to stand
-           for these unknowns. *)
-        let@ v1 = exist in
-        let@ v2 = exist in
-        (* [w] must be the function type [v1 -> v2]. *)
-        let+ () = w --- arrow v1 v2
-        (* Under the assumption that [x] has type [domain], the term [u] must
-           have type [codomain]. *)
-        and+ u' = def (X.Var x) v1 (hastype u v2)
-        and+ ty1 = decode v1
-        in
-        (* Once these constraints are solved, we obtain the translated function
-           body [u']. There remains to construct an explicitly-typed abstraction
-           in the target calculus. *)
-        F.Abs (pos, x, ty1, u')
-
-      (* Application. *)
-    | ML.App (pos, t1, t2) ->
-
-        (* Introduce a type variable to stand for the unknown argument type. *)
-       let@ v = exist in
-       let+ t1' = lift hastype t1 (arrow v w)
-       and+ t2' = hastype t2 v
-       in F.App (pos, t1', t2')
-
-      (* Generalization. *)
-    | ML.Let (pos, x, t, u) ->
-
-        (* Construct a ``let'' constraint. *)
-        let+ (a, (b, _), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
-        (* [a] are the type variables that we must bind (via Lambda abstractions)
-           while type-checking [t]. [(b, _)] is the type scheme that [x] must
-           receive while type-checking [u]. Its quantifiers [b] are guaranteed to
-           form a subset of [a]. Hence, in general, we must re-bind [x] to an
-           application of a suitable coercion to [x]. We use smart constructors so
-           that, if the lists [a] and [b] happen to be equal, no extra code is
-           produced. *)
-        F.Let (pos, x, F.ftyabs a t',
-        flet (x, coerce a b (F.Var (F.dummy_range, x)),
-        u'))
-
-    | ML.Annot (pos, t, annot) ->
-
-       let convert_annot typedecl_env params w t ty =
-         let@ v = convert typedecl_env params ty in
-         let+ () = v -- w
-         and+ t' = hastype t v
-         and+ ty' = decode v
-         in F.Annot (pos, t', ty')
-       in
-
-       begin match annot with
-       | (_, [], ty) ->
+    (* Variable. *)
+    | ML.Var (loc, x) ->
+
+      (* [w] must be an instance of the type scheme associated with [x]. *)
+      let+ tys = instance (X.Var x) w in
+      (* The translation makes the type application explicit. *)
+      F.ftyapp ~loc (F.Var (loc, x)) tys
+
+    (* Abstraction. *)
+    | ML.Abs (loc, x, u) ->
+
+      (* We do not know a priori what the domain and codomain of this function
+         are, so we must infer them. We introduce two type variables to stand
+         for these unknowns. *)
+      let@ v1 = exist in
+      let@ v2 = exist in
+      (* [w] must be the function type [v1 -> v2]. *)
+      let+ () = w --- arrow v1 v2
+      (* Under the assumption that [x] has type [domain], the term [u] must
+         have type [codomain]. *)
+      and+ u' = def (X.Var x) v1 (hastype u v2)
+      and+ ty1 = decode v1
+      in
+      (* Once these constraints are solved, we obtain the translated function
+         body [u']. There remains to construct an explicitly-typed abstraction
+         in the target calculus. *)
+      F.Abs (loc, x, ty1, u')
+
+    (* Application. *)
+    | ML.App (loc, t1, t2) ->
+
+      (* Introduce a type variable to stand for the unknown argument type. *)
+      let@ v = exist in
+      let+ t1' = lift hastype t1 (arrow v w)
+      and+ t2' = hastype t2 v
+      in F.App (loc, t1', t2')
+
+    (* Generalization. *)
+    | ML.Let (loc, x, t, u) ->
+
+      (* Construct a ``let'' constraint. *)
+      let+ (a, (b, _), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
+      (* [a] are the type variables that we must bind (via Lambda abstractions)
+         while type-checking [t]. [(b, _)] is the type scheme that [x] must
+         receive while type-checking [u]. Its quantifiers [b] are guaranteed to
+         form a subset of [a]. Hence, in general, we must re-bind [x] to an
+         application of a suitable coercion to [x]. We use smart constructors so
+         that, if the lists [a] and [b] happen to be equal, no extra code is
+         produced. *)
+      F.Let (loc, x, F.ftyabs ~loc a t',
+             flet ~loc (x, coerce ~loc a b (F.Var (loc, x)),
+                        u'))
+
+    | ML.Annot (loc, t, annot) ->
+
+      let convert_annot typedecl_env params w t ty =
+        let@ v = convert typedecl_env params ty in
+        let+ () = v -- w
+        and+ t' = hastype t v
+        and+ ty' = decode v
+        in F.Annot (loc, t', ty')
+      in
+
+      begin match annot with
+        | (_, [], ty) ->
           convert_annot typedecl_env [] w t ty
-       | (ML.Flexible, vs, ty) ->
+        | (ML.Flexible, vs, ty) ->
           let@ params =
             vs |> mapM_now (fun alpha k -> let@ v = exist in k (alpha, v)) in
           convert_annot typedecl_env params w t ty
-       | (ML.Rigid, vs, ty) ->
+        | (ML.Rigid, vs, ty) ->
           (* See "The Essence of ML type inference", long version, exercise 1.10.8 page 112:
                <<(t : forall 'a 'b. ty) : 'w>>
              is elaborated into a rigid constraint
@@ -381,7 +390,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
              constraint between the polymorphic scheme of x and the
              result type 'w. This enforces that 'a, 'b are used polymorphically
              by t, but they can still be instantiated in the rest of the term.
-           *)
+          *)
           let x = X.fresh () in
           let+ (alphas, (betas, _), t', tys) =
             letr1 (List.length vs) x
@@ -390,59 +399,59 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
                  convert_annot typedecl_env tyvs z t ty)
               (instance x w)
           in
-          F.ftyapp (coerce alphas betas (F.ftyabs alphas t')) tys
-       end
-
-    | ML.Tuple (pos, ts) ->
-        let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
-          fun (k : ('b * 'c co) -> 'r co) : 'r co ->
-            let@ v : 'b = exist in
-            let t = hastype t v in
-            k (v, t)
-        in
+          F.ftyapp ~loc (coerce ~loc alphas betas (F.ftyabs ~loc alphas t')) tys
+      end
+
+    | ML.Tuple (loc, ts) ->
+      let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
+        fun (k : ('b * 'c co) -> 'r co) : 'r co ->
+          let@ v : 'b = exist in
+          let t = hastype t v in
+          k (v, t)
+      in
 
-        let@ (vs, ts') = mapM_both on_term ts in
-        let+ () = w --- product vs
-        and+ ts' = ts'
-        in F.Tuple (pos, ts')
+      let@ (vs, ts') = mapM_both on_term ts in
+      let+ () = w --- product vs
+      and+ ts' = ts'
+      in F.Tuple (loc, ts')
 
-    | ML.LetProd (pos, xs, t, u) ->
-        let on_var (x:ML.tevar) : ('a, 'r) binder =
-          fun (k : 'b -> 'r co) : 'r co ->
-            let@ v = exist in
-            def (X.Var x) v (k v)
-        in
+    | ML.LetProd (loc, xs, t, u) ->
+      let on_var (x:ML.tevar) : ('a, 'r) binder =
+        fun (k : 'b -> 'r co) : 'r co ->
+          let@ v = exist in
+          def (X.Var x) v (k v)
+      in
 
-        let@ vs = mapM_now on_var xs in
-        let+ t' = lift hastype t (product vs)
-        and+ u' = hastype u w
-        in F.LetProd(pos, xs, t', u')
+      let@ vs = mapM_now on_var xs in
+      let+ t' = lift hastype t (product vs)
+      and+ u' = hastype u w
+      in F.LetProd(loc, xs, t', u')
 
-    | ML.Variant (pos, c, t) ->
-        let@ (dty, v) = hastype_variant typedecl_env c w in
+    | ML.Variant (loc, c, t) ->
+      let@ (dty, v) = hastype_variant typedecl_env ~loc c w in
 
-        let+ dty = dty
-        and+ t' =
-          match t with
-          | None ->
-              pure (F.Tuple (F.dummy_range, []))
-          | Some t ->
-              hastype t v
-        in F.Variant (pos, c, dty, t')
-
-    | ML.Match (pos, t, branches) ->
-        (* Inference variable for the type of the scrutinee
-           (and of the patterns) *)
-        let@ v = exist in
+      let+ dty = dty
+      and+ t' =
+        match t with
+        | None ->
+          pure (F.Tuple (loc, []))
+        | Some t ->
+          hastype t v
+      in F.Variant (loc, c, dty, t')
 
-        let@ branches' = hastype_branches typedecl_env branches w v in
+    | ML.Match (loc, t, branches) ->
+      (* Inference variable for the type of the scrutinee
+         (and of the patterns) *)
+      let@ v = exist in
 
-        let+ t = hastype t v
-        and+ branches' = branches'
-        and+ ty = decode w
-        in F.Match (pos, ty, t, branches')
+      let@ branches' = hastype_branches typedecl_env branches w v in
 
-    | ML.Hole (pos, ts) ->
+      let+ t = hastype t v
+      and+ branches' = branches'
+      and+ ty = decode w
+      in F.Match (loc, ty, t, branches')
+
+    | ML.Hole (loc, ts) ->
       (* A hole ...[t1, t2, .., tn] has any type, and its subterms
          [t1, .., tn] can themselves have any type; our return type
          w is unconstrained and we type each ti at a new inference
@@ -453,9 +462,9 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
       let@ ts' = mapM_later on_subterm ts in
       let+ ts' = ts'
       and+ ty = decode w
-      in F.Hole (pos, ty, ts')
+      in F.Hole (loc, ty, ts')
 
-  and hastype_variant typedecl_env c w
+  and hastype_variant typedecl_env ~loc c w
     : (F.nominal_datatype co * variable, 'r) binder
     = fun k ->
       let Datatype.{ type_name ; arg_type ; _ } =
@@ -467,15 +476,19 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
         | Datatype.Variant ->
           ()
         | Datatype.Record ->
+          (* TODO: this error should be turned into a proper 'error'
+             constructor like the others, but we probably need to
+             figure out how to deal with all Datatype exceptions at
+             once. *)
           raise Datatype.Env.UnexpectedRecord
       end;
 
       let arg_type =
         match arg_type with
         | None ->
-           ML.TyProduct (ML.dummy_pos, [])
+          ML.TyProduct (loc, [])
         | Some ty ->
-           ty
+          ty
       in
 
       let@ type_param_vars = mapM_now (fun _x -> exist) type_params in
@@ -503,24 +516,24 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
       : F.nominal_term co
       = match pat_env with
       | [] ->
-          (* Here we use [v_return] because [t] should have the same type
-             as the whole match statement *)
-          hastype u v_return
+        (* Here we use [v_return] because [t] should have the same type
+           as the whole match statement *)
+        hastype u v_return
       | (x, v1) :: pat_env ->
-          def (X.Var x) v1 @@ bind_pattern_vars pat_env u
+        def (X.Var x) v1 @@ bind_pattern_vars pat_env u
     in
 
     let on_branch ((pat,u) : ML.branch)
       : (F.nominal_branch co, 'r) binder
       = fun k ->
-      let@ (pat_env, pat) = hastype_pat typedecl_env pat v_scrutinee in
+        let@ (pat_env, pat) = hastype_pat typedecl_env pat v_scrutinee in
 
-      let u = bind_pattern_vars pat_env u in
+        let u = bind_pattern_vars pat_env u in
 
-      k (
-        let+ pat = pat and+ u = u
-        in (pat, u)
-      )
+        k (
+          let+ pat = pat and+ u = u
+          in (pat, u)
+        )
     in
 
     mapM_later on_branch branches
@@ -530,41 +543,41 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
   and hastype_pat typedecl_env pat w
     : (type_env * F.nominal_pattern co, 'r) binder
     = fun k ->
-    match pat with
-    | ML.PVar (pos, x) ->
+      match pat with
+      | ML.PVar (loc, x) ->
         let pat_env = [(x, w)] in
-        k (pat_env, pure (F.PVar (pos, x)))
+        k (pat_env, pure (F.PVar (loc, x)))
 
-    | ML.PWildcard pos ->
-        k ([], pure (F.PWildcard pos))
+      | ML.PWildcard loc ->
+        k ([], pure (F.PWildcard loc))
 
-    | ML.PAnnot (pos, pat, (rigidity, vars, ty)) ->
+      | ML.PAnnot (loc, pat, (rigidity, vars, ty)) ->
         begin match rigidity with
-        | ML.Rigid ->
-           failwith "Rigid variables are not supported in pattern annotation"
-        | ML.Flexible ->
-           let@ params =
-             vars |> mapM_now (fun alpha k ->
-                         let@ v = exist in k(alpha,v)
-                       )
-           in
-           let@ v = convert typedecl_env params ty in
-           let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
-           let+ () = v -- w
-           and+ res = k (pat_env,
-                         let+ pat = pat
-                         and+ ty' = decode v
-                         in F.PAnnot(pos, pat, ty'))
-           in res
+          | ML.Rigid ->
+            failwith "Rigid variables are not supported in pattern annotation"
+          | ML.Flexible ->
+            let@ params =
+              vars |> mapM_now (fun alpha k ->
+                let@ v = exist in k(alpha,v)
+              )
+            in
+            let@ v = convert typedecl_env params ty in
+            let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
+            let+ () = v -- w
+            and+ res = k (pat_env,
+                          let+ pat = pat
+                          and+ ty' = decode v
+                          in F.PAnnot(loc, pat, ty'))
+            in res
         end
 
-    | ML.PTuple (pos, pats) ->
+      | ML.PTuple (loc, pats) ->
 
         let check_no_duplicate accu env =
           List.iter (fun (x,_) ->
-              if List.mem_assoc x accu then
-                raise (VariableConflict x)
-            ) env
+            if List.mem_assoc x accu then
+              raise (Error (loc, VariableConflict x))
+          ) env
         in
 
         let union_ accu env =
@@ -579,9 +592,9 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
           : ((variable * (ML.tevar * variable) list)
              * F.nominal_pattern co, 'r) binder
           = fun k ->
-          let@ v = exist in
-          let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
-          k ((v,pat_env), pat)
+            let@ v = exist in
+            let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
+            k ((v,pat_env), pat)
         in
 
         let@ (l, pats) = mapM_both on_pattern pats in
@@ -591,51 +604,35 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
         k (pat_env,
            let+ () = w --- product vs
            and+ pats = pats
-           in F.PTuple (pos, pats))
+           in F.PTuple (loc, pats))
 
-    | ML.PVariant (pos, c, pat) ->
-        let@ (dty, v) = hastype_variant typedecl_env c w in
+      | ML.PVariant (loc, c, pat) ->
+        let@ (dty, v) = hastype_variant typedecl_env ~loc c w in
 
         let@ (pat_env, pat') =
           match pat with
           | None ->
-             (fun k ->
-               k ([], pure (F.PTuple (F.dummy_range, []))))
+            (fun k ->
+               k ([], pure (F.PTuple (loc, []))))
           | Some pat ->
-              hastype_pat typedecl_env pat v
+            hastype_pat typedecl_env pat v
         in
         k(pat_env,
           let+ dty = dty
           and+ pat' = pat'
-          in F.PVariant (pos, c, dty, pat'))
+          in F.PVariant (loc, c, dty, pat'))
   in
   hastype t w
 
 (* The top-level wrapper uses [let0]. It does not require an expected
    type; it creates its own using [exist]. And it runs the solver. *)
 
-type nonrec range = range
-exception Unbound of range * ML.tevar
-exception Unify = Solver.Unify
-exception Cycle = Solver.Cycle
-exception VariableScopeEscape = Solver.VariableScopeEscape
-
 let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
+  let loc = get_range t in
   let+ (vs, t) =
-    correlate (get_range t) (let0 (exist (hastype env t))) in
+    correlate loc (let0 (exist (hastype env t))) in
   (* [vs] are the binders that we must introduce *)
-  F.ftyabs vs t
-
-let get_tevar x =
-  match x with
-  | X.Sym _ -> assert false
-  | X.Var x -> x
-
-let translate ~rectypes env t =
-  try
-    Solver.solve ~rectypes (hastype env t)
-  with Solver.Unbound (range, x) ->
-    raise (Unbound (range, get_tevar x))
+  F.ftyabs ~loc vs t
 
 let hastype_with_hook ~(hook : unit -> 'a) (env : ML.datatype_env) (t : ML.term)
 : ('a * F.nominal_term) co
@@ -644,8 +641,49 @@ let hastype_with_hook ~(hook : unit -> 'a) (env : ML.datatype_env) (t : ML.term)
   and+ u = hastype env t in
   a, u
 
+let get_tevar x =
+  match x with
+  | X.Sym _ -> assert false
+  | X.Var x -> x
+
 let translate_with_hook ~hook ~rectypes env t =
-  try
-    Solver.solve ~rectypes (hastype_with_hook ~hook env t)
-  with Solver.Unbound (range, x) ->
-    raise (Unbound (range, get_tevar x))
+  try Solver.solve ~rectypes (hastype_with_hook ~hook env t) with
+  | Solver.Unbound (range, x) ->
+    raise (Error (range, Unbound (get_tevar x)))
+  | Solver.Unify (range, t1, t2) ->
+    raise (Error (range, Unify (t1, t2)))
+  | Solver.Cycle (range, ty) ->
+    raise (Error (range, Cycle ty))
+  | Solver.VariableScopeEscape range ->
+    raise (Error (range, VariableScopeEscape))
+
+let translate ~rectypes env t =
+  let ((), res) = translate_with_hook ~hook:ignore ~rectypes env t in
+  res
+
+let emit_error range (error : error) =
+  let emit_type ty =
+    Utils.emit_endline (FPrinter.print_type ty)
+  in
+  Utils.emit_range range;
+  begin match error with
+  | Unbound (s) ->
+      Printf.printf "Type error: unbound variable \"%s\".\n"
+        s
+  | Cycle (ty) ->
+      Printf.printf "Type error: a cyclic type arose.\n";
+      emit_type ty
+  | Unify (ty1, ty2) ->
+      Printf.printf "Type error: mismatch between the type:\n";
+      emit_type ty1;
+      Printf.printf "and the type:\n";
+      emit_type ty2;
+  | VariableScopeEscape ->
+      Printf.printf
+        "A rigid variable escapes its scope.\n"
+  | VariableConflict (x) ->
+      Printf.printf
+        "Scope error: variable %s is already bound in this pattern."
+        x
+  end;
+  flush stdout
diff --git a/client/Infer.mli b/client/Infer.mli
index ebf90c9..5e2698c 100644
--- a/client/Infer.mli
+++ b/client/Infer.mli
@@ -1,8 +1,11 @@
-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
+type error =
+  | Unbound of ML.tevar
+  | Unify of F.nominal_type * F.nominal_type
+  | Cycle of F.nominal_type
+  | VariableConflict of ML.tevar
+  | VariableScopeEscape
+
+exception Error of Utils.range * error
 
 (* Contraint generation, constraint solving and elaboration, combined. *)
 val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term
@@ -14,3 +17,5 @@ val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term
 val translate_with_hook:
   hook:(unit -> 'a) ->
   rectypes:bool -> ML.datatype_env -> ML.term -> 'a * F.nominal_term
+
+val emit_error : Utils.range -> error -> unit
diff --git a/client/ML.ml b/client/ML.ml
index 991c1af..4903395 100644
--- a/client/ML.ml
+++ b/client/ML.ml
@@ -7,10 +7,9 @@ type 'a list = 'a List.t =
   | (::) of 'a * 'a list
   [@@deriving compare]
 
-type range =
-  Lexing.position * Lexing.position
+type range = Utils.range
 
-(* We generate a comparison function [compare] that ignores all ranges.
+(* We generate a comparison function [compare_range] that ignores all ranges.
    This is useful while testing. *)
 let compare_range _ _ = 0
 
diff --git a/client/Utils.ml b/client/Utils.ml
index 0b2a32c..4f3c607 100644
--- a/client/Utils.ml
+++ b/client/Utils.ml
@@ -18,6 +18,12 @@ let emit_endline doc =
 
 type range = Lexing.position * Lexing.position
 
-let emit_error range doc =
+let dummy_range : range = Lexing.(dummy_pos, dummy_pos)
+
+let emit_range range =
   print_string (MenhirLib.LexerUtil.range range);
+  flush stdout
+
+let emit_error range doc =
+  emit_range range;
   emit_endline doc
diff --git a/client/Utils.mli b/client/Utils.mli
index 70338aa..341f7f8 100644
--- a/client/Utils.mli
+++ b/client/Utils.mli
@@ -17,6 +17,8 @@ val emit : PPrint.document -> unit
 val emit_endline : PPrint.document -> unit
 
 type range = Lexing.position * Lexing.position
+val dummy_range : range
+val emit_range : range -> unit
 
 (* Similar to {!emit_endline}, but starts by printing
    a source location range. *)
diff --git a/client/test/CheckML.ml b/client/test/CheckML.ml
index 6f7c775..264644a 100644
--- a/client/test/CheckML.ml
+++ b/client/test/CheckML.ml
@@ -8,42 +8,12 @@ module LexUtil = MenhirLib.LexerUtil
    as normal, since our terms are randomly generated, so we translate the client
    exceptions to [None]. *)
 
-let print_type ty =
-  Utils.emit_endline (FPrinter.print_type ty)
-
 let translate ~verbose ~rectypes e t =
-  try
-    Some (Infer.translate ~rectypes e t)
-  with
-  | Infer.Unbound (range, s) ->
-      Printf.fprintf stdout "%sType error: unbound variable \"%s\".\n%!"
-        (LexUtil.range range) s;
-      None
-  | Infer.Cycle (range, ty) ->
-      if verbose then begin
-        Printf.fprintf stdout "%sType error: a cyclic type arose.\n%!"
-          (LexUtil.range range);
-        print_type ty
-      end;
-      None
-  | Infer.Unify (range, ty1, ty2) ->
-      if verbose then begin
-        Printf.fprintf stdout "%sType error: type mismatch.\n"
-            (LexUtil.range range);
-        Printf.fprintf stdout "Type error: mismatch between the type:\n";
-        print_type ty1;
-        Printf.fprintf stdout "and the type:\n";
-        print_type ty2;
-        Printf.fprintf stdout "%!";
-      end;
-      None
-  | Infer.VariableScopeEscape range ->
-      if verbose then begin
-          Printf.fprintf stdout
-            "%sA rigid variable escapes its scope.\n%!"
-            (LexUtil.range range);
-        end;
-      None
+  match Infer.translate ~rectypes e t with
+  | x -> Some x
+  | exception Infer.Error(range, error) ->
+    if verbose then Infer.emit_error range error;
+    None
 
 let equal_term t1 t2 =
   ML.compare_term t1 t2 = 0
@@ -51,7 +21,7 @@ let equal_term t1 t2 =
 
 (* -------------------------------------------------------------------------- *)
 
-exception ParsingError of Infer.range
+exception ParsingError of Utils.range
 
 let wrap parser lexbuf =
   let lexbuf = LexUtil.init "test" lexbuf in
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index 936c16c..d9c7f5b 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -1,5 +1,7 @@
 open Client
 
+let dummy_range = Utils.dummy_range
+
 (* -------------------------------------------------------------------------- *)
 
 (* AST helper functions *)
@@ -8,13 +10,13 @@ let (-->) ty1 ty2 =
   F.TyArrow (ty1, ty2)
 
 let unit =
-  F.Tuple (F.dummy_range, [])
+  F.Tuple (dummy_range, [])
 
 let unit_type =
   F.TyProduct []
 
 let unit_pattern =
-  F.PTuple (F.dummy_range, [])
+  F.PTuple (dummy_range, [])
 
 let var x =
   F.(Var (dummy_range, x))
diff --git a/client/test/suite.t/run.t b/client/test/suite.t/run.t
index c87f0bd..5ba32dc 100644
--- a/client/test/suite.t/run.t
+++ b/client/test/suite.t/run.t
@@ -346,7 +346,6 @@ variables.
   $ midml id-rigid-wrong.midml
   Type inference and translation to System F...
   File "test", line 2, characters 12-13:
-  Type error: type mismatch.
   Type error: mismatch between the type:
   r2
   and the type:
@@ -362,7 +361,6 @@ with some structure.
   $ midml unit-rigid-wrong.midml
   Type inference and translation to System F...
   File "test", line 2, characters 3-5:
-  Type error: type mismatch.
   Type error: mismatch between the type:
   r2
   and the type:
-- 
GitLab


From 3df581777ce1918c4d99bd9d602247fdb1fb216b Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sun, 12 Feb 2023 09:08:01 +0100
Subject: [PATCH 3/5] consistently use 'loc' instead of 'range' to describe
 source locations

The problem with 'range' is that this word has a much more general
meaning, it could be an integer range; typically it is also used in
comments to describe range of levels or scopes.

In the context of Menhir, which is centered on parsing, 'range'
clearly associates with 'source range'. But for more general project
this association is lost and 'range' is confusing.
---
 client/F.ml                 |  44 ++++-----
 client/F.mli                |  48 +++++-----
 client/FTypeChecker.ml      |   2 +-
 client/FTypeChecker.mli     |   4 +-
 client/Infer.ml             |  37 +++++---
 client/Infer.mli            |   4 +-
 client/ML.ml                |  46 +++++----
 client/ML2F.ml              |   2 +-
 client/MLParser.mly         |  53 ++++++-----
 client/Utils.ml             |  16 ++--
 client/Utils.mli            |   9 +-
 client/bin/midml.ml         |   7 +-
 client/test/CheckF.ml       |   2 +-
 client/test/CheckML.ml      |  18 ++--
 client/test/RandomML.ml     |  17 ++--
 client/test/TestF.ml        |  40 ++++----
 client/test/TestML.ml       | 180 ++++++++++++++++++------------------
 client/test/TestMLRandom.ml |   6 +-
 src/Solver.ml               |  86 ++++++++---------
 src/Solver.mli              |  25 +++--
 20 files changed, 325 insertions(+), 321 deletions(-)

diff --git a/client/F.ml b/client/F.ml
index f72903d..88c0c8a 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -23,7 +23,7 @@
    while the de Bruijn representation is more convenient when type-checking
    F. *)
 
-type range = Utils.range
+type loc = Utils.loc
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -82,31 +82,31 @@ 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
-  | Absurd of range * ('a,'b) typ
-  | Refl of range * ('a,'b) typ
-  | Use of range * ('a,'b) term * ('a,'b) term
+  | 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 * tevar * ('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) term
 
 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
diff --git a/client/F.mli b/client/F.mli
index 7c062de..8203727 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -23,7 +23,7 @@
    while the de Bruijn representation is more convenient when type-checking
    F. *)
 
-type range = Utils.range
+type loc = Utils.loc
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -83,31 +83,31 @@ 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
-  | Absurd of range * ('a,'b) typ
-  | Refl of range * ('a,'b) typ
-  | Use of range * ('a,'b) term * ('a,'b) term
+  | 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 * tevar * ('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) term
 
 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
@@ -125,8 +125,8 @@ type debruijn_term =
 
 (* Constructors. *)
 
-val ftyabs: loc:Utils.range -> 'b list -> ('a, 'b) term -> ('a, 'b) term
-val ftyapp: loc:Utils.range -> ('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
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 7a12b7e..4d67c61 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -18,7 +18,7 @@ type type_error =
 
 and arity_requirement = Index of int | Total of int
 
-exception TypeError of range * type_error
+exception TypeError of loc * type_error
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/client/FTypeChecker.mli b/client/FTypeChecker.mli
index 8aa3866..1bb09ef 100644
--- a/client/FTypeChecker.mli
+++ b/client/FTypeChecker.mli
@@ -24,7 +24,7 @@ type type_error =
 *)
 and arity_requirement = Index of int | Total of int
 
-exception TypeError of range * type_error
+exception TypeError of loc * type_error
 
 (* [typeof env t] type-checks the closed term [t] in datatype environment [env]
    and constructs its type.
@@ -34,4 +34,4 @@ val typeof: debruijn_datatype_env -> debruijn_term -> debruijn_type
 
 (* Similar to {!typeof}, but returns a [result] type instead of raising an exception. *)
 val typeof_result:
-  debruijn_datatype_env -> debruijn_term -> (debruijn_type, range * type_error) result
+  debruijn_datatype_env -> debruijn_term -> (debruijn_type, loc * type_error) result
diff --git a/client/Infer.ml b/client/Infer.ml
index 485c796..441136b 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -105,7 +105,7 @@ type error =
   | VariableConflict of ML.tevar
   | VariableScopeEscape
 
-exception Error of range * error
+exception Error of Utils.loc * error
 
 (* -------------------------------------------------------------------------- *)
 
@@ -274,8 +274,8 @@ let convert env params ty =
 
 (* -------------------------------------------------------------------------- *)
 
-(* [get_range t] returns the range of [t]. *)
-let get_range t =
+(* [get_loc t] returns the location of [t]. *)
+let get_loc t =
   match t with
   | ML.Var (pos, _) | ML.Hole (pos, _) | ML.Abs (pos, _, _)
   | ML.App (pos, _, _) | ML.Let (pos, _, _, _) | ML.Annot (pos, _, _)
@@ -283,6 +283,13 @@ let get_range t =
   | ML.Variant (pos, _, _) | ML.Match (pos, _, _)
     -> pos
 
+let correlate loc c =
+  (* We (the client) use optional locations,
+     whereas the solver uses non-optional locations. *)
+  match loc with
+  | None -> c
+  | Some loc -> Solver.correlate loc c
+
 (* -------------------------------------------------------------------------- *)
 
 (* We will need a type environment to keep trace of term variables that must
@@ -305,7 +312,7 @@ type type_env = (ML.tevar * variable) list
 let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.nominal_term co
   =
   let rec hastype t w =
-    let loc = get_range t in
+    let loc = get_loc t in
     correlate loc @@
     match t with
     (* Variable. *)
@@ -628,7 +635,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
    type; it creates its own using [exist]. And it runs the solver. *)
 
 let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
-  let loc = get_range t in
+  let loc = get_loc t in
   let+ (vs, t) =
     correlate loc (let0 (exist (hastype env t))) in
   (* [vs] are the binders that we must introduce *)
@@ -648,24 +655,24 @@ let get_tevar x =
 
 let translate_with_hook ~hook ~rectypes env t =
   try Solver.solve ~rectypes (hastype_with_hook ~hook env t) with
-  | Solver.Unbound (range, x) ->
-    raise (Error (range, Unbound (get_tevar x)))
-  | Solver.Unify (range, t1, t2) ->
-    raise (Error (range, Unify (t1, t2)))
-  | Solver.Cycle (range, ty) ->
-    raise (Error (range, Cycle ty))
-  | Solver.VariableScopeEscape range ->
-    raise (Error (range, VariableScopeEscape))
+  | Solver.Unbound (loc, x) ->
+    raise (Error (loc, Unbound (get_tevar x)))
+  | Solver.Unify (loc, t1, t2) ->
+    raise (Error (loc, Unify (t1, t2)))
+  | Solver.Cycle (loc, ty) ->
+    raise (Error (loc, Cycle ty))
+  | Solver.VariableScopeEscape loc ->
+    raise (Error (loc, VariableScopeEscape))
 
 let translate ~rectypes env t =
   let ((), res) = translate_with_hook ~hook:ignore ~rectypes env t in
   res
 
-let emit_error range (error : error) =
+let emit_error loc (error : error) =
   let emit_type ty =
     Utils.emit_endline (FPrinter.print_type ty)
   in
-  Utils.emit_range range;
+  Utils.emit_loc loc;
   begin match error with
   | Unbound (s) ->
       Printf.printf "Type error: unbound variable \"%s\".\n"
diff --git a/client/Infer.mli b/client/Infer.mli
index 5e2698c..7cb977e 100644
--- a/client/Infer.mli
+++ b/client/Infer.mli
@@ -5,7 +5,7 @@ type error =
   | VariableConflict of ML.tevar
   | VariableScopeEscape
 
-exception Error of Utils.range * error
+exception Error of Utils.loc * error
 
 (* Contraint generation, constraint solving and elaboration, combined. *)
 val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term
@@ -18,4 +18,4 @@ val translate_with_hook:
   hook:(unit -> 'a) ->
   rectypes:bool -> ML.datatype_env -> ML.term -> 'a * F.nominal_term
 
-val emit_error : Utils.range -> error -> unit
+val emit_error : Utils.loc -> error -> unit
diff --git a/client/ML.ml b/client/ML.ml
index 4903395..f91cf3c 100644
--- a/client/ML.ml
+++ b/client/ML.ml
@@ -7,20 +7,20 @@ type 'a list = 'a List.t =
   | (::) of 'a * 'a list
   [@@deriving compare]
 
-type range = Utils.range
+type loc = Utils.loc
 
-(* We generate a comparison function [compare_range] that ignores all ranges.
+(* We generate a comparison function [compare_loc] that ignores all locations.
    This is useful while testing. *)
-let compare_range _ _ = 0
+let compare_loc _ _ = 0
 
 type tevar = String.t [@@deriving compare]
 type tyvar = String.t [@@deriving compare]
 
 type typ =
-  | TyVar of range * tyvar
-  | TyArrow of range * typ * typ
-  | TyProduct of range * typ list
-  | TyConstr of range * Datatype.TyConstrId.t * typ list
+  | TyVar of loc * tyvar
+  | TyArrow of loc * typ * typ
+  | TyProduct of loc * typ list
+  | TyConstr of loc * Datatype.TyConstrId.t * typ list
  [@@deriving compare]
 
 type rigidity = Flexible | Rigid
@@ -31,27 +31,25 @@ type type_annotation = rigidity * tyvar list * typ [@@deriving compare]
   (* some <flexible vars> . <ty> *)
 
 type term =
-  | Var of range * tevar
-  | Hole of range * term list
-  | Abs of range * tevar * term
-  | App of range * term * term
-  | Let of range * tevar * term * term
-  | Annot of range * term * type_annotation
-  | Tuple of range * term list
-  | LetProd of range * tevar list * term * term
-  | Variant of range * Datatype.LabelId.t * term Option.t
-  | Match of range * term * branch list
+  | Var of loc * tevar
+  | Hole of loc * term list
+  | Abs of loc * tevar * term
+  | App of loc * term * term
+  | Let of loc * tevar * term * term
+  | Annot of loc * term * type_annotation
+  | Tuple of loc * term list
+  | LetProd of loc * tevar list * term * term
+  | Variant of loc * Datatype.LabelId.t * term Option.t
+  | Match of loc * term * branch list
 
 and branch = pattern * term
 
 and pattern =
-  | PVar of range * tevar
-  | PWildcard of range
-  | PAnnot of range * pattern * type_annotation
-  | PVariant of range * Datatype.LabelId.t * pattern Option.t
-  | PTuple of range * pattern list
+  | PVar of loc * tevar
+  | PWildcard of loc
+  | PAnnot of loc * pattern * type_annotation
+  | PVariant of loc * Datatype.LabelId.t * pattern Option.t
+  | PTuple of loc * pattern list
   [@@deriving compare]
 
 type datatype_env = (tyvar, typ option) Datatype.Env.t
-
-let dummy_pos = (Lexing.( dummy_pos, dummy_pos ))
diff --git a/client/ML2F.ml b/client/ML2F.ml
index 071d079..676090b 100644
--- a/client/ML2F.ml
+++ b/client/ML2F.ml
@@ -38,7 +38,7 @@ let translate_datatype tdescr =
     let arg_type =
       match ldescr.Datatype.arg_type with
       | None ->
-         ML.TyProduct (ML.dummy_pos, [])
+         ML.TyProduct (None, [])
       | Some ty ->
          ty
     in
diff --git a/client/MLParser.mly b/client/MLParser.mly
index 91ecc90..13cda8c 100644
--- a/client/MLParser.mly
+++ b/client/MLParser.mly
@@ -39,7 +39,7 @@
 
 %token EOF
 
-%type<(string list * ML.datatype_env * (string * ML.term) list)> prog
+%type<(string list * ML.datatype_env * (Utils.loc * string * ML.term) list)> prog
 %type<ML.term> self_contained_term
 %type<ML.datatype_env> self_contained_type_decls
 
@@ -61,7 +61,7 @@ let self_contained_type_decls :=
 
 (***************** TERMS ***************)
 let toplevel_term_decl :=
-  | LET ; x = tevar_ ; "=" ; t = term ;   { (x, t) }
+  | LET ; x = tevar_ ; "=" ; t = term ;   { (Some $loc, x, t) }
 
 let term :=
   | ~ = term_abs ; <>
@@ -69,12 +69,12 @@ let term :=
 let term_abs :=
   | FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
     {
-      List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
+      List.fold_right (fun x t -> Abs (Some $loc, x, t)) xs t
     }
 
-  | (x, t1, t2) = letin(tevar) ;          { Let ($loc, x, t1, t2) }
+  | (x, t1, t2) = letin(tevar) ;          { Let (Some $loc, x, t1, t2) }
 
-  | (xs, t1, t2) = letin(tuple(tevar)) ;  { LetProd ($loc, xs, t1, t2) }
+  | (xs, t1, t2) = letin(tuple(tevar)) ;  { LetProd (Some $loc, xs, t1, t2) }
 
   | ~ = term_app ; <>
 
@@ -82,30 +82,35 @@ let term_app :=
   | t1 = term_app ; t2 = term_atom ;
     {
       match t1 with
-      | Variant ((start_pos, _), l, None) ->
-	 Variant ((start_pos, $endpos), l, Some t2)
+      | Variant (loc, l, None) ->
+         let loc = match loc with
+           | None -> Some $loc
+           | Some (start_pos, _end_pos) ->
+              Some (start_pos, $endpos)
+         in
+	 Variant (loc, l, Some t2)
       | _ ->
-	 App ($loc, t1, t2)
+	 App (Some $loc, t1, t2)
     }
 
   | ~ = term_atom ; <>
 
 let term_atom :=
-  | x = tevar ;                           { Var ($loc, x) }
+  | x = tevar ;                           { Var (Some $loc, x) }
 
-  | l = UIDENT ;                          { Variant ($loc, Datatype.Label l, None) }
+  | l = UIDENT ;                          { Variant (Some $loc, Datatype.Label l, None) }
 
-  | ts = tuple (term) ;                   { Tuple ($loc, ts) }
+  | ts = tuple (term) ;                   { Tuple (Some $loc, ts) }
 
   | MATCH ; t = term ; WITH ;
     brs = branches ;
-    END ;                                 { Match ($loc, t, brs) }
+    END ;                                 { Match (Some $loc, t, brs) }
 
   | "..."; "["; ts = item_sequence(term, COMMA); "]";
-                                          { Hole ($loc, ts) }
+                                          { Hole (Some $loc, ts) }
 
   | "(" ; t = term ; ":" ; tyannot = type_annotation ; ")" ;
-                                          { Annot ($loc, t, tyannot) }
+                                          { Annot (Some $loc, t, tyannot) }
 
   | "(" ; ~ = term ; ")" ; <>
 
@@ -116,21 +121,21 @@ let branch :=
   | pat = pattern ; "->" ; t = term ;     { (pat, t) }
 
 let pattern :=
-  | l = UIDENT ; pat = pattern_atom ;     { PVariant ($loc, Datatype.Label l, Some pat) }
+  | l = UIDENT ; pat = pattern_atom ;     { PVariant (Some $loc, Datatype.Label l, Some pat) }
 
   | ~ = pattern_atom ; <>
 
 let pattern_atom :=
-  | x = tevar ;                           { PVar ($loc, x) }
+  | x = tevar ;                           { PVar (Some $loc, x) }
 
-  | l = UIDENT;                           { PVariant ($loc, Datatype.Label l, None) }
+  | l = UIDENT;                           { PVariant (Some $loc, Datatype.Label l, None) }
 
-  | WILDCARD ;                            { PWildcard $loc }
+  | WILDCARD ;                            { PWildcard (Some $loc) }
 
-  | ps = tuple (pattern) ;                { PTuple ($loc, ps) }
+  | ps = tuple (pattern) ;                { PTuple (Some $loc, ps) }
 
   | "(" ; p = pattern ; ":" ; tyannot = type_annotation ; ")" ;
-                                          { PAnnot ($loc, p, tyannot) }
+                                          { PAnnot (Some $loc, p, tyannot) }
 
 let tevar :=
   | ~ = LIDENT ; <>
@@ -146,22 +151,22 @@ let typ :=
 
 let type_arrow :=
   | ty1 = type_tyconstr ; "->" ; ty2 = type_arrow ;
-                                          { TyArrow ($loc, ty1, ty2) }
+                                          { TyArrow (Some $loc, ty1, ty2) }
 
   | ~ = type_tyconstr ; <>
 
 
 let type_tyconstr :=
   | ~ = tyname ; typarams = list (type_atom) ;
-                                          { TyConstr ($loc, tyname, typarams)}
+                                          { TyConstr (Some $loc, tyname, typarams)}
 
   | ~ = type_atom ; <>
 
 let type_atom :=
-  | x = tyvar ;                           { TyVar ($loc, x) }
+  | x = tyvar ;                           { TyVar (Some $loc, x) }
 
   | "{" ; tys = separated_list ("*", typ) ; "}" ;
-                                          { TyProduct ($loc, tys) }
+                                          { TyProduct (Some $loc, tys) }
 
   | "(" ; ~ = typ ; ")" ;                 <>
 
diff --git a/client/Utils.ml b/client/Utils.ml
index 4f3c607..90a1522 100644
--- a/client/Utils.ml
+++ b/client/Utils.ml
@@ -16,14 +16,14 @@ let emit_endline doc =
   emit PPrint.(doc ^^ hardline);
   flush stdout
 
-type range = Lexing.position * Lexing.position
+type loc = (Lexing.position * Lexing.position) option
 
-let dummy_range : range = Lexing.(dummy_pos, dummy_pos)
+let emit_loc = function
+  | None -> ()
+  | Some range ->
+    print_string (MenhirLib.LexerUtil.range range);
+    flush stdout
 
-let emit_range range =
-  print_string (MenhirLib.LexerUtil.range range);
-  flush stdout
-
-let emit_error range doc =
-  emit_range range;
+let emit_error loc doc =
+  emit_loc loc;
   emit_endline doc
diff --git a/client/Utils.mli b/client/Utils.mli
index 341f7f8..f7da6cb 100644
--- a/client/Utils.mli
+++ b/client/Utils.mli
@@ -16,10 +16,9 @@ val emit : PPrint.document -> unit
    end and flushes [stdout]. *)
 val emit_endline : PPrint.document -> unit
 
-type range = Lexing.position * Lexing.position
-val dummy_range : range
-val emit_range : range -> unit
+type loc = (Lexing.position * Lexing.position) option
+val emit_loc : loc -> unit
 
 (* Similar to {!emit_endline}, but starts by printing
-   a source location range. *)
-val emit_error : range -> PPrint.document -> unit
+   a source location. *)
+val emit_error : loc -> PPrint.document -> unit
diff --git a/client/bin/midml.ml b/client/bin/midml.ml
index ff1d990..8aab9ce 100644
--- a/client/bin/midml.ml
+++ b/client/bin/midml.ml
@@ -6,9 +6,10 @@ let rectypes =
 
 let test_ok filename =
   match from_file filename with
-  | exception (ParsingError range) ->
-    Printf.eprintf "%!%sSyntax error.\n%!"
-      (LexUtil.range range)
+  | exception (ParsingError loc) ->
+    loc |> Option.iter (fun range ->
+      prerr_string (LexUtil.range range));
+    prerr_endline "Syntax error."
   | (datatype_env, t) ->
   let rectypes = !rectypes in
   let _ = Test.CheckML.test ~verbose:true ~rectypes datatype_env t in ()
diff --git a/client/test/CheckF.ml b/client/test/CheckF.ml
index 0614a89..7ff73b8 100644
--- a/client/test/CheckF.ml
+++ b/client/test/CheckF.ml
@@ -4,7 +4,7 @@ open Client
    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, F.range * FTypeChecker.type_error) result
+  : (F.debruijn_type, Utils.loc * FTypeChecker.type_error) result
   =
   Printf.printf "Formatting the System F term...\n%!";
   let doc = FPrinter.print_term t in
diff --git a/client/test/CheckML.ml b/client/test/CheckML.ml
index 264644a..33e9e98 100644
--- a/client/test/CheckML.ml
+++ b/client/test/CheckML.ml
@@ -21,14 +21,14 @@ let equal_term t1 t2 =
 
 (* -------------------------------------------------------------------------- *)
 
-exception ParsingError of Utils.range
+exception ParsingError of Utils.loc
 
 let wrap parser lexbuf =
   let lexbuf = LexUtil.init "test" lexbuf in
   try parser MLLexer.read lexbuf
   with MLParser.Error ->
     let range = Lexing.(lexbuf.lex_start_p, lexbuf.lex_curr_p) in
-    raise (ParsingError range)
+    raise (ParsingError (Some range))
 
 (* Main parsing function *)
 let parse_term lexbuf = wrap MLParser.self_contained_term lexbuf
@@ -45,10 +45,10 @@ let letify xts =
     match xts with
     | [] ->
         assert false
-    | [(_, t)] ->
+    | [(_loc, _last_var, t)] ->
         t
-    | (x, t) :: xts ->
-        ML.Let (ML.dummy_pos, x, t, aux xts)
+    | (loc, x, t) :: xts ->
+        ML.Let (loc, x, t, aux xts)
   in
   aux xts
 
@@ -93,9 +93,11 @@ let test_with_args
   let s = MLPrinter.to_string t in
   let lexbuf = Lexing.from_string s in
   match MLParser.self_contained_term MLLexer.read lexbuf with
-  | exception (ParsingError range) ->
-    Printf.eprintf "%!%sSyntax error on re-parsing.\n%!"
-      (LexUtil.range range);
+  | exception (ParsingError loc) ->
+    loc |> Option.iter (fun range ->
+      prerr_string (LexUtil.range range)
+    );
+    prerr_endline "Syntax error on re-parsing.";
     false
   | t' ->
      assert (equal_term t t');
diff --git a/client/test/RandomML.ml b/client/test/RandomML.ml
index b772dea..e320cf8 100644
--- a/client/test/RandomML.ml
+++ b/client/test/RandomML.ml
@@ -14,36 +14,33 @@ let split n st =
 
 open QCheck.Gen
 
-let pos =
-  ML.dummy_pos
-
 let int2var k =
   "x" ^ string_of_int k
 
 let var x =
-  ML.Var (pos, int2var x)
+  ML.Var (None, int2var x)
 
 let bind k =
   int2var <$> pure k
 
 let abs self k n =
   let+ x, t = pair (bind k) (self (k + 1, n - 1))
-  in ML.Abs (pos, x, t)
+  in ML.Abs (None, x, t)
 
 let app self k n =
   let* n1, n2 = split (n - 1) in
   let+ t1, t2 = pair (self (k, n1)) (self (k, n2))
-  in ML.App (pos, t1, t2)
+  in ML.App (None, t1, t2)
 
 let let_ self k n =
   let* n1, n2 = split (n - 1) in
   let+ x, t1, t2 = triple (bind k) (self (k, n1)) (self (k + 1, n2))
-  in ML.Let (pos, x, t1, t2)
+  in ML.Let (None, x, t1, t2)
 
 let pair self k n =
   let* n1, n2 = split (n - 1) in
   let+ t1, t2 = pair (self (k, n1)) (self (k, n2))
-  in ML.Tuple (pos, [t1; t2])
+  in ML.Tuple (None, [t1; t2])
 
 let let_pair self k n =
   let* n1, n2 = split (n - 1) in
@@ -53,11 +50,11 @@ let let_pair self k n =
       (bind (k + 1))
       (self (k, n1))
       (self (k + 2, n2))
-  in ML.LetProd (pos, [x1; x2], t1, t2)
+  in ML.LetProd (None, [x1; x2], t1, t2)
 
 let annot self k n =
   let+ t = self (k, n - 1) in
-  ML.Annot (pos, t, (ML.Flexible, ["'a"], ML.TyVar (pos, "'a")))
+  ML.Annot (None, t, (ML.Flexible, ["'a"], ML.TyVar (None, "'a")))
 
 let term = fix (fun self (k, n) ->
   if n = 0 then begin
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index d9c7f5b..c2e431f 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -1,7 +1,5 @@
 open Client
 
-let dummy_range = Utils.dummy_range
-
 (* -------------------------------------------------------------------------- *)
 
 (* AST helper functions *)
@@ -10,64 +8,64 @@ let (-->) ty1 ty2 =
   F.TyArrow (ty1, ty2)
 
 let unit =
-  F.Tuple (dummy_range, [])
+  F.Tuple (None, [])
 
 let unit_type =
   F.TyProduct []
 
 let unit_pattern =
-  F.PTuple (dummy_range, [])
+  F.PTuple (None, [])
 
 let var x =
-  F.(Var (dummy_range, x))
+  F.(Var (None, x))
 
 let annot ty t =
-  F.(Annot (dummy_range, ty, t))
+  F.(Annot (None, ty, t))
 
 let abs x ty t =
-  F.(Abs (dummy_range, x, ty, t))
+  F.(Abs (None, x, ty, t))
 
 let app t u =
-  F.(App (dummy_range, t, u))
+  F.(App (None, t, u))
 
 let tyabs x t =
-  F.(TyAbs (dummy_range, x, t))
+  F.(TyAbs (None, x, t))
 
 let tyapp t ty =
-  F.(TyApp (dummy_range, t, ty))
+  F.(TyApp (None, t, ty))
 
 let tuple ts =
-  F.(Tuple (dummy_range, ts))
+  F.(Tuple (None, ts))
 
 let letprod xs t u =
-  F.(LetProd (dummy_range, xs, t, u))
+  F.(LetProd (None, xs, t, u))
 
 let variant lbl datatype t =
-  F.(Variant (dummy_range, lbl, datatype, t))
+  F.(Variant (None, lbl, datatype, t))
 
 let match_ ty scrutinee branches =
-  F.(Match (dummy_range, ty, scrutinee, branches))
+  F.(Match (None, ty, scrutinee, branches))
 
 let absurd ty =
-  F.(Absurd (dummy_range, ty))
+  F.(Absurd (None, ty))
 
 let refl ty =
-  F.(Refl (dummy_range, ty))
+  F.(Refl (None, ty))
 
 let use t u =
-  F.(Use (dummy_range, t, u))
+  F.(Use (None, t, u))
 
 let pvar x =
-  F.(PVar (dummy_range, x))
+  F.(PVar (None, x))
 
 let pwildcard =
-  F.(PWildcard dummy_range)
+  F.(PWildcard None)
 
 let ptuple ps =
-  F.(PTuple (dummy_range, ps))
+  F.(PTuple (None, ps))
 
 let pvariant lbl datatype t =
-  F.(PVariant (dummy_range, lbl, datatype, t))
+  F.(PVariant (None, lbl, datatype, t))
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/client/test/TestML.ml b/client/test/TestML.ml
index 1d690c8..c55da53 100644
--- a/client/test/TestML.ml
+++ b/client/test/TestML.ml
@@ -2,57 +2,55 @@ open Client
 
 (* A few manually constructed terms. *)
 
-let dummy_pos = ML.dummy_pos
-
 let hole =
-  ML.Hole (dummy_pos, [])
+  ML.Hole (None, [])
 
 let x =
-  ML.Var (dummy_pos, "x")
+  ML.Var (None, "x")
 
 let y =
-  ML.Var (dummy_pos, "y")
+  ML.Var (None, "y")
 
 let id =
-  ML.Abs (dummy_pos, "x", x)
+  ML.Abs (None, "x", x)
 
 let delta =
-  ML.Abs (dummy_pos, "x", ML.App (dummy_pos, x, x))
+  ML.Abs (None, "x", ML.App (None, x, x))
 
 (* unused *)
 let _deltadelta =
-  ML.App (dummy_pos, delta, delta)
+  ML.App (None, delta, delta)
 
 let idid =
-  ML.App (dummy_pos, id, id)
+  ML.App (None, id, id)
 
 let k =
-  ML.Abs (dummy_pos, "x", ML.Abs (dummy_pos, "y", x))
+  ML.Abs (None, "x", ML.Abs (None, "y", x))
 
 let genid =
-  ML.Let (dummy_pos, "x", id, x)
+  ML.Let (None, "x", id, x)
 
 let genidid =
-  ML.Let (dummy_pos, "x", id, ML.App (dummy_pos, x, x))
+  ML.Let (None, "x", id, ML.App (None, x, x))
 
 let genkidid =
-  ML.Let (dummy_pos, "x", ML.App (dummy_pos, k, id), ML.App (dummy_pos, x, id))
+  ML.Let (None, "x", ML.App (None, k, id), ML.App (None, x, id))
 
 let genkidid2 =
-  ML.Let (dummy_pos, "x", ML.App (dummy_pos, ML.App (dummy_pos, k, id), id), x)
+  ML.Let (None, "x", ML.App (None, ML.App (None, k, id), id), x)
 
 (* unused *)
 let _app_pair = (* ill-typed *)
-  ML.App (dummy_pos, ML.Tuple (dummy_pos, [id; id]), id)
+  ML.App (None, ML.Tuple (None, [id; id]), id)
 
 let unit =
-  ML.Tuple (dummy_pos, [])
+  ML.Tuple (None, [])
 
 (* "let x1 = (...[], ...[]) in ...[] x1" *)
 let regression1 =
-  ML.Let (dummy_pos, "x1", ML.Tuple (dummy_pos, [ ML.Hole (dummy_pos, []) ;
-                                                  ML.Hole (dummy_pos, []) ]),
-          ML.App (dummy_pos, ML.Hole (dummy_pos, []), ML.Var (dummy_pos, "x1")))
+  ML.Let (None, "x1", ML.Tuple (None, [ ML.Hole (None, []) ;
+                                                  ML.Hole (None, []) ]),
+          ML.App (None, ML.Hole (None, []), ML.Var (None, "x1")))
 
 (* "let f = fun x ->
               let g = fun y -> (x, y) in
@@ -61,34 +59,34 @@ let regression1 =
             fun x -> fun y -> f" *)
 let regression2 =
   ML.(
-    Let (dummy_pos,
+    Let (None,
       "f",
-      Abs (dummy_pos,
+      Abs (None,
         "x",
-        Let (dummy_pos,
+        Let (None,
           "g",
-          Abs (dummy_pos,
+          Abs (None,
             "y",
-            Tuple (dummy_pos, [x; y])
+            Tuple (None, [x; y])
           ),
-          Var (dummy_pos, "g")
+          Var (None, "g")
         )),
-        Abs(dummy_pos,
+        Abs(None,
           "x",
-          Abs(dummy_pos,
+          Abs(None,
             "y",
-            Var (dummy_pos, "f"))))
+            Var (None, "f"))))
   )
 
 let abs_match_with =
   ML.(
     Abs(
-      dummy_pos,
+      None,
       "x",
       Match(
-        dummy_pos,
-        Tuple (dummy_pos, []),
-        [ (PTuple (dummy_pos, []), Tuple (dummy_pos, [])) ]
+        None,
+        Tuple (None, []),
+        [ (PTuple (None, []), Tuple (None, [])) ]
       )
     )
   )
@@ -110,43 +108,43 @@ let option_env =
       } ; {
         label_name = Label "Some";
         type_name = Type "option";
-        arg_type = Some (ML.TyVar (dummy_pos,"'a"));
+        arg_type = Some (ML.TyVar (None,"'a"));
       }
     ]
   } in
   Datatype.Env.add_decl Datatype.Env.empty option_typedecl
 
-let none = ML.Variant (dummy_pos, Datatype.Label "None" , None )
+let none = ML.Variant (None, Datatype.Label "None" , None )
 
 let some =
   ML.Variant (
-    dummy_pos,
+    None,
     Datatype.Label "Some",
     Some id
   )
 
 let match_none = ML.(
-    Match (dummy_pos, none, [
-      PVariant (dummy_pos, Datatype.Label "None", None), none ;
-      PVariant (dummy_pos, Datatype.Label "Some", Some (PVar (dummy_pos, "x"))), x ;
+    Match (None, none, [
+      PVariant (None, Datatype.Label "None", None), none ;
+      PVariant (None, Datatype.Label "Some", Some (PVar (None, "x"))), x ;
     ])
   )
 
 let match_some = ML.(
-    Match (dummy_pos, some, [
-      PVariant (dummy_pos, Datatype.Label "None", None), none ;
-      PVariant (dummy_pos, Datatype.Label "Some", Some (PWildcard dummy_pos)), none
+    Match (None, some, [
+      PVariant (None, Datatype.Label "None", None), none ;
+      PVariant (None, Datatype.Label "Some", Some (PWildcard None)), none
     ])
   )
 
 let match_some_annotated = ML.(
-    Match (dummy_pos, some, [
-      ( PVariant (dummy_pos, Datatype.Label "None", None), none );
-      ( PAnnot (dummy_pos,
-                PVariant (dummy_pos, Datatype.Label "Some",
-                          Some (PWildcard dummy_pos)),
-                (Flexible, ["'a"], TyConstr (dummy_pos, Datatype.Type "option",
-                                   [ TyVar (dummy_pos, "'a") ]))),
+    Match (None, some, [
+      ( PVariant (None, Datatype.Label "None", None), none );
+      ( PAnnot (None,
+                PVariant (None, Datatype.Label "Some",
+                          Some (PWildcard None)),
+                (Flexible, ["'a"], TyConstr (None, Datatype.Type "option",
+                                   [ TyVar (None, "'a") ]))),
         none );
     ])
   )
@@ -168,11 +166,11 @@ let list_env =
       } ; {
         label_name = Label "Cons";
         type_name = Type "list";
-        arg_type = Some (ML.(TyProduct (dummy_pos,
-                                        [ TyVar (dummy_pos, "'a") ;
-                                          TyConstr (dummy_pos,
+        arg_type = Some (ML.(TyProduct (None,
+                                        [ TyVar (None, "'a") ;
+                                          TyConstr (None,
                                                     Type "list",
-                                                    [ TyVar (dummy_pos, "'a") ])
+                                                    [ TyVar (None, "'a") ])
                                         ]
                      )));
       }
@@ -181,35 +179,35 @@ let list_env =
 
   Datatype.Env.add_decl option_env list_typedecl
 
-let nil = ML.Variant (dummy_pos, Datatype.Label "Nil" , None )
+let nil = ML.Variant (None, Datatype.Label "Nil" , None )
 
 let cons =
   ML.Variant (
-    dummy_pos,
+    None,
     Datatype.Label "Cons",
-    Some (ML.Tuple (dummy_pos, [ id ; nil ]))
+    Some (ML.Tuple (None, [ id ; nil ]))
   )
 
 (* unused *)
 let _list_annotated =
   let open ML in
   Annot (
-    dummy_pos,
+    None,
     Variant (
-      dummy_pos,
+      None,
       Datatype.Label "Cons",
-      Some (Tuple (dummy_pos, [
-                  Annot (dummy_pos, id,
-                         (Flexible, ["'a"], TyArrow (dummy_pos,
-                                           TyVar (dummy_pos, "'a"),
-                                           TyVar (dummy_pos, "'a"))));
+      Some (Tuple (None, [
+                  Annot (None, id,
+                         (Flexible, ["'a"], TyArrow (None,
+                                           TyVar (None, "'a"),
+                                           TyVar (None, "'a"))));
                   nil ]))
     ),
-    (Flexible, ["'a"; "'b"], TyConstr (dummy_pos,
+    (Flexible, ["'a"; "'b"], TyConstr (None,
                              Datatype.Type "list",
-                             [TyArrow (dummy_pos,
-                                       TyVar (dummy_pos, "'a"),
-                                       TyVar (dummy_pos, "'b"))]))
+                             [TyArrow (None,
+                                       TyVar (None, "'a"),
+                                       TyVar (None, "'b"))]))
   )
 
 (* tree *)
@@ -229,10 +227,10 @@ let tree_env =
       } ; {
         label_name = Label "Node";
         type_name = Type "tree";
-        arg_type = Some (ML.(TyProduct (dummy_pos, [
-          TyConstr (dummy_pos, Type "tree", [ TyVar (dummy_pos, "'a") ]);
-          TyVar (dummy_pos, "'a");
-          TyConstr (dummy_pos, Type "tree", [ TyVar (dummy_pos, "'a") ]);
+        arg_type = Some (ML.(TyProduct (None, [
+          TyConstr (None, Type "tree", [ TyVar (None, "'a") ]);
+          TyVar (None, "'a");
+          TyConstr (None, Type "tree", [ TyVar (None, "'a") ]);
         ])))
       }
     ];
@@ -240,13 +238,13 @@ let tree_env =
 
   Datatype.Env.add_decl list_env tree_typedecl
 
-let leaf = ML.Variant (dummy_pos, Datatype.Label "Leaf" , None )
+let leaf = ML.Variant (None, Datatype.Label "Leaf" , None )
 
 let node =
   ML.Variant (
-    dummy_pos,
+    None,
     Datatype.Label "Node",
-    Some (ML.Tuple (dummy_pos, [
+    Some (ML.Tuple (None, [
       leaf ;
       id ;
       leaf ;
@@ -353,25 +351,25 @@ let test_abs_match_with () =
   test_ok "fun x -> match () with () -> () end" abs_match_with
 
 let test_let () =
-  test_ok "let y = fun x -> x in ()" (ML.Let(dummy_pos, "y", id, unit))
+  test_ok "let y = fun x -> x in ()" (ML.Let(None, "y", id, unit))
 
 let test_let_prod_singleton () =
   test_ok "let (y,) = (fun x -> x,) in ()"
-    (ML.LetProd (dummy_pos, ["y"], ML.Tuple (dummy_pos, [id]), unit))
+    (ML.LetProd (None, ["y"], ML.Tuple (None, [id]), unit))
 
 let test_let_prod () =
   test_ok "let (y,z) = (fun x -> x, ()) in ()"
-  (ML.LetProd (dummy_pos, ["y";"z"], ML.Tuple (dummy_pos, [id;unit]), unit))
+  (ML.LetProd (None, ["y";"z"], ML.Tuple (None, [id;unit]), unit))
 
 let test_singleton () =
   test_ok
     "(fun x -> x,)"
-    (ML.Tuple (dummy_pos, [id]))
+    (ML.Tuple (None, [id]))
 
 let test_pair_tuple () =
   test_ok
     "(fun x -> x, fun x -> x)"
-    (ML.Tuple (dummy_pos, [id; id]))
+    (ML.Tuple (None, [id; id]))
 
 let option_env_str =
   "type option 'a = None | Some of 'a"
@@ -392,8 +390,8 @@ let test_some_pair () =
   test_ok
     ~typedecl:option_env_str
     "Some (fun x -> x, fun x -> x)"
-    (ML.Variant (dummy_pos, Datatype.Label "Some",
-                 Some (ML.Tuple (dummy_pos, [id;id]))))
+    (ML.Variant (None, Datatype.Label "Some",
+                 Some (ML.Tuple (None, [id;id]))))
 
 let list_env_str = "type list 'a = Nil | Cons of {'a * list 'a}"
 
@@ -413,17 +411,17 @@ let test_arrow () =
   test_ok
     ~typedecl:"type func 'a 'b = Func of 'a -> 'b"
     "Func (fun x -> x)"
-    (ML.Variant (dummy_pos, Datatype.Label "Func", Some id))
+    (ML.Variant (None, Datatype.Label "Func", Some id))
 
 let test_match_tuple () =
   test_ok
     "match (fun x -> x, ()) with (f, ()) -> f end"
     (ML.Match
-       (dummy_pos,
-        ML.Tuple (dummy_pos, [id;unit]),
-        [ (ML.PTuple (dummy_pos, [ML.PVar (dummy_pos, "f");
-                                  ML.PTuple (dummy_pos, [])]),
-           ML.Var (dummy_pos, "f")) ]
+       (None,
+        ML.Tuple (None, [id;unit]),
+        [ (ML.PTuple (None, [ML.PVar (None, "f");
+                                  ML.PTuple (None, [])]),
+           ML.Var (None, "f")) ]
     ))
 
 let test_match_none () =
@@ -464,21 +462,21 @@ let test_regression2 () =
     "let f = fun x -> let g = fun y -> (x, y) in g in fun x -> fun y -> f"
     regression2
 
-let a = ML.TyVar (dummy_pos, "'a")
-let b = ML.TyVar (dummy_pos, "'b")
+let a = ML.TyVar (None, "'a")
+let b = ML.TyVar (None, "'b")
 
 let id_annot annot =
-  ML.(Annot (dummy_pos, Abs(dummy_pos, "x", Var (dummy_pos, "x")), annot))
+  ML.(Annot (None, Abs(None, "x", Var (None, "x")), annot))
 
 let test_id_rigid () =
   test_ok
     "(fun x -> x : for 'a. 'a -> 'a)"
-    (id_annot (ML.Rigid, ["'a"], ML.TyArrow (dummy_pos, a, a)))
+    (id_annot (ML.Rigid, ["'a"], ML.TyArrow (None, a, a)))
 
 let test_id_flexible () =
   test_ok
     "(fun x -> x : some 'a 'b. 'a -> 'b)"
-    (id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (dummy_pos, a, b)))
+    (id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (None, a, b)))
 
 let test_suite =
   let open Alcotest in
diff --git a/client/test/TestMLRandom.ml b/client/test/TestMLRandom.ml
index 618d9a3..33081fb 100644
--- a/client/test/TestMLRandom.ml
+++ b/client/test/TestMLRandom.ml
@@ -54,7 +54,7 @@ module Shrinker = struct
     (p, subst_under_pat p t x u)
 
   let remove_variable t x =
-    subst t x (ML.Hole (ML.dummy_pos, []))
+    subst t x (ML.Hole (None, []))
 
   let remove_variables t xs =
     List.fold_left remove_variable t xs
@@ -86,12 +86,12 @@ module Shrinker = struct
          important to reproduce typing bugs.
          So we start with just (t1) and (t2) as shrinking choices,
          even though they typically do not preserve typability. *)
-      of_list ts <+> return (ML.Hole (ML.dummy_pos, ts)) in
+      of_list ts <+> return (ML.Hole (None, ts)) in
     (match t with
      | ML.Hole (_, []) ->
         empty
      | _ ->
-       return (ML.Hole (ML.dummy_pos, []))
+       return (ML.Hole (None, []))
     ) <+> (
       match t with
       | ML.Var _ ->
diff --git a/src/Solver.ml b/src/Solver.ml
index b9fae2b..6ab4e80 100644
--- a/src/Solver.ml
+++ b/src/Solver.ml
@@ -50,7 +50,7 @@ module VarTable = Hashtbl
 
 (* The syntax of constraints. *)
 
-type range =
+type loc =
   Lexing.position * Lexing.position
 
 type shallow_ty =
@@ -74,9 +74,9 @@ type schemes =
    elaboration in an elegant way. *)
 type _ co =
 
-| CRange : range * 'a co -> 'a co
-    (**The constraint [CRange (range, c)] is equivalent to the constraint [c],
-       and is annotated with [range], a range of positions in some piece of
+| CLoc : loc * 'a co -> 'a co
+    (**The constraint [CLoc (loc, c)] is equivalent to the constraint [c],
+       and is annotated with [loc], a source location in some piece of
        source code. *)
 
 | CTrue : unit co
@@ -146,10 +146,10 @@ type _ co =
 (* -------------------------------------------------------------------------- *)
 (* Exceptions. *)
 
-exception Unbound of range * tevar
-exception Unify of range * O.ty * O.ty
-exception Cycle of range * O.ty
-exception VariableScopeEscape of range
+exception Unbound of loc option * tevar
+exception Unify of loc option * O.ty * O.ty
+exception Cycle of loc option * O.ty
+exception VariableScopeEscape of loc option
 
 (* A pretty-printer for constraints, used while debugging. *)
 
@@ -178,7 +178,7 @@ module Printer = struct
      [conj], [simple]. The [entry] layer is a synonym for [binders] and is
      the entry point. *)
 
-  (* [CRange] and [CMap] constructors are ignored by this printer. *)
+  (* [CLoc] and [CMap] constructors are ignored by this printer. *)
 
   let rec entry : type a . a co -> document = fun c ->
     binders c
@@ -187,7 +187,7 @@ module Printer = struct
     let next = conj in
     let self = binders in
     group @@ match c with
-    | CRange (_, c) ->
+    | CLoc (_, c) ->
         self c
     | CMap (c, _) ->
         self c
@@ -219,7 +219,7 @@ module Printer = struct
     let self = conj in
     let next = simple in
     group @@ match c with
-    | CRange (_, c) ->
+    | CLoc (_, c) ->
         self c
     | CMap (c, _) ->
         self c
@@ -231,7 +231,7 @@ module Printer = struct
   and simple : type a . a co -> document = fun c ->
     let self = simple in
     group @@ match c with
-    | CRange (_, c) ->
+    | CLoc (_, c) ->
         self c
     | CMap (c, _) ->
         self c
@@ -288,11 +288,11 @@ module Env = struct
   let table =
     TeVarMap.create 8
 
-  let lookup range x =
+  let lookup ~loc x =
     try
       TeVarMap.find table x
     with Not_found ->
-      raise (Unbound (range, x))
+      raise (Unbound (loc, x))
 
   let bind x s =
     (* Shadowing allowed. *)
@@ -398,25 +398,25 @@ let decode_scheme (s : G.scheme) : scheme =
    A cyclic decoder is used even if [rectypes] is [false]. Indeed, recursive
    types can appear before the occurs check has been performed. *)
 
-let unify range v1 v2 =
+let unify ~loc v1 v2 =
   try
     U.unify v1 v2
   with
   | U.Unify (v1, v2) ->
      let decode = D.new_cyclic_decoder() in
-     raise (Unify (range, decode v1, decode v2))
+     raise (Unify (loc, decode v1, decode v2))
   | G.VariableScopeEscape ->
-     raise (VariableScopeEscape range)
+     raise (VariableScopeEscape loc)
 
-let exit range ~rectypes vs =
+let exit ~loc ~rectypes vs =
   try
     G.exit ~rectypes vs
   with
   | G.Cycle v ->
      let decode = D.new_cyclic_decoder() in
-     raise (Cycle (range, decode v))
+     raise (Cycle (loc, decode v))
   | G.VariableScopeEscape ->
-     raise (VariableScopeEscape range)
+     raise (VariableScopeEscape loc)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -433,7 +433,7 @@ let exit range ~rectypes vs =
 
 let rec ok : type a . a co -> bool =
   function
-  | CRange (_, c) ->
+  | CLoc (_, c) ->
       ok c
   | CTrue | CPure _ ->
       true
@@ -478,26 +478,27 @@ type 'a on_sol =
    closure of type ['a on_sol], which implements the second phase: it
    describes how to compute a result once resolution is successful.
 
-   [solve] is parameterized with an environment (which maps term variables to
-   type schemes) and with a range (the range annotation that was most recently
-   encountered on the way down). *)
+   [solve] is parameterized with an environment (which maps term
+   variables to type schemes) and with an optional source location
+   (the location annotation that was most recently encountered on the
+   way down). *)
 
 open UVar
 
-let rec solve : type a . range -> a co -> a on_sol =
-  fun range c -> match c with
-  | CRange (range, c) ->
-      solve range c
+let rec solve : type a . loc:loc option -> a co -> a on_sol =
+  fun ~loc c -> match c with
+  | CLoc (loc, c) ->
+      solve ~loc:(Some loc) c
   | CTrue ->
       On_sol (fun () -> ())
   | CPure x ->
       On_sol (fun () -> x)
   | CMap (c, f) ->
-      let (On_sol r) = solve range c in
+      let (On_sol r) = solve ~loc c in
       On_sol (fun () -> f (r ()))
   | CConj (c1, c2) ->
-      let (On_sol r1) = solve range c1 in
-      let (On_sol r2) = solve range c2 in
+      let (On_sol r1) = solve ~loc c1 in
+      let (On_sol r2) = solve ~loc c2 in
       On_sol (fun () ->
         (* Even though we recommend using semantic actions without side
            effects, it seems wise to impose left-to-right evaluation of
@@ -507,11 +508,11 @@ let rec solve : type a . range -> a co -> a on_sol =
         a1, a2
       )
   | CEq (v, w) ->
-      unify range (uvar v) (uvar w);
+      unify ~loc (uvar v) (uvar w);
       On_sol (fun () -> ())
   | CExist (v, s, c) ->
       ignore (flexible v s);
-      let result = solve range c in
+      let result = solve ~loc c in
       uunbind v;
       result
   | CDecode v ->
@@ -519,16 +520,16 @@ let rec solve : type a . range -> a co -> a on_sol =
       On_sol (fun () -> decode uv)
   | CInstance (x, w) ->
       (* The environment provides a type scheme for [x]. *)
-      let s = Env.lookup range x in
+      let s = Env.lookup ~loc x in
       (* Instantiating this type scheme yields a variable [v], which we
          unify with [w]. It also yields a list of witnesses, which we
          record, as they will be useful during the decoding phase. *)
       let witnesses, v = G.instantiate s in
-      unify range v (uvar w);
+      unify ~loc v (uvar w);
       On_sol (fun () -> List.map decode witnesses)
   | CDef (x, v, c) ->
       Env.bind x (G.trivial (uvar v));
-      let a = solve range c in
+      let a = solve ~loc c in
       Env.unbind x;
       a
   | CLet (rs, xs, vs, c1, c2) ->
@@ -542,7 +543,7 @@ let rec solve : type a . range -> a co -> a on_sol =
          basically, but they also serve as named entry points. *)
       let uvs = List.map (fun v -> flexible v None) vs in
       (* Solve the constraint [c1]. *)
-      let (On_sol r1) = solve range c1 in
+      let (On_sol r1) = solve ~loc c1 in
       (* Ask the generalization engine to perform an occurs check, to adjust
          the ranks of the type variables in the young generation (i.e., all
          of the type variables that were registered since the call to
@@ -550,7 +551,7 @@ let rec solve : type a . range -> a co -> a on_sol =
          our entry points. The generalization engine also produces a list
          [gammas] of the young variables that should be universally
          quantified here. *)
-      let gammas, ss = exit range ~rectypes uvs in
+      let gammas, ss = exit ~loc ~rectypes uvs in
       (* All rigid variables of [rs] must be generalizable. This assertion
          may be costly and should be removed or disabled in the future. *)
       assert (urs |> List.for_all (fun r -> List.mem r gammas));
@@ -558,7 +559,7 @@ let rec solve : type a . range -> a co -> a on_sol =
       (* Extend the environment [env]. *)
       List.iter2 Env.bind xs ss;
       (* Proceed to solve [c2] in the extended environment. *)
-      let (On_sol r2) = solve range c2 in
+      let (On_sol r2) = solve ~loc c2 in
       List.iter Env.unbind xs;
       On_sol (fun () ->
         List.map decode_variable gammas,
@@ -578,9 +579,8 @@ let main (type a) (c : a co) : a =
   if not (ok c) then
     invalid_arg "solve: ill-formed toplevel constraint";
 
-  let range = Lexing.(dummy_pos, dummy_pos) in
   (* Phase 1: solve the constraint. *)
-  let (On_sol r) = solve range c in
+  let (On_sol r) = solve ~loc:None c in
   (* Phase 2: elaborate. *)
   r()
 
@@ -803,8 +803,8 @@ let let0 c1 =
 
 (* Correlation with the source code. *)
 
-let correlate range c =
-  CRange (range, c)
+let correlate loc c =
+  CLoc (loc, c)
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/src/Solver.mli b/src/Solver.mli
index 1452dbd..cb27ff9 100644
--- a/src/Solver.mli
+++ b/src/Solver.mli
@@ -385,41 +385,40 @@ module Make
 
   (* Correlation with the source code. *)
 
-  (**The type [range] describes a range in some source code. It is not
+  (**The type [loc] describes a range in some source code. It is not
      interpreted by the solver. It is used only as part of error reports. *)
-  type range =
-    Lexing.position * Lexing.position
+  type loc = Lexing.position * Lexing.position
 
-  (**The constraint [correlate range c] is equivalent to [c], but records that
-     this constraint is correlated with the range [range] in the source code.
+  (**The constraint [correlate loc c] is equivalent to [c], but records that
+     this constraint is correlated with the source code location [loc].
      This information is used in error reports. The exceptions {!Unbound},
-     {!Unify}, {!Cycle}, and {!VariableScopeEscape} carry a range: it is the
-     nearest range that encloses the abstract syntax tree node where the error
-     is detected. *)
-  val correlate: range -> 'a co -> 'a co
+     {!Unify}, {!Cycle}, and {!VariableScopeEscape} carry an optional location:
+     it is the nearest location that encloses the abstract syntax tree node
+     where the error is detected. *)
+  val correlate: loc -> 'a co -> 'a co
 
   (** {2 Solving Constraints} *)
 
   (**This exception is raised by {!solve} when an instantiation constraint
      [instance x α] refers to an unbound variable [x]. *)
-  exception Unbound of range * tevar
+  exception Unbound of loc option * tevar
 
   (**This exception is raised by {!solve} when an equality constraint cannot
      be satisfied. It carries two decoded types, representing the equality
      constraint that could not be satisfied. *)
-  exception Unify of range * ty * ty
+  exception Unify of loc option * ty * ty
 
   (**This exception is raised by {!solve} when a cyclic equality constraint
      is detected, if [rectypes] is [false]. It carries a decoded type, which
      is a recursive type: that is, this type involves a μ binder. *)
-  exception Cycle of range * ty
+  exception Cycle of loc option * ty
 
   (**This exception is raised by {!solve} when a rigid variable escapes its
      scope, that is, roughly speaking, when one attempts to unify a rigid
      variable with a more ancient flexible variable. For example, attempting
      to solve the constraints [∃α. ∀β. α = β] or [∃α. ∀β. ∃γ. α = β → γ]
      causes this exception to be raised. *)
-  exception VariableScopeEscape of range
+  exception VariableScopeEscape of loc option
 
   (**[solve ~rectypes c] determines whether the constraint [c] is satisfiable,
      and if so, computes and returns its semantic value. (The constraint [c]
-- 
GitLab


From 85743ed827763e2df02a1ed8798d5573643bf662 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sun, 12 Feb 2023 10:54:34 +0100
Subject: [PATCH 4/5] use an error type in the Solver as well

---
 client/Infer.ml | 24 ++++++++++++++++--------
 src/Solver.ml   | 23 +++++++++++++----------
 src/Solver.mli  | 48 +++++++++++++++++++++++++++---------------------
 3 files changed, 56 insertions(+), 39 deletions(-)

diff --git a/client/Infer.ml b/client/Infer.ml
index 441136b..6851e1d 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -655,14 +655,22 @@ let get_tevar x =
 
 let translate_with_hook ~hook ~rectypes env t =
   try Solver.solve ~rectypes (hastype_with_hook ~hook env t) with
-  | Solver.Unbound (loc, x) ->
-    raise (Error (loc, Unbound (get_tevar x)))
-  | Solver.Unify (loc, t1, t2) ->
-    raise (Error (loc, Unify (t1, t2)))
-  | Solver.Cycle (loc, ty) ->
-    raise (Error (loc, Cycle ty))
-  | Solver.VariableScopeEscape loc ->
-    raise (Error (loc, VariableScopeEscape))
+  | Solver.Error (loc, solver_error) ->
+    (* TODO: it would be nice to be able to share the definition
+       of errors of the solver, instead of duplicating them
+       in a separate type.
+
+       This is not obvious to do, because the Solver error type is
+       defined inside the functor, and the functor application is no
+       mentioned at all in the Infer interface currently.
+    *)
+    let error : error = match solver_error with
+      | Solver.Unbound x -> Unbound (get_tevar x)
+      | Solver.Unify (t1, t2) -> Unify (t1, t2)
+      | Solver.Cycle (ty) -> Cycle (ty)
+      | Solver.VariableScopeEscape -> VariableScopeEscape
+    in
+    raise (Error (loc, error))
 
 let translate ~rectypes env t =
   let ((), res) = translate_with_hook ~hook:ignore ~rectypes env t in
diff --git a/src/Solver.ml b/src/Solver.ml
index 6ab4e80..fe6d540 100644
--- a/src/Solver.ml
+++ b/src/Solver.ml
@@ -144,12 +144,15 @@ type _ co =
        - the semantic value [v2] of the constraint [c2]. *)
 
 (* -------------------------------------------------------------------------- *)
-(* Exceptions. *)
+(* Errors. *)
 
-exception Unbound of loc option * tevar
-exception Unify of loc option * O.ty * O.ty
-exception Cycle of loc option * O.ty
-exception VariableScopeEscape of loc option
+  type error =
+    | Unbound of tevar
+    | Unify of O.ty * O.ty
+    | Cycle of O.ty
+    | VariableScopeEscape
+
+  exception Error of loc option * error
 
 (* A pretty-printer for constraints, used while debugging. *)
 
@@ -292,7 +295,7 @@ module Env = struct
     try
       TeVarMap.find table x
     with Not_found ->
-      raise (Unbound (loc, x))
+      raise (Error (loc, Unbound x))
 
   let bind x s =
     (* Shadowing allowed. *)
@@ -404,9 +407,9 @@ let unify ~loc v1 v2 =
   with
   | U.Unify (v1, v2) ->
      let decode = D.new_cyclic_decoder() in
-     raise (Unify (loc, decode v1, decode v2))
+     raise (Error (loc, Unify (decode v1, decode v2)))
   | G.VariableScopeEscape ->
-     raise (VariableScopeEscape loc)
+     raise (Error (loc, VariableScopeEscape))
 
 let exit ~loc ~rectypes vs =
   try
@@ -414,9 +417,9 @@ let exit ~loc ~rectypes vs =
   with
   | G.Cycle v ->
      let decode = D.new_cyclic_decoder() in
-     raise (Cycle (loc, decode v))
+     raise (Error (loc, Cycle (decode v)))
   | G.VariableScopeEscape ->
-     raise (VariableScopeEscape loc)
+     raise (Error (loc, VariableScopeEscape))
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/src/Solver.mli b/src/Solver.mli
index cb27ff9..4e2a8e2 100644
--- a/src/Solver.mli
+++ b/src/Solver.mli
@@ -399,26 +399,29 @@ module Make
 
   (** {2 Solving Constraints} *)
 
-  (**This exception is raised by {!solve} when an instantiation constraint
-     [instance x α] refers to an unbound variable [x]. *)
-  exception Unbound of loc option * tevar
-
-  (**This exception is raised by {!solve} when an equality constraint cannot
-     be satisfied. It carries two decoded types, representing the equality
-     constraint that could not be satisfied. *)
-  exception Unify of loc option * ty * ty
-
-  (**This exception is raised by {!solve} when a cyclic equality constraint
-     is detected, if [rectypes] is [false]. It carries a decoded type, which
-     is a recursive type: that is, this type involves a μ binder. *)
-  exception Cycle of loc option * ty
-
-  (**This exception is raised by {!solve} when a rigid variable escapes its
-     scope, that is, roughly speaking, when one attempts to unify a rigid
-     variable with a more ancient flexible variable. For example, attempting
-     to solve the constraints [∃α. ∀β. α = β] or [∃α. ∀β. ∃γ. α = β → γ]
-     causes this exception to be raised. *)
-  exception VariableScopeEscape of loc option
+  type error =
+    | Unbound of tevar
+      (**An instantiation constraint [instance x α]
+         refers to an unbound variable [x]. *)
+
+    | Unify of ty * ty
+      (**An equality constraint cannot be satisfied. The error
+         carries two decoded types, representing the equality
+         constraint that could not be satisfied. *)
+
+    | Cycle of ty
+      (**A cyclic equality constraint is detected, and [rectypes] is
+         [false]. The error carries a decoded type, which is
+         a recursive type: that is, this type involves a μ binder. *)
+
+    | VariableScopeEscape
+      (**A rigid variable escapes its scope, that is, roughly
+         speaking, one attempts to unify a rigid variable with a more
+         ancient flexible variable. For example, attempting to solve
+         the constraints [∃α. ∀β. α = β] or [∃α. ∀β. ∃γ. α = β → γ]
+         causes this error. *)
+
+  exception Error of loc option * error
 
   (**[solve ~rectypes c] determines whether the constraint [c] is satisfiable,
      and if so, computes and returns its semantic value. (The constraint [c]
@@ -432,7 +435,10 @@ module Make
      every (binding or free) occurrence of a type variable must be wrapped in
      {!let0} or in the left-hand side of {!let1} or its variants ({!letr1},
      {!letn}, {!letrn}). To turn an arbitrary constraint [c] into a toplevel
-     constraint, just write [let0 c]. *)
+     constraint, just write [let0 c].
+
+     @raise Error
+  *)
   val solve: rectypes:bool -> 'a co -> 'a
 
   (**/**)
-- 
GitLab


From c00f5569d8feaad09ed7181100a4bfc744e27470 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sun, 12 Feb 2023 22:35:20 +0100
Subject: [PATCH 5/5] include all Infer errors in the testsuite

---
 client/test/suite.t/error-cycle.midml         |  1 +
 client/test/suite.t/error-unbound.midml       |  1 +
 client/test/suite.t/error-unify-app-arg.midml |  2 +
 client/test/suite.t/error-unify-app-fun.midml |  2 +
 client/test/suite.t/error-unify-letprod.midml |  2 +
 .../suite.t/error-variable-scope-escape.midml |  2 +
 client/test/suite.t/run.t                     | 82 +++++++++++++++++--
 7 files changed, 87 insertions(+), 5 deletions(-)
 create mode 100644 client/test/suite.t/error-cycle.midml
 create mode 100644 client/test/suite.t/error-unbound.midml
 create mode 100644 client/test/suite.t/error-unify-app-arg.midml
 create mode 100644 client/test/suite.t/error-unify-app-fun.midml
 create mode 100644 client/test/suite.t/error-unify-letprod.midml
 create mode 100644 client/test/suite.t/error-variable-scope-escape.midml

diff --git a/client/test/suite.t/error-cycle.midml b/client/test/suite.t/error-cycle.midml
new file mode 100644
index 0000000..c3f189f
--- /dev/null
+++ b/client/test/suite.t/error-cycle.midml
@@ -0,0 +1 @@
+let self_app = fun x -> x x
diff --git a/client/test/suite.t/error-unbound.midml b/client/test/suite.t/error-unbound.midml
new file mode 100644
index 0000000..1d840c8
--- /dev/null
+++ b/client/test/suite.t/error-unbound.midml
@@ -0,0 +1 @@
+let x = (fun y -> z)
diff --git a/client/test/suite.t/error-unify-app-arg.midml b/client/test/suite.t/error-unify-app-arg.midml
new file mode 100644
index 0000000..f6c72f5
--- /dev/null
+++ b/client/test/suite.t/error-unify-app-arg.midml
@@ -0,0 +1,2 @@
+let x =
+  (fun y z -> y z) ()
diff --git a/client/test/suite.t/error-unify-app-fun.midml b/client/test/suite.t/error-unify-app-fun.midml
new file mode 100644
index 0000000..495dd5c
--- /dev/null
+++ b/client/test/suite.t/error-unify-app-fun.midml
@@ -0,0 +1,2 @@
+let app_error = fun x ->
+  (x, x) (fun y -> y)
diff --git a/client/test/suite.t/error-unify-letprod.midml b/client/test/suite.t/error-unify-letprod.midml
new file mode 100644
index 0000000..64ae2f0
--- /dev/null
+++ b/client/test/suite.t/error-unify-letprod.midml
@@ -0,0 +1,2 @@
+let letprod_error =
+  let (x, y) = (fun z -> z) in x
diff --git a/client/test/suite.t/error-variable-scope-escape.midml b/client/test/suite.t/error-variable-scope-escape.midml
new file mode 100644
index 0000000..5c4ec49
--- /dev/null
+++ b/client/test/suite.t/error-variable-scope-escape.midml
@@ -0,0 +1,2 @@
+let rigid_escape = fun f ->
+  (fun x -> f x : for 'a . 'a -> 'a)
diff --git a/client/test/suite.t/run.t b/client/test/suite.t/run.t
index 5ba32dc..8b8ef78 100644
--- a/client/test/suite.t/run.t
+++ b/client/test/suite.t/run.t
@@ -1,4 +1,4 @@
-Basics
+# Basics
 
   $ cat id.midml
   let id =
@@ -63,7 +63,79 @@ Basics
   File "test", line 2, characters 10-10:
   Syntax error.
 
-Option type
+# Errors
+
+Unbound variables.
+
+  $ cat error-unbound.midml
+  let x = (fun y -> z)
+
+  $ midml error-unbound.midml
+  Type inference and translation to System F...
+  File "test", line 1, characters 18-19:
+  Type error: unbound variable "z".
+
+Some unification errors (not exhaustive!)
+
+  $ cat error-unify-letprod.midml
+  let letprod_error =
+    let (x, y) = (fun z -> z) in x
+
+  $ midml error-unify-letprod.midml
+  Type inference and translation to System F...
+  File "test", line 2, characters 16-26:
+  Type error: mismatch between the type:
+  {r2*r4}
+  and the type:
+  r8 -> r10
+
+  $ cat error-unify-app-fun.midml
+  let app_error = fun x ->
+    (x, x) (fun y -> y)
+
+  $ midml error-unify-app-fun.midml
+  Type inference and translation to System F...
+  File "test", line 2, characters 2-8:
+  Type error: mismatch between the type:
+  r8 -> r4
+  and the type:
+  {r12*r14}
+
+  $ cat error-unify-app-arg.midml
+  let x =
+    (fun y z -> y z) ()
+
+  $ midml error-unify-app-arg.midml
+  Type inference and translation to System F...
+  File "test", line 2, characters 19-21:
+  Type error: mismatch between the type:
+  r12 -> r14
+  and the type:
+  {}
+
+Cycles
+
+  $ cat error-cycle.midml
+  let self_app = fun x -> x x
+
+  $ midml error-cycle.midml
+  Type inference and translation to System F...
+  File "test", line 1, characters 15-27:
+  Type error: a cyclic type arose.
+  mu  a0. a0 -> r4
+
+Variable scope escape
+
+  $ cat error-variable-scope-escape.midml
+  let rigid_escape = fun f ->
+    (fun x -> f x : for 'a . 'a -> 'a)
+
+  $ midml error-variable-scope-escape.midml
+  Type inference and translation to System F...
+  File "test", line 2, characters 2-36:
+  A rigid variable escapes its scope.
+
+# Option type
 
   $ cat none.midml
   #use option.midml
@@ -108,7 +180,7 @@ Option type
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
-List type
+# List type
 
   $ cat nil.midml
   #use list.midml
@@ -178,7 +250,7 @@ List type
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
-Annotations
+# Annotations
 
   $ cat nat-annot.midml
   type nat = | Zero | Succ of nat
@@ -192,7 +264,7 @@ Annotations
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
-Pattern-matching
+# Pattern-matching
 
   $ cat match-tuple.midml
   let _ =
-- 
GitLab