Repository navigation
Land type wildcards, rows-in-kinds constraints, and polykind application #87
Description
Part of #75 (Phase 2). 22 passing files stop in type lowering. The blockers cluster into three groups.
1. Type wildcards — _ as a type
passing/TypeWildcards.purs, passing/WildcardType.purs, passing/TypeWildcardsRecordExtension.purs, passing/WildcardInInstance.purs, passing/PolykindGeneralization.purs (Proxy :: _ Proxy, Proxy :: _ "foo").
FE-17 owns this: "explicit type-application elaboration and hole/wildcard diagnostics." A wildcard is a hole that unifies with anything and is never generalized; it must be a binder on the type spine with a diagnostic when it cannot be solved, not a synthesized type variable in a side table.
2. Rows in kinds and Prim.Row constraints
passing/RowConstructors.purs uses type Baz = { | Foo }, passing/RowLacks.purs, passing/RowNub.purs, passing/PolykindRowCons.purs. FE-13 records that Prim.Row.Cons, Lacks, Union, and Nub "stay with issue #63" — #63 is now closed, so this has no owner. Prim.Row.Cons is a type-class constraint and belongs to FE-14's constraint machinery; the runtime half is a different question, since an open row has no runtime layout and closure conversion rejects a function whose type still contains a row variable.
3. Kinded type application and polykind generalization
passing/EntailsKindedType.purs, passing/PolykindInstantiatedInstance.purs, passing/PolykindInstantiation.purs, passing/PolykindGeneralizedTypeSynonym.purs, passing/StandaloneKindSignatures.purs, passing/TypeSynonymsInKinds.purs, passing/Rank2Kinds.purs. These overlap the M3 kind gate — see the L3 slice.
Acceptance
The type-lowering blocker count drops to zero, Prim.Row constraints have a frontend owner recorded in FE-13/FE-14, and the L3 kind scoreboard reflects the kinded-application work.
Activity
biuld commentedon Oct 2, 2026
Partially addressed in #119 (branch
feat/phase2-wildcards-rows-polykind-87, two commits). Not closing: the issue's acceptance condition cannot be measured yet, and one of the three groups has no measurable evidence at all.What landed
Group 3, the standalone kind signature. A standalone kind signature on a
classreached the class scheme and was used to infer that class's kind, but nothing applied the scheme to aninstance. An instance head was the one place a type met a kind signature and was never checked, soclass C :: Constraint -> Constraintacceptedinstance C Int.check_definitionsnow walks the module's instances and elaborates each head against its class scheme. M3 kind agreement is 30/48, up from 29/48, withKindsDoNotUnify12/24;failing/StandaloneKindSignatures4.pursnow agrees. The other three standalone-signature cases already agreed, so the signature was never lost — the issue's premise that it was discarded does not hold.Two rules keep that from over-reporting, and both were found by measurement rather than by reading:
ClassInstanceArityMismatch, owned by the class environment. Without a guard the new check reportedKindsDoNotUnifyin place of the official code and suppressed the arity diagnostic, movingfailing/MPTCs.purs,TooFewClassInstanceArgs, andTooFewUnnamedClassInstanceArgsout of "blocked" into "disagreeing".(->) ris how a higher-kinded class parameter is written andinstance functorFunction :: Functor ((->) r)is the standard library's own instance; read on its own the same argument is the partially applied function synonym offailing/TypeSynonyms9.purs. The upstream deriving differential cases are what caught this.Group 1, the type wildcard. The premise needs correcting: a wildcard in a value signature already worked. Every shape
pursaccepts was checked against realpurs0.15.16 and already accepted here —_ -> Int,(_ -> _) -> _,_ -> _, a wildcard as a row tail, and a wildcard underforall— and the three positionsfailing/TypeWildcards1/2/4.pursname are still rejected at parse. What was missing is the opposite case: a wildcard in an instance head is the pattern the solver matches against and has nothing to solve against, sofailing/TypeWildcards3.purswas accepted wherepursreportsInvalidInstanceHead. That is now raised wherepursraises it, and a wildcard in an instance context stays legal. No board number moved:TypeWildcards3.pursimportsPreludeforShow, so it stops at P3 andInvalidInstanceHeadstays at 0/7.What is not done, and why
Polykind generalization. An unannotated
data/newtype/typeparameter gets a fresh kind variable in a monomorphic scheme, so its first use fixes that variable and a later use at a different kind is rejected. Quantifying those variables was implemented and measured: it lowered M3 from 30/48 to 28/48, breakingfailing/InfiniteKind2.purs(data Tree m = Tree (m Tree)) andfailing/MonoKindDataBindingGroup.purs(data A a = A (B a)withtype B a = F A). Both depend on a parameter kind their own definition determines, and generalizing it loses the occurs check and the fundep mismatch. So the rule has to be infer the parameter kind from the declaration's own definition, then quantify only what is left unconstrained, which requires the declaration check to run before the scheme is fixed. That reordering was not attempted.failing/PolykindInstantiatedInstance.pursandfailing/PolykindGeneralizationLet.pursstay open. This is the "higher-kinded application" that FE-17 lists as incomplete.Group 2, rows in kinds. Not started, and it has no measurable evidence in the current state: all four
failingcases produce[ModuleNotFound,UnknownName], so none of them reaches kind checking.failing/RowConstructors1/2/3.pursandfailing/RowLacks.pursimportEffect.Console(andType.Proxy), which this library does not provide. The issue asks for aPrim.Rowowner to be recorded in FE-13/FE-14; that part is still outstanding, andLacksentailment is entangled with #97 either way.Why this cannot be closed yet
The acceptance condition is "the type-lowering blocker count drops to zero". Every one of the 22
passingfiles the issue names is blocked at P3 resolve onEffect.Console,Effect, orType.Proxy, not at type lowering, because Phase 3 (#94, #95, #96) has not written those modules. Measured with a per-case missing-module probe: 334 of the 413 non-FFIpassingfiles are blocked onEffect.Consolealone and 56 onEffect, and 333 files have no missing module outside that pair. Until those exist there is no way to observe a type-lowering blocker count for this issue moving, in either direction.What would unblock the rest:
EffectandEffect.Console, which makes the 22 files measurable.stdlib/lib/WASI/Console.pursalready implementsloganderror, soEffect.Consoleis mostly a naming and re-export layer; the expensive part ofEffectis theControl.Apply/Control.Applicative/Control.Monadclass hierarchy, andlogShowneedsShowwith a real instance set.failing-side cases to measure even before thepassingside opens up.Prim.Rowentailment and an owner recorded in FE-13/FE-14.Validation for what did land:
cargo fmt --all --check,cargo clippy --workspace --all-targets -- -D warnings,PSRS_REQUIRE_WASMTIME=1 cargo test --workspace(1136 passed, 0 failed, 5 ignored),PURESCRIPT_REPO=… cargo test -p psrs-driver --test upstream(4 passed, including the four deriving differential cases), and the full scoreboards. L1, L2, L4, L5, and the L6/M7 runtime board are unchanged.Record the Prim.Row owner and what the kind work still needs
biuld commentedon Oct 2, 2026
Follow-up to the previous comment: #119 now carries a third, documentation-only commit (
5c17760) that closes this issue's middle acceptance clause — "Prim.Rowconstraints have a frontend owner recorded in FE-13/FE-14". That was the one item reachable without Phase 3.The owner is now split by kind of thing rather than left as a pointer to two issues:
Prim.Rowsyntax — a row constructor in a type synonym (type Baz = { | Foo }) and a label-typed synonym parameter (type Foo r = (x :: Number | r)) — is a type form, so it is FE-17's, tracked by Land type wildcards, rows-in-kinds constraints, and polykind application #87.Prim.Row.Cons,Lacks,Union, andNubconstraints are type-class constraints, so they are FE-14's constraint machinery, tracked by Add the missing class and instance checks (M5 codes without a checker kind) #97.failing/RowLacks.pursexpectsNoInstanceFoundfrom aLacksconstraint this compiler does not solve.Two corrections that matter for the architecture review
InvalidInstanceHeadis one rule, not a wildcard special case. All seven cases expecting it are the same check — an instance head must be fully determined — reached by four different triggers:TypeWildcards3TypeSynonyms7instance showX :: Show (X r))3510,InvalidDerivedInstance2derive instance eqT :: Eq Tfortype T = {})RowInInstanceNotDetermined0/1/2Only the wildcard trigger is implemented, so the rule is currently narrower than
purs's. It should grow as one determined-head check rather than as more triggers. None of the seven is measurable today: all stop at P3 withModuleNotFound, andTypeWildcards3additionally needs aShowthis library does not provide — so the implemented trigger has no official-suite evidence and rests on unit tests alone.Kind generalization is the remaining kind work, and its shape is now known. The obvious implementation — quantifying the kind variables of unannotated
data/newtype/typeparameters inbuild_schemes— was written and measured, and it lowered M3 from 30/48 to 28/48, breakingfailing/InfiniteKind2.purs(data Tree m = Tree (m Tree)) andfailing/MonoKindDataBindingGroup.purs(data A a = A (B a)withtype B a = F A). Both depend on a parameter kind their own definition determines. So the rule has to be infer the parameter kind from the declaration's own definition, then quantify only what is left unconstrained — which requires the declaration check to run before the scheme is fixed, i.e. a phase-ordering change inside the kind checker rather than a change to any one declaration's scheme. That reordering was not attempted.failing/PolykindInstantiatedInstance.pursandfailing/PolykindGeneralizationLet.pursstay open, and they are the only measurable evidence for it.Also recorded in FE-15 and not fixed: a wildcard standing for a fundep-determined position is a fundep conflict here and only a warning in
purs, whichpassing/WildcardInInstance.pursstates in its own comment.biuld commentedon Oct 2, 2026
Reopened. PR #119's body contained the phrase "Closes #87's middle acceptance clause" — intended to mean it closes that acceptance clause, but GitHub read it as a closing keyword at merge time and closed this issue one second after the merge. The intent stated in the PR and in the two comments above is that this issue stays open.
Merged state, for the record: #119 () landed the two code commits and the documentation commit. Nothing here is finished:
passingfiles named above stop at P3 onEffect.Console,Effect, orType.Proxy.Board status is
Blocked, because the blocker is Phase 3 rather than anything inside this issue.biuld commentedon Oct 2, 2026
Reopened. PR #119's body contained the phrase "Closes #87's middle acceptance clause" — intended to mean it closes that acceptance clause, but GitHub read it as a closing keyword at merge time and closed this issue one second after the merge. The intent stated in the PR and in the two comments above is that this issue stays open.
Merged state, for the record: #119 (
af13bd5) landed the two code commits and the documentation commit. Nothing here is finished:Prim.Rowowner is now recorded in FE-13/FE-14. Those are two of the three acceptance clauses, the second of which is documentation.passingfiles named above stop at P3 onEffect.Console,Effect, orType.Proxy.Board status is
Blocked, because the blocker is Phase 3 rather than anything inside this issue.Merge p5/w5cmp: the two ordering relations
Record that L4 agreement is by code, and correct the CompareInt list
biuld commentedon Oct 3, 2026
Landed by #122, merged to
masterasfe40d17. Adding the evidence, since themerge closed this issue automatically.
Acceptance
The type-lowering blocker count is zero. Measured on the merged tree with
PSRS_ORACLE=annotations cargo test -p psrs-driver --test suite -- --ignored --nocapture:l6_runtime_scoreboardreports no P2 surface-lowering failures, down from 61 atthe
5298aadbaseline and 5 before this PR.Prim.Rowconstraints have a frontend owner recorded in FE-13/FE-14. Thathalf was already satisfied when #120 landed — all twelve
Prim.Row,Prim.RowList,Prim.Symbol, andPrim.Intrelations have a rule-table entry.The note in this issue that they "stay with issue #63 — #63 is now closed, so
this has no owner" was the stale part.
The L3 kind scoreboard is unchanged at 31/48. The kinded-application work in
group 3 had already cleared P2 in the #119/#121 work; what remained was never a
kind-checking gap.
What this issue's named files now do
All sixteen files listed here are past P2 and stop at P3 on missing
Effect/Effect.Consolemodules — the same stage as each other. The five thatwere still P2 are fixed by #122:
IntToString.purs,ParseTypeInt.purs— negative type-level integer prefixes.- 1is the literal-1on the shared spine, not a prefix-operator node.4500.purs,4535.purs,VTAsClassHeads.purs— visible type applicatione @T, elaborated by the checker and erased, like an ascription.Remaining work this issue does not claim
Recorded in D-04 FE-17 and the type-inference design, each with the corpus case
that measures it:
forallbinder visibility is not modelled, sofailing/VisibleTypeApplications1.pursis accepted here and rejected bypurs.failing/ClassHeadNoVTA3.purs. This is the one place the work costagreement — M5 moved 49/91 → 49/92, denominator up one with no gain.
f @A @Bis reported rather than resolved.(1) and (3) close together: the scheme needs to record which of its variables a
visible application consumed, and whether the source binder was visible. That is
purs'sTypeVarVisibility, whichCST/Convert.hsderives fromforall @a.and this compiler's
TypeVarBindercurrently discards.Board
Statusmoved to Done.feat(frontend): check the expression ascription against its written type
Record the Prim.Row owner and what the kind work still needs
Merge p5/w5cmp: the two ordering relations
Record that L4 agreement is by code, and correct the CompareInt list
Lower visible type application and negative type-level integers
Correct the first-stage blocker decomposition and close out Phase 2