Allow bidirectional typechecking in the plugin #105
Merged
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
The plugin used to choke on this: ```haskell flipShouldBe 11 . sum . fst . run . runFoldMapOutput id $ do output [1] output $ replicate 2 5 ``` because it would fail to unify `Output (t Int)` (the polymorphic `Traversable` variable in `sum`) with `Output [Int]`. In this case, there are no given constraints, so the plugin is attempting to solve a `Member (Output (t Int)) '[Output [Int]]`. We reuse the codepath for unifying wanted/givens, pretending like the `Output (t Int)` is a given.[^1] [^1]: Pretending it's a wanted breaks something else that I don't remember right now. This code is brittle :( So now we have a "wanted" `Output [Int]`, and a "given" `Output (t Int)`. In general, this thing isn't OK to solve. Consider a real example: ```haskell foo :: Member (Output (t Int)) r => Sem r () foo = output [5] ``` This is a type error, because the polymorphism goes the wrong way. We have no guarantees that `t` is supposed to be `[]`. But in our original example, this isn't a problem, because our `t` isn't actually in given position. It's just an artifact of reusing the code! `mkWanted` now takes a new parameter for whether or not it's OK to allow the givens to be polymorphic. Such a thing necessitates a change though. We never want to unify a polymorphic *effect* in given position. Doing so will break Haskell's regular type inference that determines what the effect row should be, based on the order in which the interpreters are run. Fixes #95
|
I've tested this against |
|
If someone tries to put this into ghci (as I did 😄) - the reason it works here is that ghci has |
TheMatten
approved these changes
Jun 14, 2019
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.
The plugin used to choke on this:
because it would fail to unify
Output (t Int)(the polymorphicTraversablevariable insum) withOutput [Int].In this case, there are no given constraints, so the plugin is attempting to solve a
Member (Output (t Int)) '[Output [Int]]. We reuse the codepath for unifying wanted/givens, pretending like theOutput (t Int)is a given.1So now we have a "wanted"
Output [Int], and a "given"Output (t Int). In general, this thing isn't OK to solve. Consider a real example:This is a type error, because the polymorphism goes the wrong way. We have no guarantees that
tis supposed to be[].But in our original example, this isn't a problem, because our
tisn't actually in given position. It's just an artifact of reusing the code!mkWantednow takes a new parameter for whether or not it's OK to allowthe givens to be polymorphic.
Such a thing necessitates a change though. We never want to unify a polymorphic effect in given position. Doing so will break Haskell's regular type inference that determines what the effect row should be, based on the order in which the interpreters are run.
Fixes #95
Footnotes
Pretending it's a wanted breaks the common case of trying to call, eg.
runState (5 :: Num a => a)on an effectState Int. ↩