Why only inference in type checking?

[Simon Peyton-Jones]

| For actual arguments of f, there is no issue whatsoever with
| decidability. The type checker in my brain uses unification, i.e.
| top-down. The type checker in GHC uses inference, i.e. bottom-up. Why
| inference potentially suffers from non-termination for this program, I
| understand.

Actually GHC's type check uses checking when it knows the types, and inference only when it doesn't.

| My question is this: Is there a reason why type checking in GHC is
| inference-only, as opposed to a meet-in-the-middle combination of
| unification and inference?

It exactly does meet-in-the-middle.  Maybe you can elaborate your reasoning?

In any case, the restrictions on fundeps are needed for checking too. I believe.


Simon