Why only inference in type checking?

Simon Peyton-Jones simonpj at microsoft.com
Thu Oct 18 10:13:48 EDT 2007

| 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.


More information about the Glasgow-haskell-users mailing list