confusing type error

[Evan Laforge]

On Thu, Dec 4, 2014 at 12:59 PM, migmit <migmit at gmail.com> wrote:
> It tries to get `m Bool` by applying f1 to three arguments: 0, 0, and 'a'. Now, since `f2` has the type `Int -> Float -> n Bool`, where `n` is of kind `* -> *` (and an instance of `Monad` class, but it's not yet the time to look for instances), we have `f2 0 :: Float -> n Bool` and `f2 0 0 :: n Bool`. Since that is applied to 'a', Haskell deduces that the last type should be something like `Char -> Something` — or, equivalently, `(->) Char Something`. Therefore, it can see that `n` is in fact `(->) Char` and `Something` is `Bool`. Therefore, `f2 0 0 'a' :: Bool`. But it is expecting `m Bool`, not `Bool` — which is exactly what an error message says.

Right, that's what I suspected was happening.  The confusion arrises
because it guesses that 'm' should be (->), and that deduction then
leads to a dead-end.  But when it reports the problem, it uses its
guessed 'm', rather that backing up to the declared value.

But surely always backing up to the declared unspecialized value is no
good either, because then you get vague errors.  All the compiler
knows is that when it simplifies as far as it can, it winds up with a
/= b, it doesn't know that I would have been surprised by its path a
few steps back.

But arity errors are common, and intentionally instantiating a prefix
type constructor like 'm a' as (->) is probably much less common.  So
perhaps there could be a heuristic that treats (->) specially and
includes an extra clause in the error if it unified a type variable to
(->)?

I suspect the "expected n but got n" error is also due to the same
thing, it counts arrows on one side but inferred arrows on the other?
Or something?  In any case, it seems like the two sides are counting
inconsistently.