Register no witness for finalized protocols - #3045
Open
plajjan wants to merge 2 commits into
Open
Conversation
Three build-failure projects capture how witness resolution behaves when extensions of one class are spread over modules. witness_rival_direct__bf: two modules, neither importing the other, each declare a conditional Pick extension for Box. Both witnesses are genuine rival implementations, so resolving Pick[Box[Both]] is ambiguous. This must keep failing. witness_rival_ancestry__bf: the same rivalry, except each module implements Pick through its own child protocol, so both witnesses reach Pick through their inheritance ancestry rather than declaring it directly. Equally ambiguous, and it must also keep failing, in either import order. witness_canonical_import__bf: module points declares Pt and extends it with Ord, which covers Eq; module hashpt extends Pt with Hashable, whose inherited Eq slots are thereby finalized, so hashpt implements none of them. There is exactly one Eq[Pt] implementation, yet declaring the Hashable extension makes every == involving Pt fail to resolve, both inside hashpt and in any module importing both. This failure is a deficiency; the next commit makes resolution find the one implementation, and flips this project into a running test.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ef70c0fbd3
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
An extension covers its protocol's whole inheritance ancestry:
extending Pt with Ord also makes the extension a witness for Eq,
because Ord inherits Eq. The first extension to cover a protocol owns
it: the type checker requires it to implement the protocol's methods,
and every later extension covering the same protocol is forbidden
from implementing them again (checkAttributes calls these methods
finalized). So for each protocol and type there is exactly one
implementation, held by whichever extension came first.
Witness registration did not follow that rule. An extension
registered a witness for every protocol in its ancestry, including
the finalized ones it holds no implementation for. Such an entry is
an empty shell: resolution that lands on it finds methods the
extension was not allowed to write. Within one module the shells were
harmless, because registration deduplicates against the local table
and the owning extension's earlier entry wins. Across modules there
was no deduplication at all, since the local table and the imported
interfaces are enumerated separately:
# module points
extension Pt (Ord):
def __eq__(a, b): ... # the one Eq[Pt] implementation
...
# module hashpt
extension points.Pt (Hashable): # Hashable inherits Eq
def hash(self, h): ...
hashpt's extension implements nothing of Eq, which is finalized by
points' Ord extension, yet it registered a second Eq witness for Pt.
The constraint solver requires exactly one candidate per witness
lookup, so every == involving Pt stopped compiling, inside hashpt and
in every module importing both. In practice, extending an imported
class with any protocol that inherits something was unusable.
Nothing about a registration itself distinguishes a shell from a
genuine implementation declared in an unrelated module; the
distinction exists only at the moment the extension is checked, when
hasWitness tells us whether an earlier witness covers the protocol.
So record that answer: NExt gains a field listing the extension's
finalized protocols (bumping the .tydb interface version), and those
protocols are skipped everywhere witnesses are registered: the local
type table (setupWits), the extension's own self-witnesses used while
checking its body (tydefineInst), and the entries importers read from
its interface (extWitnesses).
Every remaining registration is backed by an implementation. A
protocol with one implementation resolves to it from any module, in
any import order. And nothing is silently legalized: if two
independent modules, neither importing the other, both implement the
same protocol for the same type, then neither was finalized, both
register, and every use remains ambiguous and rejected in either
import order, whether they cover the protocol directly or through
their ancestry.
Of the three projects pinned by the previous commit, the two rival
ones keep failing unchanged; witness_canonical_import, previously
rejected despite its single Eq implementation, now builds and runs.
plajjan
force-pushed
the
canonical-witness-resolution
branch
from
July 29, 2026 09:58
ef70c0f to
839ce3e
Compare
Contributor
Author
|
@nordlander I don't normally hope for rain in your location... :P anyhow, please have a look at this, when you have time. Is this the right direction / solution? I didn't see any other way than to store more stuff. |
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
1 participant
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.
An extension covers its protocol's whole inheritance ancestry: extending Pt with Ord also makes the extension a witness for Eq, because Ord inherits Eq. The first extension to cover a protocol owns it: the type checker requires it to implement the protocol's methods, and every later extension covering the same protocol is forbidden from implementing them again (the checker calls these methods finalized). So for each protocol and type there is exactly one implementation, held by whichever extension came first.
Witness registration did not follow that rule. An extension registered a witness for every protocol in its ancestry, including the finalized ones it holds no implementation for. Such an entry is an empty shell: resolution that lands on it finds methods the extension was not allowed to write. Within one module the shells were harmless, because registration deduplicates against the local table and the owning extension's earlier entry wins. Across modules there was no deduplication at all, since the local table and the imported interfaces are enumerated separately. Declaring extension points.Pt (Hashable) in a module that imports points, where points already extends Pt with Ord, registered a second Eq witness for Pt even though the extension implements nothing of Eq. The constraint solver requires exactly one candidate per witness lookup, so every == involving Pt stopped compiling, inside the extending module and in every module importing both. In practice, extending an imported class with any protocol that inherits something was unusable.
Nothing about a registration itself distinguishes a shell from a genuine implementation declared in an unrelated module; the distinction exists only at the moment the extension is checked, when we know whether an earlier witness covers the protocol. So the extension record now lists its finalized protocols (bumping the .tydb interface version), and those protocols are skipped everywhere witnesses are registered: the local type table, the extension's own self-witnesses used while checking its body, and the entries importers read from its interface. Every remaining registration is backed by an implementation. A protocol with one implementation resolves to it from any module, in any import order. And nothing is silently legalized: if two independent modules, neither importing the other, both implement the same protocol for the same type, then neither was finalized, both register, and every use remains ambiguous and rejected in either import order, whether they cover the protocol directly or through their ancestry.
The first commit pins the three outcomes as build-failure projects under the unchanged compiler: two rival arrangements that must keep failing, and the single-implementation arrangement that failed for no good reason. The second commit's diff flips only the third into a running test and leaves the rival projects untouched.