Dear All, A while ago, I had trouble understanding the coverage condition and I raised a question on this mailing list. Help was swift and adequate, especially the reference to the paper entitled "Understanding Functional Dependencies via Constraint Handling Rules" was very useful. However, having considered the problem of non-termination of the type checker, I can't help but wonder why the type checker is "inference only." From the paper mentioned above, consider the following example: class Mul a b c | a b -> c where (*) :: a -> b -> c type Vec b = [b] instance Mul a b c => Mul a (Vec b) (Vec c) where ... f b x y = if b then (*) x [y] else y 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. 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? Would the type checker use both unification and inference (let's say alternating evaluation of both), the number of programs for which termination can be guaranteed is considerably larger - if I'm not mistaken, but I may very well have gotten it wrong. Regards, Philip PS. I realize that for this dependent typing scenario is useless once Type Families are here. I can't wait for a GHC with TFs. I raise this question, simply to understand why inference was chosen exclusively.