Haskell extensible effects: effect in another effect

Question

I'm trying to use extensible-skeleton package. Stacking an effect in another effect results compile error. I tried some other language extensions and type annotations but could not remove these errors. How to resolve these errors?

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import Data.Extensible
import Data.Extensible.Effect
import Data.Type.Equality

type In0 effs = Lookup effs "io" IO
type In1 effs = Lookup effs "reader-float" (ReaderEff Double)

run0 :: forall a. Eff '["io" >: IO] a -> IO a
run0 = retractEff

run1 :: forall effs a. Double -> Eff (("reader-float" >: ReaderEff Double) ': effs) a -> Eff effs a
run1 x = peelEff0 pure $ \Refl k -> k x

lift0 :: forall effs a. In0 effs => IO a -> Eff effs a
lift0 = liftEff (Proxy :: Proxy "io")

ask1 :: forall effs. In1 effs => Eff effs Double
ask1 = askEff (Proxy :: Proxy "reader-float")

eff0 :: forall effs. In0 effs => Eff effs ()
eff0 = do
  lift0 $ print "eff0"
  run1 2.5 eff1

eff1 :: forall effs. (In0 effs, In1 effs) => Eff effs ()
eff1 = do
  x <- ask1
  lift0 $ print "eff1"
  lift0 $ print (floor x)

main :: IO ()
main = do
  run0 eff0

errors at compile time:

[1 of 2] Compiling Main
app/Main.hs:32:12: error:
    • Couldn't match type ‘membership-0:Type.Membership.Internal.Elaborate
                             "io" (membership-0:Type.Membership.Internal.FindAssoc 1 "io" effs)’
                     with ‘'membership-0:Type.Membership.Internal.Expecting (n0 ':> IO)’
        arising from a use of ‘eff1’
      The type variable ‘n0’ is ambiguous
    • In the second argument of ‘run1’, namely ‘eff1’
      In a stmt of a 'do' block: run1 2.5 eff1
      In the expression:
        do lift0 $ print "eff0"
           run1 2.5 eff1
    • Relevant bindings include
        eff0 :: Eff effs () (bound at app/Main.hs:30:1)
   |
32 |   run1 2.5 eff1
   |            ^^^^

What's wrong?

Answer 1

The problem seems to be that run1 (which is already available as runReaderEff, by the way) accepts an effect whose outermost layer is "reader-float", but the effect eff1 that you're trying to run1 only satisfies In1 effs, which guarantees "reader-float" is in there somewhere, but not necessarily at the outermost layer.

This reflects the fact that you can't run an arbitrary layer buried in the stack. You need to run the layers from the outside-in.

What does work is constructing an explicit effect stack for eff1 and then upcasting:

eff0 :: forall effs. In0 effs => Eff effs ()
eff0 = do
  lift0 $ print "eff0"
  castEff $ run1 2.5 (eff1 :: Eff '["reader-float" :> ReaderEff Double, "io" :> IO] ())

It might seem like you want to prepend "reader-float" to the effs for eff0 and so write:

{-# LANGUAGE ScopedTypeVariables #-}

eff0 :: forall effs. In0 effs => Eff effs ()
eff0 = do
  lift0 $ print "eff0"
  castEff $ run1 2.5 (eff1 :: Eff (("reader-float" :> ReaderEff Double) ': effs) ())

but this doesn't work. However, if you think about it for a bit, there's no reason to run eff1 here in anything other than the specific ["reader-float", "io"] stack.

Remember, the reason for having general effs in the type signatures for eff0 and eff1 is to let them be used in any effects stack with their required layers; the general type signatures are for the benefit of the caller. In this case, eff0 is calling eff1, and it has no reason to supply eff1 with anything other than the layers it needs, the new "reader-float" layer that it constructs locally, and the "io" layer that it casts into its own general effs environment. There's nothing else in effs of interest to eff0 or eff1, so no need to propagate effs down from eff0 to eff1.