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

Learn
#1

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
#2

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.

2 Likes
#3

That feature never got taken out of Hugs – you can still try it. And trying your example indeed gives

ERROR - Type error in result type
*** Term           : let {...} in (\xs -> map g (zip (reverse xs) xs))
*** Type           : [a] -> [(a,a)]
*** Does not match : [a] -> [a]
*** Because        : unification would give infinite type

I believe there’s a proposal to put ‘result type signatures’ back into GHC. Ah yes: accepted nearly a year ago. You could check with @int-index where it’s got to.

#4

BTW ResultSignatures is an avoidable feature/you can always put the signature after the RHS:

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

Note I’ve put ( ) round the RHS, to make sure the signature scopes over the lot. I’ve used tyvar aa to keep the PatternSignatures distinct from the top-level signature. (If you’ve got ScopedTypeVariables switched on there’s danger of variable capture.)