RE: Why only inference in type checking?

| 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