Merge pull request #1491 from sliquister/ill-typed-functor

Improve error reporting for ill-typed applicative functor type

11 files changed, 195 insertions, 53 deletions

diff --git a/.depend b/.depend
index 7a1a06acb5..e009bb2ac3 100644
--- a/.depend
+++ b/.depend
@@ -475,18 +475,20 @@ typing/types.cmi : typing/primitive.cmi typing/path.cmi \
 typing/typetexp.cmo : typing/types.cmi typing/typedtree.cmi utils/tbl.cmi \
     typing/printtyp.cmi typing/predef.cmi typing/path.cmi \
     parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
-    parsing/location.cmi typing/env.cmi typing/ctype.cmi utils/clflags.cmi \
-    parsing/builtin_attributes.cmi typing/btype.cmi parsing/asttypes.cmi \
-    parsing/ast_helper.cmi typing/typetexp.cmi
+    parsing/location.cmi typing/includemod.cmi typing/env.cmi \
+    typing/ctype.cmi utils/clflags.cmi parsing/builtin_attributes.cmi \
+    typing/btype.cmi parsing/asttypes.cmi parsing/ast_helper.cmi \
+    typing/typetexp.cmi
 typing/typetexp.cmx : typing/types.cmx typing/typedtree.cmx utils/tbl.cmx \
     typing/printtyp.cmx typing/predef.cmx typing/path.cmx \
     parsing/parsetree.cmi utils/misc.cmx parsing/longident.cmx \
-    parsing/location.cmx typing/env.cmx typing/ctype.cmx utils/clflags.cmx \
-    parsing/builtin_attributes.cmx typing/btype.cmx parsing/asttypes.cmi \
-    parsing/ast_helper.cmx typing/typetexp.cmi
+    parsing/location.cmx typing/includemod.cmx typing/env.cmx \
+    typing/ctype.cmx utils/clflags.cmx parsing/builtin_attributes.cmx \
+    typing/btype.cmx parsing/asttypes.cmi parsing/ast_helper.cmx \
+    typing/typetexp.cmi
 typing/typetexp.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
     parsing/parsetree.cmi parsing/longident.cmi parsing/location.cmi \
-    typing/env.cmi parsing/asttypes.cmi
+    typing/includemod.cmi typing/env.cmi parsing/asttypes.cmi
 typing/untypeast.cmo : typing/typedtree.cmi typing/path.cmi \
     parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
     parsing/location.cmi typing/ident.cmi typing/env.cmi parsing/asttypes.cmi \
diff --git a/Changes b/Changes
index 49ae35dcf7..b1e320078e 100644
--- a/Changes
+++ b/Changes
@@ -12,9 +12,8 @@ Working version
 
 ### Type system:
 
-- GPR#1370: Fix code duplication in Cmmgen
-  (Vincent Laviron, with help from Pierre Chambart,
-   reviews by Gabriel Scherer and Luc Maranget)
+- MPR#7611, GPR#1491: reject the use of generative functors as applicative
+  (Valentin Gatien-Baron)
 
 - GPR#1469: Use the information from [@@immediate] annotations when
   computing whether a type can be [@@unboxed]
@@ -49,6 +48,10 @@ Working version
   (Arthur Charguéraud and Armaël Guéneau, with help from Gabriel Scherer and
   Frédéric Bour)
 
+- GPR#1491: Improve error reporting for ill-typed applicative functor
+  types, F(M).t.
+  (Valentin Gatien-Baron, review by Florian Angeletti and Gabriel Radanne)
+
 - GPR#1496: Refactor the code printing explanation for unification type errors,
   in order to avoid duplicating pattern matches
   (Armaël Guéneau, review by Florian Angeletti and Gabriel Scherer)
@@ -60,6 +63,10 @@ Working version
 
 ### Code generation and optimizations:
 
+- GPR#1370: Fix code duplication in Cmmgen
+  (Vincent Laviron, with help from Pierre Chambart,
+   reviews by Gabriel Scherer and Luc Maranget)
+
 ### Runtime system:
 
 - GPR#1431: remove ocamlrun dependencies on curses/terminfo/termcap C library
diff --git a/testsuite/tests/typing-modules/Test.ml b/testsuite/tests/typing-modules/Test.ml
index 1da12967c1..610c8fcae7 100644
--- a/testsuite/tests/typing-modules/Test.ml
+++ b/testsuite/tests/typing-modules/Test.ml
@@ -119,5 +119,5 @@ module F : functor (X : sig  end) -> sig val x : int end
 Line _, characters 0-3:
   F.x;; (* fail *)
   ^^^
-Error: The module F is a functor, not a structure
+Error: The module F is a functor, it cannot have any components
 |}];;
diff --git a/testsuite/tests/typing-modules/applicative_functor_type.ml b/testsuite/tests/typing-modules/applicative_functor_type.ml
new file mode 100644
index 0000000000..b02a882d24
--- /dev/null
+++ b/testsuite/tests/typing-modules/applicative_functor_type.ml
@@ -0,0 +1,83 @@
+(* TEST
+   * expect
+*)
+
+type t = Set.Make(String).t
+[%%expect{|
+type t = Set.Make(String).t
+|} ]
+
+
+(* Check the error messages of an ill-typed applicatived functor type. *)
+module M = struct type t let equal = (=) end
+[%%expect{|
+module M : sig type t val equal : 'a -> 'a -> bool end
+|} ]
+
+type t = Set.Make(M).t
+[%%expect{|
+Line _, characters 9-22:
+  type t = Set.Make(M).t
+           ^^^^^^^^^^^^^
+Error: The type of M does not match Set.Make's parameter
+       Modules do not match:
+         sig type t = M.t val equal : 'a -> 'a -> bool end
+       is not included in
+         Set.OrderedType
+       The value `compare' is required but not provided
+       File "set.mli", line 52, characters 4-31: Expected declaration
+|} ]
+
+
+(* We would report the wrong error here if we didn't strengthen the
+   type of the argument (type t wouldn't match). *)
+module F(X : sig type t = M.t val equal : unit end)
+  = struct type t end
+[%%expect{|
+module F :
+  functor (X : sig type t = M.t val equal : unit end) -> sig type t end
+|} ]
+
+type t = F(M).t
+[%%expect{|
+Line _, characters 9-15:
+  type t = F(M).t
+           ^^^^^^
+Error: The type of M does not match F's parameter
+       Modules do not match:
+         sig type t = M.t val equal : 'a -> 'a -> bool end
+       is not included in
+         sig type t = M.t val equal : unit end
+       Values do not match:
+         val equal : 'a -> 'a -> bool
+       is not included in
+         val equal : unit
+|} ]
+
+
+(* MPR#7611 *)
+module Generative() = struct type t end
+[%%expect{|
+module Generative : functor () -> sig type t end
+|}]
+
+type t = Generative(M).t
+[%%expect{|
+Line _, characters 9-24:
+  type t = Generative(M).t
+           ^^^^^^^^^^^^^^^
+Error: The functor Generative is generative, it cannot be applied in type
+       expressions
+|}]
+
+
+
+module F(X : sig module type S module F : S end) = struct
+  type t = X.F(Parsing).t
+end
+[%%expect{|
+Line _, characters 11-25:
+    type t = X.F(Parsing).t
+             ^^^^^^^^^^^^^^
+Error: The module X.F is abstract, it cannot be applied
+|}]
diff --git a/testsuite/tests/typing-modules/ocamltests b/testsuite/tests/typing-modules/ocamltests
index 924b049058..f8c9fcdb51 100644
--- a/testsuite/tests/typing-modules/ocamltests
+++ b/testsuite/tests/typing-modules/ocamltests
@@ -1,4 +1,5 @@
 aliases.ml
+applicative_functor_type.ml
 firstclass.ml
 generative.ml
 pr5911.ml
diff --git a/typing/env.ml b/typing/env.ml
index bc109da269..8bf5d8677e 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -1136,7 +1136,9 @@ let rec lookup_module_descr_aux ?loc ~mark lid env =
       begin match get_components desc1 with
         Functor_comps f ->
           let loc = match loc with Some l -> l | None -> Location.none in
-          Misc.may (!check_modtype_inclusion ~loc env mty2 p2) f.fcomp_arg;
+          (match f.fcomp_arg with
+          | None ->  raise Not_found (* PR#7611 *)
+          | Some arg -> !check_modtype_inclusion ~loc env mty2 p2 arg);
           (Papply(p1, p2), !components_of_functor_appl' f env p1 p2)
       | Structure_comps _ ->
           raise Not_found
@@ -1204,7 +1206,9 @@ and lookup_module ~load ?loc ~mark lid env : Path.t =
       begin match get_components desc1 with
         Functor_comps f ->
           let loc = match loc with Some l -> l | None -> Location.none in
-          Misc.may (!check_modtype_inclusion ~loc env mty2 p2) f.fcomp_arg;
+          (match f.fcomp_arg with
+          | None -> raise Not_found (* PR#7611 *)
+          | Some arg -> (!check_modtype_inclusion ~loc env mty2 p2) arg);
           p
       | Structure_comps _ ->
           raise Not_found
diff --git a/typing/includemod.ml b/typing/includemod.ml
index 9b12e77855..6f46daf3e8 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -482,14 +482,14 @@ let can_alias env path =
   no_apply path && not (Env.is_functor_arg path env)
 
 let check_modtype_inclusion ~loc env mty1 path1 mty2 =
-  try
-    let aliasable = can_alias env path1 in
-    ignore(modtypes ~loc env [] Subst.identity
-                    (Mtype.strengthen ~aliasable env mty1 path1) mty2)
-  with Error _ ->
-    raise Not_found
+  let aliasable = can_alias env path1 in
+  ignore(modtypes ~loc env [] Subst.identity
+           (Mtype.strengthen ~aliasable env mty1 path1) mty2)
 
-let _ = Env.check_modtype_inclusion := check_modtype_inclusion
+let () =
+  Env.check_modtype_inclusion := (fun ~loc a b c d ->
+    try (check_modtype_inclusion ~loc a b c d : unit)
+    with Error _ -> raise Not_found)
 
 (* Check that an implementation of a compilation unit meets its
    interface. *)
diff --git a/typing/includemod.mli b/typing/includemod.mli
index d5d3cbfc48..ac36544d48 100644
--- a/typing/includemod.mli
+++ b/typing/includemod.mli
@@ -23,6 +23,12 @@ val modtypes:
   loc:Location.t -> Env.t ->
   module_type -> module_type -> module_coercion
 
+val check_modtype_inclusion :
+  loc:Location.t -> Env.t -> Types.module_type -> Path.t -> Types.module_type -> unit
+(** [check_modtype_inclusion ~loc env mty1 path1 mty2] checks that the
+    functor application F(M) is well typed, where mty2 is the type of
+    the argument of F and path1/mty1 is the path/unstrenghened type of M. *)
+
 val signatures: Env.t -> signature -> signature -> module_coercion
 
 val compunit:
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 84fc649017..e0928156eb 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -214,9 +214,7 @@ let retype_applicative_functor_type ~loc env funct arg =
     | Mty_functor (_, Some mty_param, _) -> mty_param
     | _ -> assert false (* could trigger due to MPR#7611 *)
   in
-  let aliasable = not (Env.is_functor_arg arg env) in
-  ignore(Includemod.modtypes ~loc env
-           (Mtype.strengthen ~aliasable env mty_arg arg) mty_param)
+  Includemod.check_modtype_inclusion ~loc env mty_arg arg mty_param
 
 (* When doing a deep destructive substitution with type M.N.t := .., we change M
    and M.N and so we have to check that uses of the modules other than just
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 086686ff78..4603218f3d 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -52,10 +52,15 @@ type error =
   | Unbound_class of Longident.t
   | Unbound_modtype of Longident.t
   | Unbound_cltype of Longident.t
-  | Ill_typed_functor_application of Longident.t
+  | Ill_typed_functor_application
+      of Longident.t * Longident.t * Includemod.error list option
   | Illegal_reference_to_recursive_module
-  | Access_functor_as_structure of Longident.t
-  | Apply_structure_as_functor of Longident.t
+  | Wrong_use_of_module of Longident.t * [ `Structure_used_as_functor
+                                         | `Abstract_used_as_functor
+                                         | `Functor_used_as_structure
+                                         | `Abstract_used_as_structure
+                                         | `Generative_used_as_applicative
+                                         ]
   | Cannot_scrape_alias of Longident.t * Path.t
   | Opened_object of Path.t option
   | Not_an_object of type_expr
@@ -81,6 +86,7 @@ let rec narrow_unbound_lid_error : 'a. _ -> _ -> _ -> _ -> 'a =
     | Env.Recmodule ->
         raise (Error (loc, env, Illegal_reference_to_recursive_module))
   in
+  let error e = raise (Error (loc, env, e)) in
   begin match lid with
   | Longident.Lident _ -> ()
   | Longident.Ldot (mlid, _) ->
@@ -88,31 +94,42 @@ let rec narrow_unbound_lid_error : 'a. _ -> _ -> _ -> _ -> 'a =
       let md = Env.find_module (Env.lookup_module ~load:true mlid env) env in
       begin match Env.scrape_alias env md.md_type with
       | Mty_functor _ ->
-          raise (Error (loc, env, Access_functor_as_structure mlid))
-      | Mty_alias(_, p) ->
-          raise (Error (loc, env, Cannot_scrape_alias(mlid, p)))
-      | _ -> ()
+         error (Wrong_use_of_module (mlid, `Functor_used_as_structure))
+      | Mty_ident _ ->
+         error (Wrong_use_of_module (mlid, `Abstract_used_as_structure))
+      | Mty_alias(_, p) -> error (Cannot_scrape_alias(mlid, p))
+      | Mty_signature _ -> ()
       end
   | Longident.Lapply (flid, mlid) ->
       check_module flid;
       let fmd = Env.find_module (Env.lookup_module ~load:true flid env) env in
-      begin match Env.scrape_alias env fmd.md_type with
-      | Mty_signature _ ->
-          raise (Error (loc, env, Apply_structure_as_functor flid))
-      | Mty_alias(_, p) ->
-          raise (Error (loc, env, Cannot_scrape_alias(flid, p)))
-      | _ -> ()
-      end;
+      let mty_param =
+        match Env.scrape_alias env fmd.md_type with
+        | Mty_signature _ ->
+           error (Wrong_use_of_module (flid, `Structure_used_as_functor))
+        | Mty_ident _ ->
+           error (Wrong_use_of_module (flid, `Abstract_used_as_functor))
+        | Mty_alias(_, p) -> error (Cannot_scrape_alias(flid, p))
+        | Mty_functor (_, None, _) ->
+           error (Wrong_use_of_module (flid, `Generative_used_as_applicative))
+        | Mty_functor (_, Some mty_param, _) -> mty_param
+      in
       check_module mlid;
-      let mmd = Env.find_module (Env.lookup_module ~load:true mlid env) env in
+      let mpath = Env.lookup_module ~load:true mlid env in
+      let mmd = Env.find_module mpath env in
       begin match Env.scrape_alias env mmd.md_type with
-      | Mty_alias(_, p) ->
-          raise (Error (loc, env, Cannot_scrape_alias(mlid, p)))
-      | _ ->
-          raise (Error (loc, env, Ill_typed_functor_application lid))
+      | Mty_alias(_, p) -> error (Cannot_scrape_alias(mlid, p))
+      | mty_arg ->
+         let details =
+           try Includemod.check_modtype_inclusion
+                 ~loc env mty_arg mpath mty_param;
+               None (* should be impossible *)
+           with Includemod.Error e -> Some e
+         in
+         error (Ill_typed_functor_application (flid, mlid, details))
       end
   end;
-  raise (Error (loc, env, make_error lid))
+  error (make_error lid)
 
 let find_component (lookup : ?loc:_ -> ?mark:_ -> _) make_error env loc lid =
   try
@@ -953,14 +970,33 @@ let report_error env ppf = function
   | Unbound_cltype lid ->
       fprintf ppf "Unbound class type %a" longident lid;
       spellcheck ppf fold_cltypes env lid;
-  | Ill_typed_functor_application lid ->
-      fprintf ppf "Ill-typed functor application %a" longident lid
+  | Ill_typed_functor_application (flid, mlid, details) ->
+     (match details with
+     | None ->
+        fprintf ppf "@[Ill-typed functor application %a(%a)@]"
+          longident flid longident mlid
+     | Some inclusion_error ->
+        fprintf ppf "@[The type of %a does not match %a's parameter@\n%a@]"
+          longident mlid longident flid Includemod.report_error inclusion_error)
   | Illegal_reference_to_recursive_module ->
-      fprintf ppf "Illegal recursive module reference"
-  | Access_functor_as_structure lid ->
-      fprintf ppf "The module %a is a functor, not a structure" longident lid
-  | Apply_structure_as_functor lid ->
-      fprintf ppf "The module %a is a structure, not a functor" longident lid
+     fprintf ppf "Illegal recursive module reference"
+  | Wrong_use_of_module (lid, details) ->
+     (match details with
+     | `Structure_used_as_functor ->
+        fprintf ppf "@[The module %a is a structure, it cannot be applied@]"
+          longident lid
+     | `Abstract_used_as_functor ->
+        fprintf ppf "@[The module %a is abstract, it cannot be applied@]"
+          longident lid
+     | `Functor_used_as_structure ->
+        fprintf ppf "@[The module %a is a functor, \
+                       it cannot have any components@]" longident lid
+     | `Abstract_used_as_structure ->
+        fprintf ppf "@[The module %a is abstract, \
+                       it cannot have any components@]" longident lid
+     | `Generative_used_as_applicative ->
+        fprintf ppf "@[The functor %a is generative,@ it@ cannot@ be@ \
+                       applied@ in@ type@ expressions@]" longident lid)
   | Cannot_scrape_alias(lid, p) ->
       fprintf ppf
         "The module %a is an alias for module %a, which is missing"
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index c6bc5e4302..87e95505da 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -64,10 +64,15 @@ type error =
   | Unbound_class of Longident.t
   | Unbound_modtype of Longident.t
   | Unbound_cltype of Longident.t
-  | Ill_typed_functor_application of Longident.t
+  | Ill_typed_functor_application
+      of Longident.t * Longident.t * Includemod.error list option
   | Illegal_reference_to_recursive_module
-  | Access_functor_as_structure of Longident.t
-  | Apply_structure_as_functor of Longident.t
+  | Wrong_use_of_module of Longident.t * [ `Structure_used_as_functor
+                                         | `Abstract_used_as_functor
+                                         | `Functor_used_as_structure
+                                         | `Abstract_used_as_structure
+                                         | `Generative_used_as_applicative
+                                         ]
   | Cannot_scrape_alias of Longident.t * Path.t
   | Opened_object of Path.t option
   | Not_an_object of type_expr