[Haskell-cafe] MPTCs and rigid variables

[Simon Peyton-Jones]

| > 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