I previously wrote:
The typechecker commits to the instance and adds to the current constraints TypeCast x Int, Ord Bool, Eq Bool The latter two are obviously satisfied and so discharged. The former leads to the substitution {x->Int}.
I should have been more precise and said: The former _eventually_ leads to the substitution {x->Int}. Your analysis is right on the mark. That's exactly how I think of TypeCast.
This is all very beautiful, but it's a little annoying that the cornerstone "silver bullet" TypeCast has to be defined in a way that fools the typechecker into doing the right thing in spite of itself.
One of the drafts of the HList paper, when describing TypeCast, literally had a phrase about `fooling the typechecker'... Well, it seems things like TypeCast were not envisioned by the Founding Fathers. In this respect, the story of C++ templates come to mind. My feeling is that we're still discovering the capabilities of the Haskell typechecker and the right abstractions. We should view TypeCast as an ungainly _encoding_ of a simple abstraction, or just as a tool for implementing type-level typecase and local improvement rules. When the right abstraction emerges (and perhaps it already has: CHR), GHC might implement it directly. Until then, we can use the encoding...