[Haskell-cafe] Re: Typeclass vs. Prolog programming

[Michael Shulman]

Thank you Oleg!  That explanation is very clear.

On 9/28/06, oleg at pobox.com <oleg at pobox.com> 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}.

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