Rebinding do notation for indexed monads

Question

I was following Conor McBride's "Kleisli arrows of outrageous fortune" paper and I've posted my implementation of his code here. Briefly, he defines the following types and classes:

type a :-> b = forall i . a i -> b i  class IFunctor f where imap :: (a :-> b) -> (f a :-> f b)  class (IFunctor m) => IMonad m where     skip :: a :-> m a     bind :: (a :-> m b) -> (m a :-> m b)  data (a := i) j where     V :: a -> (a := i) i 

Then he defines two types of binds, the latter of which uses (:=) to restrict the initial index:

-- Conor McBride's "demonic bind" (?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i (?>=) = flip bind  -- Conor McBride's "angelic bind"    (>>=) :: (IMonad m) => m (a := j) i -> (a -> m b j) -> m b i m >>= f = bind (\(V a) -> f a) m 

The latter bind works perfectly fine for rebinding do notation to use indexed monads with the RebindableSyntax extension, using the following corresponding definitions for return and fail:

return :: (IMonad m) => a -> m (a := i) i return = skip . V  fail :: String -> m a i fail = error 

... but the problem is that I cannot get the former bind (i.e. (?>=)) to work. I tried instead defining (>>=) and return to be:

(>>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i (>>=) = (?>=)  return :: (IMonad m) => a :-> m a return = skip 

Then I created a data type guaranteed to inhabit a specific index:

data Unit a where     Unit :: Unit () 

But when I try to rebind do notation using the new definitions for (>>=) and return, it does not work, as demonstrated in the following example:

-- Without do notation test1 = skip Unit >>= \Unit -> skip Unit  -- With do notation test2 = do     Unit <- skip Unit     skip Unit 

test1 type-checks, but test2 does not, which is weird, since I thought all that RebindableSyntax did was let do notation desugar test2 to test1, so if test1 type-checks, then why does not test2? The error I get is:

Couldn't match expected type `t0 -> t1'             with actual type `a0 :-> m0 b0' Expected type: m0 a0 i0 -> (t0 -> t1) -> m Unit ()   Actual type: m0 a0 i0 -> (a0 :-> m0 b0) -> m0 b0 i0 In a stmt of a 'do' block: Unit <- skip Unit In the expression:   do { Unit <- skip Unit;        skip Unit } 

The error remains even when I use the explicit forall syntax instead of the :-> type operator.

Now, I know there is another problem with using the "demonic bind", which is that you can't define (>>), but I still wanted to see how far I could go with it. Can anybody explain why I cannot get GHC to desugar the "demonic bind", even when it would normally type-check?

Answer 1

IIUC, the GHC desugarer actually runs after the typechecker (source). That explains why the situation you observe is theoretically possible. The typechecker probably has some special typing rules for the do-notation, and those may be inconsistent with what the typechecker would do with the desugarred code.

Of course, it's reasonable to expect them to be consistent, so I would recommend filing a GHC bug.