share code that checks that the functor application F(M) is well-typed
parent
e172c398c8
commit
c5722f1e4d
|
@ -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. *)
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue