(type theoretical) How is ([] ==) [] typed in haskell?
- by Ingo
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].
