| > 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
