first attempt: handles only unification errors

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/short-paths@12065 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

10 files changed, 207 insertions, 146 deletions

diff --git a/driver/errors.ml b/driver/errors.ml
index 9400e9ebc5..95380526a7 100644
--- a/driver/errors.ml
+++ b/driver/errors.ml
@@ -39,14 +39,14 @@ let report_error ppf exn =
       fprintf ppf
       "In this program,@ variant constructors@ `%s and `%s@ \
        have the same hash value.@ Change one of them." l l'
-  | Typecore.Error(loc, err) ->
-      Location.print_error ppf loc; Typecore.report_error ppf err
+  | Typecore.Error(loc, env, err) ->
+      Location.print_error ppf loc; Typecore.report_error env ppf err
   | Typetexp.Error(loc, err) ->
       Location.print_error ppf loc; Typetexp.report_error ppf err
   | Typedecl.Error(loc, err) ->
       Location.print_error ppf loc; Typedecl.report_error ppf err
-  | Typeclass.Error(loc, err) ->
-      Location.print_error ppf loc; Typeclass.report_error ppf err
+  | Typeclass.Error(loc, env, err) ->
+      Location.print_error ppf loc; Typeclass.report_error env ppf err
   | Includemod.Error err ->
       Location.print_error_cur_file ppf;
       Includemod.report_error ppf err
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 2b5470ea48..1f3dbe10ea 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -189,6 +189,36 @@ let raw_type_expr ppf t =
 
 let () = Btype.print_raw := raw_type_expr
 
+(* Normalize paths *)
+
+let printing_env = ref Env.empty
+
+let rec path_length = function
+    Pident _ -> 1
+  | Pdot (p, _, _) -> 1 + path_length p
+  | Papply (p1, p2) -> 1 + path_length p1 + path_length p2
+
+let same_type t t' = repr t == repr t'
+
+let rec best_type_path p =
+  try
+    let desc = Env.find_type p !printing_env in
+    if desc.type_private = Private then p else
+    match desc.type_manifest with
+      Some ty ->
+        begin match repr ty with
+          {desc = Tconstr (p1, tyl, _)} ->
+            if List.length desc.type_params = List.length tyl
+            && List.for_all2 same_type desc.type_params tyl then
+              let p' = best_type_path p1 in
+              if path_length p' < path_length p then p' else p
+            else p
+        | _ -> p
+        end
+    | None -> p
+  with
+    Not_found -> p
+
 (* Print a type expression *)
 
 let names = ref ([] : (type_expr * string) list)
@@ -384,7 +414,8 @@ let rec tree_of_typexp sch ty =
     | Ttuple tyl ->
         Otyp_tuple (tree_of_typlist sch tyl)
     | Tconstr(p, tyl, abbrev) ->
-        Otyp_constr (tree_of_path p, tree_of_typlist sch tyl)
+        let p' = best_type_path p in
+        Otyp_constr (tree_of_path p', tree_of_typlist sch tyl)
     | Tvariant row ->
         let row = row_repr row in
         let fields =
@@ -402,7 +433,8 @@ let rec tree_of_typexp sch ty =
         let all_present = List.length present = List.length fields in
         begin match row.row_name with
         | Some(p, tyl) when namable_row row ->
-            let id = tree_of_path p in
+            let p' = best_type_path p in
+            let id = tree_of_path p' in
             let args = tree_of_typlist sch tyl in
             if row.row_closed && all_present then
               Otyp_constr (id, args)
@@ -410,7 +442,7 @@ let rec tree_of_typexp sch ty =
               let non_gen = is_non_gen sch px in
               let tags =
                 if all_present then None else Some (List.map fst present) in
-              Otyp_variant (non_gen, Ovar_name(tree_of_path p, args),
+              Otyp_variant (non_gen, Ovar_name(id, args),
                             row.row_closed, tags)
         | _ ->
             let non_gen =
@@ -491,7 +523,8 @@ and tree_of_typobject sch fi nm =
   | Some (p, ty :: tyl) ->
       let non_gen = is_non_gen sch (repr ty) in
       let args = tree_of_typlist sch tyl in
-      Otyp_class (non_gen, tree_of_path p, args)
+      let p' = best_type_path p in
+      Otyp_class (non_gen, tree_of_path p', args)
   | _ ->
       fatal_error "Printtyp.tree_of_typobject"
   end
@@ -923,8 +956,19 @@ let signature ppf sg =
 
 (* Print an unification error *)
 
+let same_path t t' =
+  let t = repr t and t' = repr t' in
+  t == t' ||
+  match t.desc, t'.desc with
+    Tconstr(p,tl,_), Tconstr(p',tl',_) ->
+      Path.same (best_type_path p) (best_type_path p') &&
+      List.length tl = List.length tl' &&
+      List.for_all2 same_type tl tl'
+  | _ ->
+      false
+
 let type_expansion t ppf t' =
-  if t == t' then type_expr ppf t else
+  if same_path t t' then type_expr ppf t else
   let t' = if proxy t == proxy t' then unalias t' else t' in
   fprintf ppf "@[<2>%a@ =@ %a@]" type_expr t type_expr t'
 
@@ -941,7 +985,7 @@ let rec filter_trace = function
       []
   | (t1, t1') :: (t2, t2') :: rem ->
       let rem' = filter_trace rem in
-      if t1 == t1' && t2 == t2'
+      if same_path t1 t1' && same_path t2 t2'
       then rem'
       else (t1, t1') :: (t2, t2') :: rem'
   | _ -> []
@@ -957,7 +1001,8 @@ let hide_variant_name t =
 
 let prepare_expansion (t, t') =
   let t' = hide_variant_name t' in
-  mark_loops t; if t != t' then mark_loops t';
+  mark_loops t;
+  if not (same_path t t') then mark_loops t';
   (t, t')
 
 let may_prepare_expansion compact (t, t') =
@@ -1068,7 +1113,8 @@ let rec path_same_name p1 p2 =
 
 let type_same_name t1 t2 =
   match (repr t1).desc, (repr t2).desc with
-    Tconstr (p1, _, _), Tconstr (p2, _, _) -> path_same_name p1 p2
+    Tconstr (p1, _, _), Tconstr (p2, _, _) ->
+      path_same_name (best_type_path p1) (best_type_path p2)
   | _ -> ()
 
 let rec trace_same_names = function
@@ -1105,8 +1151,11 @@ let unification_error unif tr txt1 ppf txt2 =
       print_labels := true;
       raise exn
 
-let report_unification_error ppf tr txt1 txt2 =
-  unification_error true tr txt1 ppf txt2;;
+let report_unification_error ppf env tr txt1 txt2 =
+  printing_env := env;
+  unification_error true tr txt1 ppf txt2;
+  printing_env := Env.empty
+;;
 
 let trace fst txt ppf tr =
   print_labels := not !Clflags.classic;
@@ -1121,7 +1170,8 @@ let trace fst txt ppf tr =
     print_labels := true;
     raise exn
 
-let report_subtyping_error ppf tr1 txt1 tr2 =
+let report_subtyping_error ppf env tr1 txt1 tr2 =
+  printing_env := env;
   reset ();
   let tr1 = List.map prepare_expansion tr1
   and tr2 = List.map prepare_expansion tr2 in
@@ -1129,4 +1179,5 @@ let report_subtyping_error ppf tr1 txt1 tr2 =
   if tr2 = [] then () else
   let mis = mismatch true tr2 in
   trace false "is not compatible with type" ppf tr2;
-  explanation true mis ppf
+  explanation true mis ppf;
+  printing_env := Env.empty
diff --git a/typing/printtyp.mli b/typing/printtyp.mli
index 5417ebf41f..3336578d88 100644
--- a/typing/printtyp.mli
+++ b/typing/printtyp.mli
@@ -60,9 +60,9 @@ val unification_error:
     (formatter -> unit) -> formatter -> (formatter -> unit) ->
     unit
 val report_unification_error:
-    formatter -> (type_expr * type_expr) list ->
+    formatter -> Env.t -> (type_expr * type_expr) list ->
     (formatter -> unit) -> (formatter -> unit) ->
     unit
 val report_subtyping_error:
-    formatter -> (type_expr * type_expr) list ->
+    formatter -> Env.t -> (type_expr * type_expr) list ->
     string -> (type_expr * type_expr) list -> unit
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 512f7cf8b2..fd85fbfaec 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -50,7 +50,7 @@ type error =
   | Mutability_mismatch of string * mutable_flag
   | No_overriding of string * string
 
-exception Error of Location.t * error
+exception Error of Location.t * Env.t * error
 
 
                        (**********************)
@@ -206,13 +206,15 @@ let enter_val cl_num vars inh lab mut virt ty val_env met_env par_env loc =
   let (id, virt) =
     try
       let (id, mut', virt', ty') = Vars.find lab !vars in
-      if mut' <> mut then raise (Error(loc, Mutability_mismatch(lab, mut)));
+      if mut' <> mut then
+        raise (Error(loc, val_env, Mutability_mismatch(lab, mut)));
       Ctype.unify val_env (instance ty) (instance ty');
       (if not inh then Some id else None),
       (if virt' = Concrete then virt' else virt)
     with
       Ctype.Unify tr ->
-        raise (Error(loc, Field_type_mismatch("instance variable", lab, tr)))
+        raise (Error(loc, val_env,
+                     Field_type_mismatch("instance variable", lab, tr)))
     | Not_found -> None, virt
   in
   let (id, _, _, _) as result =
@@ -238,7 +240,7 @@ let inheritance self_type env ovf concr_meths warn_vals loc parent =
       with Ctype.Unify trace ->
         match trace with
           _::_::_::({desc = Tfield(n, _, _, _)}, _)::rem ->
-            raise(Error(loc, Field_type_mismatch ("method", n, rem)))
+            raise(Error(loc, env, Field_type_mismatch ("method", n, rem)))
         | _ ->
             assert false
       end;
@@ -263,7 +265,7 @@ let inheritance self_type env ovf concr_meths warn_vals loc parent =
                  (cname :: Concr.elements over_vals));
       | Some Override
         when Concr.is_empty over_meths && Concr.is_empty over_vals ->
-        raise (Error(loc, No_overriding ("","")))
+        raise (Error(loc, env, No_overriding ("","")))
       | _ -> ()
       end;
 
@@ -273,7 +275,7 @@ let inheritance self_type env ovf concr_meths warn_vals loc parent =
       (cl_sig, concr_meths, warn_vals)
 
   | _ ->
-      raise(Error(loc, Structure_expected parent))
+      raise(Error(loc, env, Structure_expected parent))
 
 let virtual_method val_env meths self_type lab priv sty loc =
   let (_, ty') =
@@ -281,7 +283,7 @@ let virtual_method val_env meths self_type lab priv sty loc =
   in
   let ty = transl_simple_type val_env false sty in
   try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
-    raise(Error(loc, Field_type_mismatch ("method", lab, trace)))
+    raise(Error(loc, val_env, Field_type_mismatch ("method", lab, trace)))
 
 let delayed_meth_specs = ref []
 
@@ -291,7 +293,7 @@ let declare_method val_env meths self_type lab priv sty loc =
   in
   let unif ty =
     try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
-      raise(Error(loc, Field_type_mismatch ("method", lab, trace)))
+      raise(Error(loc, val_env, Field_type_mismatch ("method", lab, trace)))
   in
   match sty.ptyp_desc, priv with
     Ptyp_poly ([],sty), Public ->
@@ -304,7 +306,7 @@ let type_constraint val_env sty sty' loc =
   let ty  = transl_simple_type val_env false sty in
   let ty' = transl_simple_type val_env false sty' in
   try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
-    raise(Error(loc, Unconsistent_constraint trace))
+    raise(Error(loc, val_env, Unconsistent_constraint trace))
 
 let mkpat d = { ppat_desc = d; ppat_loc = Location.none }
 let make_method cl_num expr =
@@ -371,7 +373,7 @@ and class_signature env sty sign =
   begin try
     Ctype.unify env self_type dummy_obj
   with Ctype.Unify _ ->
-    raise(Error(sty.ptyp_loc, Pattern_type_clash self_type))
+    raise(Error(sty.ptyp_loc, env, Pattern_type_clash self_type))
   end;
 
   (* Class type fields *)
@@ -391,19 +393,19 @@ and class_type env scty =
     Pcty_constr (lid, styl) ->
       let (path, decl) = Typetexp.find_cltype env scty.pcty_loc lid in
       if Path.same decl.clty_path unbound_class then
-        raise(Error(scty.pcty_loc, Unbound_class_type_2 lid));
+        raise(Error(scty.pcty_loc, env, Unbound_class_type_2 lid));
       let (params, clty) =
         Ctype.instance_class decl.clty_params decl.clty_type
       in
       if List.length params <> List.length styl then
-        raise(Error(scty.pcty_loc,
+        raise(Error(scty.pcty_loc, env,
                     Parameter_arity_mismatch (lid, List.length params,
                                                    List.length styl)));
       List.iter2
         (fun sty ty ->
            let ty' = transl_simple_type env false sty in
            try Ctype.unify env ty' ty with Ctype.Unify trace ->
-             raise(Error(sty.ptyp_loc, Parameter_mismatch trace)))
+             raise(Error(sty.ptyp_loc, env, Parameter_mismatch trace)))
         styl params;
       Tcty_constr (path, params, clty)
 
@@ -493,12 +495,12 @@ let rec class_field cl_num self_type meths vars
           Location.prerr_warning loc (Warnings.Instance_variable_override[lab])
       end else begin
         if ovf = Override then
-          raise(Error(loc, No_overriding ("instance variable", lab)))
+          raise(Error(loc, val_env, No_overriding ("instance variable", lab)))
       end;
       if !Clflags.principal then Ctype.begin_def ();
       let exp =
         try type_exp val_env sexp with Ctype.Unify [(ty, _)] ->
-          raise(Error(loc, Make_nongen_seltype ty))
+          raise(Error(loc, val_env, Make_nongen_seltype ty))
       in
       if !Clflags.principal then begin
         Ctype.end_def ();
@@ -521,7 +523,8 @@ let rec class_field cl_num self_type meths vars
         if ovf = Fresh then
           Location.prerr_warning loc (Warnings.Method_override [lab])
       end else begin
-        if ovf = Override then raise(Error(loc, No_overriding("method", lab)))
+        if ovf = Override then
+          raise(Error(loc, val_env, No_overriding("method", lab)))
       end;
       let (_, ty) =
         Ctype.filter_self_method val_env lab priv meths self_type
@@ -546,7 +549,7 @@ let rec class_field cl_num self_type meths vars
           end
       | _ -> assert false
       with Ctype.Unify trace ->
-        raise(Error(loc, Field_type_mismatch ("method", lab, trace)))
+        raise(Error(loc, val_env, Field_type_mismatch ("method", lab, trace)))
       end;
       let meth_expr = make_method cl_num expr in
       (* backup variables for Pexp_override *)
@@ -611,7 +614,7 @@ and class_structure cl_num final val_env met_env loc (spat, str) =
     else self_type in
   begin try Ctype.unify val_env public_self ty with
     Ctype.Unify _ ->
-      raise(Error(spat.ppat_loc, Pattern_type_clash public_self))
+      raise(Error(spat.ppat_loc, val_env, Pattern_type_clash public_self))
   end;
   let get_methods ty =
     (fst (Ctype.flatten_fields
@@ -654,7 +657,7 @@ and class_structure cl_num final val_env met_env loc (spat, str) =
         (fun name (mut, vr, ty) l -> if vr = Virtual then name :: l else l)
         sign.cty_vars [] in
     if mets <> [] || vals <> [] then
-      raise(Error(loc, Virtual_class(true, mets, vals)));
+      raise(Error(loc, val_env, Virtual_class(true, mets, vals)));
     let self_methods =
       List.fold_right
         (fun (lab,kind,ty) rem ->
@@ -670,7 +673,7 @@ and class_structure cl_num final val_env met_env loc (spat, str) =
       Ctype.unify val_env private_self
         (Ctype.newty (Tobject(self_methods, ref None)));
       Ctype.unify val_env public_self self_type
-    with Ctype.Unify trace -> raise(Error(loc, Final_self_clash trace))
+    with Ctype.Unify trace -> raise(Error(loc, val_env, Final_self_clash trace))
     end;
   end;
 
@@ -701,7 +704,7 @@ and class_expr cl_num val_env met_env scl =
     Pcl_constr (lid, styl) ->
       let (path, decl) = Typetexp.find_class val_env scl.pcl_loc lid in
       if Path.same decl.cty_path unbound_class then
-        raise(Error(scl.pcl_loc, Unbound_class_2 lid));
+        raise(Error(scl.pcl_loc, val_env, Unbound_class_2 lid));
       let tyl = List.map
           (fun sty -> transl_simple_type val_env false sty, sty.ptyp_loc)
           styl
@@ -711,13 +714,13 @@ and class_expr cl_num val_env met_env scl =
       in
       let clty' = abbreviate_class_type path params clty in
       if List.length params <> List.length tyl then
-        raise(Error(scl.pcl_loc,
+        raise(Error(scl.pcl_loc, val_env,
                     Parameter_arity_mismatch (lid, List.length params,
                                                    List.length tyl)));
       List.iter2
         (fun (ty',loc) ty ->
            try Ctype.unify val_env ty' ty with Ctype.Unify trace ->
-             raise(Error(loc, Parameter_mismatch trace)))
+             raise(Error(loc, val_env, Parameter_mismatch trace)))
         tyl params;
       let cl =
         rc {cl_desc = Tclass_ident path;
@@ -838,10 +841,11 @@ and class_expr cl_num val_env met_env scl =
               if ignore_labels && not (Btype.is_optional l) then begin
                 match sargs, more_sargs with
                   (l', sarg0)::_, _ ->
-                    raise(Error(sarg0.pexp_loc, Apply_wrong_label(l')))
+                    raise(Error(sarg0.pexp_loc, val_env, Apply_wrong_label l'))
                 | _, (l', sarg0)::more_sargs ->
                     if l <> l' && l' <> "" then
-                      raise(Error(sarg0.pexp_loc, Apply_wrong_label l'))
+                      raise(Error(sarg0.pexp_loc, val_env,
+                                  Apply_wrong_label l'))
                     else ([], more_sargs,
                           Some (type_argument val_env sarg0 ty ty))
                 | _ ->
@@ -878,9 +882,9 @@ and class_expr cl_num val_env met_env scl =
             match sargs @ more_sargs with
               (l, sarg0)::_ ->
                 if omitted <> [] then
-                  raise(Error(sarg0.pexp_loc, Apply_wrong_label l))
+                  raise(Error(sarg0.pexp_loc, val_env, Apply_wrong_label l))
                 else
-                  raise(Error(cl.cl_loc, Cannot_apply cl.cl_type))
+                  raise(Error(cl.cl_loc, val_env, Cannot_apply cl.cl_type))
             | [] ->
                 (List.rev args,
                  List.fold_left
@@ -902,7 +906,7 @@ and class_expr cl_num val_env met_env scl =
         try
           Typecore.type_let val_env rec_flag sdefs None
         with Ctype.Unify [(ty, _)] ->
-          raise(Error(scl.pcl_loc, Make_nongen_seltype ty))
+          raise(Error(scl.pcl_loc, val_env, Make_nongen_seltype ty))
       in
       let (vals, met_env) =
         List.fold_right
@@ -954,7 +958,7 @@ and class_expr cl_num val_env met_env scl =
 
       begin match Includeclass.class_types val_env cl.cl_type clty with
         []    -> ()
-      | error -> raise(Error(cl.cl_loc, Class_match_failure error))
+      | error -> raise(Error(cl.cl_loc, val_env, Class_match_failure error))
       end;
       let (vals, meths, concrs) = extract_constraints clty in
       rc {cl_desc = Tclass_constraint (cl, vals, meths, concrs);
@@ -1074,7 +1078,7 @@ let class_infos define_class kind
       let params, loc = cl.pci_params in
       List.map (enter_type_variable true loc) params
     with Already_bound ->
-      raise(Error(snd cl.pci_params, Repeated_parameter))
+      raise(Error(snd cl.pci_params, env, Repeated_parameter))
   in
 
   (* Allow self coercions (only for class declarations) *)
@@ -1112,7 +1116,7 @@ let class_infos define_class kind
     begin try
       List.iter2 (Ctype.unify env) obj_params obj_params'
     with Ctype.Unify _ ->
-      raise(Error(cl.pci_loc,
+      raise(Error(cl.pci_loc, env,
             Bad_parameters (obj_id, constr,
                             Ctype.newconstr (Path.Pident obj_id)
                                             obj_params')))
@@ -1120,7 +1124,7 @@ let class_infos define_class kind
     begin try
       Ctype.unify env ty constr
     with Ctype.Unify _ ->
-      raise(Error(cl.pci_loc,
+      raise(Error(cl.pci_loc, env,
         Abbrev_type_clash (constr, ty, Ctype.expand_head env constr)))
     end
   end;
@@ -1134,7 +1138,7 @@ let class_infos define_class kind
     begin try
       List.iter2 (Ctype.unify env) cl_params cl_params'
     with Ctype.Unify _ ->
-      raise(Error(cl.pci_loc,
+      raise(Error(cl.pci_loc, env,
             Bad_parameters (cl_id,
                             Ctype.newconstr (Path.Pident cl_id)
                                             cl_params,
@@ -1145,7 +1149,7 @@ let class_infos define_class kind
       Ctype.unify env ty cl_ty
     with Ctype.Unify _ ->
       let constr = Ctype.newconstr (Path.Pident cl_id) params in
-      raise(Error(cl.pci_loc, Abbrev_type_clash (constr, ty, cl_ty)))
+      raise(Error(cl.pci_loc, env, Abbrev_type_clash (constr, ty, cl_ty)))
     end
   end;
 
@@ -1155,7 +1159,7 @@ let class_infos define_class kind
       (constructor_type constr obj_type)
       (Ctype.instance env constr_type)
   with Ctype.Unify trace ->
-    raise(Error(cl.pci_loc,
+    raise(Error(cl.pci_loc, env,
                 Constructor_type_mismatch (cl.pci_name, trace)))
   end;
 
@@ -1188,7 +1192,7 @@ let class_infos define_class kind
         (fun name (mut, vr, ty) l -> if vr = Virtual then name :: l else l)
         sign.cty_vars [] in
     if mets <> []  || vals <> [] then
-      raise(Error(cl.pci_loc, Virtual_class(true, mets, vals)));
+      raise(Error(cl.pci_loc, env, Virtual_class(true, mets, vals)));
   end;
 
   (* Misc. *)
@@ -1250,7 +1254,7 @@ let final_decl env define_class
 
   begin try Ctype.collapse_conj_params env clty.cty_params
   with Ctype.Unify trace ->
-    raise(Error(cl.pci_loc, Non_collapsable_conjunction (id, clty, trace)))
+    raise(Error(cl.pci_loc, env, Non_collapsable_conjunction (id, clty, trace)))
   end;
 
   List.iter Ctype.generalize clty.cty_params;
@@ -1271,7 +1275,7 @@ let final_decl env define_class
   end;
 
   if not (closed_class clty) then
-    raise(Error(cl.pci_loc, Non_generalizable_class (id, clty)));
+    raise(Error(cl.pci_loc, env, Non_generalizable_class (id, clty)));
 
   begin match
     Ctype.closed_class clty.cty_params
@@ -1284,7 +1288,7 @@ let final_decl env define_class
         then function ppf -> Printtyp.class_declaration id ppf clty
         else function ppf -> Printtyp.cltype_declaration id ppf cltydef
       in
-      raise(Error(cl.pci_loc, Unbound_type_var(printer, reason)))
+      raise(Error(cl.pci_loc, env, Unbound_type_var(printer, reason)))
   end;
 
   (id, clty, ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr,
@@ -1332,10 +1336,10 @@ let check_coercions env
       in
       begin try Ctype.subtype env cl_ty obj_ty ()
       with Ctype.Subtype (tr1, tr2) ->
-        raise(Typecore.Error(loc, Typecore.Not_subtype(tr1, tr2)))
+        raise(Typecore.Error(loc, env, Typecore.Not_subtype(tr1, tr2)))
       end;
       if not (Ctype.opened_object cl_ty) then
-        raise(Error(loc, Cannot_coerce_self obj_ty))
+        raise(Error(loc, env, Cannot_coerce_self obj_ty))
   end;
   (id, clty, ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr,
    arity, pub_meths, expr)
@@ -1449,16 +1453,16 @@ let approx_class_declarations env sdecls =
 
 open Format
 
-let report_error ppf = function
+let report_error env ppf = function
   | Repeated_parameter ->
       fprintf ppf "A type parameter occurs several times"
   | Unconsistent_constraint trace ->
       fprintf ppf "The class constraints are not consistent.@.";
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (fun ppf -> fprintf ppf "Type")
         (fun ppf -> fprintf ppf "is not compatible with type")
   | Field_type_mismatch (k, m, trace) ->
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "The %s %s@ has type" k m)
         (function ppf ->
@@ -1497,7 +1501,7 @@ let report_error ppf = function
        Printtyp.type_expr actual
        Printtyp.type_expr expected
   | Constructor_type_mismatch (c, trace) ->
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "The expression \"new %s\" has type" c)
         (function ppf ->
@@ -1522,7 +1526,7 @@ let report_error ppf = function
            but is here applied to %i type argument(s)@]"
         Printtyp.longident lid expected provided
   | Parameter_mismatch trace ->
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "The type parameter")
         (function ppf ->
@@ -1579,11 +1583,11 @@ let report_error ppf = function
         "@[The type of this class,@ %a,@ \
            contains non-collapsible conjunctive types in constraints@]"
         (Printtyp.class_declaration id) clty;
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (fun ppf -> fprintf ppf "Type")
         (fun ppf -> fprintf ppf "is not compatible with type")
   | Final_self_clash trace ->
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "This object is expected to have type")
         (function ppf ->
diff --git a/typing/typeclass.mli b/typing/typeclass.mli
index 9841ed4010..b898284a80 100644
--- a/typing/typeclass.mli
+++ b/typing/typeclass.mli
@@ -75,6 +75,6 @@ type error =
   | Mutability_mismatch of string * mutable_flag
   | No_overriding of string * string
 
-exception Error of Location.t * error
+exception Error of Location.t * Env.t * error
 
-val report_error : formatter -> error -> unit
+val report_error : Env.t -> formatter -> error -> unit
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 88401efe44..401f7f79c2 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -62,7 +62,7 @@ type error =
   | Recursive_local_constraint of (type_expr * type_expr) list
   | Unexpected_existential
 
-exception Error of Location.t * error
+exception Error of Location.t * Env.t * error
 
 (* Forward declaration, to be filled in by Typemod.type_module *)
 
@@ -255,7 +255,7 @@ let unify_pat_types loc env ty ty' =
     unify env ty ty'
   with
     Unify trace ->
-      raise(Error(loc, Pattern_type_clash(trace)))
+      raise(Error(loc, env, Pattern_type_clash(trace)))
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
 
@@ -267,7 +267,7 @@ let unify_exp_types loc env ty expected_ty =
     unify env ty expected_ty
   with
     Unify trace ->
-      raise(Error(loc, Expr_type_clash(trace)))
+      raise(Error(loc, env, Expr_type_clash(trace)))
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
 
@@ -288,11 +288,11 @@ let unify_pat_types_gadt loc env ty ty' =
     unify_gadt ~newtype_level env ty ty'
   with
     Unify trace ->
-      raise(Error(loc, Pattern_type_clash(trace)))
+      raise(Error(loc, !env, Pattern_type_clash(trace)))
   | Tags(l1,l2) ->
       raise(Typetexp.Error(loc, Typetexp.Variant_tags (l1, l2)))
   | Unification_recursive_abbrev trace ->
-      raise(Error(loc, Recursive_local_constraint trace))
+      raise(Error(loc, !env, Recursive_local_constraint trace))
 
 
 (* Creating new conjunctive types is not allowed when typing patterns *)
@@ -356,12 +356,13 @@ let reset_pattern scope allow =
 
 let enter_variable ?(is_module=false) ?(is_as_variable=false) loc name ty =
   if List.exists (fun (id, _, _, _) -> Ident.name id = name) !pattern_variables
-  then raise(Error(loc, Multiply_bound_variable name));
+  then raise(Error(loc, Env.empty, Multiply_bound_variable name));
   let id = Ident.create name in
   pattern_variables := (id, ty, loc, is_as_variable) :: !pattern_variables;
   if is_module then begin
     (* Note: unpack patterns enter a variable of the same name *)
-    if not !allow_modules then raise (Error (loc, Modules_not_allowed));
+    if not !allow_modules then
+      raise (Error (loc, Env.empty, Modules_not_allowed));
     module_variables := (name, loc) :: !module_variables
   end else begin
     match !pattern_scope with
@@ -390,18 +391,18 @@ let enter_orpat_variables loc env  p1_vs p2_vs =
               unify env t1 t2
             with
             | Unify trace ->
-                raise(Error(loc, Pattern_type_clash(trace)))
+                raise(Error(loc, env, Pattern_type_clash(trace)))
             end;
           (x2,x1)::unify_vars rem1 rem2
           end
       | [],[] -> []
-      | (x,_,_,_)::_, [] -> raise (Error (loc, Orpat_vars x))
-      | [],(x,_,_,_)::_  -> raise (Error (loc, Orpat_vars x))
+      | (x,_,_,_)::_, [] -> raise (Error (loc, env, Orpat_vars x))
+      | [],(x,_,_,_)::_  -> raise (Error (loc, env, Orpat_vars x))
       | (x,_,_,_)::_, (y,_,_,_)::_ ->
           let min_var =
             if Ident.name x < Ident.name y then x
             else y in
-          raise (Error (loc, Orpat_vars min_var)) in
+          raise (Error (loc, env, Orpat_vars min_var)) in
   unify_vars p1_vs p2_vs
 
 let rec build_as_type env p =
@@ -465,7 +466,7 @@ let build_or_pat env loc lid =
     let ty = expand_head env (newty(Tconstr(path, tyl, ref Mnil))) in
     match ty.desc with
       Tvariant row when static_row row -> row
-    | _ -> raise(Error(loc, Not_a_variant_type lid))
+    | _ -> raise(Error(loc, env, Not_a_variant_type lid))
   in
   let pats, fields =
     List.fold_left
@@ -494,7 +495,7 @@ let build_or_pat env loc lid =
       pats
   in
   match pats with
-    [] -> raise(Error(loc, Not_a_variant_type lid))
+    [] -> raise(Error(loc, env, Not_a_variant_type lid))
   | pat :: pats ->
       let r =
         List.fold_left
@@ -548,7 +549,7 @@ let check_recordpat_labels loc lbl_pat_list closed =
       let defined = Array.make (Array.length all) false in
       let check_defined (label, _) =
         if defined.(label.lbl_pos)
-        then raise(Error(loc, Label_multiply_defined
+        then raise(Error(loc, Env.empty, Label_multiply_defined
                                        (Longident.Lident label.lbl_name)))
         else defined.(label.lbl_pos) <- true in
       List.iter check_defined lbl_pat_list;
@@ -667,7 +668,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
         | _ ->  Typetexp.find_constructor !env loc lid
       in
       if no_existentials && constr.cstr_existentials <> [] then
-        raise (Error (loc, Unexpected_existential));
+        raise (Error (loc, !env, Unexpected_existential));
       (* if constructor is gadt, we must verify that the expected type has the
          correct head *)
       if constr.cstr_generalized then
@@ -684,7 +685,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
             replicate_list sp constr.cstr_arity
         | Some sp -> [sp] in
       if List.length sargs <> constr.cstr_arity then
-        raise(Error(loc, Constructor_arity_mismatch(lid,
+        raise(Error(loc, !env, Constructor_arity_mismatch(lid,
                                      constr.cstr_arity, List.length sargs)));
       let (ty_args, ty_res) =
         instance_constructor ~in_pattern:(env, get_newtype_level ()) constr
@@ -723,7 +724,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
         begin try
           unify_pat_types loc !env ty_res expected_ty
         with Unify trace ->
-          raise(Error(loc, Label_mismatch(lid_of_label label, trace)))
+          raise(Error(loc, !env, Label_mismatch(lid_of_label label, trace)))
         end;
         let arg = type_pat sarg ty_arg in
         if vars <> [] then begin
@@ -734,7 +735,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty =
             let tv = expand_head !env tv in
             not (is_Tvar tv) || tv.level <> generic_level in
           if List.exists instantiated vars then
-            raise (Error(loc, Polymorphic_label (lid_of_label label)))
+            raise (Error(loc, !env, Polymorphic_label (lid_of_label label)))
         end;
         (label, arg)
       in
@@ -1021,9 +1022,9 @@ let type_format loc fmt =
   let ty_arrow gty ty = newty (Tarrow ("", instance_def gty, ty, Cok)) in
 
   let bad_conversion fmt i c =
-    raise (Error (loc, Bad_conversion (fmt, i, c))) in
+    raise (Error (loc, Env.empty, Bad_conversion (fmt, i, c))) in
   let incomplete_format fmt =
-    raise (Error (loc, Incomplete_format fmt)) in
+    raise (Error (loc, Env.empty, Incomplete_format fmt)) in
 
   let rec type_in_format fmt =
 
@@ -1251,7 +1252,7 @@ let rec type_approx env sexp =
       and ty1 = approx_ty_opt sty1
       and ty2 = approx_ty_opt sty2 in
       begin try unify env ty ty1 with Unify trace ->
-        raise(Error(sexp.pexp_loc, Expr_type_clash trace))
+        raise(Error(sexp.pexp_loc, env, Expr_type_clash trace))
       end;
       if sty2 = None then ty1 else ty2
   | _ -> newvar ()
@@ -1289,7 +1290,7 @@ let check_univars env expans kind exp ty_expected vars =
   if List.length vars = List.length vars' then () else
   let ty = newgenty (Tpoly(repr exp.exp_type, vars'))
   and ty_expected = repr ty_expected in
-  raise (Error (exp.exp_loc,
+  raise (Error (exp.exp_loc, env,
                 Less_general(kind, [ty, ty; ty_expected, ty_expected])))
 
 (* Check that a type is not a function *)
@@ -1441,7 +1442,7 @@ and type_expect ?in_function env sexp ty_expected =
                 in
                 Texp_ident(path, desc)
             | Val_unbound ->
-                raise(Error(loc, Masked_instance_variable lid))
+                raise(Error(loc, env, Masked_instance_variable lid))
             | _ ->
                 Texp_ident(path, desc)
             end;
@@ -1539,9 +1540,9 @@ and type_expect ?in_function env sexp ty_expected =
         with Unify _ ->
           match expand_head env ty_expected with
             {desc = Tarrow _} as ty ->
-              raise(Error(loc, Abstract_wrong_label(l, ty)))
+              raise(Error(loc, env, Abstract_wrong_label(l, ty)))
           | _ ->
-              raise(Error(loc_fun,
+              raise(Error(loc_fun, env,
                           Too_many_arguments (in_function <> None, ty_fun)))
       in
       let ty_arg =
@@ -1681,7 +1682,7 @@ and type_expect ?in_function env sexp ty_expected =
         match (lid_sexp, lbl_exp) with
           ((lid, _) :: rem1, (lbl, _) :: rem2) ->
             if List.mem lbl.lbl_pos seen_pos
-            then raise(Error(loc, Label_multiply_defined lid))
+            then raise(Error(loc, env, Label_multiply_defined lid))
             else check_duplicates (lbl.lbl_pos :: seen_pos) rem1 rem2
         | (_, _) -> () in
       check_duplicates [] lid_sexp_list lbl_exp_list;
@@ -1723,7 +1724,7 @@ and type_expect ?in_function env sexp ty_expected =
               else lbl :: missing_labels (n + 1) rem
         in
         let missing = missing_labels 0 label_names in
-        raise(Error(loc, Label_missing missing))
+        raise(Error(loc, env, Label_missing missing))
       end
       else if opt_sexp <> None && List.length lid_sexp_list = num_fields then
         Location.prerr_warning loc Warnings.Useless_record_with;
@@ -1748,7 +1749,7 @@ and type_expect ?in_function env sexp ty_expected =
       let (label, newval) =
         type_label_exp false env loc record.exp_type (label, snewval) in
       if label.lbl_mut = Immutable then
-        raise(Error(loc, Label_not_mutable lid));
+        raise(Error(loc, env, Label_not_mutable lid));
       rue {
         exp_desc = Texp_setfield(record, label, newval);
         exp_loc = loc;
@@ -1872,13 +1873,13 @@ and type_expect ?in_function env sexp ty_expected =
                       (Warnings.Not_principal "this ground coercion");
                 with Subtype (tr1, tr2) ->
                   (* prerr_endline "coercion failed"; *)
-                  raise(Error(loc, Not_subtype(tr1, tr2)))
+                  raise(Error(loc, env, Not_subtype(tr1, tr2)))
                 end;
             | _ ->
                 let ty, b = enlarge_type env ty' in
                 force ();
                 begin try Ctype.unify env arg.exp_type ty with Unify trace ->
-                  raise(Error(sarg.pexp_loc,
+                  raise(Error(sarg.pexp_loc, env,
                         Coercion_failure(ty', full_expand env ty', trace, b)))
                 end
             end;
@@ -1894,7 +1895,7 @@ and type_expect ?in_function env sexp ty_expected =
               let force'' = subtype env ty ty' in
               force (); force' (); force'' ()
             with Subtype (tr1, tr2) ->
-              raise(Error(loc, Not_subtype(tr1, tr2)))
+              raise(Error(loc, env, Not_subtype(tr1, tr2)))
             end;
             if separate then begin
               end_def ();
@@ -1934,7 +1935,7 @@ and type_expect ?in_function env sexp ty_expected =
           | Texp_ident(path, {val_kind = Val_anc (methods, cl_num)}) ->
               let method_id =
                 begin try List.assoc met methods with Not_found ->
-                  raise(Error(e.pexp_loc, Undefined_inherited_method met))
+                  raise(Error(e.pexp_loc, env, Undefined_inherited_method met))
                 end
               in
               begin match
@@ -1999,13 +2000,13 @@ and type_expect ?in_function env sexp ty_expected =
           exp_type = typ;
           exp_env = env }
       with Unify _ ->
-        raise(Error(e.pexp_loc, Undefined_method (obj.exp_type, met)))
+        raise(Error(e.pexp_loc, env, Undefined_method (obj.exp_type, met)))
       end
   | Pexp_new cl ->
       let (cl_path, cl_decl) = Typetexp.find_class env loc cl in
         begin match cl_decl.cty_new with
           None ->
-            raise(Error(loc, Virtual_class cl))
+            raise(Error(loc, env, Virtual_class cl))
         | Some ty ->
             rue {
               exp_desc = Texp_new (cl_path, cl_decl);
@@ -2028,19 +2029,19 @@ and type_expect ?in_function env sexp ty_expected =
               exp_type = instance_def Predef.type_unit;
               exp_env = env }
         | Val_ivar _ ->
-            raise(Error(loc,Instance_variable_not_mutable(true,lab)))
+            raise(Error(loc, env, Instance_variable_not_mutable(true,lab)))
         | _ ->
-            raise(Error(loc,Instance_variable_not_mutable(false,lab)))
+            raise(Error(loc, env, Instance_variable_not_mutable(false,lab)))
       with
         Not_found ->
-          raise(Error(loc, Unbound_instance_variable lab))
+          raise(Error(loc, env, Unbound_instance_variable lab))
       end
   | Pexp_override lst ->
       let _ =
        List.fold_right
         (fun (lab, _) l ->
            if List.exists ((=) lab) l then
-             raise(Error(loc,
+             raise(Error(loc, env,
                          Value_multiply_overridden lab));
            lab::l)
         lst
@@ -2050,7 +2051,7 @@ and type_expect ?in_function env sexp ty_expected =
           Env.lookup_value (Longident.Lident "selfpat-*") env,
           Env.lookup_value (Longident.Lident "self-*") env
         with Not_found ->
-          raise(Error(loc, Outside_class))
+          raise(Error(loc, env, Outside_class))
       with
         (_, {val_type = self_ty; val_kind = Val_self (_, vars, _, _)}),
         (path_self, _) ->
@@ -2060,7 +2061,7 @@ and type_expect ?in_function env sexp ty_expected =
               (Path.Pident id, type_expect env snewval (instance env ty))
             with
               Not_found ->
-                raise(Error(loc, Unbound_instance_variable lab))
+                raise(Error(loc, env, Unbound_instance_variable lab))
             end
           in
           let modifs = List.map type_override lst in
@@ -2093,7 +2094,7 @@ and type_expect ?in_function env sexp ty_expected =
       begin try
         Ctype.unify_var new_env ty body.exp_type
       with Unify _ ->
-        raise(Error(loc, Scoping_let_module(name, body.exp_type)))
+        raise(Error(loc, env, Scoping_let_module(name, body.exp_type)))
       end;
       re {
         exp_desc = Texp_letmodule(id, modl, body);
@@ -2228,9 +2229,9 @@ and type_expect ?in_function env sexp ty_expected =
                 (Warnings.Not_principal "this module packing");
             (p, nl, tl)
         | {desc = Tvar _} ->
-            raise (Error (loc, Cannot_infer_signature))
+            raise (Error (loc, env, Cannot_infer_signature))
         | _ ->
-            raise (Error (loc, Not_a_packed_module ty_expected))
+            raise (Error (loc, env, Not_a_packed_module ty_expected))
       in
       let (modl, tl') = !type_package env m p nl tl in
       rue {
@@ -2256,7 +2257,7 @@ and type_label_exp create env loc ty_expected (label, sarg) =
   begin try
     unify env (instance_def ty_res) (instance env ty_expected)
   with Unify trace ->
-    raise(Error(loc , Label_mismatch(lid_of_label label, trace)))
+    raise(Error(loc , env, Label_mismatch(lid_of_label label, trace)))
   end;
   (* Instantiate so that we can generalize internal nodes *)
   let ty_arg = instance_def ty_arg in
@@ -2266,8 +2267,9 @@ and type_label_exp create env loc ty_expected (label, sarg) =
     generalize_structure ty_arg
   end;
   if label.lbl_private = Private then
-    raise(Error(loc, if create then Private_type ty_expected
-                     else Private_label (lid_of_label label, ty_expected)));
+    raise(Error(loc, env,
+                if create then Private_type ty_expected
+                else Private_label (lid_of_label label, ty_expected)));
   let arg =
     let snap = if vars = [] then None else Some (Btype.snapshot ()) in
     let arg = type_argument env sarg ty_arg (instance env ty_arg) in
@@ -2285,7 +2287,7 @@ and type_label_exp create env loc ty_expected (label, sarg) =
       unify_exp env arg ty_arg;
       check_univars env false "field value" arg label.lbl_arg vars;
       arg
-    with Error (_, Less_general _) as e -> raise e
+    with Error (_, _, Less_general _) as e -> raise e
     | _ -> raise exn    (* In case of failure return the first error *)
   in
   (label, {arg with exp_type = instance env arg.exp_type})
@@ -2404,11 +2406,12 @@ and type_application env funct sargs =
               match ty_res.desc with
                 Tarrow _ ->
                   if (!Clflags.classic || not (has_label l1 ty_fun)) then
-                    raise(Error(sarg1.pexp_loc, Apply_wrong_label(l1, ty_res)))
+                    raise (Error(sarg1.pexp_loc, env,
+                                 Apply_wrong_label(l1, ty_res)))
                   else
-                    raise(Error(funct.exp_loc, Incoherent_label_order))
+                    raise (Error(funct.exp_loc, env, Incoherent_label_order))
               | _ ->
-                  raise(Error(funct.exp_loc, Apply_non_function
+                  raise(Error(funct.exp_loc, env, Apply_non_function
                                 (expand_head env funct.exp_type)))
         in
         let optional = if is_optional l1 then Optional else Required in
@@ -2453,10 +2456,12 @@ and type_application env funct sargs =
             (* In classic mode, omitted = [] *)
             match sargs, more_sargs with
               (l', sarg0) :: _, _ ->
-                raise(Error(sarg0.pexp_loc, Apply_wrong_label(l', ty_old)))
+                raise(Error(sarg0.pexp_loc, env,
+                            Apply_wrong_label(l', ty_old)))
             | _, (l', sarg0) :: more_sargs ->
                 if l <> l' && l' <> "" then
-                  raise(Error(sarg0.pexp_loc, Apply_wrong_label(l', ty_fun')))
+                  raise(Error(sarg0.pexp_loc, env,
+                              Apply_wrong_label(l', ty_fun')))
                 else
                   ([], more_sargs,
                    Some (fun () -> type_argument env sarg0 ty ty0))
@@ -2511,7 +2516,8 @@ and type_application env funct sargs =
     | _ ->
         match sargs with
           (l, sarg0) :: _ when ignore_labels ->
-            raise(Error(sarg0.pexp_loc, Apply_wrong_label(l, ty_old)))
+            raise(Error(sarg0.pexp_loc, env,
+                        Apply_wrong_label(l, ty_old)))
         | _ ->
             type_unknown_args args omitted ty_fun0
               (sargs @ more_sargs)
@@ -2547,7 +2553,7 @@ and type_construct env loc lid sarg explicit_arity ty_expected =
     | Some {pexp_desc = Pexp_tuple sel} when constr.cstr_arity > 1 -> sel
     | Some se -> [se] in
   if List.length sargs <> constr.cstr_arity then
-    raise(Error(loc, Constructor_arity_mismatch
+    raise(Error(loc, env, Constructor_arity_mismatch
                   (lid, constr.cstr_arity, List.length sargs)));
   let separate = !Clflags.principal || Env.has_local_constraints env in
   if separate then (begin_def (); begin_def ());
@@ -2577,7 +2583,7 @@ and type_construct env loc lid sarg explicit_arity ty_expected =
   let args = List.map2 (fun e (t,t0) -> type_argument env e t t0) sargs
       (List.combine ty_args ty_args0) in
   if constr.cstr_private = Private then
-    raise(Error(loc, Private_type ty_res));
+    raise(Error(loc, env, Private_type ty_res));
   { texp with exp_desc = Texp_construct(constr, args)}
 
 (* Typing of statements (expressions whose values are discarded) *)
@@ -2907,7 +2913,7 @@ let type_expression env sexp =
 open Format
 open Printtyp
 
-let report_error ppf = function
+let report_error env ppf = function
   | Polymorphic_label lid ->
       fprintf ppf "@[The record field label %a is polymorphic.@ %s@]"
         longident lid "You cannot instantiate it in a pattern."
@@ -2917,14 +2923,14 @@ let report_error ppf = function
         but is applied here to %i argument(s)@]"
        longident lid expected provided
   | Label_mismatch(lid, trace) ->
-      report_unification_error ppf trace
+      report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "The record field label %a@ belongs to the type"
                    longident lid)
         (function ppf ->
            fprintf ppf "but is mixed here with labels of type")
   | Pattern_type_clash trace ->
-      report_unification_error ppf trace
+      report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "This pattern matches values of type")
         (function ppf ->
@@ -2935,7 +2941,7 @@ let report_error ppf = function
       fprintf ppf "Variable %s must occur on both sides of this | pattern"
         (Ident.name id)
   | Expr_type_clash trace ->
-      report_unification_error ppf trace
+      report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "This expression has type")
         (function ppf ->
@@ -2993,13 +2999,13 @@ let report_error ppf = function
       else
         fprintf ppf "The value %s is not an instance variable" v
   | Not_subtype(tr1, tr2) ->
-      report_subtyping_error ppf tr1 "is not a subtype of" tr2
+      report_subtyping_error ppf env tr1 "is not a subtype of" tr2
   | Outside_class ->
       fprintf ppf "This object duplication occurs outside a method definition"
   | Value_multiply_overridden v ->
       fprintf ppf "The instance variable %s is overridden several times" v
   | Coercion_failure (ty, ty', trace, b) ->
-      report_unification_error ppf trace
+      report_unification_error ppf env trace
         (function ppf ->
            let ty, ty' = prepare_expansion (ty, ty') in
            fprintf ppf
@@ -3052,7 +3058,7 @@ let report_error ppf = function
       fprintf ppf "in an order different from other calls.@ ";
       fprintf ppf "This is only allowed when the real type is known."
   | Less_general (kind, trace) ->
-      report_unification_error ppf trace
+      report_unification_error ppf env trace
         (fun ppf -> fprintf ppf "This %s has type" kind)
         (fun ppf -> fprintf ppf "which is less general than")
   | Modules_not_allowed ->
@@ -3065,7 +3071,7 @@ let report_error ppf = function
         "This expression is packed module, but the expected type is@ %a"
         type_expr ty
   | Recursive_local_constraint trace ->
-      report_unification_error ppf trace
+      report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "Recursive local constraint when unifying")
         (function ppf ->
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 8b9ce86f02..2905fb12e1 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -104,9 +104,9 @@ type error =
   | Recursive_local_constraint of (type_expr * type_expr) list
   | Unexpected_existential
 
-exception Error of Location.t * error
+exception Error of Location.t * Env.t * error
 
-val report_error: formatter -> error -> unit
+val report_error: Env.t -> formatter -> error -> unit
 
 (* Forward declaration, to be filled in by Typemod.type_module *)
 val type_module: (Env.t -> Parsetree.module_expr -> Typedtree.module_expr) ref
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 315e066d16..789f4772c0 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -30,8 +30,8 @@ type error =
   | Recursive_abbrev of string
   | Definition_mismatch of type_expr * Includecore.type_mismatch list
   | Constraint_failed of type_expr * type_expr
-  | Inconsistent_constraint of (type_expr * type_expr) list
-  | Type_clash of (type_expr * type_expr) list
+  | Inconsistent_constraint of Env.t * (type_expr * type_expr) list
+  | Type_clash of Env.t * (type_expr * type_expr) list
   | Parameters_differ of Path.t * type_expr * type_expr
   | Null_arity_external
   | Missing_native_external
@@ -73,7 +73,7 @@ let update_type temp_env env id loc =
       let params = List.map (fun _ -> Ctype.newvar ()) decl.type_params in
       try Ctype.unify env (Ctype.newconstr path params) ty
       with Ctype.Unify trace ->
-        raise (Error(loc, Type_clash trace))
+        raise (Error(loc, Type_clash (env, trace)))
 
 (* Determine if a type is (an abbreviation for) the type "float" *)
 (* We use the Ctype.expand_head_opt version of expand_head to get access
@@ -223,7 +223,7 @@ let transl_declaration env (name, sdecl) id =
   List.iter
     (fun (ty, ty', loc) ->
       try Ctype.unify env ty ty' with Ctype.Unify tr ->
-        raise(Error(loc, Inconsistent_constraint tr)))
+        raise(Error(loc, Inconsistent_constraint (env, tr))))
     cstrs;
   Ctype.end_def ();
   (* Add abstract row *)
@@ -429,7 +429,7 @@ let check_recursion env loc path decl to_check =
         Ctype.correct_abbrev env path decl.type_params body
       with Ctype.Recursive_abbrev ->
         raise(Error(loc, Recursive_abbrev (Path.name path)))
-      | Ctype.Unify trace -> raise(Error(loc, Type_clash trace))
+      | Ctype.Unify trace -> raise(Error(loc, Type_clash (env, trace)))
       end;
       (* Check that recursion is regular *)
       if decl.type_params = [] then () else
@@ -878,7 +878,7 @@ let transl_with_constraint env id row_path orig_decl sdecl =
          Ctype.unify env (transl_simple_type env false ty)
                          (transl_simple_type env false ty')
        with Ctype.Unify tr ->
-         raise(Error(loc, Inconsistent_constraint tr)))
+         raise(Error(loc, Inconsistent_constraint (env, tr))))
     sdecl.ptype_cstrs;
   let no_row = not (is_fixed_type sdecl) in
   let decl =
@@ -1017,13 +1017,13 @@ let report_error ppf = function
       fprintf ppf
         "@[<hv>In the definition of %s, type@ %a@ should be@ %a@]"
         (Path.name path) Printtyp.type_expr ty Printtyp.type_expr ty'
-  | Inconsistent_constraint trace ->
+  | Inconsistent_constraint (env, trace) ->
       fprintf ppf "The type constraints are not consistent.@.";
-      Printtyp.report_unification_error ppf trace
+      Printtyp.report_unification_error ppf env trace
         (fun ppf -> fprintf ppf "Type")
         (fun ppf -> fprintf ppf "is not compatible with type")
-  | Type_clash trace ->
-      Printtyp.report_unification_error ppf trace
+  | Type_clash (env, trace) ->
+      Printtyp.report_unification_error ppf env trace
         (function ppf ->
            fprintf ppf "This type constructor expands to type")
         (function ppf ->
diff --git a/typing/typedecl.mli b/typing/typedecl.mli
index 25ef97711b..521c2ecbd6 100644
--- a/typing/typedecl.mli
+++ b/typing/typedecl.mli
@@ -59,8 +59,8 @@ type error =
   | Recursive_abbrev of string
   | Definition_mismatch of type_expr * Includecore.type_mismatch list
   | Constraint_failed of type_expr * type_expr
-  | Inconsistent_constraint of (type_expr * type_expr) list
-  | Type_clash of (type_expr * type_expr) list
+  | Inconsistent_constraint of Env.t * (type_expr * type_expr) list
+  | Type_clash of Env.t * (type_expr * type_expr) list
   | Parameters_differ of Path.t * type_expr * type_expr
   | Null_arity_external
   | Missing_native_external
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 506784865a..eded3a6243 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -778,7 +778,7 @@ let rec type_module sttn funct_body anchor env smod =
             modtype_of_package env smod.pmod_loc p nl tl
         | {desc = Tvar _} ->
             raise (Typecore.Error
-                     (smod.pmod_loc, Typecore.Cannot_infer_signature))
+                     (smod.pmod_loc, env, Typecore.Cannot_infer_signature))
         | _ ->
             raise (Error (smod.pmod_loc, Not_a_packed_module exp.exp_type))
       in