РангNpolymorphism и kleisli стрелки возмутительного состояния

Question

Я не понимаю, почему определение demonbind1 дает некоторые ошибки компилятора. это выглядит как глупый флип, но как-то ..

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeOperators, TypeFamilies,ImpredicativeTypes #-} 

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) 


-- Conor McBride's "demonic bind" 
(?>=) :: forall m a b i. (IFunctor m, IMonad m) => m a i -> (a :-> m b) -> m b i 
(?>=) = 
    let 
    -- OK 
    demonbind0 = flip (bind :: forall i. (forall j. a j -> m b j) -> m a i -> m b i) 
    -- KO - see error below 
    demonbind1 = flip bind :: forall i. m a i -> (forall j. a j -> m b j) -> m b i 

    -- So i have to write this 
    demonbind2 :: forall i. (m a i -> (a :-> m b) -> m b i) 
    demonbind2 mai ti = (bind ti) mai 
    in demonbind2 

Ошибка

Couldn't match type ‘a j0 -> m b j0’ … 
       with ‘forall i2. a i2 -> m b i2’ 
    Expected type: (a j0 -> m b j0) -> m a i1 -> m b i1 
     Actual type: a :-> m b -> m a i1 -> m b i1 
In the first argument of ‘flip’, namely ‘bind’ 
    In the expression: 
     flip bind :: forall i. m a i -> (forall j. a j -> m b j) -> m b i 

Answer 1

Несколько удивительно, ImpredicativeTypes кажется менее сломанными, чем обычно на снимке развития GHC 8.0! Это компилируется без ошибок:

(?>=) :: (IFunctor m, IMonad m) => m a i -> (a :-> m b) -> m b i 
(?>=) = flip bind 

Интересно, какое изменение устранило проблему.