Make NuMatchingAny1Proof an alias for a quantified NuMatching constraint
#8
Conversation
This file contains 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
…straint
Previously, there was a global `INCOHERENT` instance of the form:
```hs
instance {-# INCOHERENT #-} NuMatchingAny1 f => NuMatching (f a) where
nuMatchingProof = nuMatchingAny1Proof
```
This does not combine well with GHC 9.0+'s Template Haskell splice behavior,
where instances written after a top-level declaration splice are not visible to
instances written before the splice. In particular, this affects which instances
GHC will consider when resolving instance overlap w.r.t. incoherent instances,
so if you are not careful with the ordering of instances and TH splices, you
can accidentally change the _runtime_ behavior of your program. For more
information, see GaloisInc/saw-script#1742 and
https://gitlab.haskell.org/ghc/ghc/-/issues/22492.
This patch removes the `INCOHERENT` instance and instead makes `NuMatchingAny1`
an alias for a quantified constraint involving `NuMatching`:
```hs
class (forall a. NuMatching (f a)) => NuMatchingAny1 (f :: k -> Type)
instance (forall a. NuMatching (f a)) => NuMatchingAny1 (f :: k -> Type)
```
(Alternatively, we could have made this a type synonym, but using a class has
the advantage of not forcing downstream libraries to enable
`QuantifiedConstraints` everywhere that `NuMatchingAny1` is used.)
Aside from this change, the rest of this patch simply deletes `NuMatchingAny1`
instances, as the one instance above is the only instance we will ever need now.
Credit goes to Matthew Pickering for helping me identify this issue and for
authoring a separate fix. I have tweaked his fix and turned it into this patch,
adding him as a co-author in the process.
Co-authored-by: Matthew Pickering <matthewtpickering@gmail.com>
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Dec 5, 2022
This makes the necessary changes to adapt to eddywestbrook/hobbits#8, which turns `NuMatchingAny1` into an alias for a quantified `NuMatching` constraint. See #1742 and https://gitlab.haskell.org/ghc/ghc/-/issues/22492 for the motivation behind this. One unfortunate hiccup with this patch is that combining quantified superclasses and `TypeFamilies` doesn't quite work out of the box on pre-9.2 GHCs due to https://gitlab.haskell.org/ghc/ghc/-/issues/14860. As a result, I have to introduce explicit equality constraints to work around the issue. I have added a `Note [QuantifiedConstraints + TypeFamilies trick]` to describe why the workaround is necessary. Credit goes to Matthew Pickering for helping me identify this issue and for authoring a separate fix. I have tweaked his fix and turned it into this patch, adding him as a co-author in the process. Fixes #1742. Co-authored-by: Matthew Pickering <matthewtpickering@gmail.com>
eddywestbrook
approved these changes
Dec 5, 2022
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Dec 5, 2022
This makes the necessary changes to adapt to eddywestbrook/hobbits#8, which turns `NuMatchingAny1` into an alias for a quantified `NuMatching` constraint. See #1742 and https://gitlab.haskell.org/ghc/ghc/-/issues/22492 for the motivation behind this. One unfortunate hiccup with this patch is that combining quantified superclasses and `TypeFamilies` doesn't quite work out of the box on pre-9.2 GHCs due to https://gitlab.haskell.org/ghc/ghc/-/issues/14860. As a result, I have to introduce explicit equality constraints to work around the issue. I have added a `Note [QuantifiedConstraints + TypeFamilies trick]` to describe why the workaround is necessary. Credit goes to Matthew Pickering for helping me identify this issue and for authoring a separate fix. I have tweaked his fix and turned it into this patch, adding him as a co-author in the process. Fixes #1742. Co-authored-by: Matthew Pickering <matthewtpickering@gmail.com>
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.
Previously, there was a global
INCOHERENTinstance of the form:This does not combine well with GHC 9.0+'s Template Haskell splice behavior, where instances written after a top-level declaration splice are not visible to instances written before the splice. In particular, this affects which instances GHC will consider when resolving instance overlap w.r.t. incoherent instances, so if you are not careful with the ordering of instances and TH splices, you can accidentally change the runtime behavior of your program. For more information, see GaloisInc/saw-script#1742 and https://gitlab.haskell.org/ghc/ghc/-/issues/22492.
This patch removes the
INCOHERENTinstance and instead makesNuMatchingAny1an alias for a quantified constraint involvingNuMatching:(Alternatively, we could have made this a type synonym, but using a class has the advantage of not forcing downstream libraries to enable
QuantifiedConstraintseverywhere thatNuMatchingAny1is used.)Aside from this change, the rest of this patch simply deletes
NuMatchingAny1instances, as the one instance above is the only instance we will ever need now.Credit goes to Matthew Pickering for helping me identify this issue and for authoring a separate fix. I have tweaked his fix and turned it into this patch, adding him as a co-author in the process.