Incompleteness of type inference: must quantify over implication constraints
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