[Haskell-cafe] Why does disambiguation in RebindableSyntax sometimes requires type signatures?

[Jan Bracker]

Hello,

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".
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.

Here is my example program:

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import Prelude
import qualified Prelude as P
import qualified Control.Effect as E
import Control.Effect.State

ifThenElse :: Bool -> a -> a -> a
ifThenElse True  t e = t
ifThenElse False t e = e

main :: IO ()
main = do
  return ()
  where
    return = P.return

data Tree = Leaf Int
          | Branch Tree Tree

process :: Tree -> State '[ "flatten" :-> Bool :! 'R ] (Either Tree [Int])
process (Leaf i) = do
  flatten <- get (Var :: (Var "flatten"))
  if flatten
    then return $ Right [i]
    else return $ Left $ Leaf i
  where --(>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) ->
State (E.Plus State f g) b
        (>>=) = (E.>>=)
        (>>) :: (E.Inv State f g) => State f a -> State g b -> State
(E.Plus State f g) b
        (>>) = (E.>>)
        return = E.return
        fail = E.fail
process (Branch tl tr) = do
  eitherL <- process tl
  eitherR <- process tr
  case (eitherL, eitherR) of
    (Left  l, Left  r) -> return $ Left  $ Branch l r
    (Right l, Right r) -> return $ Right $ l ++ r
  where (>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) ->
State (E.Plus State f g) b
        (>>=) = (E.>>=)
        (>>) :: (E.Inv State f g) => State f a -> State g b -> State
(E.Plus State f g) b
        (>>) = (E.>>)
        return = E.return
        fail = E.fail

The program uses the "effect-monad" package in version 0.6.1.

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:

examples/effect/Test.hs:33:16:
    Could not deduce (E.Inv m0 f0 g0) arising from a use of ‘E.>>’
    Relevant bindings include
      (>>) :: m0 f0 a -> m0 g0 b -> m0 (E.Plus m0 f0 g0) b
        (bound at examples/effect/Test.hs:33:9)
    In the expression: (E.>>)
    In an equation for ‘>>’: (>>) = (E.>>)
    In an equation for ‘process’:
        process (Leaf i)
          = do { flatten <- get (Var :: Var "flatten");
                 if flatten then return $ Right [...] else return $ Left $
Leaf i }
          where
              (>>=) = (E.>>=)
              (>>) = (E.>>)
              return = E.return
              fail = E.fail

examples/effect/Test.hs:33:16:
    No instance for (E.Effect m0) arising from a use of ‘E.>>’
    In the expression: (E.>>)
    In an equation for ‘>>’: (>>) = (E.>>)
    In an equation for ‘process’:
        process (Leaf i)
          = do { flatten <- get (Var :: Var "flatten");
                 if flatten then return $ Right [...] else return $ Left $
Leaf i }
          where
              (>>=) = (E.>>=)
              (>>) = (E.>>)
              return = E.return
              fail = E.fail

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?

2) If I remove the type signature for the bind operation, I get the
following type error:

examples/effect/Test.hs:38:3:
    Couldn't match type ‘'["flatten" :-> (Bool :! 'R)]’ with ‘'[]’
    Expected type: State
                     '["flatten" :-> (Bool :! 'R)] (Either Tree [Int])
                   -> (Either Tree [Int] -> State '[] (Either Tree [Int]))
                   -> State '[] (Either Tree [Int])
      Actual type: State
                     '["flatten" :-> (Bool :! 'R)] (Either Tree [Int])
                   -> (Either Tree [Int] -> State '[] (Either Tree [Int]))
                   -> State
                        (E.Plus State '["flatten" :-> (Bool :! 'R)] '[])
                        (Either Tree [Int])
    In a stmt of a 'do' block: eitherR <- process tr
    In the expression:
      do { eitherL <- process tl;
           eitherR <- process tr;
           case (eitherL, eitherR) of {
             (Left l, Left r) -> return $ Left $ Branch l r
             (Right l, Right r) -> return $ Right $ l ++ r } }
    In an equation for ‘process’:
        process (Branch tl tr)
          = do { eitherL <- process tl;
                 eitherR <- process tr;
                 case (eitherL, eitherR) of {
                   (Left l, Left r) -> return $ Left $ Branch l r
                   (Right l, Right r) -> return $ Right $ l ++ r } }
          where
              (>>=) = (E.>>=)
              (>>) ::
                (E.Inv State f g) =>
                State f a -> State g b -> State (E.Plus State f g) b
              (>>) = (E.>>)
              return = E.return

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.

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?

I am working with GHC 7.10.2.

Best,
Jan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151027/4a471617/attachment.html>