Perform functor subtyping in a single name space.

[ppedrot]

Subtyping.check_modtypes compares an implementation [mtb1] living at [mp1] against a signature [mtb2] living at [mp2], and every comparison it makes happens inside one environment [env]. Write W for the name space of [env]: which kernames it can interpret, and which canonical form it gives to each of them. The code maintains, or rather ought to maintain, three invariants:

(1) [subst1] maps the names of [mtb1] into W;
(2) [subst2] maps the names of [mtb2] into W;
(3) [delta1] is [mod_delta mtb1] expressed in W -- and it is precisely the
resolver that [subst2] carries for [mp2], the two being the same value.

They hold at the entry point: [check_subtypes] passes [subst1 = empty_subst], since [mtb1] already lives at [mp1], and
[subst2 = map_mp mp2 mp1 (mod_delta sup)], whose resolver is what recomputes canonical names -- the implementation, not the signature, decides which of its own fields are identified. That resolver is [delta1], as [strengthen] is the identity on functors.

Every MoreFunctor step changes W: [env] gains the signature's parameter through [add_module_parameter arg_id2 arg_t2], so W now contains the names under [MPbound arg_id2], canonicalised by [mod_delta arg_t2], and no longer contains [MPbound arg_id1]. Re-establishing the invariants therefore amounts to applying

nsubst = map_mbid arg_id1 mparg2 (mod_delta arg_t2)

to all three components. Only [subst1] was updated; [mod_delta mtb1] was used raw, both directly -- as the resolver given to [Modops.add_structure] and as [reso1] in [check_signatures] -- and indirectly, as the resolver sitting in the codomain of [subst2].

As a result the canonical names computed on the signature side mentioned the implementation's bound parameter while the ones computed on the implementation side mentioned the signature's, and the two could never be recognised as equal. Constants recover from that by delta-reduction, so the symptom only shows on inductive types, which have no delta-rule.

Invariant (3) is restored with [add_mp mp2 mp1 delta1 subst2] rather than by composing [subst2] with [nsubst]. The two agree when the binding [subst2] provides for [mp2] is the one for [mp2] itself, but not when [mp2] is a submodule of the module the enclosing [subst2] talks about: for a functor field the inherited binding carries no information at all, since [mod_global_delta] is [None] on functors and Safe_typing consequently never merges a functor field's resolver into its parent. Re-adding the binding also mirrors the entry point, [map_mp mp2 mp1 (mod_delta sup)] being exactly [add_mp mp2 mp1 delta1] on the empty substitution.

This is not a soundness issue. The fix normalises canonical names, that is, applies a function to them, and every decision the check takes from those names is an equality test; a function can merge names but never split them, so every equality that held before still holds and the buggy version was strictly the more discriminating one.

Fixes #22411: Incompleteness due to a missing substitution in module subtyping.