Why only inference in type checking?
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
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