10 files changed, 76 insertions, 6 deletions

diff --git a/testsuite/tests/typing-objects/pr5619_bad.ml b/testsuite/tests/typing-objects/pr5619_bad.ml
new file mode 100644
index 000000000..fbecc927c
--- /dev/null
+++ b/testsuite/tests/typing-objects/pr5619_bad.ml
@@ -0,0 +1,29 @@
+class type foo_t =
+  object
+    method foo: string
+  end
+
+type 'a name = 
+    Foo: foo_t name
+  | Int: int name
+;;
+
+class foo =
+  object(self)
+    method foo = "foo"
+    method cast =
+      function
+          Foo -> (self :> <foo : string>)
+        | _ -> raise Exit
+  end
+;;
+
+class foo: foo_t =
+  object(self)
+    method foo = "foo"
+    method cast: type a. a name -> a =
+      function
+          Foo -> (self :> foo_t)
+        | _ -> ((raise Exit) : a)
+  end
+;;
diff --git a/testsuite/tests/typing-objects/pr5619_bad.ml.principal.reference b/testsuite/tests/typing-objects/pr5619_bad.ml.principal.reference
new file mode 100644
index 000000000..48777229c
--- /dev/null
+++ b/testsuite/tests/typing-objects/pr5619_bad.ml.principal.reference
@@ -0,0 +1,18 @@
+
+#                 class type foo_t = object method foo : string end
+type 'a name = Foo : foo_t name | Int : int name
+#                   class foo :
+  object method cast : foo_t name -> < foo : string > method foo : string end
+#                   Characters 22-184:
+  ..object(self)
+      method foo = "foo"
+      method cast: type a. a name -> a =
+        function
+            Foo -> (self :> foo_t)
+          | _ -> ((raise Exit) : a)
+    end
+Error: The class type
+         object method cast : 'a name -> 'a method foo : string end
+       is not matched by the class type foo_t
+       The public method cast cannot be hidden
+# 
diff --git a/testsuite/tests/typing-objects/pr5619_bad.ml.reference b/testsuite/tests/typing-objects/pr5619_bad.ml.reference
new file mode 100644
index 000000000..48777229c
--- /dev/null
+++ b/testsuite/tests/typing-objects/pr5619_bad.ml.reference
@@ -0,0 +1,18 @@
+
+#                 class type foo_t = object method foo : string end
+type 'a name = Foo : foo_t name | Int : int name
+#                   class foo :
+  object method cast : foo_t name -> < foo : string > method foo : string end
+#                   Characters 22-184:
+  ..object(self)
+      method foo = "foo"
+      method cast: type a. a name -> a =
+        function
+            Foo -> (self :> foo_t)
+          | _ -> ((raise Exit) : a)
+    end
+Error: The class type
+         object method cast : 'a name -> 'a method foo : string end
+       is not matched by the class type foo_t
+       The public method cast cannot be hidden
+# 
diff --git a/typing/btype.ml b/typing/btype.ml
index c9bdbf04d..769535bcb 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -57,6 +57,8 @@ let newmarkedgenvar () =
 let is_Tvar = function {desc=Tvar _} -> true | _ -> false
 let is_Tunivar = function {desc=Tunivar _} -> true | _ -> false
 
+let dummy_method = "*dummy method*"
+
 (**** Representative of a type ****)
 
 let rec field_kind_repr =
diff --git a/typing/btype.mli b/typing/btype.mli
index e2e4c9d6d..014f954eb 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -43,6 +43,7 @@ val newmarkedgenvar: unit -> type_expr
 
 val is_Tvar: type_expr -> bool
 val is_Tunivar: type_expr -> bool
+val dummy_method: label
 
 val repr: type_expr -> type_expr
         (* Return the canonical representative of a type. *)
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 41fa5f02f..925dc225f 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -240,8 +240,6 @@ let is_datatype decl=
 
 (**** Object field manipulation. ****)
 
-let dummy_method = "*dummy method*"
-
 let object_fields ty =
   match (repr ty).desc with
     Tobject (fields, _) -> fields
@@ -733,7 +731,8 @@ let rec update_level env level ty =
         end;
         set_level ty level;
         iter_type_expr (update_level env level) ty
-    | Tfield(lab, _, _, _) when lab = dummy_method ->
+    | Tfield(lab, _, ty1, _)
+      when lab = dummy_method && (repr ty1).level > level->
         raise (Unify [(ty, newvar2 level)])
     | _ ->
         set_level ty level;
diff --git a/typing/ctype.mli b/typing/ctype.mli
index c4d4ff13a..c0f165040 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -55,7 +55,6 @@ val none: type_expr
 val repr: type_expr -> type_expr
         (* Return the canonical representative of a type. *)
 
-val dummy_method: label
 val object_fields: type_expr -> type_expr
 val flatten_fields:
         type_expr -> (string * field_kind * type_expr) list * type_expr
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 84c0d1942..09caa227c 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -992,7 +992,7 @@ let rec mismatch unif = function
 
 let explanation unif t3 t4 ppf =
   match t3.desc, t4.desc with
-  | Tfield _, Tvar _ | Tvar _, Tfield _ ->
+  | Ttuple [], Tvar _ | Tvar _, Ttuple [] ->
       fprintf ppf "@,Self type cannot escape its class"
   | Tconstr (p, tl, _), Tvar _
     when unif && t4.level < Path.binding_time p ->
diff --git a/typing/subst.ml b/typing/subst.ml
index 4a84a4e28..f023b708f 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -110,6 +110,10 @@ let rec typexp s ty =
                         None -> None
                       | Some (p, tl) ->
                           Some (type_path s p, List.map (typexp s) tl)))
+      | Tfield (m, k, t1, t2)
+        when s == identity && ty.level < generic_level && m = dummy_method ->
+          (* not allowed to lower the level of the dummy method *)
+          Tfield (m, k, t1, typexp s t2)
       | Tvariant row ->
           let row = row_repr row in
           let more = repr row.row_more in
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 5610c3e94..5333f4126 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -62,7 +62,7 @@ exception Error of Location.t * error
    Self type have a dummy private method, thus preventing it to become
    closed.
 *)
-let dummy_method = Ctype.dummy_method
+let dummy_method = Btype.dummy_method
 
 (*
    Path associated to the temporary class type of a class being typed