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 TcSimplify
.
Trac metadata
Trac field | Value |
---|---|
Version | 6.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | Unknown |
Architecture | Unknown |