Thank you Oleg! That explanation is very clear.
On 9/28/06, oleg@pobox.com
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}.
By the rules just enumerated, this substitution would be forbidden, since the type variable x is not considered variable, right? So this happens via the magic of functional dependencies? The typechecker encounters (eventually) the instance instance TypeCast'' () x x and since TypeCast'' is declared with a functional dependency: class TypeCast'' t x y | t x -> y, t y -> x it concludes that the first x in the above instance is uniquely determined by the second, which in our case is Int, and therefore x must be Int. Is that right? 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. Is this all part of the general "fundeps are very hard to get right" problem? Mike