Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow bidirectional typechecking in the plugin #105

Merged
merged 2 commits into from Jun 14, 2019

Conversation

Projects
None yet
2 participants
@isovector
Copy link
Collaborator

commented Jun 14, 2019

The plugin used to choke on this:

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 the common case of trying to call, eg. runState (5 :: Num a => a) on an effect State Int.

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:

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

Allow bidirectional typechecking in the plugin
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

@isovector isovector added the plugin label Jun 14, 2019

@isovector isovector requested a review from TheMatten Jun 14, 2019

@isovector

This comment has been minimized.

Copy link
Collaborator Author

commented Jun 14, 2019

I've tested this against polysemy-zoo. I'm also trying to run it against hskit, but currently stuck in dependency hell. Will report back when I have the results.

@TheMatten

This comment has been minimized.

Copy link
Collaborator

commented Jun 14, 2019

If someone tries to put this into ghci (as I did 😄) - the reason it works here is that ghci has ExtendedDefaultRules enabled, which probably finds Foldable t from sum and fits [] in there.

@TheMatten
Copy link
Collaborator

left a comment

Maybe you can extend comment about "given" constraint so that we don't forget what's going on here, but otherwise it seems fine to me 🙂

@isovector isovector merged commit e90c745 into master Jun 14, 2019

2 checks passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details
continuous-integration/travis-ci/push The Travis CI build passed
Details

@isovector isovector deleted the plugin-poly-given-ok branch Jun 14, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.