Merge pull request #1273 from garrigue/fix_mpr7519

Fix mpr7519

4 files changed, 52 insertions, 7 deletions

diff --git a/Changes b/Changes
index 1266afbb62..7d7eb9c6e3 100644
--- a/Changes
+++ b/Changes
@@ -387,6 +387,9 @@ Working version
 - MPR#7513: List.compare_length_with mishandles negative numbers / overflow
   (Fabrice Le Fessant, report by Jeremy Yallop)
 
+- MPR#7519: Incorrect rejection of program due to faux scope escape
+  (Jacques Garrigue, report by Markus Mottl)
+
 - MPR#7540, GPR#1179: Fixed setting of breakpoints within packed modules
   for ocamldebug
   (Hugo Herbelin, review by Gabriel Scherer, Damien Doligez)
diff --git a/testsuite/tests/typing-modules-bugs/pr7519_ok.ml b/testsuite/tests/typing-modules-bugs/pr7519_ok.ml
new file mode 100644
index 0000000000..b01da15055
--- /dev/null
+++ b/testsuite/tests/typing-modules-bugs/pr7519_ok.ml
@@ -0,0 +1,18 @@
+module Gen_spec = struct type 't extra = unit end
+
+module type S = sig
+  module Spec : sig type 't extra = unit end
+
+  type t
+  val make : unit -> t Spec.extra
+end (* S *)
+
+module Make () : S with module Spec := Gen_spec = struct
+  type t = int
+  let make () = ()
+end (* Make *)
+
+let () =
+  let module M = Make () in
+  M.make ()
+  (* (M.make () : unit) *)
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 8ca5389d9f..5c4e5e5ad8 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -699,7 +699,7 @@ let rec normalize_package_path env p =
           normalize_package_path env (Path.Pdot (p1', s, n))
       | _ -> p
 
-let rec update_level env level ty =
+let rec update_level env level expand ty =
   let ty = repr ty in
   if ty.level > level then begin
     begin match Env.gadt_instance_level env ty with
@@ -712,22 +712,30 @@ let rec update_level env level ty =
         begin try
           (* if is_newtype env p then raise Cannot_expand; *)
           link_type ty (!forward_try_expand_once env ty);
-          update_level env level ty
+          update_level env level expand ty
         with Cannot_expand ->
           (* +++ Levels should be restored... *)
           (* Format.printf "update_level: %i < %i@." level (get_level env p); *)
           if level < get_level env p then raise (Unify [(ty, newvar2 level)]);
-          iter_type_expr (update_level env level) ty
+          iter_type_expr (update_level env level expand) ty
         end
+    | Tconstr(_, _ :: _, _) when expand ->
+        begin try
+          link_type ty (!forward_try_expand_once env ty);
+          update_level env level expand ty
+        with Cannot_expand ->
+          set_level ty level;
+          iter_type_expr (update_level env level expand) ty
+        end          
     | Tpackage (p, nl, tl) when level < Path.binding_time p ->
         let p' = normalize_package_path env p in
         if Path.same p p' then raise (Unify [(ty, newvar2 level)]);
         log_type ty; ty.desc <- Tpackage (p', nl, tl);
-        update_level env level ty
+        update_level env level expand ty
     | Tobject(_, ({contents=Some(p, _tl)} as nm))
       when level < get_level env p ->
         set_name nm None;
-        update_level env level ty
+        update_level env level expand ty
     | Tvariant row ->
         let row = row_repr row in
         begin match row.row_name with
@@ -737,14 +745,27 @@ let rec update_level env level ty =
         | _ -> ()
         end;
         set_level ty level;
-        iter_type_expr (update_level env level) ty
+        iter_type_expr (update_level env level expand) ty
     | Tfield(lab, _, ty1, _)
       when lab = dummy_method && (repr ty1).level > level ->
         raise (Unify [(ty1, newvar2 level)])
     | _ ->
         set_level ty level;
         (* XXX what about abbreviations in Tconstr ? *)
-        iter_type_expr (update_level env level) ty
+        iter_type_expr (update_level env level expand) ty
+  end
+
+(* First try without expanding, then expand everything,
+   to avoid combinatorial blow-up *)
+let update_level env level ty =
+  let ty = repr ty in
+  if ty.level > level then begin
+    let snap = snapshot () in
+    try
+      update_level env level false ty
+    with Unify _ ->
+      backtrack snap;
+      update_level env level true ty
   end
 
 (* Generalize and lower levels of contravariant branches simultaneously *)
diff --git a/typing/typecore.ml b/typing/typecore.ml
index a1e47a10e6..74a82c355a 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -2808,6 +2808,9 @@ and type_expect_ ?in_function ?(recarg=Rejected) env sexp ty_expected =
          i.e. if generative types rooted at id show up in the
          type body.exp_type.  Thus, this unification enforces the
          scoping condition on "let module". *)
+      (* Note that this code will only be reached if ty_expected
+         is a generic type variable, otherwise the error will occur
+         above in type_expect *)
       begin try
         Ctype.unify_var new_env ty body.exp_type
       with Unify _ ->