Read a value's trait requirements together, and write back what they determine - #94
Merged
Merged
Conversation
dpmills
force-pushed
the
dmills/unsatisfiable-trait-operand
branch
7 times, most recently
from
August 13, 2026 19:18
61fd4da to
7ff5c6d
Compare
dpmills
force-pushed
the
dmills/unsatisfiable-trait-operand
branch
from
August 13, 2026 23:42
7ff5c6d to
1bcffa3
Compare
dpmills
force-pushed
the
dmills/unsatisfiable-trait-operand
branch
from
August 14, 2026 19:49
1bcffa3 to
9f6523e
Compare
dpmills
marked this pull request as ready for review
August 14, 2026 21:00
dpmills
force-pushed
the
dmills/unsatisfiable-trait-operand
branch
from
August 14, 2026 22:00
9f6523e to
82ef013
Compare
sortalongo
approved these changes
Aug 17, 2026
…determine
Discharge is delivery-driven: an obligation learns only what is *offered* to
it, one contribution at a time. That is enough to reject a bad call and not
enough to reject a bad definition. In
```
f = \a -> (a + 1, a + "s")
```
each obligation is narrowed through its **other** operand — one to `{Int}`, the
other to `{String}` — and neither set is empty, so neither fails. Nothing ever
compares them. `a` is required to be `Int` *and* `String`, no argument can
satisfy both, and with no call site the definition type-checks. On `main` the
two demands collide as `IncompatibleBounds` on one variable; making operand
requirements independent is what opened the hole.
Delivery cannot close it, because the hole *is* the case where nothing arrives.
So after emission the solver reads each value's requirements together.
The value a requirement constrains is not always a variable. `\a, b -> …`
passes its parameters through a tuple, so each occurrence of `a` is a separate
variable and no variable carries both of `a`'s requirements — while curried,
the same program shares one variable and does. Only the spelling differs, so
the unit cannot be the variable.
A **place** is a variable plus the path of field selections reaching it.
Requirements are gathered by following **upper** bounds, since `v <: U` means
`v`'s value reaches `U`; a variable bound stays at the same place, a structural
one descends, so `U₀`'s requirements in `v <: (U₀, U₁)` belong to `v`'s
component 0 and never to `v`.
This is deliberately not what `link_watches` computes. That runs when an edge is
*recorded*, so an edge predating an obligation never carries it, and it follows
*variable* edges only, so it stops at exactly the structural hop a
multi-parameter lambda introduces. Reading the graph once, at the end, depends
on neither accident — which is what makes currying unobservable and rejects
programs that are unsatisfiable only transitively:
```
f = \a, b -> (a + b, a + 1, b + "s")
```
No single requirement is wrong and no variable carries two; `a + 1` pins `a`,
which leaves `a + b` one row and pins `b`, which `b + "s"` contradicts.
- **Empty** — no type satisfies them all, so no argument could. Rejected as
`UnsatisfiableOperand`, listing the requirements rather than naming a type
that "doesn't match", because none arrived.
- **One base** — deposited as an **upper** bound on every variable at the place,
and the obligations there are narrowed by it (the bound alone would not reach
them: it is an upper bound, and narrowing consumes lower ones).
- **Several** — genuinely open, which is the honest answer.
The deposit is not merely how a determined type is published. It is the only
half that can catch a requirement contradicting something that is *not* a
requirement — an annotation, or a monomorphic operator's operand are ordinary
bounds, invisible to any intersection.
An operand takes an **upper** bound, an associated position a **lower** one.
The table's claim about an operand is not what flows in but what *may* — the
requirement restated where the solver can read it. A lower bound there would
manufacture a value the program never supplied and would let an under-connected
lowering pass by inventing the type its missing edge should have carried; an
upper bound cannot, because it gives coalesce nothing to resolve *to*.
`\a, b -> a + b` is the check: every row still stands, nothing is determined,
both parameters stay open.
The visible consequence is that operand types get more precise —
`\x -> x + 1` is now `Int ⇒ Int` rather than `?α ⇒ Int`. One test asserted the
old imprecision and is updated.
The sweep runs **after emission**, when a definition's requirements are all
recorded, and **before coalesce**, because a generalized definition's subtree is
never coalesced in place — walking the tree instead would see only use-site
clones, and a clone that goes unsatisfiable already fails by delivery. It runs
**to a fixpoint**, because determining one place can leave a neighbouring
obligation with a single row and so determine another; a single pass would make
the answer depend on the order variables happened to be minted in
(`a_determined_operand_cascades` pins both binder orders).
That placement rests on a definition's candidate sets being final once the sweep
has run — the kind of assumption that fails silently, since a later pass
narrowing a definition's obligation would leave the verdict stale and quietly
stop rejecting programs. `narrow` therefore carries a `debug_assert!` that
afterwards only an obligation minted since the sweep — a freshened clone — may
still shrink.
Blame is read out of the tree (`blame_node_for_place`), not stamped onto the
obligation: a `NodeId` is provenance, and one cached in the solver would be
copied onward by every clone the obligation makes, outliving the construct it
identifies. A place can be interior, named by no node's type, so blame tries
every variable standing there and falls back to the root — coarse, never wrong.
`OperandFailure::Conflict` is kept only because `constrain_subtype` is fallible,
and is documented as not known to be reachable: constrain *records* a bound
rather than checking it against those already present, so a contradiction
surfaces at coalesce as an ordinary `IncompatibleBounds`. A probe across the
suite and over programs written to provoke it never entered that arm.
Also extracts `accepted_at`, the candidate-set projection previously written
inline in both `reject` and `narrow`.
`blame_node_for_place` answers "which node's type is written in terms of
this variable", outermost-first, and read that off `walk_type_slots` —
which also visits binder slots. Main now fills a `let`'s binder slot
during emission rather than leaving it for coalesce, so for
g = 2
f = \a -> (a + 1, a + "s")
g
the `let` binding `f` mentions the variable one level above the lambda
that actually carries the conflicting requirements, and shadowed it.
A binder's type is always mirrored somewhere the walk already reaches:
a lambda's parameter type is its own type's domain, a `let` binder's is
its definition's. So a binder slot never makes a variable reachable that
would otherwise be missed — it only lets an enclosing node answer for a
type its child owns. Blame now reads the node's own slots (its type, an
annotation written on it, a cast target) and leaves binders to the nodes
that own them.
Review feedback on the requirement sweep's design section: the definition introduced "place" without saying what kind of variable it was about, and the example silently switched between the two senses. A specific field of a structural bound *is* itself a variable — `descend` follows a component only when it is a `Type::Infer` — so defining a place as "a variable plus a path" reads as though the path led somewhere that is not a variable. The value is the unit; the variable-plus-path is how it is named, and several variables stand at one place. Say that, and say that the positions are *inference* variables, since the lambda example is about a source-level parameter and the two were being used interchangeably. Also drop the exhaustive-match rationale from the doc: `places_under`'s own comment already carries it, and repeating it here was the second copy.
Three definitions of "place" were in circulation and no two agreed. The type alias was the path alone, `PlaceInfo` was what stood at the path, and both doc comments called a place "a variable plus a field path" — while the loop header read `for (_, place) in places_under(root)`, binding a `PlaceInfo` to `place` and discarding the value actually typed `Place`. Within one line, `Place` and `place` were different types. Give each name the thing it describes: * `Place` is now the struct — the variables standing at one value together with every requirement landing on them. That is the unit the sweep intersects over, and the thing the design doc defines. * `StepPath` is the `Vec<Step>` key. It is only ever a key, only within one `places_under` call, and nothing reads it back, so `resolve_pass` iterates `into_values()` and states that. Naming the struct `Place` also answers the question the old wording invited — whether a field of a structural bound is itself a variable. It is, and `Place.vars` is plural for exactly that reason. No behavior change.
dpmills
force-pushed
the
dmills/unsatisfiable-trait-operand
branch
from
August 18, 2026 03:26
b0cfc59 to
780cc03
Compare
dpmills
added a commit
that referenced
this pull request
Aug 18, 2026
…ong question
Both surfaced from PR 54, and both are this PR's to fix — one is a regression it
introduced, the other it makes reachable.
**A variant found positively is the value, not a gap.** `no_concrete` excluded a
variant shape at every polarity, so the collapse fired past one and the fallback
arm replaced it. Read negatively that exclusion is right — an arm binder's upper
bounds are the arms the body can *handle*, and a domain must still fetch the
argument. Read positively the variant comes off the lower bounds and is what the
value is, so overwriting it hands back the position's own upper bound: with
`x <: {`some{Int} | `none} = `some(1)`, the binder came out as the annotation,
`none` tag and all, instead of `{`some{Int@1}}`. A bounded annotation had stopped
behaving like a bound. Records and atoms need no such split, being the same claim
from either side.
**The pin's gate asked what determines the position, not what reached it.** An
ordinary resolve reads the opposite side when the polarity-correct walk comes up
empty — so an upper bound alone makes a never-inhabited position report a type,
and reading a value's trait requirements together (#94) deposits exactly that on a
dead arm's payload. The pin then skipped the arm, its slot recorded `Int`, and the
merge over the arms could not see that position contribute: the recorded node type
came out narrower than the join and the post-inference wall rejected a program
that type-checks. `compact_type_polarity_only` asks the other question — the
polarity-correct walk alone, collapse suppressed — and `value_reaches` is the pin
gating on it. Walk-wide rather than at the entry, which is the same thing:
`fallback_allowed` already confines the collapse to the entered position.
Both are IR-expressible, so both regression tests sit in `inference_variants.rs`.
The second asserts through `check_pre_desugar`, since inference itself reports
`Int` and no error — the wall is where the disagreement surfaces.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Currently, satisfying a trait obligation is delivery-driven: it learns only what arrives, one contribution at a time. That rejects a bad call, not a bad definition. In
f = \a -> (a + 1, a + "s")each obligation narrows through its other operand — one to{Int}, one to{String}— so neither set empties and nothing ever compares them: no argument satisfiesa, yet uncalled the definition type-checks.This PR adds a pass between emission and coalesce that reads each value's requirements together, rejects a value no type satisfies, and writes back what they determine as an additional constraint
This lets us correctly reject uncalled functions with trait bounds that are unsatisfiable, and also lets us give principal types to at least some more uncalled functions (e.g. \x -> x + 1 can now be typed as Int => Int, at least until we add heterogenous Addable). It's also a requirement for any future work that wants to correctly assign principal ForAll types to functions that are legitimately polymorphic