> I can't see why [Joe's "silly"] example should cause any problems.
> What happens is
> 1) The class defines a class G with method g
> (the default method does not have to be consulted to
> do this).
> 2) There is an instance saying that if (G a) holds then
> so does (G [a])
> 3) The default method is typechecked. G holds for x
> According to the instance we can then get (G [a]) so
> G holds for [x] as well, so the (recursive) call to
> g is ok.
>
> -- Lennart
>
Lennart is right, but so (in some sense) is Phil. Given that
g :: G a => a -> bool
is the global assumption, the natural typing of "g" in the definition
g x = g [x]
is (the additional context "G b" could be assumed but isn't needed)
g:: G [b] => b -> bool
where the occurrence of "g" on the *left* had side of "g x = g [x]" is a "new"
function, whereas the one on the *right* is an occurrence of the overloaded
function with the original signature. Now for the definition to work for the
instance "G [a]", the required type "G [a] => [a] -> bool" must be an instance
of the actual type "G [b] => b -> bool", which it isn't, *unless* we assume
the additional context "G [[a]]". This is why the declaration
instance G [a] => G a
should work (and does work in Gofer). The context "G [a]" used here can be
inferred from the definition and need not be explicitly given.
So why does
instance G a => G [a] where
work in hbc and ghc? It works because the context "G [b]" in the "natural"
typing for the definition of "g" is simplified (using the *explicit* instance
context) to "G b", and thus the typing reduces to
g:: G b => b -> bool
which is what is required. In other words, this is one of those pathological
cases mentioned in the 1.2 report (page R-32 in the Sigplan Notices version)
where the instance context cannot be inferred from the definition in a
reasonable way---it constitutes the missing base case for the inductive proof
that all list types are instances.
Satish
