interpretM sometimes needs extra constraints

[rkanati]

So compositions of interpretM seem to have trouble carrying through LastMember constraints, somehow. This is the smallest example I could construct that reproduces.

Removing the marked line works around the problem.

{-# LANGUAGE RankNTypes, TypeOperators, GADTs, DataKinds, FlexibleContexts #-}

module Main where

import Control.Monad.Freer

data Fx1 a where
  Fx1 :: Fx1 ()

data Fx2 a where
  Fx2 :: Fx2 ()

runFx :: forall effs a
      .  ( LastMember IO effs
         , LastMember IO (Fx1 ': effs) -- COMMENT OUT TO FIX
         )
      => Eff (Fx2 ': Fx1 ': effs) a
      -> Eff effs a
runFx
  = interpretM (\Fx1 -> putStrLn "Fx1")
  . interpretM (\Fx2 -> putStrLn "Fx2")

main :: IO ()
main = runM . runFx $ do
  send Fx1
  send Fx2

src/Main.hs:21:5: error:
    • Could not deduce (Monad (Data.OpenUnion.Last (Fx1 : effs)))
        arising from a use of ‘interpretM’
      from the context: LastMember IO effs
        bound by the type signature for:
                   runFx :: forall (effs :: [* -> *]) a.
                            LastMember IO effs =>
                            Eff (Fx2 : Fx1 : effs) a -> Eff effs a
        at src/Main.hs:(13,1)-(18,19)
      There are instances for similar types:
        instance Monad Data.Semigroup.Last -- Defined in ‘Data.Semigroup’
    • In the second argument of ‘(.)’, namely
        ‘interpretM (\ Fx2 -> putStrLn "Fx2")’
      In the expression:
        interpretM (\ Fx1 -> putStrLn "Fx1")
          . interpretM (\ Fx2 -> putStrLn "Fx2")
      In an equation for ‘runFx’:
          runFx
            = interpretM (\ Fx1 -> putStrLn "Fx1")
                . interpretM (\ Fx2 -> putStrLn "Fx2")
   |
21 |   . interpretM (\Fx2 -> putStrLn "Fx2")
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Main.hs:21:25: error:
    • Could not deduce: Data.OpenUnion.Last (Fx1 : effs) ~ IO
      from the context: LastMember IO effs
        bound by the type signature for:
                   runFx :: forall (effs :: [* -> *]) a.
                            LastMember IO effs =>
                            Eff (Fx2 : Fx1 : effs) a -> Eff effs a
        at src/Main.hs:(13,1)-(18,19)
      or from: x ~ ()
        bound by a pattern with constructor: Fx2 :: Fx2 (),
                 in a lambda abstraction
        at src/Main.hs:21:18-20
      Expected type: Data.OpenUnion.Last (Fx1 : effs) x
        Actual type: IO ()
    • In the expression: putStrLn "Fx2"
      In the first argument of ‘interpretM’, namely
        ‘(\ Fx2 -> putStrLn "Fx2")’
      In the second argument of ‘(.)’, namely
        ‘interpretM (\ Fx2 -> putStrLn "Fx2")’
    • Relevant bindings include
        runFx :: Eff (Fx2 : Fx1 : effs) a -> Eff effs a
          (bound at src/Main.hs:19:1)
   |
21 |   . interpretM (\Fx2 -> putStrLn "Fx2")
   |

[lexi-lambda]

I have pushed a fix for this problem, and I plan on releasing a new version with the fix shortly. However, I will note that it does not make your program work as-written, since removing the LastMember IO (Fx1 ': effs) now results in a different type error:

src/Main.hs:20:5: error:
    • Could not deduce (Monad m0) arising from a use of ‘interpretM’
      from the context: LastMember IO effs
        bound by the type signature for:
                   runFx :: LastMember IO effs =>
                            Eff (Fx2 : Fx1 : effs) a -> Eff effs a
        at src/Main.hs:(12,1)-(17,19)
      The type variable ‘m0’ is ambiguous
      These potential instances exist:
        instance Monad (Either e) -- Defined in ‘Data.Either’
        instance Monad (Eff effs)
          -- Defined in ‘Control.Monad.Freer.Internal’
        instance Monad IO -- Defined in ‘GHC.Base’
        ...plus four others
        ...plus 14 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the second argument of ‘(.)’, namely
        ‘interpretM (\ Fx2 -> putStrLn "Fx2")’
      In the expression:
        interpretM (\ Fx1 -> putStrLn "Fx1")
        . interpretM (\ Fx2 -> putStrLn "Fx2")
      In an equation for ‘runFx’:
          runFx
            = interpretM (\ Fx1 -> putStrLn "Fx1")
              . interpretM (\ Fx2 -> putStrLn "Fx2")

src/Main.hs:20:25: error:
    • Couldn't match type ‘m0’ with ‘IO’
        ‘m0’ is untouchable
          inside the constraints: x ~ ()
          bound by a pattern with constructor: Fx2 :: Fx2 (),
                   in a lambda abstraction
          at src/Main.hs:20:18-20
      Expected type: m0 x
        Actual type: IO ()
    • In the expression: putStrLn "Fx2"
      In the first argument of ‘interpretM’, namely
        ‘(\ Fx2 -> putStrLn "Fx2")’
      In the second argument of ‘(.)’, namely
        ‘interpretM (\ Fx2 -> putStrLn "Fx2")’

I’m not entirely sure why this happens, since it’s unclear to me why the local constraint x ~ () makes m0 untouchable. It’s especially odd to me that it only occurs in the second use of interpretM, not the first.

It can be solved by adding a type annotation:

runFx :: forall effs a
      .  ( LastMember IO effs )
      => Eff (Fx2 ': Fx1 ': effs) a
      -> Eff effs a
runFx
  = interpretM (\Fx1 -> putStrLn "Fx1")
  . interpretM ((\Fx2 -> putStrLn "Fx2") :: Fx2 ~> IO)

…or with explicit type application:

runFx :: forall effs a
      .  ( LastMember IO effs )
      => Eff (Fx2 ': Fx1 ': effs) a
      -> Eff effs a
runFx
  = interpretM (\Fx1 -> putStrLn "Fx1")
  . interpretM @_ @IO (\Fx2 -> putStrLn "Fx2")

I may look into the actual reason for this secondary problem, but it seems separate, and it might have more to due with GHC’s inference mechanism than this library.

[rkanati]

Thanks!

Super strange - It definitely typechecks for me with the change I mentioned. Holler at me if you want any extra details for any reason.

[lexi-lambda]

I can’t reproduce your behavior, even on GHC 8.2.1 with your set of extensions. Perhaps you can set up a self-contained stack project that pins everything that produces the behavior you describe?

[rkanati]

I'll have a go in a few hours.

[lexi-lambda]

Many thanks!