Why does this function that uses a scoped type variable in a where clause not typecheck?

Question

I have a function that has a value defined in a where clause, and I want to give it an explicit type annotation. The annotation needs to use a type variable from the top-level function, so it was my understanding that I needed to use ScopedTypeVariables. Here is a minimal reduction of the problem:

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.Trans.Except
import Data.Functor.Identity

f :: ExceptT String Identity a -> Maybe a
f m = Nothing
  where x :: Identity (Either String a)
        x = runExceptT m

This code does not typecheck. It fails with the following error message:

Couldn't match type ‘a’ with ‘a1’
  ‘a’ is a rigid type variable bound by
      the type signature for f :: ExceptT String Identity a -> Maybe a
      at src/Lib.hs:20:6
  ‘a1’ is a rigid type variable bound by
       the type signature for x :: Identity (Either String a1)
       at src/Lib.hs:22:14
Expected type: ExceptT String Identity a1
  Actual type: ExceptT String Identity a
Relevant bindings include
  x :: Identity (Either String a1) (bound at src/Lib.hs:23:9)
  m :: ExceptT String Identity a (bound at src/Lib.hs:21:3)
  f :: ExceptT String Identity a -> Maybe a
    (bound at src/Lib.hs:21:1)
In the first argument of ‘runExceptT’, namely ‘m’
In the expression: runExceptT m

Why does this fail? I do not understand why this would cause problems—it seems like a textbook use of scoped type variables. For reference, I am using GHC 7.10.3.

Answer 1

You need an explicit forall:

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.Trans.Except
import Data.Functor.Identity

f :: forall a. ExceptT String Identity a -> Maybe a
f m = Nothing
  where x :: Identity (Either String a)
        x = runExceptT m

but why

That is a great question. This appears to be a rule of ScopedTypeVariables. We know in GHC Haskell that all top-level variables are implicitly forall'd, as documented here. One would suspect that the GHC devs added this behavior for backwards compatibility: without this rule, a file without the extension turned on could stop type-checking once the extension was turned on. We can easily imagine a scenario where helper functions declared in the where block to inadvertently reuse the common type variable names a, b, c, t, so on. It would be great if someone could find the exact spot in the GHC source code where this distinction between explicit and implicit forall'd variables arose.

update

Here we go (although this is all guesswork from the comments and grepping):

• While type-checking user signatures, the function tcUserTypeSig invokes findScopedTyVars. TcBinds.hs:ef44606:L1786

• findScopedTyVars in TcRnTypes filters for foralls by calling tcSplitForAllTys. TcRnTypes.hs:ef44606:L1221

• Which is a wrapper around splitForAllTys, which folds over a type's subtypes to build up a list of type variables introduced by foralls. Types/Type.hs:ef44606:L1361