Fix module+GADT typechecking regression#11339
Conversation
This regression was introduced in eed1110, as part of PR ocaml#10277. This change introduces `Ctype.wrap_no_update_gadt_scopes`, used to disable scope checks in `Ctype.expand_abbrev_gen`. By using this wrapper in `Includemod.signatures`, modules inside expressions can still be constrained by signatures and packed/unpacked while containing types with GADT equalities. The only way that these checks can be run is by providing an explicit module signature, either by packing a module, annotating a module with a signature, or applying a functor. This avoids re-introducing the 'ambiguous results of applications' problem that ocaml#10277 was intended to solve.
|
For the record, #10348 does not help here, as it fixes unification, but the problem here comes from the use of expansion in Whether the fix preserves ambivalence is not completely clear to me. |
|
FWIW, here is the diff for the substitution approach. It appears to work with the example in #10768. --- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -2062,9 +2062,11 @@ let () = Ctype.package_subtype := package_subtype
let wrap_constraint env mark arg mty explicit =
let mark = if mark then Includemod.Mark_both else Includemod.Mark_neither in
+ let mty1 = Subst.modtype Keep Subst.identity arg.mod_type in
+ let mty2 = Subst.modtype Keep Subst.identity mty in
let coercion =
try
- Includemod.modtypes ~loc:arg.mod_loc env ~mark arg.mod_type mty
+ Includemod.modtypes ~loc:arg.mod_loc env ~mark mty1 mty2
with Includemod.Error msg ->
raise(Error(arg.mod_loc, env, Not_included msg)) in
{ mod_desc = Tmod_constraint(arg, mty, explicit, coercion); |
|
For safety reasons, I would rather go with the fix in #11340: copying cannot break anything, while disabling checks on shared types seems potentially dangerous. |
That makes sense, and your changes LGTM. Closing this in favour of your PR, thanks for the quick turn-around! |
This PR fixes the regression described in #10768. This regression was introduced between 4.12 and 4.13 in eed1110, as part of PR #10277.
This PR introduces
Ctype.wrap_no_update_gadt_scopes, which can be used to disable scope checks inCtype.expand_abbrev_gen. By calling this inIncludemod.signatures, modules inside expressions can still be constrained by signatures or packed/unpacked while they contain types with GADT equalities.The scope checks are only skipped when a module is constrained to a signature, which happens when we are either packing a module, annotating a module with a signature, or applying a functor. All of these thus require an explicit signature at some point in the affected program. As far as I can tell, none of these provide a vector for re-introducing the 'ambiguous results of applications' problem that #10277 was intended to solve.
The attached testsuite builds on the example cases in #10768, and introduces some extra failure cases related to the tests from #10277 as an extra sanity check.
cc @garrigue