Scoped type variables require explicit foralls. Why?

Question

If you want to use GHC's lexically scoped type variables, you also have to use explicit universal quantification. That is, you have to add forall declarations to your functions' type signatures:

{-# LANGUAGE ExplicitForAll, ScopedTypeVariables #-}  f :: forall a . [a] -> [a]      -- The `forall` is required here ... f (x:xs) = xs ++ [x :: a]       -- ... to relate this `a` to the ones above. 

Does this actually have anything to do with quantification, or did the extension writers just coopt the forall keyword as a convenient marker for where the new, wider scoping applies?

In other words, why can't we leave out the forall as usual? Wouldn't it be clear that type variables in annotations within the function body refer to variables of the same name in the function signature? Or would the typing be somehow problematic or ambiguous?

Answer 1

Yes, the quantifier is meaningful and is required for the types to make sense.

First note that there's really no such thing as an "unquantified" type signature in Haskell. Signatures without a forall are really implicitly quantified. This code ...

f :: [a] -> [a]                         -- No `forall` here ... f (x:xs) = xs ++ [x :: a]               -- ... or here. 

... really means this:

f :: forall a . [a] -> [a]              -- With a `forall` here ... f (x:xs) = xs ++ [x :: forall a . a]    -- ... and another one here. 

So let's figure out what this says. The important thing is to notice that the type variables named a in the signatures for f and for x are bound by separate quantifiers. This means that they are different variables, despite sharing a name. So the above code is equivalent to this:

f :: forall a . [a] -> [a] f (x:xs) = xs ++ [x :: forall b . b]    -- I've changed `a` to `b` 

With the names differentiated, it's now clear not only that the type variables in the signatures for f and x are unrelated, but that the signature for x claims that x can have any type. But this is impossible, since x must have the particular type bound to a when f is applied to an argument. And indeed the type-checker rejects this code.

On the other hand, with a single forall in the signature for f ...

f :: forall a . [a] -> [a]              -- A `forall` here ... f (x:xs) = xs ++ [x :: a]               -- ... but not here. 

... the a in the signature on x is bound by the quantifier at the beginning of f's type signature, so this a represents the same type as the type represented by the variables called a in f's signature.