Amelioration des messages d'erreurs d'unification (expansion des

abbreviations).
Typeclass: correction d'un bug de typage.


git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@828 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

10 files changed, 304 insertions, 214 deletions

diff --git a/toplevel/topdirs.ml b/toplevel/topdirs.ml
index 4e4f4a7ba4..a319c6304f 100644
--- a/toplevel/topdirs.ml
+++ b/toplevel/topdirs.ml
@@ -158,7 +158,7 @@ let find_printer_type lid =
     Not_found ->
       print_string "Unbound value "; Printtyp.longident lid;
       print_newline(); raise Exit
-  | Ctype.Unify ->
+  | Ctype.Unify _ ->
       Printtyp.longident lid;
       print_string " has the wrong type for a printing function";
       print_newline(); raise Exit
diff --git a/typing/ctype.ml b/typing/ctype.ml
index fe26b31a3d..af94250499 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -17,7 +17,7 @@ open Misc
 open Asttypes
 open Typedtree
 
-exception Unify
+exception Unify of (type_expr * type_expr) list
 
 let current_level = ref 0
 let global_level = ref 1
@@ -361,6 +361,26 @@ let expand_abbrev env path args abbrev level =
       with Not_found ->
         raise Cannot_expand
 
+let rec expand_root env ty =
+  let ty = repr ty in
+  match ty.desc with
+    Tconstr(p, tl, abbrev) ->
+      begin try
+        expand_root env (expand_abbrev env p tl (ref !abbrev) ty.level)
+      with Cannot_expand ->
+        ty
+      end
+  | _ ->
+      ty
+
+let rec full_expand env ty =
+  let ty = repr (expand_root env ty) in
+  match ty.desc with
+    Tobject (fi, {contents = Some nm}) when opened_object ty ->
+      { desc = Tobject (fi, ref None); level = ty.level }
+  | _ ->
+      ty
+
 let generic_abbrev env path =
   try
     let decl = Env.find_type path env in
@@ -380,7 +400,7 @@ let occur env ty0 ty =
       Tlink ty' ->
         occur_rec ty'
     | Tvar ->
-        if ty == ty0 then raise Unify else
+        if ty == ty0 then raise (Unify []) else
         ()
     | Tarrow(t1, t2) ->
         occur_rec t1; occur_rec t2
@@ -391,7 +411,7 @@ let occur env ty0 ty =
     | Tconstr(p, tl, abbrev) ->
         if not (List.memq ty !visited) then begin
           visited := ty :: !visited;
-          try List.iter occur_rec tl with Unify ->
+          try List.iter occur_rec tl with Unify _ ->
           try occur_rec (expand_abbrev env p tl abbrev ty.level)
           with Cannot_expand ->
           ()
@@ -408,53 +428,59 @@ let rec unify_rec env a1 a2 t1 t2 =     (* Variables and abbreviations *)
   let t1 = repr2 t1 in
   let t2 = repr2 t2 in
   if t1 == t2 then () else
-  match (t1.desc, t2.desc) with
-    (Tvar, _) ->
-       update_level t1.level t2;
-       begin match a2 with
-         None    -> occur env t1 t2; t1.desc <- Tlink t2
-       | Some l2 -> occur env t1 l2; t1.desc <- Tlink l2
-       end
-  | (_, Tvar) ->
-       update_level t2.level t1;
-       begin match a1 with
-         None    -> occur env t2 t1; t2.desc <- Tlink t1
-       | Some l1 -> occur env t2 l1; t2.desc <- Tlink l1
-       end
-  | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
-       unify_core env a1 a2 t1 t2
-  | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) ->
-      begin
-        try
+  try
+    match (t1.desc, t2.desc) with
+      (Tvar, _) ->
+         update_level t1.level t2;
+         begin match a2 with
+           None    -> occur env t1 t2; t1.desc <- Tlink t2
+         | Some l2 -> occur env t1 l2; t1.desc <- Tlink l2
+         end
+    | (_, Tvar) ->
+         update_level t2.level t1;
+         begin match a1 with
+           None    -> occur env t2 t1; t2.desc <- Tlink t1
+         | Some l1 -> occur env t2 l1; t2.desc <- Tlink l1
+         end
+    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
+         unify_core env a1 a2 t1 t2
+    | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) ->
+        begin
+          try
+            let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
+            update_level t2.level t1;
+            unify_rec env (Some t1) a2 t3 t2
+          with Cannot_expand ->
+          try
+            let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
+            update_level t1.level t2;
+            unify_rec env a1 (Some t2) t1 t3
+          with Cannot_expand ->
+            raise (Unify [])
+        end
+    | (Tconstr (p1, tl1, abbrev1), _) ->
+        begin try
           let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
           update_level t2.level t1;
           unify_rec env (Some t1) a2 t3 t2
         with Cannot_expand ->
-        try
+          unify_core env a1 a2 t1 t2
+        end
+    | (_, Tconstr (p2, tl2, abbrev2)) ->
+        begin try
           let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
           update_level t1.level t2;
           unify_rec env a1 (Some t2) t1 t3
         with Cannot_expand ->
-          raise Unify
-      end
-  | (Tconstr (p1, tl1, abbrev1), _) ->
-      begin try
-        let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
-        update_level t2.level t1;
-        unify_rec env (Some t1) a2 t3 t2
-      with Cannot_expand ->
-        unify_core env a1 a2 t1 t2
-      end
-  | (_, Tconstr (p2, tl2, abbrev2)) ->
-      begin try
-        let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
-        update_level t1.level t2;
-        unify_rec env a1 (Some t2) t1 t3
-      with Cannot_expand ->
+          unify_core env a1 a2 t1 t2
+        end
+    | (_, _) ->
         unify_core env a1 a2 t1 t2
-      end
-  | (_, _) ->
-      unify_core env a1 a2 t1 t2
+  with
+    Unify [] ->
+      raise (Unify [(t1, t2)])
+  | Unify (_::l) ->
+      raise (Unify ((t1, t2)::l))
 
 and unify_core env a1 a2 t1 t2 =        (* Other cases *)
   let d1 = t1.desc and d2 = t2.desc in
@@ -487,17 +513,22 @@ and unify_core env a1 a2 t1 t2 =        (* Other cases *)
           raise exn
         end
     | (_, _) ->
-        raise Unify
-  with exn ->
-    t1.desc <- d1;
-    t2.desc <- d2;
-    raise exn
+        raise (Unify [])
+  with
+    Unify l ->
+      t1.desc <- d1;
+      t2.desc <- d2;
+      raise (Unify ((t1, t2)::l))
+  | exn ->
+      t1.desc <- d1;
+      t2.desc <- d2;
+      raise exn
 
 and unify_list env tl1 tl2 =
   try
     List.iter2 (unify_rec env None None) tl1 tl2
   with Invalid_argument _ ->
-    raise Unify
+    raise (Unify [])
 
 and unify_fields env ty1 ty2 =
   let (fields1, rest1) = flatten_fields ty1
@@ -510,7 +541,7 @@ and unify_fields env ty1 ty2 =
         update_level rest1.level nr;
         rest1.desc <- Tlink nr
     | Tnil ->
-        if miss2 <> [] then raise Unify;
+        if miss2 <> [] then raise (Unify []);
         va.desc <- Tlink {desc = Tnil; level = va.level}
     | _ ->
         fatal_error "Ctype.unify_fields (1)"
@@ -521,15 +552,43 @@ and unify_fields env ty1 ty2 =
         update_level rest2.level nr;
         rest2.desc <- Tlink nr
     | Tnil ->
-        if miss1 <> [] then raise Unify;
+        if miss1 <> [] then raise (Unify []);
         va.desc <- Tlink {desc = Tnil; level = va.level}
     | _ ->
         fatal_error "Ctype.unify_fields (2)"
     end;
     List.iter (fun (t1, t2) -> unify_rec env None None t1 t2) pairs
 
+let expand_types env (ty1, ty2) =
+  (ty1, full_expand env ty1), (ty2, full_expand env ty2)
+
+let expand_trace env trace =
+  List.fold_right
+    (fun (t1, t2) rem ->
+       (t1, full_expand env t1)::(t2, full_expand env t2)::rem)
+    trace []
+
+let rec filter_trace =
+  function
+    (t1, t1')::(t2, t2')::rem ->
+      let rem' = filter_trace rem in
+      if (t1 == t1') & (t2 == t2') then
+        rem'
+      else
+        (t1, t1')::(t2, t2')::rem
+  | _ ->
+      []
+
 let unify env ty1 ty2 =
-  unify_rec env None None ty1 ty2
+  try
+    unify_rec env None None ty1 ty2
+  with Unify trace ->
+    let trace = expand_trace env trace in
+    match trace with
+      t1::t2::rem ->
+        raise (Unify (t1::t2::filter_trace rem))
+    | _ ->
+        fatal_error "Ctype.unify"
 
 let rec filter_arrow env t =
   let t = repr t in
@@ -546,10 +605,10 @@ let rec filter_arrow env t =
       begin try
         filter_arrow env (expand_abbrev env p tl abbrev t.level)
       with Cannot_expand ->
-        raise Unify
+        raise (Unify [])
       end
   | _ ->
-      raise Unify
+      raise (Unify [])
 
 let rec filter_method_field name ty =
   let ty = repr ty in
@@ -566,7 +625,7 @@ let rec filter_method_field name ty =
       else
         filter_method_field name ty2
   | _ ->
-      raise Unify
+      raise (Unify [])
 
 let rec filter_method env name ty =
   let ty = repr ty in
@@ -583,10 +642,10 @@ let rec filter_method env name ty =
       begin try
         filter_method env name (expand_abbrev env p tl abbrev ty.level)
       with Cannot_expand ->
-        raise Unify
+        raise (Unify [])
       end
   | _ ->
-      raise Unify
+      raise (Unify [])
 
 (* Matching between type schemes *)
 
@@ -602,7 +661,7 @@ let rec moregen_occur ty0 ty =
          and cannot be instantiated by a type that contains
          generic variables. *)
       if ty.level = generic_level & ty0.level < !current_level
-      then raise Unify
+      then raise (Unify [])
   | Tarrow(t1, t2) ->
       occur_rec t1; occur_rec t2
   | Ttuple tl ->
@@ -635,7 +694,7 @@ let rec moregen env t1 t2 =
   try
     begin match (t1.desc, t2.desc) with
       (Tvar, _) ->
-        if t1.level = generic_level then raise Unify;
+        if t1.level = generic_level then raise (Unify []);
         occur env t1 t2;
         moregen_occur t1 t2;
         t1.desc <- Tlink t2
@@ -655,7 +714,7 @@ let rec moregen env t1 t2 =
           try
             moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
           with Cannot_expand ->
-            raise Unify
+            raise (Unify [])
         end
     | (Tobject(f1, _), Tobject(f2, _)) ->
         t1.desc <- Tlink t2;
@@ -665,16 +724,16 @@ let rec moregen env t1 t2 =
         begin try
           moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
         with Cannot_expand ->
-          raise Unify
+          raise (Unify [])
         end
     | (_, Tconstr(p2, tl2, abbrev2)) ->
         begin try
           moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
         with Cannot_expand ->
-          raise Unify
+          raise (Unify [])
         end
     | (_, _) ->
-        raise Unify
+        raise (Unify [])
     end
   with exn ->
     t1.desc <- d1;
@@ -684,21 +743,21 @@ and moregen_list env tl1 tl2 =
   try
     List.iter2 (moregen env) tl1 tl2
   with Invalid_argument _ ->
-    raise Unify
+    raise (Unify [])
 
 and moregen_fields env ty1 ty2 =
   let (fields1, rest1) = flatten_fields ty1
   and (fields2, rest2) = flatten_fields ty2 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-  if miss1 <> [] then raise Unify;
+  if miss1 <> [] then raise (Unify []);
   begin match rest1.desc with
     Tvar ->
-      if rest1.level = generic_level then raise Unify;
+      if rest1.level = generic_level then raise (Unify []);
       let fi = build_fields miss2 rest2 in
       moregen_occur rest1 fi
   | Tnil ->
-      if miss2 <> [] then raise Unify;
-      if rest2.desc <> Tnil then raise Unify
+      if miss2 <> [] then raise (Unify []);
+      if rest2.desc <> Tnil then raise (Unify [])
   | _ ->
       fatal_error "moregen_fields"
   end;
@@ -711,7 +770,7 @@ let moregeneral env sch1 sch2 =
     remove_abbrev sch2;
     end_def();
     true
-  with Unify ->
+  with Unify _ ->
     remove_abbrev sch2;
     end_def();
     false
@@ -948,13 +1007,13 @@ let rec subtype_rec env vars t1 t2 =
         else
           unify env t1 t2
     | (_, _) ->
-        raise Unify
+        raise (Unify [])
 
 and subtype_list env vars tl1 tl2 =
   try
     List.iter2 (subtype_rec env vars) tl1 tl2
   with Invalid_argument _ ->
-    raise Unify
+    raise (Unify [])
 
 and subtype_fields env vars ty1 ty2 =
   let (fields1, rest1) = flatten_fields ty1 in
@@ -965,7 +1024,7 @@ and subtype_fields env vars ty1 ty2 =
       let nr = build_fields miss2 (newvar ()) in
       update_level rest1.level nr;
       rest1.desc <- Tlink nr
-  | Tnil   -> if miss2 <> [] then raise Unify
+  | Tnil   -> if miss2 <> [] then raise (Unify [])
   | _      -> fatal_error "Ctype.subtype_fields (1)"
   end;
   begin match rest2.desc with
@@ -1186,18 +1245,6 @@ let remove_object_name ty =
   | Tconstr (_, _, _) -> ()
   | _                 -> fatal_error "Ctype.remove_object_name"
 
-let rec expand_root env ty =
-  let ty = repr ty in
-  match ty.desc with
-    Tconstr(p, tl, abbrev) ->
-      begin try
-        expand_root env (expand_abbrev env p tl (ref !abbrev) ty.level)
-      with Cannot_expand ->
-        ty
-      end
-  | _ ->
-      ty
-
 (* Abbreviation correctness *)
 
 exception Nonlinear_abbrev
diff --git a/typing/ctype.mli b/typing/ctype.mli
index dc3750d0b0..e0d3299e71 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -113,7 +113,7 @@ val arity: type_expr -> int
 val none: type_expr
         (* A dummy type expression *)
 
-exception Unify
+exception Unify of (type_expr * type_expr) list
 exception Cannot_expand
 exception Nonlinear_abbrev
 exception Recursive_abbrev
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 9f90bbab63..5597855d5f 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -522,3 +522,45 @@ let signature sg =
   open_vbox 0;
   signature_body false sg;
   close_box()
+
+(* Print an unification error *)
+
+let type_expansion t t' =
+  if t == t' then
+    type_expr t
+  else begin
+    open_hovbox 2;
+    type_expr t;
+    print_space (); print_string "="; print_space ();
+    type_expr t';
+    close_box ()
+  end
+
+let rec unification_trace =
+  function
+    (t1, t1')::(t2, t2')::rem ->
+      print_cut ();
+      open_hovbox 0;
+      print_string "Type"; print_break 1 2;
+      type_expansion t1 t1'; print_space ();
+      print_string "is not compatible with type"; print_break 1 2;
+      type_expansion t2 t2';
+      close_box ();
+      unification_trace rem
+  | _ ->
+      ()
+
+let unification_error trace txt1 txt2 =
+  reset ();
+  List.iter
+    (function (t, t') -> mark_loops t; if t != t' then mark_loops t')
+    trace;
+  open_hovbox 0;
+  let (t1, t1') = List.hd trace in
+  let (t2, t2') = List.hd (List.tl trace) in
+  txt1 (); print_break 1 2;
+  type_expansion t1 t1'; print_space();
+  txt2 (); print_break 1 2;
+  type_expansion t2 t2';
+  close_box();
+  unification_trace (List.tl (List.tl trace))
diff --git a/typing/printtyp.mli b/typing/printtyp.mli
index eddf841aad..c1e7e08b0d 100644
--- a/typing/printtyp.mli
+++ b/typing/printtyp.mli
@@ -30,3 +30,6 @@ val signature: signature -> unit
 val signature_body: bool -> signature -> unit
 val modtype_declaration: Ident.t -> modtype_declaration -> unit
 val class_type: Ident.t -> class_type -> unit
+val unification_error:
+        (type_expr * type_expr) list -> (unit -> unit) -> (unit -> unit) ->
+        unit
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index d57cecd76c..d773b8ceb5 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -29,17 +29,17 @@ type error =
   | Non_closed of Ident.t * type_expr list * type_expr
   | Mutable_var of string
   | Undefined_var of string
-  | Variable_type_mismatch of string * type_expr * type_expr
-  | Method_type_mismatch of string * type_expr * type_expr
+  | Variable_type_mismatch of string * (type_expr * type_expr) list
+  | Method_type_mismatch of string * (type_expr * type_expr) list
   | Unconsistent_constraint
   | Unbound_class of Longident.t
-  | Argument_type_mismatch of type_expr * type_expr
+  | Argument_type_mismatch of (type_expr * type_expr) list
   | Abbrev_type_clash of type_expr * type_expr * type_expr
   | Bad_parameters of Ident.t * type_expr * type_expr
   | Illdefined_class of string
   | Argument_arity_mismatch of Path.t * int * int
   | Parameter_arity_mismatch of Path.t * int * int
-  | Parameter_mismatch of type_expr * type_expr
+  | Parameter_mismatch of (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
@@ -60,6 +60,21 @@ let rec add_methods env self concr concr_lst t =
   | _ ->
       ()
 
+let equalize_methods env self obj =
+  match (Ctype.expand_root env obj).desc with
+    Tobject (ty, _) ->
+      let rec equalize_methods_rec t =
+        match (Ctype.repr t).desc with
+          Tfield (lab, _, t') ->
+            Ctype.filter_method env lab self;
+            equalize_methods_rec t'
+        | _ ->
+            ()
+      in
+        equalize_methods_rec ty
+  | _ ->
+      fatal_error "Typeclass.equalize_methods"
+
 let make_stub env cl =
   Ctype.begin_def ();
 
@@ -163,9 +178,9 @@ let rec type_meth env loc self ty =
     Tfield (lab, ty, ty') ->
       let ty0 = Ctype.filter_method env lab self in
       begin try
-        Ctype.unify env ty0 ty
-      with Ctype.Unify ->
-        raise(Error(loc, Method_type_mismatch (lab, ty, ty0)))
+        Ctype.unify env ty ty0
+      with Ctype.Unify trace ->
+        raise(Error(loc, Method_type_mismatch (lab, trace)))
       end;
       type_meth env loc self ty'
   | _ ->
@@ -178,7 +193,7 @@ let missing_method env ty ty' =
         begin try
       	  Ctype.filter_method env lab ty;
 	  missing_method_rec met'
-        with Ctype.Unify ->
+        with Ctype.Unify _ ->
       	  lab
         end
     | _ ->
@@ -207,8 +222,8 @@ let insert_value env lab priv mut ty loc vals =
   begin try
     let (mut', ty') = Vars.find lab vals in
     check_mutable loc lab mut mut';
-    try Ctype.unify env ty ty' with Ctype.Unify ->
-      raise(Error(loc, Variable_type_mismatch(lab, ty, ty')))
+    try Ctype.unify env ty ty' with Ctype.Unify trace ->
+      raise(Error(loc, Variable_type_mismatch(lab, trace)))
   with Not_found -> () end;
   if priv = Private then
     vals_remove lab vals
@@ -245,8 +260,8 @@ let type_class_field env var_env self cl (met_env, fields, vars_sig) =
       List.iter2
         (fun sty ty ->
            let ty' = Typetexp.transl_simple_type var_env false sty in
-           try Ctype.unify var_env ty ty' with Ctype.Unify ->
-             raise(Error(sty.ptyp_loc, Parameter_mismatch(ty', ty))))
+           try Ctype.unify var_env ty' ty with Ctype.Unify trace ->
+             raise(Error(sty.ptyp_loc, Parameter_mismatch trace)))
         params params';
 
       (* Type arguments *)
@@ -278,7 +293,7 @@ let type_class_field env var_env self cl (met_env, fields, vars_sig) =
               begin try
                 Ctype.unify var_env self
                   (Ctype.newobj (closed_scheme fi))
-              with Ctype.Unify ->
+              with Ctype.Unify _ ->
                 let lab = missing_method var_env self' self in
                 raise(Error(loc, Closed_ancestor
                                    (cl.pcl_name, path, lab)))
@@ -338,16 +353,16 @@ let type_class_field env var_env self cl (met_env, fields, vars_sig) =
   | Pcf_virt (lab, ty, loc) ->
       let ty = transl_simple_type met_env false ty in
       let ty' = Ctype.filter_method met_env lab self in
-      begin try Ctype.unify met_env ty ty' with Ctype.Unify ->
-        raise(Error(loc, Method_type_mismatch (lab, ty, ty')))
+      begin try Ctype.unify met_env ty ty' with Ctype.Unify trace ->
+        raise(Error(loc, Method_type_mismatch (lab, trace)))
       end;
       (met_env, fields, vars_sig)
 
   | Pcf_meth (lab, expr, loc)  ->
       let (texp, ty) = type_method met_env self cl.pcl_self expr in
       let ty' = Ctype.filter_method met_env lab self in
-        begin try Ctype.unify met_env ty ty' with Ctype.Unify ->
-          raise(Error(loc, Method_type_mismatch (lab, ty, ty')))
+        begin try Ctype.unify met_env ty ty' with Ctype.Unify trace ->
+          raise(Error(loc, Method_type_mismatch (lab, trace)))
         end;
       (met_env, Cf_meth (lab, texp)::fields, vars_sig)
   
@@ -381,7 +396,7 @@ let transl_class temp_env env
        try
          Ctype.unify temp_env
            (type_variable loc v) (transl_simple_type temp_env false ty)
-       with Ctype.Unify ->
+       with Ctype.Unify _ ->
          raise(Error(loc, Unconsistent_constraint)))
     cl.pcl_cstr;
 
@@ -407,13 +422,13 @@ let transl_class temp_env env
 
   (* Temporary class abbreviation *)
   let (cl_params, cl_ty) = Ctype.instance_parameterized_type params self in
-  begin try Ctype.unify temp_env temp_cl cl_ty with Ctype.Unify ->
+  begin try Ctype.unify temp_env temp_cl cl_ty with Ctype.Unify _ ->
     Ctype.remove_object_name temp_cl;
     raise(Error(cl.pcl_loc, Abbrev_type_clash (cl_abbrev, cl_ty, temp_cl)))
   end;
   begin try
     List.iter2 (Ctype.unify temp_env) temp_cl_params cl_params
-  with Ctype.Unify ->
+  with Ctype.Unify _ ->
     raise(Error(cl.pcl_loc,
       	  Bad_parameters (cl_id, cl_abbrev,
       	                  Ctype.newty (Tconstr (Path.Pident cl_id, cl_params,
@@ -424,12 +439,12 @@ let transl_class temp_env env
   let (obj_params, arg_sig', obj_ty) =
     Ctype.instance_parameterized_type_2 params arg_sig self
   in
-  begin try Ctype.unify temp_env abbrev obj_ty with Ctype.Unify ->
+  begin try Ctype.unify temp_env abbrev obj_ty with Ctype.Unify _ ->
     raise(Error(cl.pcl_loc, Abbrev_type_clash (abbrev, obj_ty, temp_obj)))
   end;
   begin try
     List.iter2 (Ctype.unify temp_env) temp_obj_params obj_params
-  with Ctype.Unify ->
+  with Ctype.Unify _ ->
     raise(Error(cl.pcl_loc,
           Bad_parameters (obj_id, abbrev,
        	       	          Ctype.newty (Tconstr (Path.Pident obj_id, obj_params,
@@ -439,9 +454,9 @@ let transl_class temp_env env
   List.iter2
     (fun ty (exp, ty') ->
        begin try
-	 Ctype.unify temp_env ty ty'
-       with Ctype.Unify ->
-	 raise(Error(exp.pat_loc, Argument_type_mismatch(ty', ty)))
+	 Ctype.unify temp_env ty' ty
+       with Ctype.Unify trace ->
+	 raise(Error(exp.pat_loc, Argument_type_mismatch trace))
        end)
     new_args (List.combine args arg_sig');
 
@@ -480,12 +495,14 @@ let build_new_type temp_env env
     let concr = Ctype.instance concr in
     try
       Ctype.unify temp_env concr temp_obj
-    with Ctype.Unify ->
-    	let lab = missing_method temp_env concr temp_obj in
+    with Ctype.Unify _ ->
+      let lab = missing_method temp_env concr temp_obj in
       raise(Error(cl.pcl_loc,
     	       	    Virtual_class (cl.pcl_name, lab)))
   end;
 
+  equalize_methods temp_env self temp_obj;
+
   (* self should not be an abbreviation (printtyp) *)
   let exp_self = Ctype.expand_root temp_env self in
 
@@ -654,7 +671,7 @@ let type_class_type_field env temp_env cl self
 	    if not (Ctype.opened_object super) then
 	      begin try
 		Ctype.unify temp_env self (Ctype.newobj (closed_scheme fi))
-	      with Ctype.Unify ->
+	      with Ctype.Unify _ ->
 		let lab = missing_method temp_env super self in
 		raise(Error(loc,
 			    Closed_ancestor (cl.pcty_name, path, lab)))
@@ -840,10 +857,12 @@ let build_class_type env
 
   (* Check variable and method redefining *)
   List.iter
-    (check_field_redef env (fun l t t' -> Variable_type_mismatch(l, t', t)))
+    (check_field_redef env
+       (fun l t t' -> Variable_type_mismatch(l, [(t', t'); (t, t)])))
     val_redef;
   List.iter
-    (check_field_redef env (fun l t t' -> Method_type_mismatch(l, t', t)))
+    (check_field_redef env
+       (fun l t t' -> Method_type_mismatch(l, [(t', t'); (t, t)])))
     meth_redef;
 
   (* Class type skeleton *)
@@ -866,7 +885,7 @@ let build_class_type env
        try
          Ctype.unify env
            (type_variable loc v) (transl_simple_type env false ty)
-       with Ctype.Unify ->
+       with Ctype.Unify _ ->
        	 raise(Error(loc, Unconsistent_constraint)))
     cl.pcty_cstr;
 
@@ -893,7 +912,7 @@ let build_class_type env
       let temp_obj = Ctype.instance obj_ty in
       begin try
         Ctype.unify env concr temp_obj
-      with Ctype.Unify ->
+      with Ctype.Unify _ ->
       	let lab = missing_method env concr temp_obj in
 	raise(Error(cl.pcty_loc,
       	       	    Virtual_class (cl.pcty_name, lab)))
@@ -963,13 +982,15 @@ let report_error = function
       Printtyp.mark_loops typ;
       print_string
         "Some type variables are not bound in implicit type definition";
-      print_space ();
+      print_break 1 2;
       open_hovbox 0;
       Printtyp.type_expr (Ctype.newty (Tconstr(Path.Pident id, args, ref [])));
       print_space (); print_string "="; print_space ();
       Printtyp.type_expr typ;
       close_box ();
-      close_box ()
+      close_box ();
+      print_space ();
+      print_string "They should all be captured by a class type parameter."
   | Mutable_var v ->
       print_string "The variable"; print_space ();
       print_string v; print_space ();
@@ -978,45 +999,33 @@ let report_error = function
       print_string "The variable"; print_space ();
       print_string v; print_space ();
       print_string "is undefined"
-  | Variable_type_mismatch (v, actual, expected) ->
-      open_hovbox 0;
-      Printtyp.reset ();
-      Printtyp.mark_loops actual; Printtyp.mark_loops expected;
-      print_string "The variable ";
-      print_string v; print_space ();
-      print_string "has type"; print_space ();
-      Printtyp.type_expr actual;
-      print_space ();
-      print_string "but is expected to have type"; print_space ();
-      Printtyp.type_expr expected;
-      close_box ()
-  | Method_type_mismatch (m, actual, expected) ->
-      open_hovbox 0;
-      Printtyp.reset ();
-      Printtyp.mark_loops actual; Printtyp.mark_loops expected;
-      print_string "The method ";
-      print_string m; print_space ();
-      print_string "has type"; print_space ();
-      Printtyp.type_expr actual;
-      print_space ();
-      print_string "but is expected to have type"; print_space ();
-      Printtyp.type_expr expected;
-      close_box ()
+  | Variable_type_mismatch (v, trace) ->
+      Printtyp.unification_error trace
+        (function () ->
+           print_string "The variable ";
+           print_string v; print_space ();
+           print_string "has type")
+        (function () ->
+           print_string "but is expected to have type")
+  | Method_type_mismatch (m, trace) ->
+      Printtyp.unification_error trace
+        (function () ->
+           print_string "The method ";
+           print_string m; print_space ();
+           print_string "has type")
+        (function () ->
+           print_string "but is expected to have type")
   | Unconsistent_constraint ->
       print_string "The class constraints are not consistent"
   | Unbound_class cl ->
       print_string "Unbound class"; print_space ();
       Printtyp.longident cl
-  | Argument_type_mismatch (actual, expected) ->
-      open_hovbox 0;
-      Printtyp.reset ();
-      Printtyp.mark_loops actual; Printtyp.mark_loops expected;
-      print_string "This argument has type"; print_space ();
-      Printtyp.type_expr actual;
-      print_space ();
-      print_string "but is expected to have type"; print_space ();
-      Printtyp.type_expr expected;
-      close_box ()
+  | Argument_type_mismatch trace ->
+      Printtyp.unification_error trace
+        (function () ->
+           print_string "This argument has type")
+        (function () ->
+           print_string "but is expected to have type")
   | Abbrev_type_clash (abbrev, actual, expected) ->
       open_hovbox 0;
       Printtyp.reset ();
@@ -1043,15 +1052,12 @@ let report_error = function
   | Illdefined_class s ->
       print_string "The class "; print_string s;
       print_string " is ill-defined"
-  | Parameter_mismatch(actual, expected) ->
-      Printtyp.reset ();
-      Printtyp.mark_loops actual; Printtyp.mark_loops expected;
-      open_hovbox 0;
-      print_string "The type parameter"; print_space ();
-      Printtyp.type_expr actual; print_space ();
-      print_string "does not meet its constraint: it should be";
-      print_space ();
-      Printtyp.type_expr expected
+  | Parameter_mismatch trace ->
+      Printtyp.unification_error trace
+        (function () ->
+           print_string "The type parameter")
+        (function () ->
+           print_string "does not meet its constraint: it should be")
   | Argument_arity_mismatch(p, expected, provided) ->
       open_hovbox 0;
       print_string "The class "; Printtyp.path p;
diff --git a/typing/typeclass.mli b/typing/typeclass.mli
index b5e72e3c52..163e01dbe2 100644
--- a/typing/typeclass.mli
+++ b/typing/typeclass.mli
@@ -36,17 +36,17 @@ type error =
   | Non_closed of Ident.t * type_expr list * type_expr
   | Mutable_var of string
   | Undefined_var of string
-  | Variable_type_mismatch of string * type_expr * type_expr
-  | Method_type_mismatch of string * type_expr * type_expr
+  | Variable_type_mismatch of string * (type_expr * type_expr) list
+  | Method_type_mismatch of string * (type_expr * type_expr) list
   | Unconsistent_constraint
   | Unbound_class of Longident.t
-  | Argument_type_mismatch of type_expr * type_expr
+  | Argument_type_mismatch of (type_expr * type_expr) list
   | Abbrev_type_clash of type_expr * type_expr * type_expr
   | Bad_parameters of Ident.t * type_expr * type_expr
   | Illdefined_class of string
   | Argument_arity_mismatch of Path.t * int * int
   | Parameter_arity_mismatch of Path.t * int * int
-  | Parameter_mismatch of type_expr * type_expr
+  | Parameter_mismatch of (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 620611e088..660bb0b599 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -25,11 +25,11 @@ type error =
   | Unbound_constructor of Longident.t
   | Unbound_label of Longident.t
   | Constructor_arity_mismatch of Longident.t * int * int
-  | Label_mismatch of Longident.t * type_expr * type_expr
-  | Pattern_type_clash of type_expr * type_expr
+  | Label_mismatch of Longident.t * (type_expr * type_expr) list
+  | Pattern_type_clash of (type_expr * type_expr) list
   | Multiply_bound_variable
   | Orpat_not_closed
-  | Expr_type_clash of type_expr * type_expr
+  | Expr_type_clash of (type_expr * type_expr) list
   | Apply_non_function of type_expr
   | Label_multiply_defined of Longident.t
   | Label_missing
@@ -59,8 +59,8 @@ let type_constant = function
 let unify_pat env pat expected_ty =
   try
     unify env pat.pat_type expected_ty
-  with Unify ->
-    raise(Error(pat.pat_loc, Pattern_type_clash(pat.pat_type, expected_ty)))
+  with Unify trace ->
+    raise(Error(pat.pat_loc, Pattern_type_clash(trace)))
 
 let pattern_variables = ref ([]: (Ident.t * type_expr) list)
 
@@ -131,8 +131,8 @@ let rec type_pat env sp =
         let (ty_arg, ty_res) = instance_label label in
         begin try
           unify env ty_res ty
-        with Unify ->
-          raise(Error(sp.ppat_loc, Label_mismatch(lid, ty_res, ty)))
+        with Unify trace ->
+          raise(Error(sp.ppat_loc, Label_mismatch(lid, trace)))
         end;
         let arg = type_pat env sarg in
         unify_pat env arg ty_arg;
@@ -250,8 +250,8 @@ let type_format loc fmt =
 let unify_exp env exp expected_ty =
   try
     unify env exp.exp_type expected_ty
-  with Unify ->
-    raise(Error(exp.exp_loc, Expr_type_clash(exp.exp_type, expected_ty)))
+  with Unify trace ->
+    raise(Error(exp.exp_loc, Expr_type_clash(trace)))
 
 let rec type_exp env sexp =
   match sexp.pexp_desc with
@@ -300,7 +300,7 @@ let rec type_exp env sexp =
           let (ty1, ty2) =
             try
               filter_arrow env ty_fun
-            with Unify ->
+            with Unify _ ->
               raise(Error(sfunct.pexp_loc,
                           Apply_non_function funct.exp_type)) in
           let arg1 = type_expect env sarg1 ty1 in
@@ -363,8 +363,8 @@ let rec type_exp env sexp =
         let (ty_arg, ty_res) = instance_label label in
         begin try
           unify env ty_res ty
-        with Unify ->
-          raise(Error(sexp.pexp_loc, Label_mismatch(lid, ty_res, ty)))
+        with Unify trace ->
+          raise(Error(sexp.pexp_loc, Label_mismatch(lid, trace)))
         end;
         let arg = type_expect env sarg ty_arg in
         num_fields := Array.length label.lbl_all;
@@ -467,7 +467,7 @@ let rec type_exp env sexp =
             let ty = Typetexp.transl_simple_type env false sty in
             let ty' = Typetexp.transl_simple_type env false sty' in
 	    begin try subtype env (Typetexp.type_variable_list ()) ty ty' with
-	      Unify ->
+	      Unify _ ->
 	        raise(Error(sexp.pexp_loc, Not_subtype(ty, ty')))
 	    end;
 	    (ty, ty')
@@ -508,7 +508,7 @@ let rec type_exp env sexp =
 	      Texp_send(object, met)
         in
           { exp_desc = exp; exp_loc = sexp.pexp_loc; exp_type = typ}
-      with Unify ->
+      with Unify _ ->
       	raise(Error(e.pexp_loc,	Undefined_method_err met))
       end
   | Pexp_new cl ->
@@ -727,44 +727,36 @@ let report_error = function
       print_string "but is here applied to "; print_int provided;
       print_string " argument(s)";
       close_box()
-  | Label_mismatch(lid, actual, expected) ->
-      reset ();
-      mark_loops actual; mark_loops expected;
-      open_hovbox 0;
-      print_string "The label "; longident lid;
-      print_space(); print_string "belongs to the type"; print_space();
-      type_expr actual; print_space();
-      print_string "but is here mixed with labels of type"; print_space();
-      type_expr expected;
-      close_box()
-  | Pattern_type_clash(inferred, expected) ->
-      reset ();
-      mark_loops inferred; mark_loops expected;
-      open_hovbox 0;
-      print_string "This pattern matches values of type"; print_space();
-      type_expr inferred; print_space();
-      print_string "but is here used to match values of type"; print_space();
-      type_expr expected;
-      close_box()
+  | Label_mismatch(lid, trace) ->
+      unification_error trace
+        (function () ->
+           print_string "The label "; longident lid;
+           print_space(); print_string "belongs to the type")
+        (function () ->
+           print_string "but is here mixed with labels of type")
+  | Pattern_type_clash trace ->
+      unification_error trace
+        (function () ->
+           print_string "This pattern matches values of type")
+        (function () ->
+           print_string "but is here used to match values of type")
   | Multiply_bound_variable ->
       print_string "This variable is bound several times in this matching"
   | Orpat_not_closed ->
       print_string "A pattern with | must not bind variables"
-  | Expr_type_clash(inferred, expected) ->
-      reset ();
-      mark_loops inferred; mark_loops expected;
-      open_hovbox 0;
-      print_string "This expression has type"; print_space();
-      type_expr inferred; print_space();
-      print_string "but is here used with type"; print_space();
-      type_expr expected;
-      close_box()
+  | Expr_type_clash trace ->
+      unification_error trace
+        (function () ->
+           print_string "This expression has type")
+        (function () ->
+           print_string "but is here used with type")
   | Apply_non_function typ ->
       begin match (repr typ).desc with
         Tarrow(_, _) ->
           print_string "This function is applied to too many arguments"
       | _ ->
-          print_string "This expression is not a function, it cannot be applied"
+          print_string
+            "This expression is not a function, it cannot be applied"
       end
   | Label_multiply_defined lid ->
       print_string "The label "; longident lid;
diff --git a/typing/typecore.mli b/typing/typecore.mli
index 73760ef670..c16507f8ff 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -38,11 +38,11 @@ type error =
   | Unbound_constructor of Longident.t
   | Unbound_label of Longident.t
   | Constructor_arity_mismatch of Longident.t * int * int
-  | Label_mismatch of Longident.t * type_expr * type_expr
-  | Pattern_type_clash of type_expr * type_expr
+  | Label_mismatch of Longident.t * (type_expr * type_expr) list
+  | Pattern_type_clash of (type_expr * type_expr) list
   | Multiply_bound_variable
   | Orpat_not_closed
-  | Expr_type_clash of type_expr * type_expr
+  | Expr_type_clash of (type_expr * type_expr) list
   | Apply_non_function of type_expr
   | Label_multiply_defined of Longident.t
   | Label_missing
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index b76fea2c1f..374ce183a9 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -106,7 +106,7 @@ let rec transl_simple_type env fixed styp =
               occur env cstr
       	       	(Ctype.expand_abbrev env path tl (ref []) cstr.level)
             with
-	      Unify         -> raise(Error(styp.ptyp_loc, Recursive_type))
+	      Unify _       -> raise(Error(styp.ptyp_loc, Recursive_type))
 	    | Cannot_expand -> ()
 	    end;
 	    cstr.desc <- Tconstr(path, tl, ref []);
@@ -118,7 +118,7 @@ let rec transl_simple_type env fixed styp =
 	  List.iter2
            (fun ty (sty, ty') ->
 	      try Ctype.unify env (Ctype.instance ty) ty' with
-		Unify ->
+		Unify _ ->
 		  raise (Error(sty.ptyp_loc, Type_mismatch(ty, ty'))))
            decl.type_params (List.combine stl params)
       | _ ->
@@ -178,7 +178,7 @@ let rec transl_simple_type env fixed styp =
 	  List.iter2
            (fun ty (sty, ty') ->
 	      try Ctype.unify env (Ctype.instance ty) ty' with
-		Unify ->
+		Unify _ ->
 		  raise (Error(sty.ptyp_loc, Type_mismatch(ty, ty'))))
            decl.type_params (List.combine stl params)
       | _ ->