Rank-2 polymorphism & type inference
Tue, 5 Dec 2000 09:18:18 -0800
Musing on Zhanyong's problem some more, a solution occurs to me.
Curiously, it's exactly the solution required for another useful
extension to type classes. Here is is, so people can shoot holes in it.
| In more detail, here's what happens. First we typecheck the RHS of
| f, deducing the types
| x :: a where a is fresh
| y :: k a where k is fresh
| y >> return x :: k a
| op (y >> return x) :: Bool with constraint C (k a)
| \x -> op (y >> return x) :: a -> Bool with constraint C (k a)
| Now we try to generalise over a. We need to discharge the contraint
| C (k a). Later we will find that y::[Int], so k=, but we
| don't know that yet. So we can't solve the constraint.
One bad solution I thought of was to give f the type
f :: forall a. C (k a) => a -> Bool
This is bad because it's not the type signature the programmer
specified. (It's also bad operationally because we'll pass a
dictionary at runtime, which isn't necessary.)
The good solution is to say this:
\x -> op (y >> return x) :: a -> Bool
with constraint C (k a)
(just as before)
/\a \x -> op (y>>return x) :: forall a. a -> Bool
with constraint (forall a. C (k a))
This requires us to permit constraints with for-alls in them.
As luck would have it, Ralf Hinze and I propose just such a thing in
our paper "Derivable Type Classes" (Section 7)
The motivation there is this: how can you write an equality instance for
data T k a = MkT (k (T k a))
We can try:
instance ... => Eq (T k a) where
(MkT a) == (MkT b) = a == b
But what is the "..."? We need that "k" is an equality type
constructor. The right context is
instance (forall a. Eq a => Eq (k a)) => Eq (T k a) where
Aha! A constraint with a for-all.
There are some more details in the paper.
So perhaps there's a reason for adding this extension in the implementation
(to solve Zhanyong's problem) even for a Haskell 98 compiler.