Commit ff752a1a authored by Simon Peyton Jones's avatar Simon Peyton Jones

tcCheckSatisfiability: less aggressive superclass expansion

In the pattern-match check we are looking for a proof of
*unsatisfiablity* among a bunch of givens.  The unsat-ness might be
hidden in the superclasses, so we must expand them.  But in the common
case where the constraints are satisfiable, we don't want to expand
a recursive superclass forever.

This is all a bit arbitrary, but then the whole question is
undecidable anyway.

The bug in Trac #10592 comment:12 was that I expanded superclasses
forever.  This patch fixes it.
parent 9d921d6b
......@@ -429,30 +429,47 @@ tcCheckSatisfiability given_ids
; (res, _ev_binds) <- runTcS $
do { traceTcS "checkSatisfiability {" (ppr given_ids)
; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
-- Need their superclasses, because (Int ~ Bool) has (Int ~~ Bool)
-- as a superclass, and it's the latter that is insoluble
-- See Note [Superclases and satisfiability]
; insols <- solveSimpleGivens given_cts
; insols <- try_harder insols
; traceTcS "checkSatisfiability }" (ppr insols)
; return (isEmptyBag insols) }
; return res }
where
where
try_harder :: Cts -> TcS Cts
-- Maybe we have to search up the superclass chain to find
-- an unsatisfiable constraint. Example: pmcheck/T3927b.
-- At the moment we try just once
try_harder insols
| not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
= return insols -- Hurrah -- stop now.
| otherwise
= do { pending_given <- getPendingScDicts
; new_given <- makeSuperClasses pending_given
; if null new_given -- No new superclasses to try, so no point
then return emptyBag -- in continuing
else -- Some new superclasses; have a go
do { insols <- solveSimpleGivens new_given
; try_harder insols } }
; solveSimpleGivens new_given }
{- Note [Superclases and satisfiability]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand superclasses before starting, because (Int ~ Bool), has
(Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
as a superclass, and it's the latter that is insoluble. See
Note [The equality types story] in TysPrim.
If we fail to prove unsatisfiability we (arbitrarily) try just once to
find superclasses, using try_harder. Reason: we might have a type
signature
f :: F op (Implements push) => ..
where F is a type function. This happened in Trac #3972.
We could do more than once but we'd have to have /some/ limit: in the
the recurisve case, we would go on forever in the common case where
the constraints /are/ satisfiable (Trac #10592 comment:12!).
For stratightforard situations without type functions the try_harder
step does nothing.
{- ********************************************************************************
***********************************************************************************
* *
* Inference
* *
......@@ -1010,16 +1027,21 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
simpl_loop :: Int -> IntWithInf -> Cts -> Bool
-> WantedConstraints
-> TcS WantedConstraints
simpl_loop n limit floated_eqs no_new_given_scs
simpl_loop n limit floated_eqs no_new_scs
wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
| isEmptyBag floated_eqs && no_new_scs
= return wc -- Done!
| n `intGtLimit` limit
= failTcS (hang (ptext (sLit "solveWanteds: too many iterations")
<+> parens (ptext (sLit "limit =") <+> ppr limit))
2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
, ppr wc ] ))
| isEmptyBag floated_eqs && no_new_given_scs
= return wc -- Done!
2 (vcat [ ptext (sLit "Unsolved:") <+> ppr wc
, ppUnless (isEmptyBag floated_eqs) $
ptext (sLit "Floated equalities:") <+> ppr floated_eqs
, ppUnless no_new_scs $
ptext (sLit "New superclasses found")
, ptext (sLit "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit")
]))
| otherwise
= do { traceTcS "simpl_loop, iteration" (int n)
......@@ -1064,7 +1086,7 @@ expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
else
do { new_given <- makeSuperClasses pending_given
; new_insols <- solveSimpleGivens new_given
; new_wanted <- makeSuperClasses pending_wanted
; new_wanted <- makeSuperClasses pending_wanted
; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
, wc_insol = insols `unionBags` new_insols }) } }
......
......@@ -65,6 +65,9 @@ push = Socket (Proxy :: Proxy Push) f
where
f :: Restrict op (Implements Push) => SockOp Push op -> Operation op
f SWrite = undefined
-- Seeing that this pattern match is exhaustive
-- requires a reasonably vigorous effort on given
-- superclass expansion.
pull :: Socket Pull
pull = Socket (Proxy :: Proxy Pull) f
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T10592 where
import Prelude (Bool(True,False),Integer,Ordering)
import qualified Prelude
--------------------
-- class hierarchy
class Boolean (Logic a) => Eq a where
type Logic a :: *
(==) :: a -> a -> Logic a
(/=) :: a -> a -> Logic a
a/=b = not (a==b)
class Eq a => POrd a where
inf :: a -> a -> a
class POrd a => MinBound a where
minBound :: a
class POrd a => Lattice a where
sup :: a -> a -> a
class (Lattice a, MinBound a) => Bounded a where
maxBound :: a
class Bounded a => Complemented a where
not :: a -> a
class Bounded a => Heyting a where
infixr 3 ==>
(==>) :: a -> a -> a
class (Complemented a, Heyting a) => Boolean a
(||) :: Boolean a => a -> a -> a
(||) = sup
(&&) :: Boolean a => a -> a -> a
(&&) = inf
--------------------
-- Bool instances
-- (these work fine)
instance Eq Bool where
type Logic Bool = Bool
(==) = (Prelude.==)
instance POrd Bool where
inf True True = True
inf _ _ = False
instance MinBound Bool where
minBound = False
instance Lattice Bool where
sup False False = False
sup _ _ = True
instance Bounded Bool where
maxBound = True
instance Complemented Bool where
not True = False
not False = True
instance Heyting Bool where
False ==> _ = True
True ==> a = a
instance Boolean Bool
--------------------
-- Integer instances
-- (these work fine)
instance Eq Integer where
type Logic Integer = Bool
(==) = (Prelude.==)
instance POrd Integer where
inf = Prelude.min
instance Lattice Integer where
sup = Prelude.max
--------------------
-- function instances
-- (these cause GHC to loop)
instance Eq b => Eq (a -> b) where
type Logic (a -> b) = a -> Logic b
f==g = \a -> f a == g a
instance POrd b => POrd (a -> b) where
inf f g = \a -> inf (f a) (g a)
instance MinBound b => MinBound (a -> b) where
minBound = \_ -> minBound
instance Lattice b => Lattice (a -> b) where
sup f g = \a -> sup (f a) (g a)
instance Bounded b => Bounded (a -> b) where
maxBound = \_ -> maxBound
instance Complemented b => Complemented (a -> b) where
not f = \a -> not (f a)
instance Heyting b => Heyting (a -> b) where
f ==> g = \a -> f a ==> g a
instance Boolean b => Boolean (a -> b)
......@@ -480,3 +480,4 @@ test('T10770b', expect_broken(10770), compile, [''])
test('T10935', normal, compile, [''])
test('T10971a', normal, compile, [''])
test('T11237', normal, compile, [''])
test('T10592', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment