Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

interpretM sometimes needs extra constraints #6

Closed
rkanati opened this issue Feb 20, 2018 · 5 comments
Closed

interpretM sometimes needs extra constraints #6

rkanati opened this issue Feb 20, 2018 · 5 comments

Comments

@rkanati
Copy link

rkanati commented Feb 20, 2018

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
Copy link
Owner

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
Copy link
Author

rkanati commented Feb 20, 2018

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
Copy link
Owner

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
Copy link
Author

rkanati commented Feb 20, 2018

I'll have a go in a few hours.

@lexi-lambda
Copy link
Owner

Many thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants