[Peras 46] Introduce Void Peras types and helpers - #2173
Open
agustinmista wants to merge 2 commits into
Open
Conversation
agustinmista
force-pushed
the
peras/void-helpers
branch
2 times, most recently
from
August 3, 2026 08:58
b32fd94 to
50aaf94
Compare
agustinmista
force-pushed
the
peras/void-helpers
branch
from
August 3, 2026 09:18
50aaf94 to
ad1c1c1
Compare
This commit introduces Void-based Peras helpers to be used in the default BlockSupportsPeras instance for block types that do not support Peras. NOTE: we use newtypes with phantom blk parameters instead of type synonyms over Void in several places. This is deliberate, as we want these types to be usable to instantiate injective type families directly (i.e, without any extra unecessary wrapper) later on. NOTE: with the exception of the instance IsPerasError for VoidPerasError, all the necessary methods associated with these types are discharged by contradiction 'absurd'. Co-authored-by: Agustin Mista <agustin.mista@tweag.io> Co-authored-by: Thomas BAGREL <thomas.bagrel@tweag.io> Co-authored-by: Nicolas BACQUEY <nicolas.bacquey@tweag.io>
agustinmista
force-pushed
the
peras/void-helpers
branch
from
August 3, 2026 09:43
ad1c1c1 to
33c9e98
Compare
agustinmista
marked this pull request as ready for review
August 3, 2026 12:52
agustinmista
requested review from
bladyjoker,
dnadales,
geo2a,
jasagredo and
nfrisby
as code owners
August 3, 2026 12:52
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.
This PR introduces Void-based Peras helpers to be used in the default
BlockSupportsPerasinstance for block types that do not support Peras.NOTE: we use newtypes with phantom
blkparameters instead of type synonyms overVoidin several places. This is deliberate, as we want these types to be usable to instantiate injective type families directly (i.e, without any extra unnecessary wrapper) later on.NOTE: with the exception of the instance
IsPerasErrorforVoidPerasError, all the necessary methods associated with these types are discharged by contradiction 'absurd'.