I don’t think it’s all that complicated or fragile. To resolve the constraint (C T1 T2), use the appropriate instance declaration to express it in terms of (hopefully simpler) constraints. Keep doing that. If you terminate, GHC should. Example: to resolve Eq [Int], use the instance declaration instance Eq a => Eq [a] That gives rise to the new constraint Eq Int. Use the instance declaration instance Eq Int That gives rise to no new instances. Done. If you terminate and GHC does not, write down your reasoning (ie how you resolved the instance) and send it in. [NB: There is a wrinkle for “recursive dictionaries”, described in the SYB3 paper.] Simon Well, the reasoning for the "devil" camp (which I admit to being firmly in[1]) is that such proofs must rely on the algorithm the compiler uses to resolve instances. You might be able to prove it, but the proof is necessarily only valid for (possibly current versions of) GHC. The typeclass resolution algorithm is not in the report, and there are several conceivable ways of of going about it.