Type error in GHC-7 but not in GHC-6.12.3

[Simon Peyton-Jones]

| foo :: (forall s. ST s a) -> a
| foo st = ($) runST st

This is a motivating example for type inference that can deal with impredicative types.  Consider the type of ($):
	($) :: forall p q.  (p->q) -> p -> q
In the example we need to instantiate 'p' with (forall s. ST s a), and that's what impredicative polymorphism means: instantiating a type variable with a polymorphic type.

Sadly, I know of no system of reasonable complexity that can typecheck 'foo' unaided.  There are plenty of complicated systems, and I have been a co-author on papers on at least two, but they are all Too Jolly Complicated to live in GHC.  We did have an implementation of boxy types, but I took it out when implementing the new typechecker.  Nobody understood it.

However, people so often write
	runST $ do ...
that in GHC 7 I implemented a special typing rule, just for infix uses of ($).  Just think of
(f $ x) as a new syntactic form, with the obvious typing rule, and away you go.

It's very ad hoc, because it's absolutely specific to ($), and I'll take it out if you all hate it, but it's in GHC 7 for now.

Anyway, that's why you encountered the puzzling behaviour you describe below.

Simon

| -----Original Message-----
| From: Bas van Dijk [mailto:v.dijk.bas at gmail.com]
| Sent: 30 October 2010 21:14
| To: glasgow-haskell-users at haskell.org
| Cc: Simon Peyton-Jones
| Subject: Re: Type error in GHC-7 but not in GHC-6.12.3
| 
| On Sat, Oct 30, 2010 at 1:57 AM, Bas van Dijk <v.dijk.bas at gmail.com> wrote:
| > I could isolate it a bit more if you want.
| 
| And so I did. The following is another instance of the problem I'm
| having but set in a more familiar setting:
| 
| {-# LANGUAGE RankNTypes #-}
| 
| import Control.Monad.ST
| 
| foo :: (forall s. ST s a) -> a
| foo st = ($) runST st
| 
| Couldn't match expected type `forall s. ST s a'
|                 with actual type `ST s a'
|     In the second argument of `($)', namely `st'
| 
| Note that: 'foo st = runST st' type checks as expected.
| 
| Surprisingly 'foo st = runST $ st' also type checks!
| 
| I find the latter surprising because according to the report[1]: e1 op
| e2 = (op) e1 e2. So either both should type check or both should fail.
| 
| I guess that a RULE somewhere eliminates the ($) before the
| type-checker kicks in. I do find that a little strange because I
| thought RULES where applied after type checking.
| 
| Regards,
| 
| Bas
| 
| [1] http://www.haskell.org/onlinereport/exps.html#operators