Skip to content

Release (main) - #45

Merged
MicroProofs merged 1 commit into
mainfrom
release/main
Oct 25, 2026
Merged

MicroProofs merged 1 commit into
mainfrom
release/main

Conversation

@rvcas

@rvcas rvcas commented Oct 24, 2026

Copy link
Copy Markdown
Contributor

This PR was generated by Sampo GitHub Action. When you're ready to do a release, you can merge this and the packages will be published automatically. Not ready yet? Just keep adding changesets to the default branch, and this PR will stay up to date.

nash-ast 0.12.0 -> 0.13.0

Minor changes

  • de1b7097 Add select_impl with SelectPolicy and ImplSelection, the one impl selection used by inference, superclass entailment, and evidence. Every candidate is matched, and a second match stops the compiler as a coherence bug instead of picking one. — Thanks @MicroProofs!

  • 4c4e5155 Resolve superclass evidence when a type variable stays open. A phantom parameter that no use fixes, as in wrapper : tag 'p -> bool; wrapper t = same t t with same : Ord 'a => 'a -> 'a -> bool, passed type checking but stopped nash test with "superclass resolution requires a ground type". nash_solve::evidence::resolve now keeps open type variables. An open variable equals only itself. An impl that matches whatever the variable is proves the predicate, and resolution reports NonGround only when no impl does and impl selection, a representation test, or the requirements of a type need the variable. The new nash_ast::head::Open matches impl heads against open types. Under SelectPolicy::Exact, select_impl now returns Deferred when no impl is selected and a candidate is undecided. nash_codegen::evidence::Error::NonGround is removed. — Thanks @MicroProofs!

  • f205096a Reject contradictory representation contexts on type applications, such as (Big ('f 'a), Little ('f 'a)), with the existing contradictory-representation error. They used to reach impl selection, where an empty proven set matched every disjoint impl. Export nash_ast::same_type for location-free type comparison. — Thanks @MicroProofs!

  • baadec9e Add the representation coverage rule. When a rigid type variable keeps impl selection from deciding, because the impls are split by its representation class (for example Eq (list ('a : Big)) and Eq 'a => Eq (list ('a : Little))), inference accepts the predicate if the annotation states the trait at that variable and every admitted representation selects an impl whose context holds. same : Eq 'a => list 'a -> list 'a -> bool now compiles. The evidence is the new Evidence::Specialize; code generation selects the impl for each use and keeps the selecting types in the specialization key. A missing element constraint is now reported as a missing constraint, such as Eq 'a, instead of a missing impl for the container. Superclass proofs do not use the rule: an impl names a split requirement in its context. nash-ast also gains head::cover_impls and ReprTrait::exactly. — Thanks @MicroProofs!

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

nash-can 0.13.0 -> 0.14.0

Minor changes

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • 115db1d2 Check every impl context together with its superclasses for contradictory representations. An impl that defines no method, such as impl (Foo 'a, Little 'a) => Sub 'a where Foo requires Big, skipped this check and crashed the superclass entailment check; it now gets the contradictory-representation error. — Thanks @MicroProofs!
  • f205096a Reject contradictory representation contexts on type applications, such as (Big ('f 'a), Little ('f 'a)), with the existing contradictory-representation error. They used to reach impl selection, where an empty proven set matched every disjoint impl. Export nash_ast::same_type for location-free type comparison. — Thanks @MicroProofs!
  • Updated dependencies: nash-ast@0.13.0

nash-cli 0.9.0 -> 0.10.0

Minor changes

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • Updated dependencies: nash-codegen@0.8.0, nash-docs@0.2.4, nash-driver@0.15.0, nash-fmt@0.2.2, nash-language-server@0.5.0, nash-report@0.8.0

nash-codegen 0.7.0 -> 0.8.0

Minor changes

  • 4c4e5155 Resolve superclass evidence when a type variable stays open. A phantom parameter that no use fixes, as in wrapper : tag 'p -> bool; wrapper t = same t t with same : Ord 'a => 'a -> 'a -> bool, passed type checking but stopped nash test with "superclass resolution requires a ground type". nash_solve::evidence::resolve now keeps open type variables. An open variable equals only itself. An impl that matches whatever the variable is proves the predicate, and resolution reports NonGround only when no impl does and impl selection, a representation test, or the requirements of a type need the variable. The new nash_ast::head::Open matches impl heads against open types. Under SelectPolicy::Exact, select_impl now returns Deferred when no impl is selected and a candidate is undecided. nash_codegen::evidence::Error::NonGround is removed. — Thanks @MicroProofs!

  • baadec9e Add the representation coverage rule. When a rigid type variable keeps impl selection from deciding, because the impls are split by its representation class (for example Eq (list ('a : Big)) and Eq 'a => Eq (list ('a : Little))), inference accepts the predicate if the annotation states the trait at that variable and every admitted representation selects an impl whose context holds. same : Eq 'a => list 'a -> list 'a -> bool now compiles. The evidence is the new Evidence::Specialize; code generation selects the impl for each use and keeps the selecting types in the specialization key. A missing element constraint is now reported as a missing constraint, such as Eq 'a, instead of a missing impl for the container. Superclass proofs do not use the rule: an impl names a split requirement in its context. nash-ast also gains head::cover_impls and ReprTrait::exactly. — Thanks @MicroProofs!

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • Updated dependencies: nash-ast@0.13.0, nash-can@0.14.0, nash-ir@0.5.2, nash-solve@0.11.0

nash-constrain 0.9.0 -> 0.10.0

Minor changes

  • ba457678 Restore Elm's constraint tree: nash-constrain generates it from the canonical AST and nash-solve walks it, in place of direct inference. An annotated definition now publishes its declared type: a call with more arguments in the same module no longer replaces an alias in its annotation, so importers find the impls of that alias. — Thanks @MicroProofs!

  • 5655782b Record on each record-field constraint whether it comes from a module test, in place of the Constraint::TestScope wrapper. Constraint::Record and Constraint::Field gain a tests field, TestScope is removed, and pattern::State and pattern::empty_state take the flag. Field visibility is unchanged: fields that only a tests-block import makes visible are visible in tests and nowhere else. — Thanks @MicroProofs!

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • 532e437a Index kind contracts, recovery dependencies, stranded variables, and scheme records so that type checking does not scan every earlier declaration again. — Thanks @MicroProofs!
  • Updated dependencies: nash-ast@0.13.0, nash-can@0.14.0

nash-docs 0.2.3 -> 0.2.4

Patch changes

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

  • Updated dependencies: nash-ast@0.13.0, nash-can@0.14.0, nash-driver@0.15.0, nash-report@0.8.0

nash-driver 0.14.0 -> 0.15.0

Minor changes

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • Updated dependencies: nash-ast@0.13.0, nash-can@0.14.0, nash-codegen@0.8.0, nash-constrain@0.10.0, nash-nitpick@0.3.4, nash-report@0.8.0, nash-solve@0.11.0

nash-fmt 0.2.1 -> 0.2.2

Patch changes

  • Updated dependencies: nash-report@0.8.0

nash-ir 0.5.1 -> 0.5.2

Patch changes

  • Updated dependencies: nash-ast@0.13.0

nash-language-server 0.4.9 -> 0.5.0

Minor changes

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • Updated dependencies: nash-driver@0.15.0, nash-report@0.8.0

nash-nitpick 0.3.3 -> 0.3.4

Patch changes

  • Updated dependencies: nash-ast@0.13.0

nash-report 0.7.0 -> 0.8.0

Minor changes

  • 4dcd4e98 Break a tuple or record type that does not fit the line with one entry per line, as Elm does. The entries were joined without break points, so only the last entries broke and the type drifted to the right. Add Doc::pcat, Elm's D.cat. — Thanks @MicroProofs!

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • 3d86f097 Align the record after "Available fields:" under its opening brace. Its later lines started at the left margin. — Thanks @MicroProofs!
  • f205096a Reject contradictory representation contexts on type applications, such as (Big ('f 'a), Little ('f 'a)), with the existing contradictory-representation error. They used to reach impl selection, where an empty proven set matched every disjoint impl. Export nash_ast::same_type for location-free type comparison. — Thanks @MicroProofs!
  • b613c93b Stop nash check from crashing with "Doc::text must not contain newlines" when a missing-constraint or missing-impl predicate is wider than 80 columns. The help line is now part of the report layout instead of pre-rendered text. When a sentence with a predicate does not fit the line, the predicate moves to its own line, indented by 4. Sentences that fit render as before. — Thanks @MicroProofs!
  • Updated dependencies: nash-ast@0.13.0, nash-can@0.14.0, nash-constrain@0.10.0, nash-nitpick@0.3.4

nash-solve 0.10.0 -> 0.11.0

Minor changes

  • 4c4e5155 Resolve superclass evidence when a type variable stays open. A phantom parameter that no use fixes, as in wrapper : tag 'p -> bool; wrapper t = same t t with same : Ord 'a => 'a -> 'a -> bool, passed type checking but stopped nash test with "superclass resolution requires a ground type". nash_solve::evidence::resolve now keeps open type variables. An open variable equals only itself. An impl that matches whatever the variable is proves the predicate, and resolution reports NonGround only when no impl does and impl selection, a representation test, or the requirements of a type need the variable. The new nash_ast::head::Open matches impl heads against open types. Under SelectPolicy::Exact, select_impl now returns Deferred when no impl is selected and a candidate is undecided. nash_codegen::evidence::Error::NonGround is removed. — Thanks @MicroProofs!

  • baadec9e Add the representation coverage rule. When a rigid type variable keeps impl selection from deciding, because the impls are split by its representation class (for example Eq (list ('a : Big)) and Eq 'a => Eq (list ('a : Little))), inference accepts the predicate if the annotation states the trait at that variable and every admitted representation selects an impl whose context holds. same : Eq 'a => list 'a -> list 'a -> bool now compiles. The evidence is the new Evidence::Specialize; code generation selects the impl for each use and keeps the selecting types in the specialization key. A missing element constraint is now reported as a missing constraint, such as Eq 'a, instead of a missing impl for the container. Superclass proofs do not use the rule: an impl names a split requirement in its context. nash-ast also gains head::cover_impls and ReprTrait::exactly. — Thanks @MicroProofs!

  • d47d2775 Replace every separate search budget with one compile fuel counter, nash_ast::fuel. Trait resolution, impl overlap checks, superclass entailment, evidence resolution and code generation share it: each search step takes a tick, and the driver installs a fresh Fuel for each module's compile. nash check, build, test and docs run with unlimited fuel, so programs that the old fixed limits rejected now compile, such as an impl context that rewraps its argument used at 200 nested types. The language server runs with 10 million steps per module, so an editor gives up on a looping program after a second or two instead of freezing.

    Running out of fuel is one error kind, COMPILATION STEP LIMIT (nash::type::out_of_fuel), replacing ImplResolutionLimit (nash::type::impl_resolution_limit), ImplPatternLimit (nash::names::impl_pattern_limit), the superclass search limit, and the code generation specialization, evidence and recursion normalization limits. The solver reports it at the use that needed the search, canonicalization at the impl being checked, and code generation as a plain error. nash_driver::build, build_with and test_with take a Fuel argument, re-exported as nash_driver::Fuel. — Thanks @MicroProofs!

Patch changes

  • aae91168 Stop reporting ambiguous or unresolved trait constraints on values passed to a definition whose body failed to type check. Their types are unknown because of that failure; the body error is still reported, and fixing it reveals any remaining ambiguity. — Thanks @MicroProofs!
  • ba457678 Restore Elm's constraint tree: nash-constrain generates it from the canonical AST and nash-solve walks it, in place of direct inference. An annotated definition now publishes its declared type: a call with more arguments in the same module no longer replaces an alias in its annotation, so importers find the impls of that alias. — Thanks @MicroProofs!
  • 532e437a Index kind contracts, recovery dependencies, stranded variables, and scheme records so that type checking does not scan every earlier declaration again. — Thanks @MicroProofs!
  • f205096a Reject contradictory representation contexts on type applications, such as (Big ('f 'a), Little ('f 'a)), with the existing contradictory-representation error. They used to reach impl selection, where an empty proven set matched every disjoint impl. Export nash_ast::same_type for location-free type comparison. — Thanks @MicroProofs!
  • b7cb3a12 Do not select an impl for a trait constraint whose argument is an infinite type; the occurs check of the binding reports the type, as in Elm. Two impls that are disjoint on finite types can both match an infinite type, which crashed the compiler, and an impl that matches it at every depth gave a false step-limit error. — Thanks @MicroProofs!
  • 5655782b Record on each record-field constraint whether it comes from a module test, in place of the Constraint::TestScope wrapper. Constraint::Record and Constraint::Field gain a tests field, TestScope is removed, and pattern::State and pattern::empty_state take the flag. Field visibility is unchanged: fields that only a tests-block import makes visible are visible in tests and nowhere else. — Thanks @MicroProofs!
  • 37ea4873 Report a local annotation whose representation constraints contradict an enclosing annotation, such as Little 'a inside Big 'a => ..., as a contradictory-representation error. The two annotations share 'a, and their combined constraints used to reach impl selection and crash the compiler. The error no longer lists a requirement that another listed requirement implies, such as Storable next to Big. — Thanks @MicroProofs!
  • cc95d399 Keep checking callers of an annotated definition against its annotation when its body has a type error. Callers now report their own mismatches and no longer receive spurious ambiguity errors. An annotation whose type variables escape still blocks its uses. — Thanks @MicroProofs!
  • da4a4d3a Unify a type-variable application such as 'f 'a with a transparent alias through the alias body when the alias's own parameters cannot supply the applied arguments. type alias Xs = List Int now works with List.length; record aliases remain nominal. — Thanks @MicroProofs!
  • Updated dependencies: nash-ast@0.13.0, nash-can@0.14.0, nash-constrain@0.10.0

@MicroProofs
MicroProofs merged commit 1f95323 into main Oct 25, 2026
10 checks passed
@MicroProofs
MicroProofs deleted the release/main branch October 25, 2026 06:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants