fix(typing): sound module updates on sub-module and applied-functor bases

[Gustavo2622]

module M' = B with {...} re-rooted references using only the TOP path of the base mpath, appending the reference's arguments to the destination's. Consequences:

• a sub-module base P.O had every P-rooted reference re-rooted onto M': the enclosing module's state (P.g -> M'.g) and even the sub-module's own state (P.O.x -> M'.O.x) became dangling globals, silently changing the program's semantics while remaining fully usable by the program logics;
• a functor base F(A) whose body contains self-calls crashed the elaborator (assertion failure in EcEnv.Fun.by_xpath): the self-call F(A).h, unsuspended at A, was rewritten to M'(A).h with M' not a functor.

The substitution entry now records the full base expression (top path, arguments, inner path) and rewrites a reference iff it lies at or below the base's inner path AND its arguments extend the base's (references to program variables carry no arguments); the remainders are transplanted onto the destination. Non-matching references (an enclosing module's state, sibling sub-modules, other applications) denote state that is not copied along with the base's items, and are left untouched.

This makes updates of sub-modules (P.O), applied functors (F(A)), and sub-modules of applied functors (F(A).O) all well-defined: the base's items are copied, everything else is shared, and the application is baked into the copy. Behavior for plain top-level bases and for section-exit alias inlining is unchanged (empty argument and inner-path components).

Also: reject abstract-module bases with a proper error instead of an assertion, and add regression tests covering every base shape.

Closes #1085