#2256: Incompleteness of type inference: must quantify over implication
constraints
-------------------------+--------------------------------------------------
Reporter: simonpj | Owner: simonpj
Type: bug | Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler | Version: 6.8.2
Severity: normal | Keywords:
Difficulty: Unknown | Testcase:
Architecture: Unknown | Os: Unknown
-------------------------+--------------------------------------------------
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`.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2256>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
