In the following example I'm internally implementing the function f
. Its signature is using a
as if the type variable a
is scoped, and it is working without giving me a compile error even though I haven't enabled the extension ScopedTypeVariables
:
foo :: Int -> [a] -> [a]
foo n list = snd $ foldl f (1,[]) list where
f :: (Int,[a]) -> a -> (Int,[a])
f (k,l) r
| k==n = (1,l++[r])
| otherwise = (k+1,l)
I was expecting the error: "Couldn't match type ‘a1’ with ‘a’ ...."
because, as I said, I was treating the type variable a
as if it's scoped even though it is not scoped.
I know what a rigid type is, and I already know why the error appears. My question is why I'm not getting the error here.
The function
is general enough to type check on its own (assuming
n::Int
). The typea
here can indeed be any type -- there's no need to assume thata
is the samea
as the one in the signature offoo
, so no error is generated.Put in different terms, we could rename
a
intob
without any harm:Here's a simpler example to stress the point. This compiles without errors:
By contrast, changing the last line to
f y = x
would immediately trigger the error sincex
has type "thea
in the signature offoo
", not "thea
in the signature off
", and the two type variables can't be unified since they are both rigid.