[MicroProofs]

Summary

This branch holds the type-system audit work. It restores Elm's constraint tree in place of direct inference, fixes four type-system crashes and a crash in long diagnostics, fixes four wrong results in type checking and code generation, adds the representation coverage rule for impls that are split by element representation, and replaces the separate search budgets with one compile fuel counter. Twenty-four commits, seventeen changesets.

Behavior changes:

• same : Eq 'a => list 'a -> list 'a -> bool compiles. When the representation of a rigid variable selects the impl, the annotation must state the trait at that variable. A missing one is a missing-constraint error such as Eq 'a, not a missing impl for the container.
• A phantom type parameter that no use fixes no longer stops nash test or nash build with "superclass resolution requires a ground type".
• Three contradictory representation contexts are now errors at the context. Each one crashed the compiler before: (Big ('f 'a), Little ('f 'a)), Little 'a inside Big 'a => ..., and an impl context that contradicts a superclass of the impl's trait.
• A trait constraint on an infinite type no longer crashes the compiler or gives a false impl-resolution-limit error. The occurs check reports the infinite type.
• type alias Xs = List Int works with List.length and other functions over 'f 'a.
• When an annotated body fails to type check, its callers are still checked against the annotation, and values passed to it are no longer reported as ambiguous.
• An annotated definition publishes its declared type, so importers find the impls of an alias in its annotation.
• nash check, build, test and docs have no search limit. Programs that the fixed work and depth limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. On main, depths 127 and up failed. A looping impl now runs until stopped.
• The language server gives each module 10 million compilation steps, so a looping program reports COMPILATION STEP LIMIT (nash::type::out_of_fuel) after about a second and a half instead of freezing the editor. This one error replaces nash::type::impl_resolution_limit, nash::names::impl_pattern_limit, and the code generation specialization, evidence and recursion limits.
• nash check no longer crashes with "Doc::text must not contain newlines" when a missing-constraint or missing-impl predicate is wider than 80 columns. When such a sentence does not fit the line, the predicate moves to its own line, indented by 4.
• A tuple or record type wider than the line puts one entry on each line, as Elm does.
• The record after "Available fields:" lines up under its opening brace.

Versioning: minor bumps for nash-ast, nash-can, nash-cli, nash-codegen, nash-constrain, nash-driver, nash-language-server, nash-report and nash-solve; patch for nash-docs. See .sampo/changesets/.

Elm constraint tree (refactor(types): restore the Elm constraint tree)

• nash-constrain generates Elm's constraint tree from the canonical AST again, and nash-solve walks it. The direct-inference files are deleted.
• The generator and the walker are the files that 0ed0c75a ("refactor(types): infer directly from AST") deleted. The features that six later commits added to direct inference are ported into them: per-node type records for code generation (SaveType), module tests, overloaded Bool and Unit literals, assert, fail, todo, trace and comptime, native pair patterns, and the regions that diagnostics point at.
• No existing snapshot changes. The published annotation type is the one behavior change. Its regression test is annotated_alias_result_keeps_its_impl_for_importers_after_a_wider_call.
• refactor(constrain): carry the tests scope on record field constraints removes the Nash-only TestScope constraint. Record and Field constraints carry whether they come from a module test, so the solver keeps no state for it. The constraint language is now Elm's plus SaveType. Field visibility does not change. test_imports_grant_field_visibility_to_every_field_form_in_tests covers the accessor, update and record-pattern forms in both scopes.

Crash fixes

Each fix has a test for the audit case that crashed.

• fix(traits): reject contradictory representation contexts on type applications groups representation predicates by type, not only by plain variable.
• fix(solve): reject representation givens that contradict an enclosing annotation checks a local annotation together with the enclosing annotations, which share its type variables as in Elm.
• fix(traits): check every impl context through its superclasses runs the superclass check in check_impl. An impl with no methods used to skip it.
• fix(solve): do not select impls for infinite types makes the constraint wait for the occurs check of its binding, as in Elm. occurs::reaches_cycle visits each variable once.

Representation coverage (feat(traits): select representation-split impls by coverage)

• nash_ast::head::cover_impls first checks that a given states the trait at each rigid variable that selects the impl. It then selects an impl for every admitted representation of those variables.
• The evidence is the new Evidence::Specialize. Code generation selects the impl for each use and keeps the selecting types in the specialization key.
• Superclass proofs in nash-can do not use the rule.

Open types in superclass evidence

• fix(solve): resolve superclass evidence for open phantom types. nash_solve::evidence::resolve keeps open type variables. An open variable equals only itself. Resolution reports NonGround only when impl selection, a representation test, a reflexive Lift or the requirements of a type need the variable.
• The new nash_ast::head::Open gives impl selection that view. nash_codegen::evidence::Error::NonGround is removed.
• The driver test phantom_type_through_a_superclass failed before the fix. The solver test open_type_that_selects_a_superclass_impl_is_a_type_error shows that type checking rejects the case where the open variable would select the impl.
• fix(solve): let a selected impl prove an open type that another impl cannot decide keeps impl selection under SelectPolicy::Exact, so an impl that matches whatever the variable is wins over a candidate that only the variable could decide. An undecided reflexive Lift goes on to impl search. The driver test phantom_pair_through_a_superclass failed before this commit with "cannot resolve superclass: NonGround".

Solver diagnostics

• fix(solve): unify type applications with transparent aliases by their bodies
• fix(solve): keep a failed annotated body's annotation for its callers
• fix(solve): do not report types stranded by a failed call as ambiguous

Long diagnostics

• fix(report): break tuple and record entries as Elm's D.cat does adds Doc::pcat, Elm's D.cat. Tuple and record entries were joined with no break point, so a wide type broke only inside its last entries and drifted to the right. source_pipeline_tuple_wider_than_the_page shows the new layout.
• fix(report): build long trait help lines from document parts fixes the crash. The help line rendered the predicate to a string and placed it in one piece of text, which cannot hold a line break. Each sentence with a predicate is now laid out like the rest of the report, and a sentence that does not fit moves its predicate to its own line. Sentences that fit render as before. Three existing snapshots of 81 to 97 columns now wrap.
• fix(report): align the record after Available fields under its brace changes six snapshots, in indentation only.

Compile fuel, shared trait search and indexes

• refactor: replace search budgets with one compile fuel counter. Trait search, overlap checks, superclass entailment, evidence and code generation each had their own work or depth budget, and they counted work differently. On this branch before this commit, a nested impl C 'a => C (wrap 'a) used at depth 178 to 255 passed nash check and failed nash build with no location. nash_ast::fuel is now the one step counter. The driver installs it around each module's compile (Unlimited for the command line, Limited(10_000_000) for the language server), and every search loop calls tick(). The constants WORK_LIMIT, DEPTH_LIMIT, MAX_SPECIALIZATIONS and MAX_TYPE_DEPTH, the 4096-step normalization limit, and every budget parameter are deleted. Superclass cycle detection and the polymorphic recursion error stay. deeply_nested_impl_context_checks_and_builds_without_a_depth_limit checks and builds the depth-200 case, and fails before this commit. a_looping_program_reports_running_out_of_fuel_instead_of_hanging covers the language server.
• The earlier commits refactor(traits): keep the trait search limits in one place, feat: raise the trait search and specialization depth limits to 256 and test(codegen): build the deep type from the depth limit are superseded by the fuel commit. Their changesets are removed.
• refactor(traits): share impl selection between inference, entailment, and evidence adds select_impl with SelectPolicy::Defer and SelectPolicy::Exact. A second matching impl stops the compiler as a coherence bug.
• perf(solve): index kind contracts, recovery edges, and scheme records replaces scans of every earlier record with indexes that follow union-find merges. refactor(solve): remove the step 03 scan oracles removes the debug-build checks that compared each index with its old scan, and the two randomized tests that drove them.

Build and examples

• build: optimize the compiler crates in the dev profile
• fix(examples): move test-only imports into tests blocks. nash build strips tests blocks, so imports that only tests use were reported as unused.

Not in this PR

• The Plan 11 document commits and the macro work, including audit steps 01, 10 and 11. They stay on plan-11.

Test plan

• cargo fmt --all -- --check
• cargo clippy --all-targets --all-features -- -D warnings
• cargo nextest run --workspace (3,936 tests)
• nash build and nash test in examples/vesting (10 tests pass)
• nash build and nash test in examples/order. The property compare is antisymmetric fails because invert returns its argument unchanged. The example has had that since ltmkrkqv.
• nash check gives a diagnostic for each of the 13 audit reproductions, with no crash.
• nash check and nash build succeed at nesting depths 177, 178 and 200 of impl C 'a => C (wrap 'a).