Specifying the type of a function in a where clause

Question

I have the following Monad instance, based on the material in these slides:

{-# LANGUAGE InstanceSigs #-}

newtype Iter a = Iter { runIter :: Chunk -> Result a }

instance Monad Iter where
  return = Iter . Done
  (>>=) :: Iter a -> (a -> Iter b) -> Iter b
  (Iter iter0) >>= fiter = Iter $ \chunk -> continue (iter0 chunk)
    where continue :: Result a -> Result b
          continue (Done x rest)     = runIter (fiter x) rest
          continue (NeedInput iter1) = NeedInput (iter1 >>= fiter)
          continue (NeedIO ior)      = NeedIO (liftM continue ior)
          continue (Failed e)        = Failed e

This will give the following error:

• Couldn't match type ‘b’ with ‘b1’
  ‘b’ is a rigid type variable bound by
    the type signature for:
      (>>=) :: forall a b. Iter a -> (a -> Iter b) -> Iter b
    at Iteratee.hs:211:12
  ‘b1’ is a rigid type variable bound by
    the type signature for:
      continue :: forall a1 b1. Result a1 -> Result b1
    at Iteratee.hs:214:23
  Expected type: Result b1
    Actual type: Result b
• In the expression: runIter (fiter x) rest
  In an equation for ‘continue’:
      continue (Done x rest) = runIter (fiter x) rest
  In an equation for ‘>>=’:
      (Iter iter0) >>= fiter
        = Iter $ \ chunk -> continue (iter0 chunk)
        where
            continue :: Result a -> Result b
            continue (Done x rest) = runIter (fiter x) rest
            continue (NeedInput iter1) = NeedInput (iter1 >>= fiter)
            continue (NeedIO ior) = NeedIO (liftM continue ior)
            continue (Failed e) = Failed e
• Relevant bindings include
    continue :: Result a1 -> Result b1 (bound at Iteratee.hs:215:11)
    fiter :: a -> Iter b (bound at Iteratee.hs:212:20)
    (>>=) :: Iter a -> (a -> Iter b) -> Iter b
      (bound at Iteratee.hs:212:3)

To add to my confusion, if I leave continue undefined but I assign a type the code compiles.

My guess is that this problem is caused by continue actually having type

continue :: forall a1 b1. Result a1 -> Result b1

hence the two a's and b's from the types above are actually different. But nevertheless, continue above must have a type. My question is then, which is the type of this function assigned by the compiler when the types are omitted.

EDIT:

If the iter parameter is explicitly passed then the code compiles:

instance Monad Iter where
  return = Iter . Done
  (>>=) :: Iter a -> (a -> Iter b) -> Iter b
  (Iter iter0) >>= fiter0 = Iter $ \chunk -> continue fiter0 (iter0 chunk)
    where continue :: (a -> Iter b) -> Result a -> Result b
          continue fiter (Done x rest)     = runIter (fiter x) rest
          continue fiter (NeedInput iter1) = NeedInput (iter1 >>= fiter)
          continue fiter (NeedIO ior)      = NeedIO (liftM (continue fiter) ior)
          continue _ (Failed e)        = Failed e

However I'd like to avoid having to pass the parameter explicitly, while being able to give continue a type.

Answer 1

In basic Haskell, every type signature is implicitly quantified universally

foo :: Bool -> a -> a -> a
foo b x y = bar y
   where bar :: a -> a
         bar y | b         = x
               | otherwise = y 

actually means:

foo :: forall a. Bool -> a -> a -> a
foo b x y = bar y
   where bar :: forall a1. a1 -> a1
         bar y | b         = x
               | otherwise = y 

and fails to compile since x is not of type a1.

Removing the type signature of bar makes it compile, and the compiler will associate to bar the correct type a -> a where a is NOT quantified universally. Note that this is a type that the compiler can infer, but that the user is prevented to write.

This is rather inconvenient!

So, the ScopedTypeVarables GHC extension circumvents that, allowing one to write

foo :: forall a. Bool -> a -> a -> a
foo b x y = bar y
   where bar :: a -> a
         bar y | b         = x
               | otherwise = y 

and here the first forall a. makes a to be in scope in inner declarations. Further, the type of bar remains a -> a and is not universally quantified since a is now in scope. Hence, it compiles and the user was now able to write the wanted type annotation.