Amelioration de quelques messages d'erreur.

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

13 files changed, 259 insertions, 103 deletions

diff --git a/parsing/parser.mly b/parsing/parser.mly
index d93ec72a5..94c17342c 100644
--- a/parsing/parser.mly
+++ b/parsing/parser.mly
@@ -650,7 +650,7 @@ class_list:
 ;
 class_def:
         virtual_flag closed_flag
-      	type_parameters LIDENT simple_pattern_list self self_type EQUAL
+      	class_type_parameters LIDENT simple_pattern_list self self_type EQUAL
         constraints class_fields
 	  { { pcl_name = $4; pcl_param = $3; pcl_args = List.rev $5;
       	      pcl_self = $6; pcl_self_ty = $7; pcl_cstr = List.rev $9;
@@ -658,6 +658,10 @@ class_def:
 	      pcl_kind = $1; pcl_closed = $2;
       	      pcl_loc = symbol_loc () } }
 ;
+class_type_parameters:
+        type_parameters
+          { $1, symbol_loc () }
+;
 simple_pattern_list:
         simple_pattern
           { [$1] }
@@ -711,7 +715,8 @@ class_type_list:
       	  { [$1] }
 ;
 class_type:
-        virtual_flag closed_flag type_parameters LIDENT type_list self_type
+        virtual_flag closed_flag class_type_parameters LIDENT type_list
+        self_type
 	EQUAL
         constraints class_type_fields
 	  { { pcty_name = $4; pcty_param = $3; pcty_args = $5;
diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli
index b71163814..87b31c48c 100644
--- a/parsing/parsetree.mli
+++ b/parsing/parsetree.mli
@@ -115,7 +115,7 @@ type class_type_field =
 
 type class_type =
   { pcty_name: string;
-    pcty_param: string list;
+    pcty_param: string list * Location.t;
     pcty_args: core_type list;
     pcty_self: string option;
     pcty_cstr: (string * core_type * Location.t) list;
@@ -134,7 +134,7 @@ type class_field =
 
 type class_def =
   { pcl_name: string;
-    pcl_param: string list;
+    pcl_param: string list * Location.t;
     pcl_args: pattern list;
     pcl_self: string option;
     pcl_self_ty: string option;
diff --git a/typing/ctype.ml b/typing/ctype.ml
index af9425049..5af5bfb4c 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -18,6 +18,8 @@ open Asttypes
 open Typedtree
 
 exception Unify of (type_expr * type_expr) list
+exception Subtype of
+        (type_expr * type_expr) list * (type_expr * type_expr) list
 
 let current_level = ref 0
 let global_level = ref 1
@@ -134,7 +136,9 @@ let rec make_nongen ty =
     | Tarrow(t1, t2)    ->  make_nongen t1; make_nongen t2
     | Ttuple tl         -> List.iter make_nongen tl
     | Tconstr(p, tl, _) -> List.iter make_nongen tl
-    | Tobject (f, _)    -> make_nongen f
+    | Tobject(f, {contents = Some (_, p)})
+                        -> make_nongen f; List.iter make_nongen p
+    | Tobject(f, _)      -> make_nongen f
     | Tfield(_, t1, t2) -> make_nongen t1; make_nongen t2
     | Tnil              -> ()
     | Tlink _           -> fatal_error "Ctype.make_nongen"
@@ -320,6 +324,9 @@ let rec update_level level ty =
     | Tarrow(t1,t2)      -> update_level level t1; update_level level t2
     | Ttuple(ty_list)    -> List.iter (update_level level) ty_list
     | Tconstr(_, tl, _)  -> List.iter (update_level level) tl
+    | Tobject(f, {contents = Some (_, p)})
+                         -> update_level level f;
+                            List.iter (update_level level) p
     | Tobject (f, _)     -> update_level level f
     | Tfield(_, t1, t2)  -> update_level level t1; update_level level t2
     | Tnil               -> ()
@@ -376,7 +383,7 @@ let rec expand_root env 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 ->
+    Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
       { desc = Tobject (fi, ref None); level = ty.level }
   | _ ->
       ty
@@ -559,9 +566,6 @@ and unify_fields env ty1 ty2 =
     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 ->
@@ -968,52 +972,84 @@ let known_subtype t1 t2 =
 
 let rec subtype_rec env vars t1 t2 =
   if t1 == t2 then () else
-  if List.memq t1 vars or List.memq t2 vars then unify env t1 t2 else
+  if List.memq t1 vars or List.memq t2 vars then begin
+    try unify env t1 t2 with Unify trace ->
+      raise (Subtype ([List.hd trace], List.tl trace))
+  end else
+  try
     match (t1.desc, t2.desc) with
       (Tlink t1', _) ->
-        subtype_rec env vars t1' t2
+        begin try subtype_rec env vars t1' t2 with Subtype (tr1, tr2) ->
+          raise (Subtype (List.tl tr1, tr2))
+        end
     | (_, Tlink t2') ->
-        subtype_rec env vars t1 t2'
+        begin try subtype_rec env vars t1 t2' with Subtype (tr1, tr2) ->
+          raise (Subtype (List.tl tr1, tr2))
+        end
     | (Tvar, _) | (_, Tvar) ->
-        unify env t1 t2
+        begin try unify env t1 t2 with Unify trace ->
+          raise (Subtype ([List.hd trace], List.tl trace))
+        end
     | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
         subtype_rec env vars t2 t1; subtype_rec env vars u1 u2
     | (Ttuple tl1, Ttuple tl2) ->
         subtype_list env vars tl1 tl2
     | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) ->
-        if generic_abbrev env p1 then
-          subtype_rec env vars (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
-        else if generic_abbrev env p2 then
-          subtype_rec env vars t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
-        else
-          unify env t1 t2
+        if generic_abbrev env p1 then begin
+          try
+            subtype_rec env vars (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
+          with Subtype (tr1, tr2) ->
+            raise (Subtype (List.tl tr1, tr2))
+        end else if generic_abbrev env p2 then begin
+          try
+            subtype_rec env vars t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
+          with Subtype (tr1, tr2) ->
+            raise (Subtype (List.tl tr1, tr2))
+        end else begin
+          try unify env t1 t2 with Unify trace ->
+            raise (Subtype ([List.hd trace], List.tl trace))
+        end
+    | (Tconstr(p1, tl1, abbrev1), _) ->
+        if generic_abbrev env p1 then begin
+          try
+            subtype_rec env vars (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
+          with Subtype (tr1, tr2) ->
+            raise (Subtype (List.tl tr1, tr2))
+        end else begin
+          try unify env t1 t2 with Unify trace ->
+            raise (Subtype ([List.hd trace], List.tl trace))
+        end
+    | (_, Tconstr(p2, tl2, abbrev2)) ->
+        if generic_abbrev env p2 then begin
+          try
+            subtype_rec env vars t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
+          with Subtype (tr1, tr2) ->
+            raise (Subtype (List.tl tr1, tr2))
+       end else begin
+          try unify env t1 t2 with Unify trace ->
+            raise (Subtype ([List.hd trace], List.tl trace))
+        end
     | (Tobject (f1, _), Tobject (f2, _)) ->
         if not (known_subtype t1 t2) then begin
-          if opened f1 & opened f2 then
-            unify env t1 t2
-          else begin
+          if opened f1 & opened f2 then begin
+            try unify env t1 t2 with Unify trace ->
+              raise (Subtype ([List.hd trace], List.tl trace))
+          end else begin
             subtypes := (t1, t2) :: !subtypes;
             subtype_fields env vars f1 f2
           end
         end
-    | (Tconstr(p1, tl1, abbrev1), _) ->
-        if generic_abbrev env p1 then
-          subtype_rec env vars (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
-        else
-          unify env t1 t2
-    | (_, Tconstr(p2, tl2, abbrev2)) ->
-        if generic_abbrev env p2 then
-          subtype_rec env vars t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
-        else
-          unify env t1 t2
     | (_, _) ->
-        raise (Unify [])
+        raise (Subtype ([], []))
+  with
+    Subtype (tr1, tr2) ->
+      raise (Subtype ((t1, t2)::tr1, tr2))
 
 and subtype_list env vars tl1 tl2 =
   try
     List.iter2 (subtype_rec env vars) tl1 tl2
   with Invalid_argument _ ->
-    raise (Unify [])
+    raise (Subtype ([], []))
 
 and subtype_fields env vars ty1 ty2 =
   let (fields1, rest1) = flatten_fields ty1 in
@@ -1024,7 +1060,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 (Subtype ([], []))
   | _      -> fatal_error "Ctype.subtype_fields (1)"
   end;
   begin match rest2.desc with
@@ -1039,7 +1075,11 @@ and subtype_fields env vars ty1 ty2 =
 
 let subtype env vars ty1 ty2 =
   subtypes := [];
-  subtype_rec env vars ty1 ty2;
+  begin try
+    subtype_rec env vars ty1 ty2
+  with Subtype (tr1, tr2) ->
+    raise (Subtype (expand_trace env tr1, filter_trace (expand_trace env tr2)))
+  end;
   subtypes := []
 
 (* Remove dependencies *)
@@ -1358,6 +1398,68 @@ let closed_schema ty =
     visited := [];
     res
 
+type closed_schema_result = Var of type_expr | Row_var of type_expr
+exception Failed of closed_schema_result
+
+let rec closed_schema_rec ty =
+  let ty = repr ty in
+  match ty.desc with
+    Tvar -> if ty.level != generic_level then raise (Failed (Var ty))
+  | Tarrow(t1, t2) -> closed_schema_rec t1; closed_schema_rec t2
+  | Ttuple tl -> List.iter closed_schema_rec tl
+  | Tconstr(p, tl, _) ->
+      if not (List.memq ty !visited) then begin
+        visited := ty::!visited;
+        List.iter closed_schema_rec tl
+      end
+  | Tobject(f, {contents = Some (_, p)}) ->
+      if not (List.memq ty !visited) then begin
+        visited := ty::!visited;
+        begin try closed_schema_rec f with
+          Failed (Row_var v) -> raise (Failed (Var v))
+        | Failed (Var v) -> raise (Failed (Row_var v))
+        end;
+        List.iter closed_schema_rec p
+      end
+  | Tobject(f, _) ->
+      if not (List.memq ty !visited) then begin
+        visited := ty::!visited;
+        try closed_schema_rec f with
+          Failed (Row_var v) -> raise (Failed (Var v))
+        | Failed (Var v) -> raise (Failed (Row_var v))
+      end
+  | Tfield(_, t1, t2) ->
+      begin try
+        closed_schema_rec t1
+      with
+        Failed (Row_var v) -> raise (Failed (Var v))
+      | Failed (Var v) -> raise (Failed (Row_var v))
+      end;
+      closed_schema_rec t2
+  | Tnil ->
+      ()
+  | Tlink _           -> fatal_error "Ctype.closed_schema"
+
+let closed_schema ty =
+  visited := [];
+  try
+    closed_schema_rec ty;
+    visited := [];
+    true
+  with Failed _ ->
+    visited := [];
+    false
+
+let closed_schema_verbose ty =
+  visited := [];
+  try
+    closed_schema_rec ty;
+    visited := [];
+    None
+  with Failed status ->
+    visited := [];
+    Some status
+
 let is_generic ty =
   let ty = repr ty in
   match ty.desc with
diff --git a/typing/ctype.mli b/typing/ctype.mli
index e0d3299e7..12f80e98f 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -54,11 +54,13 @@ val instance_class:
       	class_type ->
         type_expr list * type_expr list *
         (mutable_flag * type_expr) Vars.t * type_expr
-val expand_abbrev :
+val expand_abbrev:
         Env.t -> Path.t -> type_expr list -> (Path.t * type_expr) list ref ->
 	int -> type_expr
 	(* Expand an abbreviation *)
-val occur : Env.t -> type_expr -> type_expr -> unit
+val full_expand: Env.t -> type_expr -> type_expr
+val expand_root: Env.t -> type_expr -> type_expr
+val occur: Env.t -> type_expr -> type_expr -> unit
         (* [occur env var ty] Raise [Unify] if [var] occurs in [ty] *)
 val unify: Env.t -> type_expr -> type_expr -> unit
         (* Unify the two types given. Raise [Unify] if not possible. *)
@@ -79,6 +81,8 @@ val enlarge_type: Env.t -> type_expr list -> type_expr -> type_expr
       	(* Make a type larger *)
 val subtype : Env.t -> type_expr list -> type_expr -> type_expr -> unit
 val closed_schema: type_expr -> bool
+type closed_schema_result = Var of type_expr | Row_var of type_expr
+val closed_schema_verbose: type_expr -> closed_schema_result option
         (* Check whether the given type scheme contains no non-generic
            type variables *)
 val nondep_type: Env.t -> Ident.t -> type_expr -> type_expr
@@ -103,7 +107,6 @@ val close_object: type_expr -> unit
 val set_object_name:
       	type_expr -> type_expr list -> Ident.t -> unit
 val remove_object_name: type_expr -> unit
-val expand_root: Env.t -> type_expr -> type_expr
 val correct_abbrev: Env.t -> Ident.t -> type_expr list -> type_expr -> unit
 val unroll_abbrev: Ident.t -> type_expr list -> type_expr -> type_expr
 val is_generic: type_expr -> bool
@@ -114,6 +117,8 @@ val none: type_expr
         (* A dummy type expression *)
 
 exception Unify of (type_expr * type_expr) list
+exception Subtype of
+        (type_expr * type_expr) list * (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 5597855d5..c356c6889 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -536,31 +536,33 @@ let type_expansion t t' =
     close_box ()
   end
 
-let rec unification_trace =
+let rec trace fst txt =
   function
     (t1, t1')::(t2, t2')::rem ->
-      print_cut ();
+      if not fst then
+        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;
+      txt (); print_break 1 2;
       type_expansion t2 t2';
       close_box ();
-      unification_trace rem
+      trace false txt rem
   | _ ->
       ()
 
-let unification_error trace txt1 txt2 =
+let unification_error tr txt1 txt2 =
   reset ();
   List.iter
     (function (t, t') -> mark_loops t; if t != t' then mark_loops t')
-    trace;
+    tr;
   open_hovbox 0;
-  let (t1, t1') = List.hd trace in
-  let (t2, t2') = List.hd (List.tl trace) in
+  let (t1, t1') = List.hd tr in
+  let (t2, t2') = List.hd (List.tl tr) 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))
+  trace false (fun _ -> print_string "is not compatible with type")
+        (List.tl (List.tl tr))
diff --git a/typing/printtyp.mli b/typing/printtyp.mli
index c1e7e08b0..638f0ea86 100644
--- a/typing/printtyp.mli
+++ b/typing/printtyp.mli
@@ -30,6 +30,8 @@ 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 type_expansion: type_expr -> type_expr -> unit
+val trace: bool -> (unit -> unit) -> (type_expr * type_expr) list -> 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 d773b8ceb..915906886 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -26,7 +26,8 @@ type error =
   | Virtual_class of string * string
   | Closed_class of string
   | Closed_ancestor of string * Path.t * string
-  | Non_closed of Ident.t * type_expr list * type_expr
+  | Non_closed of Ident.t * type_expr list * type_expr *
+                  Ctype.closed_schema_result
   | Mutable_var of string
   | Undefined_var of string
   | Variable_type_mismatch of string * (type_expr * type_expr) list
@@ -118,7 +119,9 @@ let make_stub env cl =
   Ctype.generalize concr;
 
   (* Temporary object type *)
-  let temp_obj_params = List.map (fun _ -> Ctype.newvar ()) cl.pcl_param in
+  let temp_obj_params =
+    List.map (fun _ -> Ctype.newvar ()) (fst cl.pcl_param)
+  in
   let temp_obj = Ctype.instance self in
   let obj_temp_abbrev =
     { type_params = temp_obj_params;
@@ -136,7 +139,7 @@ let make_stub env cl =
       (temp_obj_params,
        Ctype.newty (Tconstr(Path.Pident obj_id, temp_obj_params, ref [])))
     else begin
-      let params = List.map (fun _ -> Ctype.newvar ()) cl.pcl_param in
+      let params = List.map (fun _ -> Ctype.newvar ()) (fst cl.pcl_param) in
       let ty = Ctype.instance self in
       Ctype.set_object_name ty params obj_id;
       (params, ty)
@@ -378,16 +381,16 @@ let transl_class temp_env env
 
   (* Introduce parameters *)
   let params =
-    try List.map enter_type_variable cl.pcl_param with Already_bound ->
-      raise(Error(cl.pcl_loc, Repeated_parameter)) in
+    try
+      List.map (enter_type_variable true) (fst cl.pcl_param)
+    with Already_bound ->
+      raise(Error(snd cl.pcl_param, Repeated_parameter))
+  in
 
   (* Bind self type variable *)
-  begin try
-    match cl.pcl_self_ty with
-      Some v -> Ctype.unify temp_env self (enter_type_variable v)
+  begin match cl.pcl_self_ty with
+      Some v -> Ctype.unify temp_env self (enter_type_variable false v)
     | None   -> ()
-  with Already_bound ->
-    raise(Error(cl.pcl_loc, Repeated_parameter))
   end;
 
   (* Add constraints *)
@@ -557,9 +560,12 @@ let make_abbrev env
   Ctype.close_object obj_ty;
   Ctype.end_def ();
   List.iter Ctype.generalize obj_ty_params;
-  if not (Ctype.closed_schema obj_ty) then
-    raise(Error(cl.pcl_loc,
-                Non_closed(obj_id, obj_ty_params, obj_ty)));
+  begin match Ctype.closed_schema_verbose obj_ty with
+    None -> ()
+  | Some v ->
+      raise(Error(cl.pcl_loc,
+                  Non_closed(obj_id, obj_ty_params, obj_ty, v)))
+  end;
   Ctype.generalize obj_ty;
   let obj_abbrev =
     { type_params = obj_ty_params;
@@ -596,7 +602,7 @@ let transl_classes env cl =
 let enter_class env cl =
   let abstr_type =
     { type_params = [];
-      type_arity = List.length cl.pcty_param;
+      type_arity = List.length (fst cl.pcty_param);
       type_kind = Type_abstract;
       type_manifest = None }
   in
@@ -745,17 +751,16 @@ let build_abbrevs temp_env env (cl, obj_id) =
 
   (* Introduce parameters *)
   let params =
-    try List.map enter_type_variable cl.pcty_param with Already_bound ->
-      raise(Error(cl.pcty_loc, Repeated_parameter))
+    try
+      List.map (enter_type_variable true) (fst cl.pcty_param)
+    with Already_bound ->
+      raise(Error(snd cl.pcty_param, Repeated_parameter))
   in
 
   (* Bind self type variable *)
-  begin try
-    match cl.pcty_self with
-      Some v -> Ctype.unify temp_env self (enter_type_variable v)
+  begin match cl.pcty_self with
+      Some v -> Ctype.unify temp_env self (enter_type_variable false v)
     | None   -> ()
-  with Already_bound ->
-    raise(Error(cl.pcty_loc, Repeated_parameter))
   end;
 
   (* Translate argument types *)
@@ -794,9 +799,12 @@ let build_abbrevs temp_env env (cl, obj_id) =
   Ctype.close_object obj_ty;
   Ctype.end_def ();
   List.iter Ctype.generalize obj_params;
-  if not (Ctype.closed_schema obj_ty) then
-    raise(Error(cl.pcty_loc,
-                Non_closed(obj_id, obj_params, obj_ty)));
+  begin match Ctype.closed_schema_verbose obj_ty with
+    None -> ()
+  | Some v ->
+      raise(Error(cl.pcty_loc,
+                  Non_closed(obj_id, obj_params, obj_ty, v)))
+  end;
   Ctype.generalize obj_ty;
   let obj_abbrev =
     { type_params = obj_params;
@@ -872,10 +880,10 @@ let build_class_type env
 
   (* Re-introduce parameters and bind self type variable *)
   List.iter2
-    (fun v ty -> Ctype.unify env (enter_type_variable v) ty)
-    cl.pcty_param params;
+    (fun v ty -> Ctype.unify env (enter_type_variable true v) ty)
+    (fst cl.pcty_param) params;
   begin match cl.pcty_self with
-    Some v -> Ctype.unify env (enter_type_variable v) self
+    Some v -> Ctype.unify env (enter_type_variable false v) self
   | None   -> ()
   end;
 
@@ -976,12 +984,18 @@ let report_error = function
       Printtyp.path anc; print_space ();
       print_string "which has no method"; print_space ();
       print_string met
-  | Non_closed (id, args, typ) ->
+  | Non_closed (id, args, typ, var) ->
       open_hovbox 0;
       Printtyp.reset ();
       Printtyp.mark_loops typ;
-      print_string
-        "Some type variables are not bound in implicit type definition";
+      begin match var with
+        Ctype.Var v ->
+          print_string "The type variable"; print_space ();
+          Printtyp.type_expr v; print_space ();
+          print_string "is not bound in implicit type definition"
+      | _ ->
+          print_string "Unbound row variable in implicit type definition"
+      end;
       print_break 1 2;
       open_hovbox 0;
       Printtyp.type_expr (Ctype.newty (Tconstr(Path.Pident id, args, ref [])));
@@ -990,7 +1004,7 @@ let report_error = function
       close_box ();
       close_box ();
       print_space ();
-      print_string "They should all be captured by a class type parameter."
+      print_string "It should be captured by a class type parameter"
   | Mutable_var v ->
       print_string "The variable"; print_space ();
       print_string v; print_space ();
diff --git a/typing/typeclass.mli b/typing/typeclass.mli
index 163e01dbe..90ee2f32a 100644
--- a/typing/typeclass.mli
+++ b/typing/typeclass.mli
@@ -33,7 +33,8 @@ type error =
   | Virtual_class of string * string
   | Closed_class of string
   | Closed_ancestor of string * Path.t * string
-  | Non_closed of Ident.t * type_expr list * type_expr
+  | Non_closed of Ident.t * type_expr list * type_expr *
+                  Ctype.closed_schema_result
   | Mutable_var of string
   | Undefined_var of string
   | Variable_type_mismatch of string * (type_expr * type_expr) list
diff --git a/typing/typecore.ml b/typing/typecore.ml
index d01f440f4..1f56c9493 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -40,9 +40,10 @@ type error =
   | Virtual_class of Longident.t
   | Unbound_instance_variable of string
   | Instance_variable_not_mutable of string
-  | Not_subtype of type_expr * type_expr
+  | Not_subtype of (type_expr * type_expr) list * (type_expr * type_expr) list
   | Outside_class
   | Value_multiply_overridden of string
+  | Coercion_failure of type_expr * type_expr * (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
@@ -454,25 +455,32 @@ let rec type_exp env sexp =
         exp_loc = sexp.pexp_loc;
         exp_type = instance Predef.type_unit }
   | Pexp_constraint(sarg, sty, sty') ->
-      let (ty, ty') =
+      let (arg, ty') =
         match (sty, sty') with
-      	  (None, None) ->
-	    none, none
+      	  (None, None) ->               (* Case actually unused *)
+            let arg = type_exp env sarg in
+	    (arg, arg.exp_type)
 	| (Some sty, None) ->
             let ty = Typetexp.transl_simple_type env false sty in
-	    (ty, ty)
+            (type_expect env sarg ty, ty)
 	| (None, Some sty') ->
             let ty' = Typetexp.transl_simple_type env false sty' in
-            (enlarge_type env (Typetexp.type_variable_list ()) ty', ty')
+            let ty = enlarge_type env (Typetexp.type_variable_list ()) ty' in
+            let arg = type_exp env sarg in
+            begin try Ctype.unify env arg.exp_type ty with Unify trace ->
+              raise(Error(sarg.pexp_loc,
+                    Coercion_failure(ty', full_expand env ty', trace)))
+            end;
+            (arg, ty')
 	| (Some sty, Some sty') ->
             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 _ ->
-	        raise(Error(sexp.pexp_loc, Not_subtype(ty, ty')))
+	      Subtype (tr1, tr2) ->
+	        raise(Error(sexp.pexp_loc, Not_subtype(tr1, tr2)))
 	    end;
-	    (ty, ty')
-      in let arg = type_expect env sarg ty in
+	    (type_expect env sarg ty, ty')
+      in
       { exp_desc = arg.exp_desc;
         exp_loc = arg.exp_loc;
         exp_type = ty' }
@@ -783,16 +791,30 @@ let report_error = function
   | Instance_variable_not_mutable v ->
       print_string " The instance variable "; print_string v;
       print_string " is not mutable"
-  | Not_subtype(ty, ty') ->
+  | Not_subtype(tr1, tr2) ->
       reset ();
-      mark_loops ty; mark_loops ty';
-      open_hovbox 0;
-      type_expr ty; print_space();
-      print_string "is not a subtype of"; print_space ();
-      type_expr ty';
-      close_box()
+      List.iter
+        (function (t, t') -> mark_loops t; if t != t' then mark_loops t')
+        tr1;
+      List.iter
+        (function (t, t') -> mark_loops t; if t != t' then mark_loops t')
+        tr2;
+      trace true (fun _ -> print_string "is not a subtype of") tr1;
+      trace false (fun _ -> print_string "is not compatible with type") tr2
   | Outside_class ->
       print_string "Object duplication outside a class definition."
   | Value_multiply_overridden v ->
       print_string "The instance variable "; print_string v;
       print_string " is overridden several times"
+  | Coercion_failure (ty, ty', trace) ->
+      unification_error trace
+        (function () ->
+           mark_loops ty; if ty' != ty then mark_loops ty';
+           print_string "This expression cannot be coerced to type";
+           print_break 1 2;
+           type_expansion ty ty';
+           print_string ";";
+           print_space ();
+           print_string "it has type")
+        (function () ->
+           print_string "but is here used with type")
diff --git a/typing/typecore.mli b/typing/typecore.mli
index c16507f8f..8ef6bcbfb 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -53,9 +53,10 @@ type error =
   | Virtual_class of Longident.t
   | Unbound_instance_variable of string
   | Instance_variable_not_mutable of string
-  | Not_subtype of type_expr * type_expr
+  | Not_subtype of (type_expr * type_expr) list * (type_expr * type_expr) list
   | Outside_class
   | Value_multiply_overridden of string
+  | Coercion_failure of type_expr * type_expr * (type_expr * type_expr) list
 
 exception Error of Location.t * error
 
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index f87df145d..e4bad3f52 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -57,7 +57,7 @@ let transl_declaration env (name, sdecl) id =
   Ctype.begin_def();
   let params =
     try
-      List.map enter_type_variable sdecl.ptype_params
+      List.map (enter_type_variable true) sdecl.ptype_params
     with Already_bound ->
       raise(Error(sdecl.ptype_loc, Repeated_parameter)) in
   let decl =
@@ -190,7 +190,7 @@ let transl_with_constraint env sdecl =
   Ctype.begin_def();
   let params =
     try
-      List.map enter_type_variable sdecl.ptype_params
+      List.map (enter_type_variable true) sdecl.ptype_params
     with Already_bound ->
       raise(Error(sdecl.ptype_loc, Repeated_parameter)) in
   Ctype.end_def();
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 374ce183a..e3c46a902 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -40,9 +40,11 @@ let reset_type_variables () =
   reset_global_level ();
   type_variables := Tbl.empty
 
-let enter_type_variable name =
+let enter_type_variable strict name =
   try
-    Tbl.find name !type_variables; raise Already_bound
+    let v = Tbl.find name !type_variables in
+    if strict then raise Already_bound;
+    v
   with Not_found ->
     let v = new_global_var() in
     type_variables := Tbl.add name v !type_variables;
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index cf48b57b4..05cbb6eb2 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -18,7 +18,7 @@ val transl_simple_type:
 val transl_type_scheme:
         Env.t -> Parsetree.core_type -> Typedtree.type_expr
 val reset_type_variables: unit -> unit
-val enter_type_variable: string -> Typedtree.type_expr
+val enter_type_variable: bool -> string -> Typedtree.type_expr
 val type_variable : Location.t -> string -> Typedtree.type_expr
 val type_variable_list : unit -> Typedtree.type_expr list