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.