| > class Foo a b | a -> b | > instance Foo Int String | > bar :: Foo Int b => b | > bar = "rargh" | There is nothing wrong with this program. I have run into this | problem and I consider it to be a bug/weakness of the type checking | algorithm used by the implementation. | | (I also agree with you that the term "rigid variable" is rather | confusing because it is an artifact of the type checking algorithm | used by GHC.) Some brief comments a) I agree there is nothing wrong with this program, BUT it can't be translated into System F. That's why GHC rejects it. However, it *can* be translated into System FC (see "System F with type equality coercions", on my home page). But doing so requires a new implementation of type inference for functional dependencies, and I have not done that yet. b) While the program is arguably OK, I have yet to see a really convincing application that needs it. Why not write bar :: String? c) I really want to get rid of functional dependencies altogether, in favour of associated types. Thus class Foo a where type Bar a instance Foo Int where type Bar Int = String bar :: Foo a => Bar a bar = "rargh" This too requires work on type inference, and we're actively working on that. 4. The "rigid type variable" thing isn't just an implementation question. What *would* you like the error message to say when you write f :: ([a], Int) -> Int f (x:xs, y) = x+y Here we unify 'a' with Int, which is wrong. What would a nicer error message say? Simon