How is the type of `([] ==) []` inferred haskell?

16
votes

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)

2
haskelltypestype-inferencetype-systems
With GHC (not GHCi) I've got Ambiguous type variable `a' in the constraint `Eq a' arising from a use of `==' – kennytm
@Kenny - yes thats what I expected before I tried in ghci - the greater my surprise. Thanks for the hint, now my world order is restored :) – Ingo
It's interesting Hugs gives the expression [] == [] type Eq a => Bool. – sdcvvc
Sorry for "necroposting", but there is no way to specify the context for [] == [] is there? Without specializing [] themselves. – Dan M.

2 Answers

19
votes

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...

1
votes

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.