> > But shouldn't the expected type and inferred type be reversed?
>
> Actually, no. The rationale (and implementation) is this:
> * the "expected type" describes the context
> * the "inferred type" describes the term
To adhere more closely to the POLA (principle of least astonishment),
perhaps we should change this to
* the "expected type" is the one supplied by the user, when
available,
* the "inferred type" is the one calculated by the type
inference algorithm.
This doesn't seem easy to implement, though; it looks like each type (and
subtype?) would have to be tagged as to whether it was inferred or supplied.
> class C p a where
> ci :: p a -> p a
>
> f :: (C p a) => (p a) -> (p a)
> f a = case ci a of
> [] -> a
>
>
> Here, the context of "ci a" is a case expression that has
> list-typed patterns. So we *infer* the type
> ci a :: p a1
> but the list context disagrees.
but the type error is referring to "a", not "ci a". What seems to have
happened is the type checker attempts to check "ci a" in the context [a],
then proceeds to check ci, inferring the type [a]->[a], then fails when
attempting to match the (supplied) type (p a) of "a" with [a].
In this case, we know that 'a' has a supplied type, because it is an
argument of the top-level function and a type signature was supplied. This
might be a useful approximation to make.
Cheers,
Simon
