Always use QuantifiedConstraints, support inductive GADTs #17
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
…phic instances." This reverts commit 5c50d96.
Ericson2314
force-pushed
the
ghc-86-plus-only
branch
from
3c5d8c9 to
5a49608
Compare
alexfmpe
reviewed
Sep 12, 2019
Co-Authored-By: Alexandre Esteves <2335822+alexfmpe@users.noreply.github.com>
Anywhere we get an `Extract` we do it ultimately via `argDictAll`, so the `ArgDict f` constraint must already be satified in scope.
3noch
reviewed
Sep 12, 2019
Thanks! Co-Authored-By: Elliot Cameron <3noch@users.noreply.github.com>
xplat
reviewed
Sep 12, 2019
|
Is it necessary to drop support for ghc < 86? |
|
There might be a way, but only with copious CPP. I like what this PR does, but it is a solution in search of a problem. I think eventually we'll want it (e.g. IV debugging constraints), but for now we can just leave open. |
ali-abrar
changed the title
It is only allowed with GHC 8.6, and doesn't work very well there I'm told. https://gitlab.haskell.org/ghc/ghc/-/issues/14860 tracks the underlying issue.
Ericson2314
force-pushed
the
ghc-86-plus-only
branch
from
079af12 to
2283ddc
Compare
Ericson2314
changed the title
Ericson2314
commented
Jun 30, 2023
| -- @argDict@ is sufficient for most tasks, but this is slightly more powerful | ||
| -- in that this discharges the quantified constraints which are useful when | ||
| -- the GADT indices are not finite. | ||
| argDictAll :: f a -> Dict (Extract f a) |
There was a problem hiding this comment.
N.B. This wants to be:
Suggested change
| argDictAll :: f a -> Dict (Extract f a) | |
| argDictAll :: f a -> Dict (forall c. ConstraintsFor f c => c a)) |
There was a problem hiding this comment.
The big question is, is the following weaker?
argDictAll :: f a -> forall c. Dict (ConstraintsFor f c => c a))
# for free
to join this conversation on GitHub.
Already have an account?
# 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.
I put a manual instance in the README, but we could do it with TH later.