| 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@gmail.com] | Sent: 30 October 2010 21:14 | To: glasgow-haskell-users@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 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