From c5722f1e4d2b53a3ea2f3a9040ac729f2110074b Mon Sep 17 00:00:00 2001
From: Valentin Gatien-Baron <valentin.gatienbaron@gmail.com>
Date: Sun, 3 Dec 2017 11:58:28 -0500
Subject: [PATCH] share code that checks that the functor application F(M) is
 well-typed

---
 typing/includemod.ml  | 14 +++++++-------
 typing/includemod.mli |  6 ++++++
 typing/typemod.ml     |  4 +---
 3 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/typing/includemod.ml b/typing/includemod.ml
index 9b12e7785..6f46daf3e 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 d5d3cbfc4..ac36544d4 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 84fc64901..e0928156e 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