Repository navigation
Phase 4: instance-declaration checks and the official diagnostic codes - #148
Merged
Merged
Conversation
An instance head is checked against its class's checked kind scheme no matter which module declares the class: a program-level run sees every module's scheme and a module-level run receives the imported ones, so the head its module applies is checked there rather than only in the declaring module's own run, which is the recorded FE-11 gap. The arity the rule leaves to the class environment is read from the declaration at home and from the scheme abroad: the scheme's kind is one arrow per parameter ending in Constraint, and a scheme this run does not know leaves its head unguarded rather than inventing an arity for it. Failing/FoldableInstance1/2/3 and failing/NewtypeInstance6 apply classes their modules import to arguments of the wrong kind, so they now report KindsDoNotUnify at the head; the l3 kinds scoreboard moves from 39/48 to 43/48, with KindsDoNotUnify 16/24 to 20/24 and nothing else moving. Docs: frontend/type-system/kinds.md records the rule and the boundary that remains - a scheme whose kind variables the run has not quantified yet binds its first instance, which is the polykind-generalization machinery #100/#123 own.
…stances officially The common instance recorder now applies one determined-instance-head rule to every local instance: each elaborated head argument must be a type variable, a type-level literal, a type constructor, or an application over those, and a row argument is legal only where a functional dependency fully determines its position. The fully determined positions are official typeClassDeterminedArguments, ported from Environment.hs's computeCoveringSets (the arguments standing in no inclusion-minimal covering set), so a parameter determined by nothing it cannot itself determine is not, and official record helpers that put a closed record in a determined parameter keep compiling. InvalidInstanceHead is raised where purs raises it, before the instance is recorded, covering TypeWildcards3, TypeSynonyms7, 3510, InvalidDerivedInstance2, and RowInInstanceNotDetermined0/1/2 with no overlap or deriving diagnostic alongside. Superclass cycles raise CycleInTypeClassDeclaration at the class declaration that reintroduces an ancestor, replacing the unmapped UnsupportedClass report (Superclasses2, SelfCycleInTypeClassDeclaration). An instance search that exhausts its depth bound now reports PossiblyInfiniteInstance at the constraint that would be solved again, the official Entailment work bound, instead of failing silently into an enclosing NoInstanceFound (438); the code joins the constraint-failure codes so no enclosing boundary reports the obligation twice. M5 agreement measured with the annotations oracle: 81/97 to 90/99, with InvalidInstanceHead 7/7, PossiblyInfiniteInstance 1/1, and CycleInTypeClassDeclaration 2/2, while OverlappingInstances stays 8/8, NoInstanceFound 52/53, and the L2/L3/L4 boards unchanged.
Official solving unifies a picked-up Coercible constraint's argument kinds (Entailment/Coercible.hs), including a pair its role decomposition dissolves into, and raises KindsDoNotUnify there rather than falling through to a bare NoInstanceFound: a pair whose kinds share no solution is the one thing about a coercion there is nothing to search for. The Coercible rule now records that verdict from the first pair of its proof whose kind equation has no solution - the outermost pair is the first constraint official solving would have picked up - reads it only when the whole proof fails, and returns Failed under the kind equation's own diagnosis, which the enclosing resolution no longer duplicates with a NoInstanceFound. failing/CoercibleKindMismatch.purs coerces Proxy Unary to Proxy Binary, whose role decomposition needs Coercible Unary Binary for kinds k -> Type and k -> k -> Type, so its use of coerce now fails with KindsDoNotUnify attributed to its own module. The kind-check entry point the l3 scoreboard measures stops before the constraint solver, so the case's mismatch there is not closed by this; the full check and the class boards' entry points do surface it. Docs: the roles and coercions acceptance record states the verdict.
…gnatures purs routes a written type's must-have-kind-Type equation through checkTypeKind, whose failure is ExpectedType rather than the kind unifier's KindsDoNotUnify. psrs-kind solves the same equation with the same state at its two checkTypeKind positions -- value signatures and local ascriptions -- so failing/1570.purs and failing/KindStar.purs report ExpectedType, one of the two M4 codes that had no source. Class members, constructor fields, superclass constraints, instance heads, and synonym bodies keep reporting KindsDoNotUnify, matching the official checkKind positions. Local annotations now also scope their variables the officially recorded way of #2542: the forall binders written in the enclosing declaration's signature, the binders written in the local signature itself, and, for instance members, the free variables written in the instance head and context. Anything else is UndefinedTypeVariable before the kind is read, so failing/2542.purs (bar :: Array a under foo :: T with T = forall a. Array a) reports the last M3 code without a source. Scoreboards (annotations oracle, vendored v0.15.16, PSRS_STDLIB_ROOT on the pinned stdlib): L3 39/48 to 40/48 with UndefinedTypeVariable 3/4 to 4/4 and KindsDoNotUnify unchanged at 16/24; L4 39/50 to 41/50 with ExpectedType 0/2 to 2/2; L5 unchanged at 81/97; L2 failing 72/72 and passing resolution 403/413 unchanged. PolykindGeneralizationLet and SkolemEscapeKinds stay open, both anchored in the polykind model rather than in a diagnostic choice, recorded in the kinds design document.
`purs` rejects a local instance declaration whose module defines neither its class nor a type constructor covering one of the class's functional-dependency covering sets (`TypeChecker.typeCheckAll`, `findNonOrphanModules` and `checkOrphanInstance`). The head's covering-set modules are intersected, so a module that covers only some sets is still an orphan. The check runs after head synthesis — synonym resolution included — and before overlapping-instance checking, so an orphan reports exactly `OrphanInstance` and is not recorded: it can neither overlap with a visible instance nor submit a derived dictionary (the `derive instance` half never runs). The covering sets were moved into a shared fundeps module so the overlap check and the orphan check read one definition. All seven `OrphanInstance` corpus cases agree on the M5 board, and 3405's produced set is exactly [OrphanInstance] (measured 2026-10-18 with the annotations oracle).
…ndeps module
The covering-set definition '298cc585' introduced at
classes/fundeps/covering.rs enumerated every parameter subset whose
dependency closure covers the class and kept those an order-dependent
filter had not superseded, so locally-minimal-but-superset sets survived
exactly the way the sibling slice recorded for the old coherence.rs copy
(the corpus case NonOrphanInstanceFunDepExtra documents the official
{{f, l}} while the enumeration also returned {f, l, r}). The official
'typeClassCoveringSets' is the inclusion-minimal reduction of the
'computeCoveringSets' frontier search.
The frontier search that instance_head.rs carried as a reduced port now
lives in covering.rs and produces those minimal sets for every consumer:
the overlap check's apartness, the orphan rule's per-set coverage, and
the determined-instance-head rule, whose fully determined arguments are
officially the parameters standing in no covering set. One definition,
no local copies. The orphan verdict itself is unchanged: a superset of a
covered minimal set is covered, so minimal sets cannot orphan a legal
instance that the supersets accepted; the overlap check must be
re-measured instead, and OverlappingInstances stays 8/8, OrphanInstance
7/7, InvalidInstanceHead 7/7, CycleInTypeClassDeclaration 2/2 on the M5
board, and 3405's produced set stays exactly [OrphanInstance] (measured
2026-10-18 with the annotations oracle).
Focused regression tests pin the two program shapes the L6 runtime board
measured at risk: a foreign fundep class instance over locally declared
heads is accepted and executes (NonOrphanInstanceFunDepExtra), and an
export shadowing an unused import compiles and executes
(NonConflictingExports). Both pass the runtime board per program.
This was referenced Oct 18, 2026
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
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.
What lands
Five slices measured together with the annotations oracle on the vendored v0.15.16 corpus, package
e556bf2f/fnv1a64-v1:7d96f1c44d8d52cc:KindsDoNotUnify16/24 → 20/24,UndefinedTypeVariable4/4)ExpectedType0/2 → 2/2)Slices
004de7ba+54d69f92— the cross-module instance-head kind check (psrs-kind): an instance head is checked against its class's checked kind scheme whether the class is declared here or imported;FoldableInstance1/2/3,NewtypeInstance6agree.54d69f92also records the kinds verdict of an unsolvableCoercibleobligation (upstreamEntailment/Coercible.hs's behavior).56fe3cda—ExpectedTypeat the two officialcheckTypeKindpositions (value signatures; local ascriptions and typed binders), andUndefinedTypeVariablefor a free variable in a localwheresignature (2542.purs).4a078b95— the determined-instance-head rule (InvalidInstanceHead1/7 → 7/7; one rule over the wildcard, free-variable-through-synonym, derived-head, and fundep-undetermined triggers),PossiblyInfiniteInstance(438.purs), and the officialCycleInTypeClassDeclarationcode for the existing superclass-cycle check.298cc585— the official orphan-instance rule (neither the class nor a type constructor covering every official covering set is declared here →OrphanInstance, raised after head synthesis and before recording);3405.purs's produced set is exactly[OrphanInstance].fd7bf88a—DuplicateTypeClassdistinguished fromDeclConflictat the resolver's declaration registry (DeclConflictstays 11/11,DuplicateInstancestays 1/1).9a4c2e04— the sharedcovering_setsnow compute the official inclusion-minimal sets (upstreamcomputeCoveringSets/typeClassCoveringSets), one definition for the overlap check and the orphan check; the orphan rule is provably insensitive to the previous superset behavior, verified during the slice.fdb85717records the measurements: D-04 gate rows and M3/M4/M5 progress sections, README's gate table, and a new runtime-program-scoreboard record (serial per-root protocol, Wasmtime CLI 48.0.1 on this host, and the load-sensitivity caveat forNonConflictingExports.purs/NonOrphanInstanceFunDepExtra.pursat the 10-second guest wall — they pass individually, verified twice).Validation
cargo fmt --all --check,cargo clippy --workspace --all-targets -- -D warnings— pass.PSRS_STDLIB_ROOT=… PSRS_REQUIRE_WASMTIME=1 cargo test --workspace(debug) — pass, 0 failures (2111→2112+ tests; no prior test removed).pursdifferential suites (nopurson this host) — recorded, not silently skipped.Closes nothing by itself; #97 was closed with this evidence on master's tree. Remaining L4/L5 work: #123 (the only remaining L5 mismatch
ClassHeadNoVTA3+VisibleTypeApplications1), the FE-16 CoercibleProofcontract (six L4 mismatches), #99 holes, #100 kinds.