Repository navigation
Conversation
biuld
force-pushed
the
stdlib/vendor-core-libraries
branch
from
October 6, 2026 18:15
1f0b540 to
11db175
Compare
Prelude keeps the psrs:effect bindings and re-exports the official class hierarchy. Data.Show and Data.Tuple stay the implementations this compiler already lowers. Value foreign imports become intrinsics or diverging stubs. The parser accepts an `as@` named pattern and a `where` block on a pattern binding. A backticked local binds tighter than a symbolic operator. A module re-export keeps the imported data constructors, `Partial` is in scope without an import, and `T()` exports a type with none of its constructors. `-` and `/` are the library operators over `intSub` and `intQuot`. The trusted set parses. Modules that construct an algebraic `Tuple`, or that call FFI this target does not implement, still fail resolve. No scoreboard number moves. Refs #94
A rank-n dictionary field quantifies its own variables, so those variables do not make the record's layout depend on a free type variable. Parameter shapes then use the same scalar layout as other closed records instead of the erased aggregate special case.
PSRS_DUMP_CC and PSRS_DUMP_WAT write the calling-convention and text forms beside a focused runtime test without changing the compiled artifact.
The vendored official `Safe.Coerce` shadows the compiler's primitive interface for the same module. Its body is `coerce = unsafeCoerce`, whose `unsafeCoerce` is a self-recursive stub this project cannot execute, so every program that reaches it loops at runtime. Keep the vendored source faithful to upstream and resolve the module through the compiler interface instead: expose `compiler_provided_module` from `psrs-resolve` and have the driver's library loader skip such a name. Imports then fall through to the virtual interface, which maps `coerce` to the checked coercion intrinsic and `Coercible` to the shared class. `Unsafe.Coerce` has no compiler interface yet; its `foreign import` is represented as the same recursive stub, so a program that reaches it is a recorded gap rather than a working coercion.
The live-type layout filter added when the core libraries were vendored only lays out arrays and records reachable from a declaration or constructor field, so the raw-type layout fixtures never reserved their aggregates. Root those types through declarations in the tests, which is what the production builder sees. Split `psrs-ast/tests.rs` and `psrs-typecheck/classes/fundeps.rs` into module directories; both crossed the 500-line source limit earlier on this branch.
An abstract constructor application (`f a`, including `f Unit`) lowers to an erased value whose stored calling convention is established by its producer. Recovering it at a concrete consumer needs that convention; the previous code cast the erased closure directly onto the consumer signature, which trapped when a dictionary method produced a closure under its own protocol (`wasm trap: cast failure`). Add read-only checked instantiation evidence (`psrs-core`), a shared conversion planner that recovers the producer protocol and emits an explicit adapter when it differs from the consumer (`cc/lower/conversion`), and thread the evidence to each boundary (global use, direct call, dictionary field, erased local use). The Effect representation owner contributes its runtime token as the `Effect` constructor protocol. A reference cast is no longer used as an adapter, and a missing constructor binding is a source-spanned unsupported conversion rather than a fresh guess. Value-sensitive Wasmtime execution now covers the non-Effect Reader dictionary, Effect discard, delayed map, and a fixed `f Unit` payload, plus signature inspection of the generated adapter and factory. Ordinary closure and aggregate regressions are re-run through the workspace suite. PE-13 and EF-14 are recorded as verified in the acceptance documents.
A callee that is not a top-level declaration - a local closure or a class method reached through a field access - was rejected when under-applied (`call expects N arguments but received M`). Only top-level declarations had a partial-application path. Add `lower_indirect_partial_application`: evaluate the callee and the supplied arguments, capture them, and emit a generated closure that exposes the remaining parameters and calls the captured callee indirectly. The generated closure is verified like any other function before it is added. Cover both an under-applied local closure and an under-applied dictionary method with Wasmtime execution. The L6/M7 scoreboard moved from 207/413 to 210/413: three corpus cases whose first blocker was P8 closure conversion now run. D-04 and README are updated.
The runtime-representation model and checked-boundary contract was spread across the erasure and aggregate documents and referenced by name from several topics, so each feature grew its own notion of how a value is adapted. Give it a single owner, name it after industry practice, and make the target layout a total level of the same model. - New functional topic representation-and-evidence.md: the target-neutral RuntimeRep (the analogue of GHC's RuntimeRep), RepresentationPolicy, Boundary, Evidence, ConversionPlan, generic aggregate normalization and the aggregate conversion plan, the representation owners, and the one planner. A RuntimeRep a target uses has exactly one Layout, joined by a total mapping per target (heap_layout for Wasm GC; abi_layout for the Canonical ABI), which is what makes the functional backend complete. Erasure, callables, dictionaries, effects, coercion, and partial application become instances of it in their own documents, deferring to it instead of restating it. - data-representation is named as the Wasm GC heap_layout realization of each RuntimeRep, with a total ValueShape -> ValueType mapping; the former generic-aggregate-erasure design is folded into the model (normalization and conversion) and this document (layouts). - Erasure defines the policy of an erased value and its ownership (producer), grounded in GHC RuntimeRep/Any, Swift reabstraction thunks and witness tables, and Java bridge methods. - cc-ir: partial application is the standard PAP closure for every callee kind; the adapted function boundary is a reabstraction thunk; checked instantiation evidence travels through an explicit Core-to-CC side table. - effects: the token is the State# RealWorld analogue; i32 0 is a placeholder and an implementation gap. - modules-and-resolution, prim: coerce and unsafeCoerce are compiler-provided primitive values; a compiler-provided module is never shadowed. - DEC-17 records the durable decision; the backend index and IR boundaries reference the new topic and name the evidence/policy side table. - Acceptance records name the transitional mechanism and its removal target.
Replace the transitional representation mechanisms with the boundary the design names. Checked instantiation evidence and each constructor's representation policy now travel to P8 through BoundaryEvidence beside CC, the same discipline ExternalBindings uses for WIT bindings. - Add RepresentationRegistry: Function stores under its checked instantiation arguments; the trusted Effect owner registers its runtime token. An unregistered constructor is reported, not resolved by arity. - Intern one payload-erased protocol signature per registered callable constructor, keyed by the concrete signature, replacing the signature-prefix derivation in cc/layout/functions. - Delete FunctionLowerer::source, constructor_protocols, transport_signatures, protocol_parameters, and cc/lower/instantiation.rs. - Route every use (global, direct call, dictionary field, erased local) through BoundaryEvidence. Behaviour is unchanged: the focused closure_protocol, partial_application, effects, and functor cases pass, and the driver suite stays at 549 passed/10 pre-existing failures.
Register Unsafe.Coerce in the compiler-provided interface and the unsafeCoerce intrinsic in the compiler vocabulary, so the vendored module is never loaded and its self-recursive body never takes effect. - Add Intrinsic::UnsafeCoerce with the forall a b. a -> b scheme. - Infer it as an unconstrained coercion function (no Coercible wanted); finalize closes it to a THIR UnsafeCoerce node lowered to Core's RepresentationCast. - Lower the intrinsic in CC through the common conversion planner, so it reinterprets the value at the erased boundary. - Add execution evidence (newtype through unsafeCoerce) plus the compiler-spelling scope test. The driver suite stays at 551 passed/10 pre-existing failures.
Replace the transitional Int token and its i32 0 placeholder with the compiler-owned opaque state token the design names (the State# RealWorld analogue). Effect lowering interns TypeId::STATE_TOKEN, marks it opaque, and threads it through each Effect closure; run supplies the StateToken value instead of an Int literal. - Add TypeId::STATE_TOKEN and Core ExprKind::StateToken. Only effect lowering produces it; the Core verifier requires it to carry the compiler token type, and the backend lowers it to a scalar constant because the synchronous effect carries no payload. - Update every Core traversal to treat the token as a leaf. - Update the effect fixture and the model, effects, and acceptance notes. The driver suite stays at 551 passed plus one pre-existing prim_row failure; the scoreboards are unchanged (L1 904/908, L2 71/72 + 386/413, L3 39/48, L4 39/50, L5 58/81, L6/M7 210/413).
The matching module had two relation-shaped methods, subsumes and matches,
with no single entry point. Fold them into one checked relation,
TypeMatcher::relate(actual, expected, variance, instantiate), parameterized
by Variance::{Subsumption, Invariant}. Subsumption is the value-level
relation a scheme is checked against at its use; Invariant is the rigid
mode for nominal and higher-kinded applications, closed and rigid rows,
and constructor field templates.
This is a behaviour-preserving structural change: every recursion and entry
point now goes through relate, and the two modes keep their exact branch
logic. The public entry points (compatible, scheme_instance,
application_matches, instantiation) are unchanged. Checking remains the
sole owner of the relation; P8 consumes only its Instantiation evidence.
Validated: psrs-core, psrs-typecheck, and the full driver suite (551 passed,
same 10 pre-existing failures) are unchanged, and all five scoreboards are
unchanged (L1 904/908, L2 71/72 + 386/413, L3 39/48, L4 39/50, L5 58/81,
L6/M7 210/413).
A constructor field whose immediate head is a type variable, such as `f a`, is compared through the class's higher-kinded counterpart `eq1`/`compare1` instead of requiring `Eq (f a)`/`Ord (f a)`. This is upstream's `isAppliedVar` test in TypeChecker/Deriving.hs, and the vendored Data.Functor.App, Compose, Coproduct, and Product declarations rely on it. `Eq1` and `Ord1` now derive as `eq1 = eq` and `compare1 = compare`, matching upstream's deriveEq1 and deriveOrd1, so the matching `Eq`/`Ord` instance supplies the dictionary. The `Data.Foldable` graph no longer stops on `no instance for constraint Eq (_ _)` or `Ord (_ _)` in those modules.
A class-method use that is not applied, such as `eq = eq1` or `compare = compare1`, kept its method-local `forall` and constraints on the inferred type. Checking it against the plain function type the instance method expects then reported a type mismatch instead of providing the method's dictionary. The expected-type path now runs the inferred expression through the shared `instantiate_expression_use`, the same operation the application path already uses, so the method-local obligation becomes a wanted constraint. This lets Data.Functor.Product and Data.Functor.Coproduct's hand-written `eq = eq1` and `compare = compare1` type check.
…l classes Compiler-supported deriving is now its own topic: it selects rules from one registry built once from the resolved declarations, validates each field's usage and variance against the visible instance environment, and reports the official deriving errorCode for every failure. The known classes are no longer recognized by comparing class module and name strings at use time. DerivingRegistry maps resolved class identities to their methods, to the representation declarations (Data.Ordering, Data.Generic.Rep), and to the trusted core values (append, mempty, identity, apply, pure) the fold and traversal rules name. A Newtype/Generic trailing wildcard is resolved to the wrapped type or representation before the instance is recorded, so the searchable head is concrete. usage.rs walks each field with polarity and instance existence, so a field head with no mapping instance is rejected at the declaration with CannotDeriveInvalidConstructorArg, matching purs. Every structural class now has a rule: Eq/Ord/Eq1/Ord1, Functor/Bifunctor/Contravariant/Profunctor, Foldable/Bifoldable, Traversable/Bitraversable, Newtype, Generic, and derive newtype. Eq and Ord normalize field synonyms before the applied-variable test. The new diagnostics map to their official codes: CannotDerive, ExpectedTypeConstructor, InvalidDerivedInstance, InvalidNewtypeInstance, CannotDeriveNewtypeForData, CannotDeriveInvalidConstructorArg, CannotFindDerivingType, and ExpectedWildcard. derive newtype on a data type is InvalidNewtypeInstance, and deriving the Newtype class for a data type is CannotDeriveNewtypeForData, as purs reports. Deriving is documented as its own topic and split out of FE-16 into FE-22. Validated: psrs-typecheck 134 passed; the deriving source tests 16 passed, the runtime deriving tests 8 passed under PSRS_REQUIRE_WASMTIME=1, and the upstream deriving batteries 2 passed (18 accept/reject cases and an errorCode comparison). The full driver suite is 561 passed with the same 10 pre-existing failures. Traversable/Bitraversable execution is blocked by a P8 CC verification limit and is recorded as such.
Ordinary Coercible still cannot lift Coercible a b through an unknown constructor to Coercible (f a) (f b). That refusal matches purs. derive newtype does not ask for the proof. After the local single-field newtype and the underlying instance are checked, the derived methods reuse the wrapped dictionary and adapt each boundary with a representation cast authorized by that newtype. Beta-reducing the cast kept the method quantifier only on the let result. The binding now carries the same leading forall, so a variable such as Traversable's m stays in scope. The quantifier is not Coercible evidence. Validated with focused driver tests under PSRS_REQUIRE_WASMTIME=1, including unknown-constructor dictionary reuse, the ordinary Coercible rejection, and derived Traversable execution. The psrs-core optimizer tests passed. The full workspace suite was not run.
A record constructor or updater with an immediate underscore becomes a
lambda whose binders follow the written fields, not the canonical field
order. Nested update paths share that updater. An explicit field
expression or nested literal keeps its own scope, so
`field = field { value = 7 }` uses the local `field` value. AST updates
now distinguish a nested path from an expression, and resolution projects
the path from the enclosing base.
A parenthesized backticked section accepts the hole on either side and
keeps the operand order and the unresolved local name.
Validated under PSRS_REQUIRE_WASMTIME=1: the record suite (21) and the
backticked-section test. The full workspace suite was not run.
An applied foreign import data value is not a nullary handle and has no constructors. Closure conversion gives it the same non-null erased reference as an abstract type variable, so a saturated Fn2 can pass layout.
An underscore written as the condition, then branch, or else branch becomes a parameter in that order, the same way a case scrutinee already does.
A value signature depends on the type constructors and classes that remain after a saturated local synonym expands. Constructor fields count only for the constructors the export actually lists.
A.zip between backticks is that qualified value used infix, so both operands stay on the operator chain.
A synonym consumes only its declared parameters. Further arguments apply to the expanded body, so C2 a z x is (C2 a z) x.
0xFFFF fits in Int. A magnitude at or above 0x80000000 remains IntOutOfRange.
A signed declaration solves every constraint, so a where-bound function quantified its monad before a use could refine that monad. A constraint stays on the local scheme only when that binding's type determines it. A constraint that still mentions an outer unknown stays with the enclosing declaration.
A fallthrough helper is defined in the same let as the case, so it can name an outer local directly. Passing that local in as a value argument instantiated its scheme once, before the guard applied the arguments that solve its constraints.
enumFromThenTo feeds Int to a locally generalized stepper and maps the result with toEnum. The same shape, including guards, operators, and composition, has to keep that seed as Int.
biuld
force-pushed
the
stdlib/vendor-core-libraries
branch
from
October 7, 2026 09:51
dab23d7 to
820de13
Compare
HIR owns language identities, schemes, and effects. The backend selects one direct, generated, or artifact implementation, and linking checks each MIR import against the provider ABI. Euclidean division stays in the library. Retired floor bindings are rejected. The lock pins the library commit that uses a truncating quotient for array storage.
numberSqrt lowers to f64.sqrt and keeps the official Data.Number.sqrt signature. Negative zero stays negative zero, and negative inputs produce NaN. The lock pins the library binding and its source verifier.
numberAcos calls the pinned libm export in the numeric runtime and keeps the official Data.Number.acos signature. Finite inputs in [-1, 1] match the pinned Math.acos results. The lock pins the library binding and its source verifier.
numberAsin calls the pinned libm export in the numeric runtime and keeps the official Data.Number.asin signature. Negative zero stays negative zero. The lock pins the library binding and its source verifier.
numberAtan calls a scalar numeric-runtime export and keeps the official Data.Number.atan signature. Returned bits match pinned libm 0.2.15, including zero signs and both infinities. The Wasm copy does not touch the stack pointer. The lock pins the library binding and its source verifier.
Add checked scalar implementations for the thirteen remaining Data.Number foreigns, including nullary numeric constants and the NaN predicate. Use unmodified libm 0.2.15 with red-zone use disabled for the runtime and its dependencies so static stack verification can measure explicit frames. Consolidate thin math exports in number.rs while retaining the existing atan2 compatibility implementation. Rebuild the artifact and update its checked catalog, trace digest, and acceptance documentation. Validation: formatting, strict workspace Clippy, artifact byte reproduction, all runtime/linker tests, and public Number/Show runtime checks passed. Official-FFI oracle runs passed 298 atan checks and 2680 remaining Number checks, retaining the documented one-ULP exclusions. Runtime integration used the explicit development psrs-stdlib package. The full workspace run retains three documented baseline driver failures; all other targets pass.
Resolve runtime operations through a checked unit dependency graph and use one pinned dlmalloc provider for canonical allocation and memory growth. Bind its lazy initialization to an application-owned constant heap getter, verify that getter before composition, and remove the generated allocator. Organize the runtime into ABI contracts, catalog metadata, numeric code and allocator code while preserving its public exports. Reproduce both pinned artifacts through their build scripts and record the integrated evidence. Validation: mandatory-Wasmtime workspace tests, workspace Clippy, runtime all-feature tests and Clippy, formatting, and byte-for-byte reproduction of both artifacts passed. Corpus scoreboards were not remeasured; remaining allocator acceptance obligations are documented separately.
3 of 4 tasks
Owner
Author
|
The commits on this branch are contained in |
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.
Summary
This is still open.
discardandmapoverEffectstill trap in Wasmtime with a cast failure; compile acceptance is not the acceptance check for those cases.Test plan
cargo test -p psrs-backend --lib bound_rank_n_record_fields_do_not_make_dictionary_layout_dependentPSRS_REQUIRE_WASMTIME=1 cargo test -p psrs-driver --lib discard_defined_from_bind_sequences_effectsPSRS_REQUIRE_WASMTIME=1 cargo test -p psrs-driver --lib mapping_an_effect_does_not_run_it_until_the_action_runs