Ticket #2256 (new bug)

Description

Consider this program (from Iavor)

f x = let g y = let h :: Eq c => c -> ()
                    h z = sig x y z
                in ()
      in fst x

sig :: Eq (f b c) => f () () -> b -> c -> ()
sig _ _ _ = ()

This example is rejected by both Hugs and GHC but I think that it is a well typed program. The Right Type to infer for g is this:

g :: forall b. (forall c. Eq c => Eq (b,c)) => b -> ()

but GHC never quantifies over implication constraints at the moment. As a result, type inference is incomplete (although in practice no one notices). I knew about this, but I don't think it's recorded in Trac, hence this ticket.

Following this example through also led me to notice a lurking bug: see "BUG WARNING" around line 715 of TcSimplify.