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.