| Simon Peyton-Jones asks for programs that are broken by the proposed | change. Here is a nearly real world one: You may not like this but this should work: Instead of | t1 = runST (trav f [1..10] (1,52) >>= \ (s::STRef s (Set Int)) -> seen s) try t1 = runST ( (trav f [1..10] (1,52) >>= \ s -> seen s) :: forall s. ST s [Int] ) or, equivalently t1 = runST run_it where run_it :: forall s. ST s Int run_it = trav f [1..10] (1,52) >>= \s -> seen s What's interesting about this example is that you aren't trying to bind the type variable 's'. You'd be quite happy to write \ (s :: STRef _ (Set Int)) -> seen s Note the wildcard "_". Arguably, one could loosen the rules in this case. This is an avenue that I have seen suggested before, but which I have, for one, not yet explored. Maybe others have better ideas. Simon