Martin Sulzmann
- There's a class of MPTC/FD programs which enjoy sound, complete and decidable type inference. See Result 1 below. I believe that hugs and ghc faithfully implement this class. Unfortunately, for advanced type class acrobats this class of programs is too restrictive.
Not just them: monad transformers also fall foul of these restrictions. The restrictions can be relaxed to accomodate them (as you do with the Zip class), but the rules become more complicated.
Result2: Assuming we can guarantee termination, then type inference is complete if we can satisfy - the Bound Variable Condition, - the Weak Coverage Condition, - the Consistency Condition, and - and FDs are full. Effectively, the above says that type inference is sound, complete but semi-decidable. That is, we're complete if each each inference goal terminates.
I think that this is a little stronger than Theorem 2 from the paper, which assumes that the CHR derived from the instances is terminating. If termination is obtained via a depth limit (as in hugs -98 and ghc -fallow-undecidable-instances), it is conceivable that for a particular goal, one strategy might run into the limit and fail, while a different strategy might reach success in fewer steps.