Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
I'm having trouble with this:
data Foo a :: Effect where
Foo :: Foo a m x
interpretFoo :: InterpreterFor (Foo a) r
Members [Foo a, Foo [a]] r =>
Sem r ()
∀ (a :: *) r .
Sem r ()
interpretFoo @a (interpretFoo @[a] (runFoo @a))
• Couldn't match type ‘Polysemy.Internal.Union.LocateEffect
(Foo a) (Foo [a] : Foo a : r)’
arising from a use of ‘runFoo’
• In the second argument of ‘interpretFoo’, namely ‘(runFoo @a)’
In the second argument of ‘interpretFoo’, namely
‘(interpretFoo @[a] (runFoo @a))’
In the expression: interpretFoo @a (interpretFoo @[a] (runFoo @a))
• Relevant bindings include
runFoo' :: Sem r ()
(bound at /home/tek/code/tek/haskell/tvdb/packages/tvdb/lib/Tvdb/Episodes.hs:100:1)
101 | interpretFoo @a (interpretFoo @[a] (runFoo @a))
it feels like what happens when the plugin isn't used, but I'm fairly certain that it is active.
This works fine when a is concrete, is this a limitation? am I just missing something obvious?
works like this btw:
runFoo :: Sem (Foo a : Foo [a] : r) ()
Yeah, it's a limitation - class and type family that search for effect in a row have to compare effects for equality to say whether they match - but they can't be sure when those effects are polymorphic
We would need some sort of "type inequality" wired into compiler to do such stuff
foiled again by constructivism!
I mean, I guess it would be doable, it just wouldn't support inference
Oh, and in this case, any attempt to unify those would fail occurs check, so I guess this one could even be inferred :big_smile:
(or just recognized as not equal by GHC)
I came to the same conclusion, perhaps a itself is too polymorphic somehow, and it's not shared between the a and the [a], so the occurrence check isn't triggered?? Or maybe UndecidableInstances removes such a check? (if we even use it?, but I don't think we do)
idk, it should never be reasonable to try to unify a and [a] more than once, something weird is going on
No, type family just gets stuck when it tries to check equality of two effects which are polymorphic
oh come on..