diff --git a/client/F.ml b/client/F.ml
index 72891b5935d8698d7f9b806e46fdd6e2a24a19b1..88c0c8af569aababc4c421e5f25903025c4f9a13 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 loc = Utils.loc
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -86,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
@@ -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 ee46f38aafc4eacc238ff6d5f8e1e29491a778e9..82037273fd2cbb990b7b9ca51855b39d9fa8dd76 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 loc = Utils.loc
 
 type ('a, 'b) typ =
   | TyVar of 'a
@@ -86,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
@@ -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: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 d5079d2d7343f71887877792cb2a7b4576f24e86..4d67c6160b059082e5644932ebc4ac25bbd88dd4 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 loc * 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 92324a968b714b08c7e55156cdc2d80c509bf200..1bb09efaca28e017c21362486dd0792abc99a469 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 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, 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 96e0f2d5a67c3fd5f9f3f9e128bba91402a81755..6851e1de6603cf8699a70fb7e3901b19e325dff7 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 Utils.loc * 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,12 +272,10 @@ 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]. *)
-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, _, _)
@@ -274,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
@@ -296,80 +312,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_loc 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 +397,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 +406,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 +469,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 +483,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 +523,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 +550,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 +599,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 +611,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_loc 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 +648,57 @@ 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.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
+  res
+
+let emit_error loc (error : error) =
+  let emit_type ty =
+    Utils.emit_endline (FPrinter.print_type ty)
+  in
+  Utils.emit_loc loc;
+  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 ebf90c979020209c9da5519723ff966fcaa967d7..7cb977e760a0e4025010e4cd6a1837512ea6f006 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.loc * 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.loc -> error -> unit
diff --git a/client/ML.ml b/client/ML.ml
index 991c1af8d44c3e4432bb2127ce4c90d5743b37d5..f91cf3c90a87d7d7559828df864239b0d07cf62d 100644
--- a/client/ML.ml
+++ b/client/ML.ml
@@ -7,21 +7,20 @@ type 'a list = 'a List.t =
   | (::) of 'a * 'a list
   [@@deriving compare]
 
-type range =
-  Lexing.position * Lexing.position
+type loc = Utils.loc
 
-(* We generate a comparison function [compare] 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
@@ -32,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 071d07903422b99c2abda804ab0aa1ddb9ec0c53..676090b1adbc0541f5ca7fd6ac494c8fa751275d 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 91ecc90b8bad0b5cefaccb44068079ec07f189dc..13cda8c43cdcdd4062435dec1d992412a02a520d 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 f05e06453ffc66aacf97de25c4231dc5fbf8be53..90a152233738cb70f98b6bf93a938e56c21d144c 100644
--- a/client/Utils.ml
+++ b/client/Utils.ml
@@ -15,3 +15,15 @@ let emit doc =
 let emit_endline doc =
   emit PPrint.(doc ^^ hardline);
   flush stdout
+
+type loc = (Lexing.position * Lexing.position) option
+
+let emit_loc = function
+  | None -> ()
+  | Some range ->
+    print_string (MenhirLib.LexerUtil.range range);
+    flush stdout
+
+let emit_error loc doc =
+  emit_loc loc;
+  emit_endline doc
diff --git a/client/Utils.mli b/client/Utils.mli
index cab144e2c5a83b61ee89374b99ef7167487ec33c..f7da6cb606105365a8acb18cd08a877e0a82ebfe 100644
--- a/client/Utils.mli
+++ b/client/Utils.mli
@@ -15,3 +15,10 @@ 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 loc = (Lexing.position * Lexing.position) option
+val emit_loc : loc -> unit
+
+(* Similar to {!emit_endline}, but starts by printing
+   a source location. *)
+val emit_error : loc -> PPrint.document -> unit
diff --git a/client/bin/midml.ml b/client/bin/midml.ml
index ff1d9908c03e320e42486fc52ca8839110da344f..8aab9ce93c574fbbeb857b3782ef67972c0cade4 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/BenchMLRandom.ml b/client/test/BenchMLRandom.ml
index 28c94d0a71dfe29bfdad688da70a1365d8368f31..8c088561158d4149d1304a2af028cc0a00289c5c 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 8a5c68684af3015a68bd249526505753b2e78008..7ff73b8c0beae8e72f687d9dde95c257f043511d 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, Utils.loc * 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. *)
diff --git a/client/test/CheckML.ml b/client/test/CheckML.ml
index 6f7c7754ccdcc6fb14b03116841752f0cd6bcfb7..33e9e98a763b3da1a96fb7091c8fcf00da18bd4b 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,14 +21,14 @@ let equal_term t1 t2 =
 
 (* -------------------------------------------------------------------------- *)
 
-exception ParsingError of Infer.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
@@ -75,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
 
@@ -123,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 b772dea5aaa38b015ba3f56261346bb22539a966..e320cf819ae8332022966caae23286c991d1973c 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 936c16c3747c3a912dfc8b67981e85def521f6d1..c2e431fd5d84947719639e6c92a60c7c6b53ea8f 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -8,64 +8,64 @@ let (-->) ty1 ty2 =
   F.TyArrow (ty1, ty2)
 
 let unit =
-  F.Tuple (F.dummy_range, [])
+  F.Tuple (None, [])
 
 let unit_type =
   F.TyProduct []
 
 let unit_pattern =
-  F.PTuple (F.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 1d690c818198f6a93b7c044f8c829980b155dae2..c55da53331e7229f8aff1a9a476d3e6fd23fd0c6 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 618d9a3894c5c95fce510b97f3c74c1d9e580a42..33081fb56b81ce0be96641c8089fa30f06afcb61 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/client/test/suite.t/error-cycle.midml b/client/test/suite.t/error-cycle.midml
new file mode 100644
index 0000000000000000000000000000000000000000..c3f189f1fc89f30dbd6869cfc5ec615eaec870de
--- /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 0000000000000000000000000000000000000000..1d840c80279154e69876d227b325dab6a1398b8b
--- /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 0000000000000000000000000000000000000000..f6c72f5bd7e94a67f93a9b47154d431c7749b7da
--- /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 0000000000000000000000000000000000000000..495dd5cdb070c02bb6fe90c6f5a2e45913ffbe33
--- /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 0000000000000000000000000000000000000000..64ae2f0d08b56cf6c49ce42bc194626c8463900e
--- /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 0000000000000000000000000000000000000000..5c4ec498f5820337b6611b4d91572c4c3cdae700
--- /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 c87f0bdd721c2d915d5e1364bd5f895cdd452a3c..8b8ef784ba692980371fdcb6c6a0730f9bf5616d 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 _ =
@@ -346,7 +418,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 +433,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:
diff --git a/src/Solver.ml b/src/Solver.ml
index b9fae2b4e29f29adec3a7bab2fd0f594e6009fab..fe6d540521609bc28e8713d0b8a61d88889d2861 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
@@ -144,12 +144,15 @@ type _ co =
        - the semantic value [v2] of the constraint [c2]. *)
 
 (* -------------------------------------------------------------------------- *)
-(* Exceptions. *)
+(* Errors. *)
 
-exception Unbound of range * tevar
-exception Unify of range * O.ty * O.ty
-exception Cycle of range * O.ty
-exception VariableScopeEscape of range
+  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. *)
 
@@ -178,7 +181,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 +190,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 +222,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 +234,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 +291,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 (Error (loc, Unbound x))
 
   let bind x s =
     (* Shadowing allowed. *)
@@ -398,25 +401,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 (Error (loc, Unify (decode v1, decode v2)))
   | G.VariableScopeEscape ->
-     raise (VariableScopeEscape range)
+     raise (Error (loc, VariableScopeEscape))
 
-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 (Error (loc, Cycle (decode v)))
   | G.VariableScopeEscape ->
-     raise (VariableScopeEscape range)
+     raise (Error (loc, VariableScopeEscape))
 
 (* -------------------------------------------------------------------------- *)
 
@@ -433,7 +436,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 +481,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 +511,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 +523,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 +546,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 +554,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 +562,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 +582,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 +806,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 1452dbd2167412f603e0adb63c733eea395a07e8..4e2a8e2a992d58fd2da34afbad2e64e56fb9a6bf 100644
--- a/src/Solver.mli
+++ b/src/Solver.mli
@@ -385,41 +385,43 @@ 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
+  type error =
+    | Unbound of tevar
+      (**An instantiation constraint [instance x α]
+         refers to an unbound variable [x]. *)
 
-  (**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
+    | 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. *)
 
-  (**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
+    | 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. *)
 
-  (**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
+    | 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]
@@ -433,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
 
   (**/**)