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)
http://research.microsoft.com/~simonpj/#derive

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
          ...as before...

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.

Simon

_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to