Data.Parameterized.TH.GADT: Offer a helper for automating EqF instances
#175
Labels
Comments
RyanGlScott
added a commit
to GaloisInc/crucible
that referenced
this issue
Feb 25, 2025
There are many more `EqF` instances that we _could_ define in `crucible`, but defining them all would likely require coming up with a solution for GaloisInc/parameterized-utils#175 first. Until then, this patch adds an `EqF` instance for `TypeRepr` in particular, which is straightforward to define without any additional functionality and addresses the needs of a downstream project.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Data.Parameterized.TH.GADTcurrently offersstructuralTypeEquality, which automates the generation ofTestEqualityinstances, but it does not yet offer a counterpart for generatingEqFinstances. The closest thing that currently exists isstructuralEquality, but this is unsuitable forEqFinstances in general because it is implemented asisJust (... testEquality ...)under the hood. This means that you can end up with instances that look likeinstance TestEquality f => EqF (T f), which uses a stronger instance context than what is necessary.We should offer a variant of
structuralEqualitywhich generates code that gives rise toinstance Eq f => EqF (T f)instead.The text was updated successfully, but these errors were encountered: