New attempt at fixing MPR#7726 (#1676)

* Fix MPR#7726 by re-checking recursive modules in signatures after substitution
* Check module applications when translating types in Typetexp
* Check all results of functor applications lazily
* Reduce the overhead of checking module types by building the environment lazily

.depend

@@ -466,10 +466,11 @@ typing/typemod.cmx : utils/warnings.cmx typing/typetexp.cmx typing/types.cmx \
     typing/cmi_format.cmx utils/clflags.cmx parsing/builtin_attributes.cmx \
     typing/btype.cmx parsing/attr_helper.cmx parsing/asttypes.cmi \
     typing/annot.cmi typing/typemod.cmi
-typing/typemod.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
-    parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
-    parsing/location.cmi typing/includemod.cmi typing/ident.cmi \
-    typing/env.cmi typing/cmi_format.cmi parsing/asttypes.cmi
+typing/typemod.cmi : typing/types.cmi typing/typedtree.cmi \
+    typing/typedecl.cmi typing/path.cmi parsing/parsetree.cmi utils/misc.cmi \
+    parsing/longident.cmi parsing/location.cmi typing/includemod.cmi \
+    typing/ident.cmi typing/env.cmi typing/cmi_format.cmi \
+    parsing/asttypes.cmi
 typing/typeopt.cmo : typing/types.cmi typing/typedtree.cmi \
     typing/typedecl.cmi typing/predef.cmi typing/path.cmi bytecomp/lambda.cmi \
     typing/ident.cmi typing/env.cmi typing/ctype.cmi utils/config.cmi \

Changes

@@ -182,6 +182,9 @@ Working version
 
 ### Bug fixes:
 
+- MPR#7726, GPR#1676: Recursive modules, equi-recursive types and stack overflow
+  (Jacques Garrigue, report by Jeremy Yallop, review by Leo White)
+
 - GPR#1719: fix Pervasives.LargeFile functions under Windows.
   (Alain Frisch)
 

ocamldoc/stdlib_non_prefixed/.depend

@@ -169,9 +169,9 @@ typedtree.cmi : types.cmi primitive.cmi path.cmi parsetree.cmi longident.cmi \
     location.cmi ident.cmi env.cmi asttypes.cmi
 typedtreeIter.cmi : typedtree.cmi asttypes.cmi
 typedtreeMap.cmi : typedtree.cmi
-typemod.cmi : types.cmi typedtree.cmi path.cmi parsetree.cmi misc.cmi \
-    longident.cmi location.cmi includemod.cmi ident.cmi format.cmi env.cmi \
-    cmi_format.cmi asttypes.cmi
+typemod.cmi : types.cmi typedtree.cmi typedecl.cmi path.cmi parsetree.cmi \
+    misc.cmi longident.cmi location.cmi includemod.cmi ident.cmi format.cmi \
+    env.cmi cmi_format.cmi asttypes.cmi
 typeopt.cmi : types.cmi typedtree.cmi path.cmi lambda.cmi env.cmi
 types.cmi : set.cmi primitive.cmi path.cmi parsetree.cmi map.cmi \
     longident.cmi location.cmi ident.cmi asttypes.cmi

testsuite/tests/typing-modules/.gitattributes

@@ -0,0 +1 @@
+pr7726.ml ocaml-typo=long-line,missing-header

testsuite/tests/typing-modules/ocamltests

@@ -7,6 +7,7 @@ pr5911.ml
 pr6394.ml
 pr7207.ml
 pr7348.ml
+pr7726.ml
 pr7787.ml
 printing.ml
 recursive.ml

testsuite/tests/typing-modules/pr7726.ml

@@ -0,0 +1,150 @@
+(* TEST
+   * expect
+*)
+
+module type T = sig type t end
+module Fix(F:(T -> T)) = struct
+  module rec Fixed : T with type t = F(Fixed).t = F(Fixed)
+end;;
+[%%expect{|
+module type T = sig type t end
+module Fix :
+  functor (F : T -> T) ->
+    sig module rec Fixed : sig type t = F(Fixed).t end end
+|}]
+
+module T1 = Fix(functor (X:sig type t end) -> struct type t = X.t option end);;
+[%%expect{|
+Line _, characters 12-77:
+  module T1 = Fix(functor (X:sig type t end) -> struct type t = X.t option end);;
+              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the signature of this functor application:
+       The type abbreviation Fixed.t is cyclic
+|}]
+module T2 = Fix(functor (X:sig type t end) -> struct type t = X.t end);;
+[%%expect{|
+Line _, characters 12-70:
+  module T2 = Fix(functor (X:sig type t end) -> struct type t = X.t end);;
+              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In the signature of this functor application:
+       The definition of Fixed.t contains a cycle:
+       F(Fixed).t
+|}]
+
+(* Positive example *)
+module F3(X:T) = struct type t = Z | S of X.t end;;
+module T3 = Fix(F3);;
+let x : T3.Fixed.t = S Z;;
+[%%expect{|
+module F3 : functor (X : T) -> sig type t = Z | S of X.t end
+module T3 : sig module rec Fixed : sig type t = F3(Fixed).t end end
+val x : T3.Fixed.t = F3(T3.Fixed).S F3(T3.Fixed).Z
+|}]
+
+(* Torture the type checker more *)
+module M = struct
+  module F (X : T) : T = X
+  module rec Fixed : sig type t = F(Fixed).t end = Fixed
+end
+module type S = module type of M
+module Id (X : T) = X;;
+[%%expect{|
+module M :
+  sig
+    module F : functor (X : T) -> T
+    module rec Fixed : sig type t = F(Fixed).t end
+  end
+module type S =
+  sig
+    module F : functor (X : T) -> T
+    module rec Fixed : sig type t = F(Fixed).t end
+  end
+module Id : functor (X : T) -> sig type t = X.t end
+|}]
+
+module type Bad = S with module F = Id;;
+[%%expect{|
+Line _, characters 18-38:
+  module type Bad = S with module F = Id;;
+                    ^^^^^^^^^^^^^^^^^^^^
+Error: In this instantiated signature:
+       The definition of Fixed.t contains a cycle:
+       F(Fixed).t
+|}]
+
+(* More examples by lpw25 *)
+module M = Fix(Id);;
+[%%expect{|
+Line _, characters 11-18:
+  module M = Fix(Id);;
+             ^^^^^^^
+Error: In the signature of this functor application:
+       The definition of Fixed.t contains a cycle:
+       Id(Fixed).t
+|}]
+type t = Fix(Id).Fixed.t;;
+[%%expect{|
+Line _, characters 9-24:
+  type t = Fix(Id).Fixed.t;;
+           ^^^^^^^^^^^^^^^
+Error: In the signature of Fix(Id):
+       The definition of Fixed.t contains a cycle:
+       Id(Fixed).t
+|}]
+let f (x : Fix(Id).Fixed.t) = x;;
+[%%expect{|
+Line _, characters 11-26:
+  let f (x : Fix(Id).Fixed.t) = x;;
+             ^^^^^^^^^^^^^^^
+Error: In the signature of Fix(Id):
+       The definition of Fixed.t contains a cycle:
+       Id(Fixed).t
+|}]
+
+module Foo (F : T -> T) = struct
+    let f (x : Fix(F).Fixed.t) = x
+  end
+module M = Foo(Id);;
+M.f 5;;
+[%%expect{|
+module Foo :
+  functor (F : T -> T) -> sig val f : Fix(F).Fixed.t -> Fix(F).Fixed.t end
+module M : sig val f : Fix(Id).Fixed.t -> Fix(Id).Fixed.t end
+Line _:
+Error: In the signature of Fix(Id):
+       The definition of Fixed.t contains a cycle:
+       Id(Fixed).t
+|}]
+
+(* Extra tests for GPR#1676 *)
+module F() = struct type t end
+module M = struct end;;
+type t = F(M).t;;
+[%%expect{|
+module F : functor () -> sig type t end
+module M : sig  end
+Line _, characters 9-15:
+  type t = F(M).t;;
+           ^^^^^^
+Error: The functor F is generative, it cannot be applied in type expressions
+|}]
+
+module Fix2(F:(T -> T)) = struct
+  module rec Fixed : T with type t = F(Fixed).t = F(Fixed)
+  module R(X:sig end) = struct type t = Fixed.t end
+end;;
+let f (x : Fix2(Id).R(M).t) = x;;
+[%%expect{|
+module Fix2 :
+  functor (F : T -> T) ->
+    sig
+      module rec Fixed : sig type t = F(Fixed).t end
+      module R : functor (X : sig  end) -> sig type t = Fixed.t end
+    end
+Line _, characters 11-26:
+  let f (x : Fix2(Id).R(M).t) = x;;
+             ^^^^^^^^^^^^^^^
+Error: In the signature of Fix2(Id):
+       The definition of Fixed.t contains a cycle:
+       Id(Fixed).t
+|}]

typing/env.ml

@@ -506,6 +506,8 @@ let copy_local ~from env =
 
 let same_constr = ref (fun _ _ _ -> assert false)
 
+let check_well_formed_module = ref (fun _ -> assert false)
+
 (* Helper to decide whether to report an identifier shadowing
    by some 'open'. For labels and constructors, we do not report
    if the two elements are from the same re-exported declaration.
@@ -1899,6 +1901,8 @@ let components_of_functor_appl f env p1 p2 =
     let p = Papply(p1, p2) in
     let sub = Subst.add_module f.fcomp_param p2 Subst.identity in
     let mty = Subst.modtype sub f.fcomp_res in
+    !check_well_formed_module env Location.(in_file !input_name)
+      ("the signature of " ^ Path.name p) mty;
     let comps = components_of_module ~deprecated:None ~loc:Location.none
         (*???*)
         env Subst.identity p mty in

typing/env.mli

@@ -293,6 +293,9 @@ val set_type_used_callback:
 (* Forward declaration to break mutual recursion with Includemod. *)
 val check_modtype_inclusion:
       (loc:Location.t -> t -> module_type -> Path.t -> module_type -> unit) ref
+(* Forward declaration to break mutual recursion with Typemod. *)
+val check_well_formed_module:
+    (t -> Location.t -> string -> module_type -> unit) ref
 (* Forward declaration to break mutual recursion with Typecore. *)
 val add_delayed_check_forward: ((unit -> unit) -> unit) ref
 (* Forward declaration to break mutual recursion with Mtype. *)