Question about "result type signatures" example in old GHC docs

Largely out of curiosity, I’ve been digging through old GHC documentation lately. There is an old feature called “result type signatures” that appeared in GHC 4.02 and disappeared in GHC 6.6. There is an example of this feature that appears in two sources:

The example is:

f :: Int -> [a] -> [a]
f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
                      in \xs -> map g (reverse xs `zip` xs)

It seems to me that this example is erroneous, but I find that difficult to believe, given its presence in both the paper and in many versions of the GHC user’s manual. The easier explanation would be that I am misunderstanding the old semantics of scoped type variables, in which case I would like to know where I’ve gone wrong.

There are two major differences, as far as I can tell, between the modern scoped type variables I am used to, and the scoped type variables of the early aughts. The first is, of course, result type signatures, which is the feature being demonstrated here. The second is the more subtle change to scoped type variables that took placed in GHC 6.6:

A scoped type variable stands for a type variable, and not for a type. (This is a change from GHC’s earlier design.) Furthermore, distinct lexical type variables stand for distinct type variables. This means that every programmer-written type signature (includin one that contains free scoped type variables) denotes a rigid type; that is, the type is fully known to the type checker, and no inference is involved. – Scoped type variables, GHC 6.6

My complaint with the code example is that the type of f, as far as I can tell without having a sufficiently old compiler at my disposal, is actually:

f :: forall a. Int -> [a] -> [(a, a)]

To demonstrate, the following roughly comparable code passes a type check by GHC 8.6.5:

{-# LANGUAGE ScopedTypeVariables #-}

f :: forall a. Int -> [a] -> [(a, a)]
f _n = let g (x :: a, y :: a) = (y, x)
       in \xs -> map g (reverse xs `zip` xs)

I think I am able to wrap my head around the idea that, since the type variable a is wobbly prior to GHC 6.6, then [a] -> [a] is simply a less-specific expression of what is ultimately inferred as something else, such as [(a, a)] -> [(a, a)]. As the paper says (emphasis mine):

The type annotation […] claims that the right hand side of f has type [t] -> [t] for some type t […]

Emphasis on “some” (not “all”) because a is not implicitly universally quantified as it would be today. But there does not exist, as far as I can tell, any t such that [t] -> [t] unifies with [a] -> [(a, a)].

So how could this example have ever passed a type checker?

3 Likes

Maybe, this will have more chances to get feedback if cross-posted on the ghc-dev mailing list. I’m also curious about the question.

1 Like