Closed ccasin closed 2 months ago
with module
is able to strenghthen. In the manual:
After each constraint has been applied, the resulting signature must be a subtype of the signature before the constraint was applied. Thus, the with operator can only add information on the type components of a signature, but never remove information.
In the following example, both type t
and val f
is strengthened:
module type S = sig
module N : sig
type t
val f : t -> t
end
end
module N0 : sig
type t = int
val f : 'a -> 'a
end = struct
type t = int
let f a = a
end
module type S' = S with module N = N0
and I can see that typemod.patch_item
checks N0
is stronger than N
. So I think typemod is doing the right thing here.
Following the last comment, I now think that it makes sense that with module N = N0
will look inside the type of N0
(in particular, val_modalities
) to strenghthen N
on a per-signature-item basis. Therefore, val_modalities
which could be "variable" modalities need to be defaulted. And it should be zap_to_id
just to give the best compatibility - for example:
module type S = sig
module M : sig
val f : int -> int
end
end
module M0 = struct
let f a = a
end
module type S0 = S with module M = M0
If we zap_to_floor
, then S0.M.f
will have @@ portable
on it, which might confuse the user.
On the other hand, if the user write let (f @ portable) a = a
, then S0.M.f
should be @@ portable
. This is currently not the case for zap_to_id
and I will fix that shortly with a commit here.
Apologize for delaying the promised fix. I will do this ASAP.
OK to implement what I suggested would require some extra work. Currently when people write let foo @ portable = bar
, it get typed checked as let foo = bar @ portable
. A single mode variable m
will be generated to be the mode of both LHS and RHS. The @ portable
constrains m >= portable
and proceeds to check bar
at portable
. As a result, m
(which will also be the mode of foo
) is not constrained at all.
To fix this properly, we probably need to modify vb_pat_constraint
and the type checking of Ppat_constraint
.
I suggest that for now we merge this PR as it is. I will resolve conflict and push.
This fixes a bug in #2764, which "fixed" a bug in #2742.
The original bug was that
zero_alloc
and modality variables could creep into signatures in a disallowed way when using awith module
constraint. The fix was to make these variables into constants in the computed signature for the constraint. But in the case of modality variables, I picked a constant that could lead to spurious typing errors, and failed to notice it because we only create these variables if-extension mode_alpha
is used.There are three commits:
(There remain some questions about whether the revised behavior is ideal, and the tests in the third commit document the behavior.)