Make module subtyping checks proportional to the expected signature, cache repeated field checks

[JasonGross]

Fixes #22279 (quadratic time when chaining module types with <+).

Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.

Problem

Every <+ of a functor module type triggers the "Include Self" subtyping check of the whole accumulated signature against the functor's parameter signature, twice (once with universe inference in Declaremods, once in the kernel). Subtyping.check_subtypes did two things proportional to the size of the subtype side, even when the expected signature needs few or no fields checked:

1. strengthen eagerly rebuilt every accumulated constant field;
2. check_signatures eagerly built a label map (make_labmap) over the whole accumulated signature.

For a chain of n interfaces this is O(n²) with significant constants. Instrumented at n=800 (10 parameters per interface, empty parameter signature): 3.3s of CPU in the single Module Type ... := I1 <+ ... <+ In command, ~1.6s in strengthen, ~2.3s in make_labmap, across 1600 check_subtypes calls.

Fix

Commit 1 — make each check proportional to the expected signature. All non-checker callers of check_subtypes guarantee that the subtype side's fields are already in the environment, unsubstituted (the invariant documented in check_structure for the nargs = 0 case). A new direct flag makes check_signatures look fields up in the environment by name on demand, strengthening constant and submodule fields individually at lookup time (mirroring exactly what Modops.strengthen produces per field). Lookups fall back to the lazily-built label map whenever the label does not name a field (constructor names, secondary inductive types of a block), preserving existing behavior, error messages, the checker paths, and the recursive cases where the environment holds substituted fields.

Commit 2 — cache successful field checks. Prefix-shaped chains (each stage parameterized by the whole chain so far) and repeated applications of the same functor legitimately perform quadratically many field checks. Successful checks of a constant field pair are now cached under conditions that make the verdict a function of the pair alone, all checked at run time: both substitutions leave the bodies physically unchanged, and the check produced no new universe constraints (the returned state is physically the input one — true of the kernel checking mode always, and of the inference mode exactly when the needed constraints are already entailed). Cached verdicts stay valid while the environment grows monotonically, so the cache is purely functional and lives alongside the environment it was computed in: it is threaded through Mod_typing/Subtyping and stored in a field of the kernel's safe_environment on the checking side, and in a summary-registered reference on the inference side (Declaremods). Discarding or rolling back the state (Undo, Reset, document navigation) thereby discards or rolls back the cache with it — there is no global mutable state in the kernel and no invalidation obligation on callers. The cache is indexed by field label with a short capped list of physically-compared pairs, so lookups are cheap and retained memory is bounded.

Measurements

(Module Type command time from -time, or wall time for whole files; baseline is current master)

shape	baseline	this PR
#22279 benchmark: 800 chained interfaces, 10 params each, empty Args	3.33 s	0.15 s
800 chained interfaces, 2 params each, shared 3-field Args	0.46 s	0.05 s
prefix chain, 400 stages (~160k field re-checks)	6.8 s	~6.9 s, checks reduced to 400 cache misses + 160k hits totaling <0.2 s (the rest is materializing the quadratic amount of signature content, unrelated to subtyping)
100 applications of one functor to a 1000-field module	2.5 s	0.5 s

Tests

test-suite/modules/IncludeSelfChain.v covers chains over empty and non-empty parameter signatures (including definitions checked up to conversion, inductive types and submodules in the parameter signature), rejection of ill-typed chains, prefix-shaped chains, repeated functor applications, and a Reset-and-redo of a check whose universe constraints must be reproduced (exercising the cache flush). The modules, success, failure, bugs, and output test-suite subsystems pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw

[SkySkimmer]

I don't think we want such a footgun in the kernel

[JasonGross]

I had fable thread a cache instead

[ppedrot]

This still doesn't look like the correct way to fix this, even though I haven't given a lot of thought about a potential solution yet.