Repository navigation
Infer a common error type for composed relation proofs - #388
Merged
Merged
Conversation
There was a problem hiding this comment.
🟡 Changes recommended
Relation-level tests do not cover composed proofs with independent child error types.
1 open finding
What changed in this PR
Introduces shared error-type inference for composed bifunctor relation proofs.
Changes:
- Adds
CommonErrorsubtype evidence. - Widens child interpreters to a shared error type.
- Adds evidence-level regression tests.
| File | Description |
|---|---|
CommonError.scala |
Defines common-error evidence. |
bifunctor/proof.scala |
Applies shared errors across composition forms. |
CommonErrorSpec.scala |
Tests evidence inference and value preservation. |
🧠 Review effort: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
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.

Composed and zipped relation proofs need a shared error type that accepts failures from either child. Resolve the child proofs with independent error types, then infer the parent error type through
CommonErrorand widen the interpreters using its subtype evidence.Relation-level regression tests materialize single, optional, many, and zipped proofs with distinct left/right failure types. They check shared-type inference and preservation of both failures in single and batched execution, as well as successful outputs, absent optional results, and empty collections.
Validation: core tests passed on Scala 2.13 and 3.3, on JVM and Scala.js, together with
fmtCheck. Proof construction is reviewed separately in #387, stacked on this branch.