two polymorphic variants of the same effect - Polysemy

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Torsten Schmits

I'm having trouble with this:

data Foo a :: Effect where
  Foo :: Foo a m x

makeSem ''Foo

interpretFoo :: InterpreterFor (Foo a) r
interpretFoo =
  undefined

runFoo ::
  Members [Foo a, Foo [a]] r =>
  Sem r ()
runFoo =
  undefined

runFoo' ::
   (a :: *) r .
  Sem r ()
runFoo' =
  interpretFoo @a (interpretFoo @[a] (runFoo @a))

getting:

    • Couldn't match type ‘Polysemy.Internal.Union.LocateEffect
                             (Foo a) (Foo [a] : Foo a : r)’
                     with ‘'()’
        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?

Torsten Schmits

works like this btw:

runFoo :: Sem (Foo a : Foo [a] : r) ()
TheMatten

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

TheMatten

We would need some sort of "type inequality" wired into compiler to do such stuff

Torsten Schmits

foiled again by constructivism!

TheMatten

I mean, I guess it would be doable, it just wouldn't support inference

TheMatten

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:

TheMatten

(or just recognized as not equal by GHC)

Georgi Lyubenov // googleson78

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)

Georgi Lyubenov // googleson78

idk, it should never be reasonable to try to unify a and [a] more than once, something weird is going on

TheMatten

No, type family just gets stuck when it tries to check equality of two effects which are polymorphic