Commit 32eb4199 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Instances in no-evidence implications

Trac #15290 showed that it's possible that we might attempt to use a
quantified constraint to solve an equality in a situation where we
don't have anywhere to put the evidence bindings.  This made GHC crash.

This patch stops the crash, but still rejects the pogram.  See
Note [Instances in no-evidence implications] in TcInteract.

Finding this bug revealed another lurking bug:

* An infelicity in the treatment of superclasses -- we were expanding
  them locally at the leaves, rather than at their binding site; see
  (3a) in Note [The superclass story].

  As a consequence, TcRnTypes.superclassesMightHelp must look inside
  implications.

In more detail:

* Stop the crash, by making TcInteract.chooseInstance test for
  the no-evidence-bindings case.  In that case we simply don't
  use the instance.  This entailed a slight change to the type
  of chooseInstance.

* Make TcSMonad.getPendingScDicts (now renamed getPendingGivenScs)
  return only Givens from the /current level/; and make
  TcRnTypes.superClassesMightHelp look inside implications.

* Refactor the simpl_loop and superclass-expansion stuff in
  TcSimplify.  The logic is much easier to understand now, and
  has less duplication.
parent 50a35e59
......@@ -289,6 +289,15 @@ So here's the plan:
This may succeed in generating (a finite number of) extra Givens,
and extra Deriveds. Both may help the proof.
3a An important wrinkle: only expand Givens from the current level.
Two reasons:
- We only want to expand it once, and that is best done at
the level it is bound, rather than repeatedly at the leaves
of the implication tree
- We may be inside a type where we can't create term-level
evidence anyway, so we can't superclass-expand, say,
(a ~ b) to get (a ~# b). This happened in Trac #15290.
4. Go round to (2) again. This loop (2,3,4) is implemented
in TcSimplify.simpl_loop.
......
......@@ -1840,7 +1840,7 @@ doTopReactOther work_item
= do { -- Try local quantified constraints
res <- matchLocalInst pred (ctEvLoc ev)
; case res of
OneInst {} -> chooseInstance ev pred res
OneInst {} -> chooseInstance work_item res
_ -> continueWith work_item }
where
ev = ctEvidence work_item
......@@ -2235,7 +2235,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
OneInst { lir_safe_over = s }
-> do { unless s $ insertSafeOverlapFailureTcS work_item
; when (isWanted ev) $ addSolvedDict ev cls xis
; chooseInstance ev dict_pred lkup_res }
; chooseInstance work_item lkup_res }
_ -> -- NoInstance or NotSure
do { when (isImprovable ev) $
try_fundep_improvement
......@@ -2264,9 +2264,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
chooseInstance :: CtEvidence -> TcPredType -> LookupInstResult
-> TcS (StopOrContinue Ct)
chooseInstance ev pred
chooseInstance :: Ct -> LookupInstResult -> TcS (StopOrContinue Ct)
chooseInstance work_item
(OneInst { lir_new_theta = theta
, lir_mk_ev = mk_ev })
= do { traceTcS "doTopReact/found instance for" $ ppr ev
......@@ -2274,9 +2273,11 @@ chooseInstance ev pred
; if isDerived ev then finish_derived theta
else finish_wanted theta mk_ev }
where
ev = ctEvidence work_item
pred = ctEvPred ev
loc = ctEvLoc ev
deeper_loc = zap_origin (bumpCtLocDepth loc)
origin = ctLocOrigin loc
deeper_loc = zap_origin (bumpCtLocDepth loc)
zap_origin loc -- After applying an instance we can set ScOrigin to
-- infinity, so that prohibitedSuperClassSolve never fires
......@@ -2289,10 +2290,15 @@ chooseInstance ev pred
-> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
-- Precondition: evidence term matches the predicate workItem
finish_wanted theta mk_ev
= do { evc_vars <- mapM (newWanted deeper_loc) theta
= do { evb <- getTcEvBindsVar
; if isNoEvBindsVar evb
then -- See Note [Instances in no-evidence implications]
continueWith work_item
else
do { evc_vars <- mapM (newWanted deeper_loc) theta
; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
; emitWorkNC (freshGoals evc_vars)
; stopWith ev "Dict/Top (solved wanted)" }
; stopWith ev "Dict/Top (solved wanted)" } }
finish_derived theta -- Use type-class instances for Deriveds, in the hope
= -- of generating some improvements
......@@ -2302,8 +2308,28 @@ chooseInstance ev pred
; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
; stopWith ev "Dict/Top (solved derived)" }
chooseInstance ev _ lookup_res
= pprPanic "chooseInstance" (ppr ev $$ ppr lookup_res)
chooseInstance work_item lookup_res
= pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
{- Note [Instances in no-evidence implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Trac #15290 we had
[G] forall p q. Coercible p q => Coercible (m p) (m q))
[W] forall <no-ev> a. m (Int, IntStateT m a)
~R#
m (Int, StateT Int m a)
The Given is an ordinary quantified constraint; the Wanted is an implication
equality that arises from
[W] (forall a. t1) ~R# (forall a. t2)
But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
we can't generate any term evidence. So we can't actually use that
lovely quantified constraint. Alas!
This test arranges to ignore the instance-based solution under these
(rare) circumstances. It's sad, but I really don't see what else we can do.
-}
{- *******************************************************************
* *
......
......@@ -71,7 +71,7 @@ module TcRnTypes(
Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts, isCTyEqCan, isCFunEqCan,
isPendingScDict, superClassesMightHelp,
isPendingScDict, superClassesMightHelp, getPendingWantedScs,
isCDictCan_Maybe, isCFunEqCan_maybe,
isCNonCanonical, isWantedCt, isDerivedCt,
isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
......@@ -2214,16 +2214,31 @@ setPendingScDict ct@(CDictCan { cc_pend_sc = False })
= ct { cc_pend_sc = True }
setPendingScDict ct = ct
superClassesMightHelp :: Ct -> Bool
superClassesMightHelp :: WantedConstraints -> Bool
-- ^ True if taking superclasses of givens, or of wanteds (to perhaps
-- expose more equalities or functional dependencies) might help to
-- solve this constraint. See Note [When superclasses help]
superClassesMightHelp ct
= isWantedCt ct && not (is_ip ct)
superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics })
= anyBag might_help_ct simples || anyBag might_help_implic implics
where
might_help_implic ic
| IC_Unsolved <- ic_status ic = superClassesMightHelp (ic_wanted ic)
| otherwise = False
might_help_ct ct = isWantedCt ct && not (is_ip ct)
is_ip (CDictCan { cc_class = cls }) = isIPClass cls
is_ip _ = False
getPendingWantedScs :: Cts -> ([Ct], Cts)
getPendingWantedScs simples
= mapAccumBagL get [] simples
where
get acc ct | Just ct' <- isPendingScDict ct
= (ct':acc, ct')
| otherwise
= (acc, ct)
{- Note [When superclasses help]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
First read Note [The superclass story] in TcCanonical.
......@@ -2234,6 +2249,11 @@ might actually help. The function superClassesMightHelp tells if
doing this superclass expansion might help solve this constraint.
Note that
* We look inside implications; maybe it'll help to expand the Givens
at level 2 to help solve an unsolved Wanted buried inside an
implication. E.g.
forall a. Ord a => forall b. [W] Eq a
* Superclasses help only for Wanted constraints. Derived constraints
are not really "unsolved" and we certainly don't want them to
trigger superclass expansion. This was a good part of the loop
......
......@@ -58,7 +58,7 @@ module TcSMonad (
getTcSInerts, setTcSInerts,
matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
getUnsolvedInerts,
removeInertCts, getPendingScDicts,
removeInertCts, getPendingGivenScs,
addInertCan, insertFunEq, addInertForAll,
emitWorkNC, emitWork,
isImprovable,
......@@ -1935,27 +1935,36 @@ getInertGivens
$ concat (dVarEnvElts (inert_eqs inerts))
; return (filter isGivenCt all_cts) }
getPendingScDicts :: TcS [Ct]
-- Find all inert Given dictionaries whose cc_pend_sc flag is True
-- Set the flag to False in the inert set, and return that Ct
getPendingScDicts = updRetInertCans get_sc_dicts
getPendingGivenScs :: TcS [Ct]
-- Find all inert Given dictionaries, or quantified constraints,
-- whose cc_pend_sc flag is True
-- and that belong to the current level
-- Set their cc_pend_sc flag to False in the inert set, and return that Ct
getPendingGivenScs = do { lvl <- getTcLevel
; updRetInertCans (get_sc_pending lvl) }
get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
= ASSERT2( all isGivenCt sc_pending, ppr sc_pending )
-- When getPendingScDics is called,
-- there are never any Wanteds in the inert set
(sc_pending, ic { inert_dicts = dicts', inert_insts = insts' })
where
get_sc_dicts ic@(IC { inert_dicts = dicts, inert_insts = insts })
= (sc_pend_insts ++ sc_pend_dicts, ic')
where
ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts
, inert_insts = insts' }
sc_pending = sc_pend_insts ++ sc_pend_dicts
sc_pend_dicts :: [Ct]
sc_pend_dicts = foldDicts get_pending dicts []
sc_pend_dicts = foldDicts get_pending dicts []
dicts' = foldr add dicts sc_pend_dicts
(sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
(sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True
-- but flipping the flag
get_pending dict dicts
| Just dict' <- isPendingScDict dict = dict' : dicts
| otherwise = dicts
| Just dict' <- isPendingScDict dict
, belongs_to_this_level (ctEvidence dict)
= dict' : dicts
| otherwise
= dicts
add :: Ct -> DictMap Ct -> DictMap Ct
add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
......@@ -1963,12 +1972,17 @@ getPendingScDicts = updRetInertCans get_sc_dicts
add ct _ = pprPanic "getPendingScDicts" (ppr ct)
get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst cts qci
get_pending_inst cts qci@(QCI { qci_ev = ev })
| Just qci' <- isPendingScInst qci
, belongs_to_this_level ev
= (CQuantCan qci' : cts, qci')
| otherwise
= (cts, qci)
belongs_to_this_level ev = ctLocLevel (ctEvLoc ev) == this_lvl
-- We only want Givens from this level; see (3a) in
-- Note [The superclass story] in TcCanonical
getUnsolvedInerts :: TcS ( Bag Implication
, Cts -- Tyvar eqs: a ~ ty
, Cts -- Fun eqs: F a ~ ty
......
......@@ -537,7 +537,7 @@ tcCheckSatisfiability given_ids
| not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
= return insols -- Hurrah -- stop now.
| otherwise
= do { pending_given <- getPendingScDicts
= do { pending_given <- getPendingGivenScs
; new_given <- makeSuperClasses pending_given
; solveSimpleGivens new_given
; getInertInsols }
......@@ -1374,19 +1374,12 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
-- Any insoluble constraints are in 'simples' and so get rewritten
-- See Note [Rewrite insolubles] in TcSMonad
; let WC { wc_simple = simples1, wc_impl = implics1 } = wc1
; (floated_eqs, implics2) <- solveNestedImplications $
implics `unionBags` wc_impl wc1
; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
; (no_new_scs, simples2) <- expandSuperClasses simples1
; traceTcS "solveWanteds middle" $ vcat [ text "simples1 =" <+> ppr simples1
, text "simples2 =" <+> ppr simples2 ]
; dflags <- getDynFlags
; dflags <- getDynFlags
; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
no_new_scs
(WC { wc_simple = simples2
, wc_impl = implics2 })
(wc1 { wc_impl = implics2 })
; ev_binds_var <- getTcEvBindsVar
; bb <- TcS.getTcEvBindsMap ev_binds_var
......@@ -1396,14 +1389,9 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
; return final_wc }
simpl_loop :: Int -> IntWithInf -> Cts -> Bool
-> WantedConstraints
-> TcS WantedConstraints
simpl_loop n limit floated_eqs no_new_deriveds
wc@(WC { wc_simple = simples, wc_impl = implics })
| isEmptyBag floated_eqs && no_new_deriveds
= return wc -- Done!
simpl_loop :: Int -> IntWithInf -> Cts
-> WantedConstraints -> TcS WantedConstraints
simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
| n `intGtLimit` limit
= do { -- Add an error (not a warning) if we blow the limit,
-- Typically if we blow the limit we are going to report some other error
......@@ -1414,75 +1402,67 @@ simpl_loop n limit floated_eqs no_new_deriveds
2 (vcat [ text "Unsolved:" <+> ppr wc
, ppUnless (isEmptyBag floated_eqs) $
text "Floated equalities:" <+> ppr floated_eqs
, ppUnless no_new_deriveds $
text "New deriveds found"
, text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
]))
; return wc }
| not (isEmptyBag floated_eqs)
= simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
-- Put floated_eqs first so they get solved first
-- NB: the floated_eqs may include /derived/ equalities
-- arising from fundeps inside an implication
| superClassesMightHelp wc
= -- We still have unsolved goals, and apparently no way to solve them,
-- so try expanding superclasses at this level, both Given and Wanted
do { pending_given <- getPendingGivenScs
; let (pending_wanted, simples1) = getPendingWantedScs simples
; if null pending_given && null pending_wanted
then return wc -- After all, superclasses did not help
else
do { new_given <- makeSuperClasses pending_given
; new_wanted <- makeSuperClasses pending_wanted
; solveSimpleGivens new_given -- Add the new Givens to the inert set
; simplify_again n limit (null pending_given)
wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
| otherwise
= do { let n_floated = lengthBag floated_eqs
; csTraceTcS $
= return wc
simplify_again :: Int -> IntWithInf -> Bool
-> WantedConstraints -> TcS WantedConstraints
-- We have definitely decided to have another go at solving
-- the wanted constraints (we have tried at least once already
simplify_again n limit no_new_given_scs
wc@(WC { wc_simple = simples, wc_impl = implics })
= do { csTraceTcS $
text "simpl_loop iteration=" <> int n
<+> (parens $ hsep [ text "no new deriveds =" <+> ppr no_new_deriveds <> comma
, int n_floated <+> text "floated eqs" <> comma
<+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
, int (lengthBag simples) <+> text "simples to solve" ])
; traceTcS "simpl_loop: wc =" (ppr wc)
-- solveSimples may make progress if either float_eqs hold
; (unifs1, wc1) <- reportUnifications $
solveSimpleWanteds $
floated_eqs `unionBags` simples
-- Notes:
-- - Put floated_eqs first so they get solved first
-- NB: the floated_eqs may include /derived/ equalities
-- arising from fundeps inside an implication
; let WC { wc_simple = simples1, wc_impl = implics1 } = wc1
; (no_new_scs, simples2) <- expandSuperClasses simples1
simples
-- See Note [Cutting off simpl_loop]
-- We have already tried to solve the nested implications once
-- Try again only if we have unified some meta-variables
-- (which is a bit like adding more givens)
-- See Note [Cutting off simpl_loop]
; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
then return (emptyBag, implics)
else solveNestedImplications (implics `unionBags` implics1)
; simpl_loop (n+1) limit floated_eqs2 no_new_scs
(WC { wc_simple = simples2
, wc_impl = implics2 }) }
expandSuperClasses :: Cts -> TcS (Bool, Cts)
-- If there are any unsolved wanteds, expand one step of
-- superclasses for deriveds
-- Returned Bool is True <=> no new superclass constraints added
-- See Note [The superclass story] in TcCanonical
expandSuperClasses unsolved
| not (anyBag superClassesMightHelp unsolved)
= return (True, unsolved)
| otherwise
= do { traceTcS "expandSuperClasses {" (ppr unsolved)
; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
get acc ct | Just ct' <- isPendingScDict ct
= (ct':acc, ct')
| otherwise
= (acc, ct)
; pending_given <- getPendingScDicts
; if null pending_given && null pending_wanted
then do { traceTcS "End expandSuperClasses no-op }" empty
; return (True, unsolved) }
else
do { traceTcS "expandSuperClasses mid"
(vcat [ text "pending_given:" <+> ppr pending_given
, text "pending_wanted:" <+> ppr pending_wanted ])
; new_given <- makeSuperClasses pending_given
; solveSimpleGivens new_given
; new_wanted <- makeSuperClasses pending_wanted
; traceTcS "End expandSuperClasses }"
(vcat [ text "Given:" <+> ppr pending_given
, text "Wanted:" <+> ppr new_wanted ])
; return (False, unsolved' `unionBags` listToBag new_wanted) } }
-- (which is a bit like adding more givens), or we have some
-- new Given superclasses
; let new_implics = wc_impl wc1
; if unifs1 == 0 &&
no_new_given_scs &&
isEmptyBag new_implics
then -- Do not even try to solve the implications
simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
else -- Try to solve the implications
do { (floated_eqs2, implics2) <- solveNestedImplications $
implics `unionBags` new_implics
; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
} }
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
......@@ -1616,7 +1596,7 @@ setImplicationStatus implic@(Implic { ic_status = status
discard_entire_implication -- Can we discard the entire implication?
= null dead_givens -- No warning from this implication
&& not bad_telescope
&& isEmptyBag pruned_implics -- No live children
&& isEmptyWC pruned_wc -- No live children
&& isEmptyVarSet need_outer -- No needed vars to pass up to parent
final_status
......
{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
module T15290 where
import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible, coerce )
class Monad m where
join :: m (m a) -> m a
newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
instance Monad m => Monad (StateT s m) where
join = error "urk"
instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
=> Monad (IntStateT m) where
-- Fails with the impredicative instantiation of coerce, succeeds without
-- Impredicative version (fails)
-- join = coerce
-- @(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
-- @(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
-- join
-- Predicative version (succeeds)
join = (coerce
@(StateT Int m (StateT Int m a) -> StateT Int m a)
@(IntStateT m (IntStateT m a) -> IntStateT m a)
join) :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
{-# LANGUAGE TypeApplications, ImpredicativeTypes, ScopedTypeVariables,
QuantifiedConstraints, StandaloneDeriving, GeneralizedNewtypeDeriving #-}
module T15290a where
import Prelude hiding ( Monad(..) )
import Data.Coerce ( Coercible, coerce )
class Monad m where
join :: m (m a) -> m a
newtype StateT s m a = StateT { runStateT :: s -> m (s, a) }
newtype IntStateT m a = IntStateT { runIntStateT :: StateT Int m a }
instance Monad m => Monad (StateT s m) where
join = error "urk"
instance (Monad m, forall p q. Coercible p q => Coercible (m p) (m q))
=> Monad (IntStateT m) where
-- Fails with the impredicative instantiation of coerce, succeeds without
-- Impredicative version (fails)
join = coerce
@(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
@(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
join
-- Predicative version (succeeds)
-- join = (coerce
-- @(StateT Int m (StateT Int m a) -> StateT Int m a)
-- @(IntStateT m (IntStateT m a) -> IntStateT m a)
-- join) :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
T15290a.hs:25:12: error:
• Couldn't match representation of type ‘m (Int, IntStateT m a1)’
with that of ‘m (Int, StateT Int m a1)’
arising from a use of ‘coerce’
NB: We cannot know what roles the parameters to ‘m’ have;
we must assume that the role is nominal
• In the expression:
coerce
@(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
@(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
join
In an equation for ‘join’:
join
= coerce
@(forall a. StateT Int m (StateT Int m a) -> StateT Int m a)
@(forall a. IntStateT m (IntStateT m a) -> IntStateT m a)
join
In the instance declaration for ‘Monad (IntStateT m)’
• Relevant bindings include
join :: IntStateT m (IntStateT m a) -> IntStateT m a
(bound at T15290a.hs:25:5)
......@@ -10,3 +10,6 @@ test('T14961', normal, compile, [''])
test('T9123a', normal, compile, [''])
test('T15244', normal, compile, [''])
test('T15231', normal, compile_fail, [''])
test('T15290', normal, compile, [''])
test('T15290a', normal, compile_fail, [''])
......@@ -46,8 +46,7 @@ TcCoercibleFail.hs:30:9: error:
TcCoercibleFail.hs:35:8: error:
• Reduction stack overflow; size = 201
When simplifying the following type:
Coercible (Fix (Either Int)) (Fix (Either Age))
When simplifying the following type: Fix (Either Int)
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
......
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