{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

import Control.Exception

data Iterator i o m a where
   NeedInput  :: (i -> Iterator i o m a) -> Iterator i o m a
   HasOutput  ::  o -> Iterator i o m a  -> Iterator i o m a
   NeedAction ::  m   (Iterator i o m a) -> Iterator i o m a
   IsDone     ::  a                      -> Iterator i o m a
   Error      ::  SomeException          -> Iterator i o m a

feedPure :: [i] -> Iterator i o (forall m . m) a -> Iterator i o (forall m . m) a
feedPure = loop
  where
    loop []     iter = iter
    loop (i:is) (NeedInput k)    = loop is (k i)
    loop is     (HasOutput o k0) = HasOutput o (loop is k0)
    loop is     (NeedAction m)   = undefined
    loop _      (IsDone a)       = IsDone a
    loop _      (Error err)      = Error err

{-
impredicative.hs:14:34:
    Kind mis-match
    The third argument of `Iterator' should have kind `* -> *',
    but `m' has kind `*'
    In the type signature for `feedPure':
      feedPure :: [i]
                  -> Iterator i o (forall m. m) a -> Iterator i o (forall m. m) -}


feedPure' :: [i] -> Iterator i o (forall m . (m :: * -> *)) a -> Iterator i o (forall m . (m :: * -> *)) a
feedPure' = loop
  where
    loop []     iter = iter
    loop (i:is) (NeedInput k)    = loop is (k i)
    loop is     (HasOutput o k0) = HasOutput o (loop is k0)
    loop is     (NeedAction m)   = undefined
    loop _      (IsDone a)       = IsDone a
    loop _      (Error err)      = Error err

{-
impredicative.hs:34:46:
    `(m :: * -> *)' is not applied to enough type arguments
    Expected kind `*', but `(m :: * -> *)' has kind `* -> *'
    In the type signature for `feedPure'':
      feedPure' :: [i]
                   -> Iterator i o (forall m. (m :: * -> *)) a
                      -> Iterator i o (forall m. (m :: * -> *)) a
-}