Re: [GHC] #2256: Incompleteness of type inference: must quantify over implication constraints
#2256: Incompleteness of type inference: must quantify over implication
constraints
-+--
Reporter: simonpj |Owner: simonpj
Type: bug | Status: new
Priority: low |Milestone: 7.0.1
Component: Compiler | Version: 6.8.2
Keywords:| Testcase:
Blockedby:| Difficulty: Unknown
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
-+--
Changes (by simonpj):
* failure: = None/Unknown
Comment:
OK, with the new typechecker the BUG WARNING problem has gone away.
However, when we are attempting to generalise a local binding (remember,
this isn't recommended; I'd prefer to have `-XMonoLocalBinds` on), there
is a fixable incompleteness in the algorithm. Specifically, suppose we
are generalising a let-binding with constraints `(Eq a, (forall b. Ord b
= ...a...b))`, and we want to generalise over `a`. Then
* When generalising, we call `simplifyAsMuchAsPossible`.
* This in turn fails if it can't eliminate all implication constraints.
So Iavor's example fails with
{{{
T2256.hs:4:27:
Could not deduce (Eq (f b c)) from the context (Eq c)
arising from a use of `sig'
}}}
* A slightly more generous plan would be [[BR]][[BR]]
* EITHER not to generalise over any variables mentioned in the
implication, and float it. In the example, don't generalise over `a`
after all.[[BR]][[BR]]
* OR to abstract over the quantified type variables constaints, and
float that, in the hope that some later unification will render it
soluble. In the example, generate the implication `(forall a. Eq a =
(forall b. Ord b = ...a...b...))`.
I'm not sure which is better, and it's very obscure anyway, so I don't
think it's high priority. I'm just making these notes while I think of
them.
Simon
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/2256#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #2256: Incompleteness of type inference: must quantify over implication constraints
#2256: Incompleteness of type inference: must quantify over implication constraints -+-- Reporter: simonpj |Owner: simonpj Type: bug | Status: new Priority: normal|Milestone: 6.12 branch Component: Compiler | Version: 6.8.2 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase:| Os: Unknown/Multiple Architecture: Unknown/Multiple | -+-- Changes (by igloo): * milestone: 6.10 branch = 6.12 branch -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/2256#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
[GHC] #2256: Incompleteness of type inference: must quantify over implication constraints
#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
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
