<div dir="ltr">Hello,<div><br></div><div>I am currently playing around with RebindableSyntax and having several bind/return/sequence functions in scope at the same time. I thought that it would be enough to just pick the right one to use in each do-block by using a "where" or a "let".</div><div>Surprisingly, I get some type related issues I can only fix by adding in some type signatures, but I don't understand why these signatures are actually necessary.</div><div><br></div><div>Here is my example program:</div><div><div><br></div><div>{-# LANGUAGE RebindableSyntax #-}</div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE TypeOperators #-}</div><div><br></div><div>import Prelude</div><div>import qualified Prelude as P</div><div>import qualified Control.Effect as E</div><div>import Control.Effect.State</div><div><br></div><div>ifThenElse :: Bool -> a -> a -> a</div><div>ifThenElse True  t e = t</div><div>ifThenElse False t e = e</div><div><br></div><div>main :: IO ()</div><div>main = do</div><div>  return ()</div><div>  where</div><div>    return = P.return</div><div><br></div><div>data Tree = Leaf Int</div><div>          | Branch Tree Tree</div><div><br></div><div>process :: Tree -> State '[ "flatten" :-> Bool :! 'R ] (Either Tree [Int])</div><div>process (Leaf i) = do</div><div>  flatten <- get (Var :: (Var "flatten"))</div><div>  if flatten</div><div>    then return $ Right [i]</div><div>    else return $ Left $ Leaf i</div><div>  where --(>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) -> State (E.Plus State f g) b</div><div>        (>>=) = (E.>>=)</div><div>        (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b</div><div>        (>>) = (E.>>)</div><div>        return = E.return</div><div>        fail = E.fail</div><div>process (Branch tl tr) = do</div><div>  eitherL <- process tl</div><div>  eitherR <- process tr</div><div>  case (eitherL, eitherR) of</div><div>    (Left  l, Left  r) -> return $ Left  $ Branch l r</div><div>    (Right l, Right r) -> return $ Right $ l ++ r</div><div>  where (>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) -> State (E.Plus State f g) b</div><div>        (>>=) = (E.>>=)</div><div>        (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b</div><div>        (>>) = (E.>>)</div><div>        return = E.return</div><div>        fail = E.fail</div></div><div><br></div><div>The program uses the "effect-monad" package in version 0.6.1.</div><div><br></div><div>1) The type signatures in the "where" following each do-block of the "process" function are required. If I remove the type signature of the sequence functions I get a type error of the following nature:</div><div><br></div><div><div>examples/effect/Test.hs:33:16:</div><div>    Could not deduce (E.Inv m0 f0 g0) arising from a use of ‘E.>>’</div><div>    Relevant bindings include</div><div>      (>>) :: m0 f0 a -> m0 g0 b -> m0 (E.Plus m0 f0 g0) b</div><div>        (bound at examples/effect/Test.hs:33:9)</div><div>    In the expression: (E.>>)</div><div>    In an equation for ‘>>’: (>>) = (E.>>)</div><div>    In an equation for ‘process’:</div><div>        process (Leaf i)</div><div>          = do { flatten <- get (Var :: Var "flatten");</div><div>                 if flatten then return $ Right [...] else return $ Left $ Leaf i }</div><div>          where</div><div>              (>>=) = (E.>>=)</div><div>              (>>) = (E.>>)</div><div>              return = E.return</div><div>              fail = E.fail</div><div><br></div><div>examples/effect/Test.hs:33:16:</div><div>    No instance for (E.Effect m0) arising from a use of ‘E.>>’</div><div>    In the expression: (E.>>)</div><div>    In an equation for ‘>>’: (>>) = (E.>>)</div><div>    In an equation for ‘process’:</div><div>        process (Leaf i)</div><div>          = do { flatten <- get (Var :: Var "flatten");</div><div>                 if flatten then return $ Right [...] else return $ Left $ Leaf i }</div><div>          where</div><div>              (>>=) = (E.>>=)</div><div>              (>>) = (E.>>)</div><div>              return = E.return</div><div>              fail = E.fail</div></div><div><br></div><div>Which I interpret as the inability to infer the "E.Effect" and "E.Inv" constraints that are implied by the use of "E.>>". But why can't those constraints be inferred correctly? Shouldn't a definition like "(>>) = (E.>>)" just propagate the type signature and specialize it as needed?</div><div><br></div><div>2) If I remove the type signature for the bind operation, I get the following type error:</div><div><br></div><div><div>examples/effect/Test.hs:38:3:</div><div>    Couldn't match type ‘'["flatten" :-> (Bool :! 'R)]’ with ‘'[]’</div><div>    Expected type: State</div><div>                     '["flatten" :-> (Bool :! 'R)] (Either Tree [Int])</div><div>                   -> (Either Tree [Int] -> State '[] (Either Tree [Int]))</div><div>                   -> State '[] (Either Tree [Int])</div><div>      Actual type: State</div><div>                     '["flatten" :-> (Bool :! 'R)] (Either Tree [Int])</div><div>                   -> (Either Tree [Int] -> State '[] (Either Tree [Int]))</div><div>                   -> State</div><div>                        (E.Plus State '["flatten" :-> (Bool :! 'R)] '[])</div><div>                        (Either Tree [Int])</div><div>    In a stmt of a 'do' block: eitherR <- process tr</div><div>    In the expression:</div><div>      do { eitherL <- process tl;</div><div>           eitherR <- process tr;</div><div>           case (eitherL, eitherR) of {</div><div>             (Left l, Left r) -> return $ Left $ Branch l r</div><div>             (Right l, Right r) -> return $ Right $ l ++ r } }</div><div>    In an equation for ‘process’:</div><div>        process (Branch tl tr)</div><div>          = do { eitherL <- process tl;</div><div>                 eitherR <- process tr;</div><div>                 case (eitherL, eitherR) of {</div><div>                   (Left l, Left r) -> return $ Left $ Branch l r</div><div>                   (Right l, Right r) -> return $ Right $ l ++ r } }</div><div>          where</div><div>              (>>=) = (E.>>=)</div><div>              (>>) ::</div><div>                (E.Inv State f g) =></div><div>                State f a -> State g b -> State (E.Plus State f g) b</div><div>              (>>) = (E.>>)</div><div>              return = E.return</div></div><div><br></div><div>Which tells me that GHC is expecting the wrong type, but inferring the correct type. Again I don't see why this wrong type is expected and the right type is ignored.</div><div><br></div><div>In either case, why does adding or removing the type signature for the local definitions make a difference at all? I suspect the issue has to do with the language extensions I enabled or the type-level computations that are done by the "effect-monad" package, but I cannot find a satisfying answer. Does anybody have a good explanation?</div><div><br></div><div>I am working with GHC 7.10.2.</div><div><br></div><div>Best,</div><div>Jan</div><div><br></div></div>