Conversation
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.
The transport slice moved the runtime board from 164/413 to 207/413. Update the D-04 M7 progress, blocker table, and README gate row, and correct the acceptance notes that claimed no rate changed and that the workspace suite passes. Record the ten pre-existing Phase-3 failures this topic does not own.
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.
Unify structural deriving through field usage analysis, traverse records, and report missing fold symbols explicitly. Preserve scoped parameters and canonical class/value identities, and align instance arity diagnostics with purs. Repair postfix precedence, semantic type comparisons, aggregate layout convergence, and erased callable slot adapters so derived traversals, Generic, and polymorphic adapters execute through the trusted libraries. Add source, differential, and required-Wasmtime coverage; update the normative contracts, acceptance matrix, and measured L5 scoreboard. Record the existing workspace and Clippy failures without claiming FE-22 closure.
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.
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