Type annotation in a typeclass' default value causes a "could not deduce" type error

Question

This is a beginner's question, but I cannot recognize any answer to it anywhere.
The following code:

class A a where
  foo :: a
class A a => B a where
  bar :: a
  bar = (foo :: a)

fails to compile in GHC, with the error message:

Could not deduce (A a1) arising from a use of `foo'
from the context (B a)
  bound by the class declaration for `B'
...

GHC seems unconvinced that all the a's in the definition of typeclass B are the same. Can anyone please explain what exactly its line of reasoning is?

Removing the type annotation in line 5 avoids the problem of course, but I would still like to understand what is going on here...

Answer 1

You should indeed get rid of the type annotation. Type variables are not scoped in Haskell, so (foo :: a). Is interpreted as "have foo produce a value of type a for any type a", which cannot be done as foo will only produce values of those types a that are in the class A.

Put differently, your declaration of B is equivalent to

class A a => B a where
  bar :: a
  bar = (foo :: c)

That is, there is no connection between your use of the type variable a and the other uses in the declaration.

Dropping the explicit annotation solves your issue:

class A a => B a where
  bar :: a
  bar = foo

Now, the compiler can figure out for what type you want to invoke foo, i.e., for the type a that you wrote in the signature of bar and that appears in the head of the class declaration.

The Glasgow Haskell Compiler (GHC) comes with an extension that allows for scoped type variables. With that extension enabled, your fragment is type checked like you originally expected:

{-# LANGUAGE ScopedTypeVariables #-}
class A a where
  foo :: a
class A a => B a where
  bar :: a
  bar = (foo :: a)