How do I compose 'freer' effects in haskell?

Question

I'm attempting to rewrite a simple interpreter from a transformers-based monad stack to effects based on freer, but I'm running up against a difficulty communicating my intent to GHC's type system.

I am only using the State and Fresh effects at present. I'm using two states and my effect runner looks like this:

runErlish g ls = run . runGlobal g . runGensym 0 . runLexicals ls
  where runGlobal    = flip runState
        runGensym    = flip runFresh'
        runLexicals  = flip runState

On top of this, I have defined a function FindMacro with this type:

findMacro :: Members [State (Global v w), State [Scope v w]] r
             => Arr r Text (Maybe (Macro (Term v w) v w))

All of this so far works perfectly fine. The problem comes when I try to write macroexpand2 (well, macroexpand1, but i'm simplifying it so the question is easier to follow):

macroexpand2 s =
  do m <- findMacro s
     return $ case m of
       Just j -> True
       Nothing -> False

This produces the following error:

Could not deduce (Data.Open.Union.Member'
                    (State [Scope v0 w0])
                    r
                    (Data.Open.Union.FindElem (State [Scope v0 w0]) r))
from the context (Data.Open.Union.Member'
                    (State [Scope v w])
                    r
                    (Data.Open.Union.FindElem (State [Scope v w]) r),
                  Data.Open.Union.Member'
                    (State (Global v w))
                    r
                    (Data.Open.Union.FindElem (State (Global v w)) r))
  bound by the inferred type for `macroexpand2':
             (Data.Open.Union.Member'
                (State [Scope v w])
                r
                (Data.Open.Union.FindElem (State [Scope v w]) r),
              Data.Open.Union.Member'
                (State (Global v w))
                r
                (Data.Open.Union.FindElem (State (Global v w)) r)) =>
             Text -> Eff r Bool
  at /tmp/flycheck408QZt/Erlish.hs:(79,1)-(83,23)
The type variables `v0', `w0' are ambiguous
When checking that `macroexpand2' has the inferred type
  macroexpand2 :: forall (r :: [* -> *]) v (w :: [* -> *]).
                  (Data.Open.Union.Member'
                     (State [Scope v w])
                     r
                     (Data.Open.Union.FindElem (State [Scope v w]) r),
                   Data.Open.Union.Member'
                     (State (Global v w))
                     r
                     (Data.Open.Union.FindElem (State (Global v w)) r)) =>
                  Text -> Eff r Bool
Probable cause: the inferred type is ambiguous

Okay, I can add a Members annotation to the type:

macroexpand2 :: Members [State (Global v w), State [Scope  v w]] r
                => Text -> Eff r Bool

And now I get this:

Overlapping instances for Member (State [Scope v0 w0]) r
  arising from a use of `findMacro'
Matching instances:
  instance Data.Open.Union.Member'
             t r (Data.Open.Union.FindElem t r) =>
           Member t r
    -- Defined in `Data.Open.Union'
There exists a (perhaps superclass) match:
  from the context (Members
                      '[State (Global v w), State [Scope v w]] r)
    bound by the type signature for
               macroexpand2 :: Members
                                 '[State (Global v w), State [Scope v w]] r =>
                               Text -> Eff r Bool
    at /tmp/flycheck408QnV/Erlish.hs:(79,17)-(80,37)
(The choice depends on the instantiation of `r, v0, w0'
 To pick the first instance above, use IncoherentInstances
 when compiling the other instance declarations)
In a stmt of a 'do' block: m <- findMacro s
In the expression:
  do { m <- findMacro s;
       return
       $ case m of {
           Just j -> True
           Nothing -> False } }
In an equation for `macroexpand2':
    macroexpand2 s
      = do { m <- findMacro s;
             return
             $ case m of {
                 Just j -> True
             Nothing -> False } }

I was advised on irc to try forall r v w. which made no difference. Out of curiosity i tried using IncoherentInstances when compiling this code (I did not fancy checking out a fork of freer and playing) to see if perhaps it would give me a clue as to what was going on. It did not:

Could not deduce (Data.Open.Union.Member'
                    (State [Scope v0 w0])
                    r
                    (Data.Open.Union.FindElem (State [Scope v0 w0]) r))
  arising from a use of `findMacro'
from the context (Members
                    '[State (Global v w), State [Scope v w]] r)
  bound by the type signature for
             macroexpand2 :: Members
                               '[State (Global v w), State [Scope v w]] r =>
                             Text -> Eff r Bool
  at /tmp/flycheck408eru/Erlish.hs:(79,17)-(80,37)
The type variables `v0', `w0' are ambiguous
Relevant bindings include
  macroexpand2 :: Text -> Eff r Bool
    (bound at /tmp/flycheck408eru/Erlish.hs:81:1)
Note: there are several potential instances:
  instance (r ~ (t' : r'), Data.Open.Union.Member' t r' n) =>
           Data.Open.Union.Member' t r ('Data.Open.Union.S n)
    -- Defined in `Data.Open.Union'
  instance (r ~ (t : r')) =>
           Data.Open.Union.Member' t r 'Data.Open.Union.Z
    -- Defined in `Data.Open.Union'
In a stmt of a 'do' block: m <- findMacro s
In the expression:
  do { m <- findMacro s;
       return
       $ case m of {
           Just j -> True
           Nothing -> False } }
In an equation for `macroexpand2':
    macroexpand2 s
      = do { m <- findMacro s;
             return
             $ case m of {
                 Just j -> True
                 Nothing -> False } }

So, this is where my understanding of freer's internals runs out and I have questions:

1. Why is there an overlapping instance? I don't understand where that's coming from.
2. What does IncoherentInstances actually do? Autoselection sounds pretty likely to cause hard-to-debug errors.
3. How do I actually make use of findMacro within another function?

Cheers!

Answer 1

Type inference for extensible effects has been historically bad. Let's see some examples:

{-# language TypeApplications #-}

-- mtl
import qualified Control.Monad.State as M

-- freer
import qualified Control.Monad.Freer as F
import qualified Control.Monad.Freer.State as F

-- mtl works as usual
test1 = M.runState M.get 0

-- this doesn't check
test2 = F.run $ F.runState F.get 0  

-- this doesn't check either, although we have a known
-- monomorphic state type
test3 = F.run $ F.runState F.get True

-- this finally checks
test4 = F.run $ F.runState (F.get @Bool) True

-- (the same without TypeApplication)
test5 = F.run $ F.runState (F.get :: F.Eff '[F.State Bool] Bool) True

I'll try to explain the general issue and provide minimal code illustration. A self-contained version of the code can be found here.

On the most basic level (disregarding optimized representations), Eff is defined the following way:

{-# language
  GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables,
  TypeFamilies, DeriveFunctor, EmptyCase, TypeApplications,
  UndecidableInstances, StandaloneDeriving, ConstraintKinds,
  MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
  AllowAmbiguousTypes, PolyKinds
  #-}

import Control.Monad

data Union (fs :: [* -> *]) (a :: *) where
  Here  :: f a -> Union (f ': fs) a
  There :: Union fs a -> Union (f ': fs) a

data Eff (fs :: [* -> *]) (a :: *) =
  Pure a | Free (Union fs (Eff fs a))

deriving instance Functor (Union fs) => Functor (Eff fs)  

In other words, Eff is a free monad from an union of a list of functors. Union fs a behaves like an n-ary Coproduct. The binary Coproduct is like Either for two functors:

data Coproduct f g a = InL (f a) | InR (g a)

In contrast, Union fs a lets us choose a functor from a list of functors:

type MyUnion = Union [[], Maybe, (,) Bool] Int

-- choose the first functor, which is []
myUnion1 :: MyUnion
myUnion1 = Here [0..10]

-- choose the second one, which is Maybe
myUnion2 :: MyUnion
myUnion2 = There (Here (Just 0))

-- choose the third one
myUnion3 :: MyUnion
myUnion3 = There (There (Here (False, 0)))

Let's implement the State effect as an example. First, we need to have a Functor instance for Union fs, since Eff only has a Monad instance if Functor (Union fs).

Functor (Union '[]) is trivial, since the empty union doesn't have values:

instance Functor (Union '[]) where
  fmap f fs = case fs of {} -- using EmptyCase

Otherwise we prepend a functor to the union:

instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where
  fmap f (Here fa) = Here (fmap f fa)
  fmap f (There u) = There (fmap f u)

Now the State definition and the runners:

run :: Eff '[] a -> a
run (Pure a) = a

data State s k = Get (s -> k) | Put s k deriving Functor

runState :: forall s fs a. Functor (Union fs) => Eff (State s ': fs) a -> s -> Eff fs (a, s)
runState (Pure a)                 s = Pure (a, s)
runState (Free (Here (Get k)))    s = runState (k s) s
runState (Free (Here (Put s' k))) s = runState k s'
runState (Free (There u))         s = Free (fmap (`runState` s) u)

We can already start writing and running our Eff programs, although we lack all the sugar and convenience:

action1 :: Eff '[State Int] Int
action1 =
  Free $ Here $ Get $ \s ->
  Free $ Here $ Put (s + 10) $
  Pure s

-- multiple state
action2 :: Eff '[State Int, State Bool] ()
action2 =
  Free $ Here $ Get $ \n ->            -- pick the first effect
  Free $ There $ Here $ Get $ \b ->    -- pick the second effect
  Free $ There $ Here $ Put (n < 10) $ -- the second again
  Pure ()

Now:

> run $ runState action1 0
(0,10)
> run $ (`runState` False) $ (`runState` 0) action2
(((),0),True)

There are only two essential missing things here.

The first one is the monad instance for Eff which lets us use do-notation instead of Free and Pure, and also lets us use the many polymorphic monadic functions. We shall skip it here because it's straightforward to write.

The second one is inference/overloading for choosing effects from lists of effects. Previously we needed to write Here x in order to choose the first effect, There (Here x) to choose the second one, and so on. Instead, we'd like to write code that's polymorphic in effect lists, so all we have to specify is that some effect is an element of a list, and some hidden typeclass magic will insert the appropriate number of There-s.

We need a Member f fs class that can inject f a-s into Union fs a-s when f is an element of fs. Historically, people have implemented it in two ways.

First, directly with OverlappingInstances:

class Member (f :: * ->  *) (fs :: [* -> *]) where
  inj :: f a -> Union fs a

instance Member f (f ': fs) where
  inj = Here

instance {-# overlaps #-} Member f fs => Member f (g ': fs) where
  inj = There . inj

-- it works
injTest1 :: Union [[], Maybe, (,) Bool] Int
injTest1 = inj [0]

injTest2 :: Union [[], Maybe, (,) Bool] Int
injTest2 = inj (Just 0)

Second, indirectly, by first computing the index of f in fs with a type family, then implementing inj with a non-overlapping class, guided by f-s computed index. This is generally viewed as better because people tend to dislike overlapping instances.

data Nat = Z | S Nat

type family Lookup f fs where
  Lookup f (f ': fs) = Z
  Lookup f (g ': fs) = S (Lookup f fs)

class Member' (n :: Nat) (f :: * -> *) (fs :: [* -> *]) where
  inj' :: f a -> Union fs a

instance fs ~ (f ': gs) => Member' Z f fs where
  inj' = Here

instance (Member' n f gs, fs ~ (g ': gs)) => Member' (S n) f fs where
  inj' = There . inj' @n

type Member f fs = Member' (Lookup f fs) f fs

inj :: forall fs f a. Member f fs => f a -> Union fs a
inj = inj' @(Lookup f fs)

-- yay
injTest1 :: Union [[], Maybe, (,) Bool] Int
injTest1 = inj [0]

The freer library uses the second solution, while extensible-effects uses the first one for GHC versions older than 7.8, and the second for newer GHC-s.

Anyway, both solutions have the same inference limitation, namely that we can almost always Lookup only concrete monomorphic types, not types that contain type variables. Examples in ghci:

> :kind! Lookup Maybe [Maybe, []]
Lookup Maybe [Maybe, []] :: Nat
= 'Z

This works because there are no type variables in either Maybe or [Maybe, []].

> :kind! forall a. Lookup (Either a) [Either Int, Maybe]
forall a. Lookup (Either a) [Either Int, Maybe] :: Nat
= Lookup (Either a) '[Either Int, Maybe]

This one gets stuck because the a type variable blocks reduction.

> :kind! forall a. Lookup (Maybe a) '[Maybe a]
forall a. Lookup (Maybe a) '[Maybe a] :: Nat
= Z

This works, because the only thing we know about arbitrary type variables is that they are equal to themselves, and a is equal to a.

In general, type family reduction gets stuck on variables, because constraint solving can potentially refine them later to different types, so GHC can't make any assumptions about them (aside from being equal to themselves). Essentially the same issue arises with the OverlappingInstances implementation (although there aren't any type families).

Let's revisit freer in the light of this.

import Control.Monad.Freer
import Control.Monad.Freer.State

test1 = run $ runState get 0 -- error

GHC knows that we have a stack with a single effect, since run works on Eff '[] a. It also knows that that effect must be State s. But when we write get, GHC only knows that it has a State t effect for some fresh t variable, and that Num t must hold, so when it tries to compute the freer equivalent of Lookup (State t) '[State s], it gets stuck on the type variables, and any further instance resolution trips up on the stuck type family expression. Another example:

foo = run $ runState get False -- error

This also fails because GHC needs to compute Lookup (State s) '[State Bool], and although we know that the state must be Bool, this still gets stuck because of the s variable.

foo = run $ runState (modify not) False -- this works

This works because the state type of modify not can be resolved to Bool, and Lookup (State Bool) '[State Bool] reduces.

Now, after this large detour, I shall address your questions at the end of your post.

1. Overlapping instances is not indicative of any possible solution, just a type error artifact. I would need more code context to pinpoint how exactly it arises, but I'm sure it's not relevant, since as soon as Lookup gets stuck the case becomes hopeless.

2. IncoherentInstances is also irrelevant and doesn't help. We need a concrete effect position index to be able to generate code for the program, and we can't pull an index out of thin air if Lookup gets stuck.

3. The problem with findMacro is that it has State effects with type variables inside the states. Whenever you want to use findMacro you have to make sure that the v and w parameters for Scope and Global are known concrete types. You can do this by type annotations, or more conveniently you can use TypeApplications, and write findMacro @Int @Int for specifying v = Int and w = Int. If you have findMacro inside a polymorphic function, you need to enable ScopedTypeVariables, bind v and w using a forall v w. annotation for that function, and write findMacro @v @w when you use it. You also need to enable {-# language AllowAmbiguousTypes #-} for polymorphic v or w (as pointed out in the comments). I think though that in GHC 8 it's a reasonable extension to enable, together with TypeApplications.

---

Addendum:

However, fortunately new GHC 8 features let us repair type inference for extensible effects, and we can infer everything mtl can, and also some things mtl can't handle. The new type inference is also invariant with respect to the ordering of effects.

I have a minimal implementation here along with a number of examples. However, it's not yet used in any effect library that I know of. I'll probably do a write-up on it, and do a pull request in order to add it to freer.