[Haskell-cafe] MPTCs and rigid variables
simonpj at microsoft.com
Mon Mar 5 21:29:56 EST 2007
| > 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?
More information about the Haskell-Cafe