New resolution

.codex/config.toml

@@ -0,0 +1,7 @@
+[mcp_servers.metals]
+# Coursier (cs) and Git must be available on Codex's PATH.
+# Resolve the checkout at launch time, including when Codex starts in a subdirectory.
+command = "sh"
+args = ["-c", 'workspace=$(git rev-parse --show-toplevel) && exec cs launch org.scalameta:metals-mcp_2.13:1.6.9 -- --workspace "$workspace" --transport stdio']
+startup_timeout_sec = 180
+tool_timeout_sec = 600

AGENTS.md

@@ -3,6 +3,14 @@
 
 ## Workflow
 
+When working on Scala code, use the Metals MCP tools when available for semantic
+symbol searches, inspection, documentation, and finding usages, and for quick
+file or module compilation feedback. Codex's project configuration in
+`.codex/config.toml` can launch the headless Metals server automatically.
+If Metals is unavailable, continue with source searches and SBT, and report the
+connection problem. Metals compilation and test tools do not replace the SBT
+test prerequisites and final validation below.
+
 It is best to leave the SBT shell open (by just typing the `sbt` command line)
 and issue commands directly in that shell, as SBT startup is very slow.
 
@@ -21,6 +29,11 @@ Any commit that does not include the latest changes to test outputs will fail th
 
 Please also read the files in `.github/skills/hkmc2-difftests`.
 
+Use `.mls` diff tests for compiler behavior. Do not add Scala tests that duplicate
+that coverage or merely pin internal representation or assertion details. Reserve
+unit tests for properties diff tests cannot reliably observe, such as concurrency,
+cache isolation, bounded graph growth, or algebraic laws; state the extra coverage.
+
 When you create a commit, author it under your (the agent's) own identity,
 not under the user's identity.
 Set this identity for the commit command only
@@ -73,6 +86,24 @@ When appropriate, explain the history of what led to the current implementation,
 especially if it involves non-obvious decisions/trade-offs
 or if alternative approaches were considered and rejected.
 
+Comments must be understandable from the current code alone, without the conversation,
+commit history, or an earlier version of the implementation. Explain the concrete
+invariant, behavior, or failure being prevented. Name the relevant data and operations;
+avoid vague claims about where a "lifecycle" or "responsibility" belongs. If history
+or a rejected alternative matters, include enough context to explain the tradeoff
+after commits are squashed.
+
+
+## User-Facing Diagnostics
+
+Never use `showDbg`, `shwDbg`, raw AST/IR `toString` output, or other debug-only
+representations in user-facing error messages, warnings, or diagnostic notes.
+Use source-level names and user-facing descriptions, with source locations to
+identify the relevant definitions or expressions. Do not expose internal symbol
+IDs, resolution marks, or compiler representation details to users.
+Debug representations belong only in internal logs and explicitly requested
+debug output, not in ordinary diagnostics.
+
 
 ## Editing Style
 
@@ -97,4 +128,3 @@ to ensure that no needless empty-line changes are included in the PR. If you fin
 
 When working with IR representations, please refer to the "Important design notes" in `hkmc2/shared/src/main/scala/hkmc2/codegen/Block.scala`.
 
-

doc/new-resolution-design.md

@@ -0,0 +1,240 @@
+NOTE: This document was written by Codex Astra and has not been deeply reviewed;
+it is not meant to be official documentation and
+is in fact likely to contain parts that are unintelligible to readers who lack sufficient context.
+
+
+# New-resolution implementation invariants
+
+This note describes the resolver's implementation contracts. User-facing rules
+are in the [language reference](reference.md#resolution-interfaces); outstanding
+ports and implementation gaps belong in the [migration worklist](new-resolution-suite-migration.md).
+
+## Inference ownership and completed references
+
+[`NewResolverState`](../hkmc2/shared/src/main/scala/hkmc2/semantics/NewResolverState.scala)
+owns the inference graph and caches. Listeners have type
+`TermShape => NewResolverState ?=> Unit`, so imported callbacks access hosts
+through the consuming state. Importing copies accessed hosts' candidates and
+listeners lazily; caches consult individual source entries on demand. It must
+not copy or enumerate an exporter's entire resolver maps.
+
+Type-parameter references retain their originating host. This lets exporter-private
+inference on third-party parameters survive re-exporting. Legacy annotation
+interpretations also remain local, rather than attaching consumer callbacks to
+shared prelude syntax.
+
+Completion seals each file or diff-test block's recorded decisions and original
+host data read by erasure/lowering. Symbol flow and elimination listeners remain
+active against private host data, but cannot change completed reference targets.
+This applies even between worksheet blocks sharing an elaborator state. An unknown
+reaching a sealed elimination can still report an error without changing its target.
+
+[`PublisherTest`](../hkmc2/jvm/src/test/scala/hkmc2/PublisherTest.scala)
+checks independent consumers and unchanged source candidates and listeners,
+cycles, reentrant replay, transitive private inference, and bounded copying
+in the presence of unrelated exporter hosts. `newres/GenericMethods.mls` covers
+exported mapped arrays and imported generic functions and methods.
+
+## Captures and generic flow
+
+[Instance types and parameter constraints](new-resolution-type-value-flow.md)
+specifies instance wrappers, input/output constraints, variance, canonical binder
+instances, shared body views, and partial-signature inference. Its
+[shape roles](new-resolution-type-value-flow.md#value-views-consumed-schemes-and-activation-events)
+section distinguishes captured value substitutions, consumed callable schemes,
+and inference-event activations, with examples and their representation invariants.
+[Regular structural types](new-resolution-regular-types.md) specifies normalization
+and the conservative recursion restriction. Do not duplicate those algorithms in
+member lookup or value-flow handling.
+
+Context fragments compose from a definition to its consumer; argument flow
+traverses that composition in reverse. A class and its constructor share one
+resolution boundary. Methods capture their enclosing instance scope as well as
+the enclosing function scopes. Alias qualification and structural type-field
+projection introduce no value boundary; modules introduce no invocation boundary.
+
+[Lexical paths in resolution](new-resolution-scopes.md) derives the normal form,
+boundary agreement, and depth bound from walks in the lexical scope tree. It also
+states the endpoint obligations on producers and the separate requirement for
+stable identities in recursive inference graphs.
+
+A normalized mark path contains entries followed by exits, with no repeated
+lexical boundary in either direction. `Shape.scala` enables assertions for this
+invariant. Checking each new tail costs linear time in its depth; it must not be
+replaced by truncating or widening paths. In particular, wildcard exit followed
+by wildcard entry is not an identity: it can discard a caller's activation ID.
+Reference transport uses the same operations as ordinary value flow.
+
+The prelude uses its own `#lang(0.3.x)` directive. Its loader applies file
+configuration before elaboration and erasure, and supplies the block's original
+symbols for builtin lookup during bootstrap. Its signatures therefore carry the
+same `Capture` syntax as other new-resolution declarations.
+
+Legacy consumers can read completed new-resolution signature symbols through
+`legacyResolvedSym`. The lookup asserts that the referenced block is complete and
+shares erasure's symbol-selection rules, including ambiguity and error checks.
+It does not resolve imported syntax again or observe incomplete candidate sets.
+
+`newres/SpecializationCaptures.mls`, `RecursiveEnvironment.mls`, and
+`ConstructorFieldRecovery.mls` exercise captured specialization, recursion, and
+partial construction. `PrimitiveMembers.mls`, `Arrays.mls`, `GenericMethods.mls`,
+and `MutableArrays.mls` exercise prelude signature captures and array member paths.
+Receiver reconstruction and omitted-argument context precision are
+[deferred improvements](new-resolution-future-work.md).
+
+## Declared interfaces and exposure checking
+
+Type interpretations retain arrows, type arguments, and lexical captures.
+Generic aliases and inherited declared interfaces substitute their arguments;
+declared member selections carry those contexts without reading implementation
+value flow. An unannotated member read through a declared interface produces an
+unknown shape, rather than consulting its initializer or method body.
+Inferring these missing member types is a [deferred improvement](new-resolution-future-work.md#inferred-member-signatures)
+that also requires override compatibility checks.
+Callback parameter types constrain implementation parameters, and callback results
+constrain inferred type arguments. `newres/DeclaredTypes.mls` covers these paths,
+separate signatures, tuple constraints, and distinct generic instantiations.
+
+[`InterfaceExposure`](../hkmc2/shared/src/main/scala/hkmc2/semantics/InterfaceExposure.scala)
+checks values reachable through a file's exposed interface before completion.
+Worksheet blocks run this pass only under strict resolution. It seeds unannotated
+parameters with `UnknownValueShape` and follows returned functions, record/tuple
+contents, public instance members, and both interpretations of exposed overloads.
+Callable result annotations constrain returned implementations through their
+declared domains. Private helpers retain local inference unless their values escape.
+
+Discovery uses a queue and temporary observers of shape publishers. Each reached
+shape is processed once, with listeners discovering subsequent candidates;
+there is no repeated whole-graph scan. Observers detach before completion and
+are never copied into consumer states. Imported new-resolution definitions have
+already had their interfaces checked and are not recursively checked by importers.
+
+Unknown values and unresolved spreads carry shared, lazy provenance. Messages,
+locations, and diagnostic chains are materialized only on error; provenance does
+not affect shape equality. Diagnostics can identify the parameter and the storage
+and return steps that expose it. `newres/InterfaceExposure.mls` covers discovery,
+typed closures, overloads, and later exposure of a private definition from an
+earlier block; its expected failures also document remaining precision gaps.
+
+## Structural and dynamic shapes
+
+Record fields have their own `BlockMemberSymbol`s. Lookup follows overwrites and
+spreads in source order, preserving selected values' shapes and captures. Named
+fields in term tuples are expressions, not type annotations. Tuple shapes group
+them into one trailing record, matching lowering while retaining source evaluation
+order, last-write-wins lookup, computed-key uncertainty, and property identities
+across imports. See `newres/NamedFields.mls`, `ImportedNamedFields.mls`, and
+`RecordInterfaces.mls`.
+
+Tuples preserve zero-based projections and expose the builtin Array interface.
+An Array callback receives candidate shapes from every element. The
+[language reference](reference.md#10-arrays) specifies mutable-array behavior and
+the restriction imposed by explicit element annotations.
+
+For a mutable literal, all element reads and writes use the builtin `Array[T]`
+parameter's symbol. Marks distinguish allocations and enclosing calls. Cache the
+nominal view before subscribing to the initializer so empty arrays can receive
+writes and recursive arrays can refer to themselves. Numeric projections, spreads,
+patterns, and callbacks all use the same element endpoint.
+
+The nominal interface is located at the literal's use site. Its element reference
+carries the allocation exit; the interface itself does not. Member lookup already
+exits the nominal class scope. Adding the allocation exit to the entire view would
+therefore cross that boundary twice. Initializer shapes enter the allocation
+context before reaching the parameter host.
+
+When an array is returned or otherwise exposed to callers, `InterfaceExposure`
+also follows its element shapes. A function stored in that array must be checked
+for calls from outside the compilation unit, just like a directly returned
+function. `newres/MutableArrays.mls` and `CompilerTest` cover element flow,
+separation between calls and importing compilation units, and exposed functions.
+See the [migration worklist](new-resolution-suite-migration.md) for the remaining
+`splice` contract and storage-reassignment gaps.
+
+When an array's element shape is unknown, indexed access produces an unknown
+shape; that does not authorize arbitrary member access on the result.
+Tuple-pattern transfer handles leading, trailing, and rest elements, including
+declared Array element types. See `newres/Arrays.mls` and `TuplePatternBindings.mls`.
+
+An unknown-length tuple segment retains a deferred element field, just as a
+fixed tuple position does. Tuple views instantiate both through the same field
+representation, and indexing, array interfaces, argument transfer, and patterns
+observe that field through `listenTupleField`. Unknown length does not erase the
+element's type arguments or captured environment. A positional selection after
+a spread includes every field that can occupy that position, including a fixed
+suffix when the spread is empty; positions before a spread remain precise.
+`newres/ArraySpreadViews.mls` covers these cases and distinct generic callers.
+
+`DynShape` is distinct from `UnknownValueShape`: recursive widening, mutable reads,
+and other losses of precision do not license dynamic lookup or calls. Known invalid
+alternatives still report errors alongside dynamic candidates. Constructor patterns
+narrow unknown inputs to declared class interfaces, retaining unknown type arguments
+and provenance for unannotated fields instead of specializing them from local calls.
+
+Dynamic selections have no fabricated nominal definition. Lowering retains the
+runtime receiver and property name. Dynamic values propagate through record/tuple
+spreads and unique wildcard opens; competing wildcard receivers still need
+disambiguation. Class projections, constructor patterns, and type references require
+known, unambiguous identities. See `newres/Dynamic.mls`, `Records.mls`,
+`SpreadCalls.mls`, and `loose/Targets.mls`.
+
+## Recursive getter results
+
+Parameterless definition bodies have a shared result host, cached by definition
+and generic activation before following the body. Recursive references subscribe
+to that host instead of traversing the body again. An unproductive cycle has no
+normal result candidates; a productive branch publishes candidates through the
+cycle, with the publisher suppressing duplicates. No unknown or dynamic fallback
+is introduced to stop recursion.
+
+The host stores results at the body's lexical endpoint, including their activation
+events. Each reference still applies its own exit and capture marks. Resolver-state
+caches and consumer-local publisher copies preserve this graph across imports
+without sharing mutable inference between consumers. `newres/RecursiveGetters`
+checks cycles, later candidates, captures, generic specializations, imports, and
+runtime getter effects.
+
+## Normal results of control flow
+
+Resolution must agree with lowering about which expressions produce values.
+Assignments, `drop`, imperative conditionals, and loops return unit; their
+operands or branch results must not supply the result's member interface.
+A normally completed `try` returns its body's value, preserving its capture
+marks, while the `finally` clause runs for effects. `throw` and `continue` supply
+no normal result. `newres/ControlFlowResults.mls` checks these contracts, including
+backtracking assignment and independent calls through cleanup blocks.
+
+## Overloads, foreign declarations, and lowering
+
+Ordinary values select function/constructor overloads; selection receivers select
+companion modules. Preserve this distinction through nested captures and opens.
+`newres/OverloadedCalls.mls` covers direct, generic, stored-function, module-member,
+and captured uses.
+
+Bare classes can share their name with a function definition that has a parameter
+list. The generated function owns the class reference, so JS uses the existing
+`.class` property for references, selections, and imports. Arbitrary values,
+parameterless functions, and term declarations cannot supply that companion:
+their results may be primitive, aliased, or frozen, and must never be augmented.
+Instance methods cannot supply per-instance companions either, because their
+function objects are shared. Inlining may replace calls to a companion function,
+but must preserve its binding while the class is used. WASM identifies constructor
+functions by their class symbols, separately from explicit function companions.
+Session imports follow the selected definition and cast target, rather than MIR
+`freeVars`, which tracks lexical bindings introduced by `Scoped`. Importing a
+class must not also import its function companion: the two have independent
+signatures and can be shadowed independently in later worksheet blocks.
+
+Foreign declarations expose call and constructor capabilities explicitly.
+The JS backend uses native class values for `new` and patterns without generated
+MLscript `.class` storage. Bodyless foreign methods use foreign-call normalization
+even when `declare` is on the enclosing class, so JavaScript `undefined` results
+follow the existing unit normalization. Prelude declarations are parsed as one
+compilation unit, permitting references across blank lines.
+
+Generated runtime-helper selections, such as `runtime.assertFail`, are synthetic;
+they do not provide a fallback for unresolved source selections. Free-variable
+collection and assignment lowering must handle resolved direct references and
+retain the existing binding/assignment checks. Constructor-pattern resolution
+discards every nested capture when recovering class identity; leaving one behind
+can make generated patterns test a constructor function instead of its class.