Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

#10598, fix exponential blow-up with nested module types #10616

Merged
merged 2 commits into from
Sep 9, 2021
Merged

#10598, fix exponential blow-up with nested module types #10616

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f9f4ba3
#10598, fix exponetial blow-up with nested module types
Octachron Sep 7, 2021
7cc65f0
Includemod: documentation for fast equality check
Octachron Sep 9, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 4 additions & 0 deletions Changes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,10 @@ Working version
- #10555: Do not use ghost locations for type constraints
(Nicolás Ojeda Bär, report by Anton Bachin, review by Thomas Refis)

- #10598, #10616: fix an exponential blow-up when typechecking nested module
types
(Florian Angeletti, report and review by Stephen Dolan)

- #10559: Evaluate signature substitutions lazily
(Stephen Dolan, review by Leo White)

Expand Down
123 changes: 77 additions & 46 deletions typing/includemod.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -361,14 +361,30 @@ let retrieve_functor_params env mty =
Return the restriction that transforms a value of the smaller type
into a value of the bigger type. *)

let rec modtypes ~loc env ~mark subst mty1 mty2 =
match try_modtypes ~loc env ~mark subst mty1 mty2 with
(**
In the group of mutual functions below, the [~in_eq] argument is [true] when
we are in fact checking equality of module types.

The module subtyping relation [A <: B] checks that [A.T = B.T] when [A]
and [B] define a module type [T]. The relation [A.T = B.T] is equivalent
to [(A.T <: B.T) and (B.T <: A.T)], but checking both recursively would lead
to an exponential slowdown (see #10598 and #10616).
To avoid this issue, when [~in_eq] is [true], we compute a coarser relation
[A << B] which is the same as [A <: B] except that module types [T] are
checked only for [A.T << B.T] and not the reverse.
Thus, we can implement a cheap module type equality check [A.T = B.T] by
computing [(A.T << B.T) and (B.T << A.T)], avoiding the exponential slowdown
described above.
*)

let rec modtypes ~in_eq ~loc env ~mark subst mty1 mty2 =
match try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 with
| Ok _ as ok -> ok
| Error reason ->
let mty2 = Subst.modtype Make_local subst mty2 in
Error Error.(diff mty1 mty2 reason)

and try_modtypes ~loc env ~mark subst mty1 mty2 =
and try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2 =
match mty1, mty2 with
| (Mty_alias p1, Mty_alias p2) ->
if Env.is_functor_arg p2 env then
Expand All @@ -386,7 +402,7 @@ and try_modtypes ~loc env ~mark subst mty1 mty2 =
begin match expand_module_alias ~strengthen:false env p1 with
| Error e -> Error (Error.Mt_core e)
| Ok mty1 ->
match strengthened_modtypes ~loc ~aliasable:true env ~mark
match strengthened_modtypes ~in_eq ~loc ~aliasable:true env ~mark
subst mty1 p1 mty2
with
| Ok _ as x -> x
Expand All @@ -400,20 +416,20 @@ and try_modtypes ~loc env ~mark subst mty1 mty2 =
else
begin match expand_modtype_path env p1, expand_modtype_path env p2 with
| Some mty1, Some mty2 ->
try_modtypes ~loc env ~mark subst mty1 mty2
try_modtypes ~in_eq ~loc env ~mark subst mty1 mty2
| None, _ | _, None -> Error (Error.Mt_core Abstract_module_type)
end
| (Mty_ident p1, _) ->
let p1 = Env.normalize_modtype_path env p1 in
begin match expand_modtype_path env p1 with
| Some p1 ->
try_modtypes ~loc env ~mark subst p1 mty2
try_modtypes ~in_eq ~loc env ~mark subst p1 mty2
| None -> Error (Error.Mt_core Abstract_module_type)
end
| (_, Mty_ident p2) ->
let p2 = Env.normalize_modtype_path env (Subst.modtype_path subst p2) in
begin match expand_modtype_path env p2 with
| Some p2 -> try_modtypes ~loc env ~mark subst mty1 p2
| Some p2 -> try_modtypes ~in_eq ~loc env ~mark subst mty1 p2
| None ->
begin match mty1 with
| Mty_functor _ ->
Expand All @@ -424,15 +440,16 @@ and try_modtypes ~loc env ~mark subst mty1 mty2 =
end
end
| (Mty_signature sig1, Mty_signature sig2) ->
begin match signatures ~loc env ~mark subst sig1 sig2 with
begin match signatures ~in_eq ~loc env ~mark subst sig1 sig2 with
| Ok _ as ok -> ok
| Error e -> Error (Error.Signature e)
end
| Mty_functor (param1, res1), Mty_functor (param2, res2) ->
let cc_arg, env, subst =
functor_param ~loc env ~mark:(negate_mark mark) subst param1 param2
functor_param ~in_eq ~loc env ~mark:(negate_mark mark)
subst param1 param2
in
let cc_res = modtypes ~loc env ~mark subst res1 res2 in
let cc_res = modtypes ~in_eq ~loc env ~mark subst res1 res2 in
begin match cc_arg, cc_res with
| Ok Tcoerce_none, Ok Tcoerce_none -> Ok Tcoerce_none
| Ok cc_arg, Ok cc_res -> Ok (Tcoerce_functor(cc_arg, cc_res))
Expand Down Expand Up @@ -462,13 +479,14 @@ and try_modtypes ~loc env ~mark subst mty1 mty2 =

(* Functor parameters *)

and functor_param ~loc env ~mark subst param1 param2 = match param1, param2 with
and functor_param ~in_eq ~loc env ~mark subst param1 param2 =
match param1, param2 with
| Unit, Unit ->
Ok Tcoerce_none, env, subst
| Named (name1, arg1), Named (name2, arg2) ->
let arg2' = Subst.modtype Keep subst arg2 in
let cc_arg =
match modtypes ~loc env ~mark Subst.identity arg2' arg1 with
match modtypes ~in_eq ~loc env ~mark Subst.identity arg2' arg1 with
| Ok cc -> Ok cc
| Error err -> Error (Error.Mismatch err)
in
Expand All @@ -488,25 +506,26 @@ and functor_param ~loc env ~mark subst param1 param2 = match param1, param2 with
| _, _ ->
Error (Error.Incompatible_params (param1, param2)), env, subst

and strengthened_modtypes ~loc ~aliasable env ~mark subst mty1 path1 mty2 =
and strengthened_modtypes ~in_eq ~loc ~aliasable env ~mark
subst mty1 path1 mty2 =
match mty1, mty2 with
| Mty_ident p1, Mty_ident p2 when equal_modtype_paths env p1 subst p2 ->
Ok Tcoerce_none
| _, _ ->
let mty1 = Mtype.strengthen ~aliasable env mty1 path1 in
modtypes ~loc env ~mark subst mty1 mty2
modtypes ~in_eq ~loc env ~mark subst mty1 mty2

and strengthened_module_decl ~loc ~aliasable env ~mark 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 ->
Ok Tcoerce_none
| _, _ ->
let md1 = Mtype.strengthen_decl ~aliasable env md1 path1 in
modtypes ~loc env ~mark subst md1.md_type md2.md_type
modtypes ~in_eq:false ~loc env ~mark subst md1.md_type md2.md_type

(* Inclusion between signatures *)

and signatures ~loc env ~mark subst sig1 sig2 =
and signatures ~in_eq ~loc env ~mark subst sig1 sig2 =
(* Environment used to check inclusion of components *)
let new_env =
Env.add_signature sig1 (Env.in_signature true env) in
Expand Down Expand Up @@ -556,7 +575,9 @@ and signatures ~loc env ~mark subst sig1 sig2 =
let rec pair_components subst paired unpaired = function
[] ->
let oks, errors =
signature_components ~loc env ~mark new_env subst (List.rev paired) in
signature_components ~in_eq ~loc env ~mark new_env subst
(List.rev paired)
in
begin match unpaired, errors, oks with
| [], [], cc ->
if len1 = len2 then (* see PR#5098 *)
Expand Down Expand Up @@ -606,7 +627,7 @@ and signatures ~loc env ~mark subst sig1 sig2 =

(* Inclusion between signature components *)

and signature_components ~loc old_env ~mark env subst paired =
and signature_components ~in_eq ~loc old_env ~mark env subst paired =
match paired with
| [] -> [], []
| (sigi1, sigi2, pos) :: rem ->
Expand Down Expand Up @@ -634,7 +655,7 @@ and signature_components ~loc old_env ~mark env subst paired =
| Sig_module(id1, pres1, mty1, _, _), Sig_module(_, pres2, mty2, _, _)
-> begin
let item =
module_declarations ~loc env ~mark subst id1 mty1 mty2
module_declarations ~in_eq ~loc env ~mark subst id1 mty1 mty2
in
let item =
Result.map_error (fun diff -> Error.Module_type diff) item
Expand All @@ -651,7 +672,7 @@ and signature_components ~loc old_env ~mark env subst paired =
end
| Sig_modtype(id1, info1, _), Sig_modtype(_id2, info2, _) ->
let item =
modtype_infos ~loc env ~mark subst id1 info1 info2
modtype_infos ~in_eq ~loc env ~mark subst id1 info1 info2
in
id1, item, false
| Sig_class(id1, decl1, _, _), Sig_class(_id2, decl2, _, _) ->
Expand All @@ -668,14 +689,14 @@ and signature_components ~loc old_env ~mark env subst paired =
assert false
in
let oks, errors =
signature_components ~loc old_env ~mark env subst rem
signature_components ~in_eq ~loc old_env ~mark env subst rem
in
match item with
| Ok x when present_at_runtime -> (pos,x) :: oks, errors
| Ok _ -> oks, errors
| Error y -> oks , (id,y) :: errors

and module_declarations ~loc env ~mark subst id1 md1 md2 =
and module_declarations ~in_eq ~loc env ~mark subst id1 md1 md2 =
Builtin_attributes.check_alerts_inclusion
~def:md1.md_loc
~use:md2.md_loc
Expand All @@ -685,12 +706,12 @@ and module_declarations ~loc env ~mark subst id1 md1 md2 =
let p1 = Path.Pident id1 in
if mark_positive mark then
Env.mark_module_used md1.md_uid;
strengthened_modtypes ~loc ~aliasable:true env ~mark subst
strengthened_modtypes ~in_eq ~loc ~aliasable:true env ~mark subst
md1.md_type p1 md2.md_type

(* Inclusion between module type specifications *)

and modtype_infos ~loc env ~mark subst id info1 info2 =
and modtype_infos ~in_eq ~loc env ~mark subst id info1 info2 =
Builtin_attributes.check_alerts_inclusion
~def:info1.mtd_loc
~use:info2.mtd_loc
Expand All @@ -703,26 +724,33 @@ and modtype_infos ~loc env ~mark subst id info1 info2 =
(None, None) -> Ok Tcoerce_none
| (Some _, None) -> Ok Tcoerce_none
| (Some mty1, Some mty2) ->
check_modtype_equiv ~loc env ~mark mty1 mty2
check_modtype_equiv ~in_eq ~loc env ~mark mty1 mty2
| (None, Some mty2) ->
check_modtype_equiv ~loc env ~mark (Mty_ident(Path.Pident id)) mty2 in
let mty1 = Mty_ident(Path.Pident id) in
check_modtype_equiv ~in_eq ~loc env ~mark mty1 mty2 in
match r with
| Ok _ as ok -> ok
| Error e -> Error Error.(Module_type_declaration (diff info1 info2 e))

and check_modtype_equiv ~loc env ~mark mty1 mty2 =
match
(modtypes ~loc env ~mark Subst.identity mty1 mty2,
modtypes ~loc env ~mark:(negate_mark mark) Subst.identity mty2 mty1)
with
(Ok Tcoerce_none, Ok Tcoerce_none) -> Ok Tcoerce_none
| (Ok c1, Ok _c2) ->
and check_modtype_equiv ~in_eq ~loc env ~mark mty1 mty2 =
let c1 = modtypes ~in_eq:true ~loc env ~mark Subst.identity mty1 mty2 in
let c2 =
(* For nested module type paths, we check only one side of the equivalence:
the outer module type is the one responsible for checking the other side
of the equivalence.
*)
if in_eq then None
else Some (modtypes ~in_eq:true ~loc env ~mark Subst.identity mty2 mty1)
in
match c1, c2 with
| Ok Tcoerce_none, (Some Ok Tcoerce_none|None) -> Ok Tcoerce_none
| Ok c1, (Some Ok _ | None) ->
(* Format.eprintf "@[c1 = %a@ c2 = %a@]@."
print_coercion _c1 print_coercion _c2; *)
print_coercion _c1 print_coercion _c2; *)
Error Error.(Illegal_permutation c1)
| Ok _, Error e -> Error Error.(Not_greater_than e)
| Error e, Ok _ -> Error Error.(Not_less_than e)
| Error less_than, Error greater_than ->
| Ok _, Some Error e -> Error Error.(Not_greater_than e)
| Error e, (Some Ok _ | None) -> Error Error.(Not_less_than e)
| Error less_than, Some Error greater_than ->
Error Error.(Incomparable {less_than; greater_than})


Expand Down Expand Up @@ -751,7 +779,7 @@ exception Apply_error of {

let check_modtype_inclusion_raw ~loc env mty1 path1 mty2 =
let aliasable = can_alias env path1 in
strengthened_modtypes ~loc ~aliasable env ~mark:Mark_both
strengthened_modtypes ~in_eq:false ~loc ~aliasable env ~mark:Mark_both
Subst.identity mty1 path1 mty2

let check_modtype_inclusion ~loc env mty1 path1 mty2 =
Expand Down Expand Up @@ -787,8 +815,8 @@ let () =

let compunit env ~mark impl_name impl_sig intf_name intf_sig =
match
signatures ~loc:(Location.in_file impl_name) env ~mark Subst.identity
impl_sig intf_sig
signatures ~in_eq:false ~loc:(Location.in_file impl_name) env ~mark
Subst.identity impl_sig intf_sig
with Result.Error reasons ->
let cdiff =
Error.In_Compilation_unit(Error.diff impl_name intf_name reasons) in
Expand Down Expand Up @@ -891,7 +919,8 @@ module Functor_inclusion_diff = struct
let test st mty1 mty2 =
let loc = Location.none in
let res, _, _ =
functor_param ~loc st.env ~mark:Mark_neither st.subst mty1 mty2
functor_param ~in_eq:false ~loc st.env ~mark:Mark_neither
st.subst mty1 mty2
in
res
let update = update
Expand Down Expand Up @@ -991,8 +1020,8 @@ module Functor_app_diff = struct
Result.Error (Error.Incompatible_params(arg,param))
| ( Anonymous | Named _ ) , Named (_, param) ->
match
modtypes ~loc state.env ~mark:Mark_neither state.subst
arg_mty param
modtypes ~in_eq:false ~loc state.env ~mark:Mark_neither
state.subst arg_mty param
with
| Error mty -> Result.Error (Error.Mismatch mty)
| Ok _ as x -> x
Expand All @@ -1013,11 +1042,13 @@ end
(* Hide the context and substitution parameters to the outside world *)

let modtypes ~loc env ~mark mty1 mty2 =
match modtypes ~loc env ~mark Subst.identity mty1 mty2 with
match modtypes ~in_eq:false ~loc env ~mark Subst.identity mty1 mty2 with
| Ok x -> x
| Error reason -> raise (Error (env, Error.(In_Module_type reason)))
let signatures env ~mark sig1 sig2 =
match signatures ~loc:Location.none env ~mark Subst.identity sig1 sig2 with
match signatures ~in_eq:false ~loc:Location.none env ~mark
Subst.identity sig1 sig2
with
| Ok x -> x
| Error reason -> raise (Error(env,Error.(In_Signature reason)))

Expand All @@ -1042,7 +1073,7 @@ let expand_module_alias ~strengthen env path =
raise (Error(env,In_Expansion(Error.Unbound_module_path path)))

let check_modtype_equiv ~loc env id mty1 mty2 =
match check_modtype_equiv ~loc env ~mark:Mark_both mty1 mty2 with
match check_modtype_equiv ~in_eq:false ~loc env ~mark:Mark_both mty1 mty2 with
| Ok _ -> ()
| Error e ->
raise (Error(env,
Expand Down