As to your original code, the only actual bug is that someA :: a is wrong. The actual type of someA is someA :: C a => a, so you could have written
class C a where
someA :: a
f :: C a => a -> Int
f a =
let x :: C a => a
x = someA -- absolutely works
in 0
But remember that in x, 'a' is not the same as the 'a' in f, so you might as well have written this
f :: C a => a -> Int
f a =
let x :: C b => b
x = someA -- also works
in 0
This is how it works. When you write
f :: C a => a -> ()
f =
let x = someA -- without ':: a'
()
The problem is that by not giving an explicit type to x, ghc infers a type and for all intents and purposes it is as though you wrote
f :: C a => a -> ()
f =
let x :: C a1 => a1
x = someA
-- also if you had written x = some :: a, it just means you effectively wrote
-- let x :: C a1 => a1
-- x = someA :: a
-- but 'a1' is not equivalent to 'a', so it errors.
()
And so it says hey wait, a and a1 could be different types. That is why you often see ghc referring to 'a1' or 'a0' in error messages, because when it infers a type it has to give a name to it in order to report on it.
What ScopedTypeVariables does is allow you to specify that for the entire scope of this forall, 'a' in any type signature always refers to the same type.
f :: forall a. C a => a -> ()
f = undefined
where
some :: a -- this is guaranteed to be the a from above.
some = undefined
somethingelse :: forall a. a -- this is a different a
somethingelse = undefined
some :: a -- this toplevel a is of course also different.
some = undefined
So you could just go
{-# LANGUAGE ScopedTypeVariables #-}
f :: forall a. C a => a -> Int
f a =
let
x :: a -- now the a is the same a as above, so the constraint C a is understood.
x = someA
in 0
I really love the ScopedTypeVariables extension, and so do a lot of other people. I honestly think it should be on by default because the pitfalls of not having it on are a lot worse than the pitfalls of having it on. The only pitfall I know of to having it on is that if you have a function with tons of lets and / or wheres, you might not notice you had used the type variable 'a' in two different incompatible places.
Hopefully all this makes sense.