Never substitute bound type variables; defer rigid fundep improvements

[nanavati]

A functional-dependency improvement that meets a rigid (signature- or instance-quantified) type variable must become an equality constraint, never a substitution. Numeric and ATF positions already worked this way; this PR extends the same design to value kinds: mgu now refuses to bind a bound type variable to structure, closing the hole, found by the bound-variable audit, where fundep improvement could rewrite a signature out from under its binder (misreported as T0029 "signature too general"). It also adds the complementary check at the other end of a quantifier's life: a locally quantified variable must not escape into enclosing bindings (T0161).

Stacked on #1036 (which carries #1032, #1033, and #1035): the 5 commits from "Never substitute bound type variables; defer rigid fundep improvements" onward are this PR's content.

Rigid-induced failure defers; structural clash stays final

A unification failure induced by the rigid-variable guard is not a conflict — the predicate may be satisfiable by a given, or at a call site that instantiates the variable. matchTop and matchTopIsReducible distinguish the two by re-running the fundep mgu unguarded: guard-induced failures defer the match (an approximation of an explicit type-equality constraint), structural clashes remain final (T0159, from #1035). This keeps the recursive AppendTuple''/Curry' instance methods in the Prelude compiling — they re-encounter their class with the instance's own rigid variables, and the discharge is the instance's given — while genuine output clashes still fail fast. In the Match result type this is a new Defer arm, discriminated in matchFDRow and ranked by firstMatch (Match > Conflict > Defer > NoMatch).

Modal checks ask "could this ever match?" — so they unify unguarded

The commitment machinery's modal checks — the walk's incoherence accumulator, sat's given-escape gate, matchTopIsReducible's could-eventually-unify probe — quantify over futures in which call sites instantiate rigid variables and enclosing frames supply givens over distinct rigid variables. Guarded, they turned "not yet" into "never", and "never" is what licenses a commitment: the Generic-default catch-all was committed for PrimDeepSeqCond predicates inside definitions whose call sites would have selected specific instances, stranding unsolvable Generic subgoals. The instance-overlap check likewise went blind to orthogonal overlaps. These probes now unify unguarded. orderInstHead and the ContextErrors message-selection probes get a dedicated modal unifier, mguModal, which keeps the bound set as a variable-direction preference only, preserving how orderInstHead attributes specificity by which side of a unification lands in the substitution's domain.

The discipline is enforced mechanically: local substitutions are built everywhere (scheme instantiation, instance freshening, the modal probes), but the global substitution has exactly one add-path, extSubst, and under the development flag -check-subst-bound it rejects any extension whose domain contains a bound variable — "bound variables have exactly one binder", checked at the point where unification results become globally visible.

Skolem escapes are rejected at generalization (T0161)

The unifier's guards keep a skolem from being substituted, but an outer metavariable may legally be bound to a skolem — the allowed direction — and if such a binding survives the type check of the definition that binds the skolem, an enclosing binding generalizes or instantiates the locally quantified variable. Previously this was accepted and exploded downstream as an elaboration-time internal error. The check is one set intersection at tiExpl''': this definition's bound variables against the free variables of the substituted outer assumptions — a set the generalization machinery already computes. A hit reports T0161, naming the escaping variable and the enclosing bindings that would capture it. HREscape2, previously an ICE, is now a positioned type error.

Reporting

Deferred predicates are re-reduced outside the bound set they failed under, so findReducedPreds tolerates preds that re-reduce fully at report time. T0020 suppresses generated _tc... temporaries as subjects (a bare "Type mismatch" plus the position, instead of an internal name with unstable numbering). Two module-arity tests now report the precise T0084 (naming the function and the expected arguments) instead of T0107/T0108 guesses; the too-general-signature tests now report at the offending expression instead of reporting T0029 at the definition. GenWrap and GenFuncWrap position wrap-field method applications at the field/function they wrap, which routes an undischarged WrapField proviso to the synthesis reporter: in NoInline_ResNotInBits, a third T0043 naming the offending type replaces the signature-mismatch T0029.

Commit-by-commit

1. Never substitute bound type variables; defer rigid fundep improvements — everything above except T0161.
2. testsuite: skolemization pins for polymorphic struct fields — higher-rank pins.
3. Reject skolem escapes at generalization (T0161).
4. testsuite: bound-variable audit goldens — behavior-shape pins from the bound-variable audit (deferral, conflict, and equality-hint message shapes).
5. testsuite: pin the modal earlier-instance-may-capture judgment — ModalCapture: the commitment gate's modal question answered across rigid instantiation.

Validation

• Full bsc.typechecker sweep including the new pins passes clean.
• The full testsuite result at this exact tip will be posted as a comment.

The stack: #1032 (instance-trie fixes) and #1033 (coherence keywords + coverage warning), independent → #1035 (ordered-clause commitment) → #1036 (SAT settlement) → #1037 (bound-variable discipline, this PR) → #1038 (solved-dictionary pool). Each PR contains the ones below it.

🤖 Generated with Claude Code

https://claude.ai/code/session_018wageSF1tZAS25nrsrbPnZ

[nanavati]

Full-testsuite result at this PR's head (6d19cdb), as promised in the description:

• 18,510 PASS / 129 XFAIL / 6 FAIL across 869 test directories (make fullparallel, Verilog backend via iverilog 12.0, C backend, and SystemC tests enabled), from a from-scratch build.
• All 6 FAILs are environment artifacts of the test machine, reproduced identically on near-main builds without this stack: 5 are the cascade from a deterministic GHC RTS stack overflow in bsc.long_tests/log2_loop/actionvalue under that test's +RTS -M300M cap, and 1 is iverilog 12's "Excess hex digits" $readmemh warning polluting bsc.long_tests/MPEG4's expected simulation output. The same two artifacts (and nothing else) appear in the runs recorded on Ordered-clause fundep semantics: commit coherent instance matches #1035 and Settle numeric provisos once per definition, in one SAT session #1036.

The count reconciles with the base exactly: #1036's 18,493 passes + 17 new checks from this PR's pins (skolemization, bound-variable audit goldens, ModalCapture, and the noinline expectation now counting a third T0043) = 18,510.

[krame505]

Relative diff nanavati/bsc@nanavati:bsc:claude/sat-batching-settlement...nanavati:claude/bound-variable-discipline seems okay to me.

[nanavati]

Rebased onto current main (941eecf) and force-pushed (6a1639a). What the rebase resolved: Adapted the StrArg type-proxy construction to main's reworked GenFuncWrap.funcDef (now threads args and builds positioned name/arg_names string literals); testsuite layers rebased clean.