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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
