diff --git a/typing/env.ml b/typing/env.ml
index 31e60414b..0e8ff2531 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -1118,6 +1118,15 @@ let normalize_type_path oloc env path =
   | Papply _ ->
       assert false
 
+let rec normalize_modtype_path env path =
+  let path = normalize_path_prefix None env path in
+  expand_modtype_path env path
+
+and expand_modtype_path env path =
+  match (find_modtype path env).mtd_type with
+  | Some (Mty_ident path) -> normalize_modtype_path env path
+  | _ | exception Not_found -> path
+
 let find_module path env =
   find_module ~alias:false path env
 
diff --git a/typing/env.mli b/typing/env.mli
index 214ed233e..51cbe6777 100644
--- a/typing/env.mli
+++ b/typing/env.mli
@@ -119,6 +119,8 @@ val normalize_path_prefix: Location.t option -> t -> Path.t -> Path.t
 (* Normalize the prefix part of other kinds of paths
    (value/modtype/etc) *)
 
+val normalize_modtype_path: t -> Path.t -> Path.t
+(* Normalize a module type path *)
 
 val reset_required_globals: unit -> unit
 val get_required_globals: unit -> Ident.t list
diff --git a/typing/includemod.ml b/typing/includemod.ml
index f9a1962e4..2a870ac75 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -128,28 +128,16 @@ let class_declarations ~old_env:_ env cxt subst id decl1 decl2 =
 
 exception Dont_match
 
-let may_expand_module_path env path =
-  try ignore (Env.find_modtype_expansion path env); true
-  with Not_found -> false
-
-let expand_module_path env cxt path =
+let try_expand_modtype_path env path =
   try
     Env.find_modtype_expansion path env
-  with Not_found ->
-    raise(Error[cxt, env, Unbound_modtype_path path])
+  with Not_found -> raise Dont_match
 
 let expand_module_alias env cxt path =
   try (Env.find_module path env).md_type
   with Not_found ->
     raise(Error[cxt, env, Unbound_module_path path])
 
-(*
-let rec normalize_module_path env cxt path =
-  match expand_module_alias env cxt path with
-    Mty_alias path' -> normalize_module_path env cxt path'
-  | _ -> path
-*)
-
 (* Extract name, kind and ident from a signature item *)
 
 type field_desc =
@@ -243,6 +231,18 @@ and print_coercion3 ppf (i, n, c) =
 
 (* Simplify a structure coercion *)
 
+let equal_module_paths env p1 subst p2 =
+  Path.same p1 p2
+  || Path.same (Env.normalize_module_path None env p1)
+       (Env.normalize_module_path None env
+          (Subst.module_path subst p2))
+
+let equal_modtype_paths env p1 subst p2 =
+  Path.same p1 p2
+  || Path.same (Env.normalize_modtype_path env p1)
+       (Env.normalize_modtype_path env
+          (Subst.modtype_path subst p2))
+
 let simplify_structure_coercion cc id_pos_list =
   let rec is_identity_coercion pos = function
   | [] ->
@@ -275,34 +275,37 @@ let rec modtypes ~loc env ~mark cxt subst mty1 mty2 =
 
 and try_modtypes ~loc env ~mark cxt subst mty1 mty2 =
   match mty1, mty2 with
-  | Mty_alias p1, Mty_alias p2 ->
+  | (Mty_alias p1, Mty_alias p2) ->
       if Env.is_functor_arg p2 env then
         raise (Error[cxt, env, Invalid_module_alias p2]);
-      if not (Path.same p1 p2) then begin
-        let p1 = Env.normalize_module_path None env p1
-        and p2 = Env.normalize_module_path None env
-            (Subst.module_path subst p2)
-        in
-        if not (Path.same p1 p2) then raise Dont_match
-      end;
+      if not (equal_module_paths env p1 subst p2) then
+        raise Dont_match;
       Tcoerce_none
-  | (Mty_alias p1, _) -> begin
+  | (Mty_alias p1, _) ->
       let p1 = try
         Env.normalize_module_path (Some Location.none) env p1
       with Env.Error (Env.Missing_module (_, _, path)) ->
         raise (Error[cxt, env, Unbound_module_path path])
       in
-      let mty1 =
-        Mtype.strengthen ~aliasable:true env
-          (expand_module_alias env cxt p1) p1
-      in
-      modtypes ~loc env ~mark cxt subst mty1 mty2
-    end
-  | (Mty_ident p1, _) when may_expand_module_path env p1 ->
+      let mty1 = expand_module_alias env cxt p1 in
+      strengthened_modtypes ~loc ~aliasable:true env ~mark cxt
+        subst mty1 p1 mty2
+  | (Mty_ident p1, Mty_ident p2) ->
+      let p1 = Env.normalize_modtype_path env p1 in
+      let p2 = Env.normalize_modtype_path env (Subst.modtype_path subst p2) in
+      if Path.same p1 p2 then Tcoerce_none
+      else
+        try_modtypes ~loc env ~mark cxt subst
+          (try_expand_modtype_path env p1)
+          (try_expand_modtype_path env p2)
+  | (Mty_ident p1, _) ->
+      let p1 = Env.normalize_modtype_path env p1 in
       try_modtypes ~loc env ~mark cxt subst
-        (expand_module_path env cxt p1) mty2
-  | (_, Mty_ident _) ->
-      try_modtypes2 ~loc env ~mark cxt mty1 (Subst.modtype Keep subst mty2)
+        (try_expand_modtype_path env p1) mty2
+  | (_, Mty_ident p2) ->
+      let p2 = Env.normalize_modtype_path env (Subst.modtype_path subst p2) in
+      try_modtypes ~loc env ~mark cxt subst mty1
+        (try_expand_modtype_path env p2)
   | (Mty_signature sig1, Mty_signature sig2) ->
       signatures ~loc env ~mark cxt subst sig1 sig2
   | (Mty_functor(Unit, res1), Mty_functor(Unit, res2)) ->
@@ -338,18 +341,21 @@ and try_modtypes ~loc env ~mark cxt subst mty1 mty2 =
   | (_, _) ->
       raise Dont_match
 
-and try_modtypes2 ~loc env ~mark cxt mty1 mty2 =
-  (* mty2 is an identifier *)
-  match (mty1, mty2) with
-    (Mty_ident p1, Mty_ident p2)
-    when Path.same (Env.normalize_path_prefix None env p1)
-                   (Env.normalize_path_prefix None env p2) ->
+and strengthened_modtypes ~loc ~aliasable env ~mark cxt subst mty1 path1 mty2 =
+  match mty1, mty2 with
+  | Mty_ident p1, Mty_ident p2 when equal_modtype_paths env p1 subst p2 ->
       Tcoerce_none
-  | (_, Mty_ident p2) when may_expand_module_path env p2 ->
-      try_modtypes ~loc env ~mark cxt Subst.identity
-        mty1 (expand_module_path env cxt p2)
-  | (_, _) ->
-      raise Dont_match
+  | _, _ ->
+      let mty1 = Mtype.strengthen ~aliasable env mty1 path1 in
+      modtypes ~loc env ~mark cxt subst mty1 mty2
+
+and strengthened_module_decl ~loc ~aliasable env ~mark cxt subst md1 path1 md2 =
+  match md1.md_type, md2.md_type with
+  | Mty_ident p1, Mty_ident p2 when equal_modtype_paths env p1 subst p2 ->
+      Tcoerce_none
+  | _, _ ->
+      let md1 = Mtype.strengthen_decl ~aliasable env md1 path1 in
+      modtypes ~loc env ~mark cxt subst md1.md_type md2.md_type
 
 (* Inclusion between signatures *)
 
@@ -510,8 +516,8 @@ and module_declarations ~loc env ~mark cxt subst id1 md1 md2 =
   let p1 = Path.Pident id1 in
   if mark_positive mark then
     Env.mark_module_used (Ident.name id1) md1.md_loc;
-  modtypes ~loc env ~mark (Module id1::cxt) subst
-    (Mtype.strengthen ~aliasable:true env md1.md_type p1) md2.md_type
+  strengthened_modtypes ~loc ~aliasable:true env ~mark (Module id1::cxt) subst
+    md1.md_type p1 md2.md_type
 
 (* Inclusion between module type specifications *)
 
@@ -558,8 +564,9 @@ let can_alias env path =
 
 let check_modtype_inclusion ~loc env mty1 path1 mty2 =
   let aliasable = can_alias env path1 in
-  ignore(modtypes ~loc env ~mark:Mark_both [] Subst.identity
-           (Mtype.strengthen ~aliasable env mty1 path1) mty2)
+  ignore
+    (strengthened_modtypes ~loc ~aliasable env ~mark:Mark_both []
+       Subst.identity mty1 path1 mty2)
 
 let () =
   Env.check_functor_application :=
@@ -591,6 +598,10 @@ let signatures env ?(mark=Mark_both) sig1 sig2 =
   signatures ~loc:Location.none env ~mark [] Subst.identity sig1 sig2
 let type_declarations ~loc env ?(mark=Mark_both) id decl1 decl2 =
   type_declarations ~loc env ~mark [] Subst.identity id decl1 decl2
+let strengthened_module_decl ~loc ~aliasable env ?(mark=Mark_both)
+      md1 path1 md2 =
+  strengthened_module_decl ~loc ~aliasable env ~mark [] Subst.identity
+    md1 path1 md2
 
 (*
 let modtypes env m1 m2 =
diff --git a/typing/includemod.mli b/typing/includemod.mli
index 4de7eee1f..325ef09c5 100644
--- a/typing/includemod.mli
+++ b/typing/includemod.mli
@@ -35,6 +35,10 @@ val modtypes:
   loc:Location.t -> Env.t -> ?mark:mark ->
   module_type -> module_type -> module_coercion
 
+val strengthened_module_decl:
+  loc:Location.t -> aliasable:bool -> Env.t -> ?mark:mark ->
+  module_declaration -> Path.t -> module_declaration -> module_coercion
+
 val check_modtype_inclusion :
   loc:Location.t -> Env.t -> Types.module_type -> Path.t -> Types.module_type ->
   unit
diff --git a/typing/subst.mli b/typing/subst.mli
index f0b1a8beb..67c015360 100644
--- a/typing/subst.mli
+++ b/typing/subst.mli
@@ -45,6 +45,7 @@ val reset_for_saving: unit -> unit
 
 val module_path: t -> Path.t -> Path.t
 val type_path: t -> Path.t -> Path.t
+val modtype_path: t -> Path.t -> Path.t
 
 val type_expr: t -> type_expr -> type_expr
 val class_type: t -> class_type -> class_type
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 089fde04e..f2ce0ff68 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -550,8 +550,9 @@ let merge_constraint initial_env remove_aliases loc sg constr =
       when Ident.name id = s ->
         let path, md' = Env.lookup_module ~loc lid'.txt initial_env in
         let aliasable = not (Env.is_functor_arg path env) in
-        let newmd = Mtype.strengthen_decl ~aliasable env md' path in
-        ignore(Includemod.modtypes ~loc env newmd.md_type md.md_type);
+        ignore
+          (Includemod.strengthened_module_decl ~loc ~aliasable env
+             md' path md);
         real_ids := [Pident id];
         (Pident id, lid, Twith_modsubst (path, lid')),
         update_rec_next rs rem