(type theoretical) How is ([] ==) [] typed in haskell?

Question

It sounds silly, but I can't get it. Why can the expression [] == [] be typed at all? More specifically, which type (in class Eq) is inferred to the type of list elements?

In a ghci session, I see the following:

Prelude> :t (==[])
(==[]) :: (Eq [a]) => [a] -> Bool

But the constraint Eq [a] implies Eq a also, as is shown here:

Prelude> (==[]) ([]::[IO ()])

<interactive>:1:1:
No instance for (Eq (IO ()))
  arising from use of `==' at <interactive>:1:1-2
Probable fix: add an instance declaration for (Eq (IO ()))
In the definition of `it': it = (== []) ([] :: [IO ()])

Thus, in []==[], the type checker must assume that the list element is some type a that is in class Eq. But which one? The type of [] is just [a], and this is certainly more general than Eq a => [a].

IMHO this should by ambiguous, at least in Haskell 98 (which is what we are talking about)

Answer 1

GHC infers the most general type:

(==[]) :: (Eq a) => [a] -> Bool

It should be read as:

• if you have an instance of Eq a,
• then Haskell can give you a function from lists of those 'a's to Bool

So yes, the implication here is that you have an instance of Eq for elements of the list, and GHC already has an instance for lists in general (relying on Eq for the elements), so we get a nice general type.

The type checker "assumes" you can supply an Eq a instance when called at a particular type.

I can't reproduce your results of having a Eq [a] constraint.

Answer 2

GHCi has extended rules for type defaulting, which is what tripped you up. In this case, I believe it would default the ambiguous type to (). The subtle ways that GHCi behaves differently are nice for the sake of better interactivity, but they do occasionally result in confusion...