Index: testsuite/tests/typing-poly/poly.ml
===================================================================
--- testsuite/tests/typing-poly/poly.ml	(revision 15774)
+++ testsuite/tests/typing-poly/poly.ml	(working copy)
@@ -667,3 +667,19 @@

 match (fun x -> x), fun x -> x with x, y -> x, y;;
 match fun x -> x with x -> x, x;;
+
+(* PR#6747 *)
+(* ok *)
+let n = object
+  method m : 'x 'o. ([< `Foo of 'x] as 'o) -> 'x = fun x -> assert false
+end;;
+(* ok, but not with -principal *)
+let n =
+  object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
+(* fail *)
+let (n : < m : 'a. [< `Foo of int] -> 'a >) =
+  object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
+(* fail *)
+let (n : 'b -> < m : 'a . ([< `Foo of int] as 'b) -> 'a >) = fun x ->
+  object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
+
Index: typing/ctype.ml
===================================================================
--- typing/ctype.ml	(revision 15774)
+++ typing/ctype.ml	(working copy)
@@ -2744,6 +2744,19 @@
             if List.memq ty tl then remq tl tl' else ty :: remq tl tl'
       in
       let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in
+      (* PR#6744 *)
+      let split_univars =
+        List.partition
+          (fun ty -> try occur_univar !env ty; true with Unify _ -> false) in
+      let (tl1',tlu1) = split_univars tl1'
+      and (tl2',tlu2) = split_univars tl2' in
+      begin match tlu1, tlu2 with
+        [], [] -> ()
+      | (tu1::tlu1), (tu2::_) ->
+          (* Attempt to merge all the types containing univars *)
+          List.iter (unify env tu1) (tlu1@tlu2)
+      | (tu::_, []) | ([], tu::_) -> occur_univar !env tu
+      end;
       (* Is this handling of levels really principal? *)
       List.iter (update_level !env (repr more).level) (tl1' @ tl2');
       let e = ref None in