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

Remove wc_insol from WantedConstraints

This patch is a pure refactoring, which I've wanted to do for
some time.  The main payload is

* Remove the wc_insol field from WantedConstraints;
  instead put all the insolubles in wc_simple

* Remove inert_insols from InertCans
  Instead put all the insolubles in inert_irreds

* Add a cc_insol flag to CIrredCan, to record that
  the constraint is definitely insoluble

Reasons

* Quite a bit of code gets slightly simpler
* Fewer concepts to keep separate
* Insolubles don't happen at all in production code that is
  just being recompiled, so previously there was a lot of
  moving-about of empty sets

A couple of error messages acutally improved.
parent 3e44562a
......@@ -78,10 +78,18 @@ last time through, so we can skip the classification step.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canonicalize :: Ct -> TcS (StopOrContinue Ct)
canonicalize ct@(CNonCanonical { cc_ev = ev })
= do { traceTcS "canonicalize (non-canonical)" (ppr ct)
; {-# SCC "canEvVar" #-}
canEvNC ev }
canonicalize (CNonCanonical { cc_ev = ev })
= {-# SCC "canNC" #-}
case classifyPredType (ctEvPred ev) of
ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
canClassNC ev cls tys
EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
canEqNC ev eq_rel ty1 ty2
IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
canIrred ev
canonicalize (CIrredCan { cc_ev = ev })
= canIrred ev
canonicalize (CDictCan { cc_ev = ev, cc_class = cls
, cc_tyargs = xis, cc_pend_sc = pend_sc })
......@@ -104,21 +112,9 @@ canonicalize (CFunEqCan { cc_ev = ev
= {-# SCC "canEqLeafFunEq" #-}
canCFunEqCan ev fn xis1 fsk
canonicalize (CIrredEvCan { cc_ev = ev })
= canIrred ev
canonicalize (CHoleCan { cc_ev = ev, cc_hole = hole })
= canHole ev hole
canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
-- Called only for non-canonical EvVars
canEvNC ev
= case classifyPredType (ctEvPred ev) of
ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
canClassNC ev cls tys
EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
canEqNC ev eq_rel ty1 ty2
IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
canIrred ev
{-
************************************************************************
* *
......@@ -500,7 +496,7 @@ canIrred old_ev
ClassPred cls tys -> canClassNC new_ev cls tys
EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
_ -> continueWith $
CIrredEvCan { cc_ev = new_ev } } }
mkIrredCt new_ev } }
canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
canHole ev hole
......@@ -911,7 +907,7 @@ Here's another place where this reflexivity check is key:
Consider trying to prove (f a) ~R (f a). The AppTys in there can't
be decomposed, because representational equality isn't congruent with respect
to AppTy. So, when canonicalising the equality above, we get stuck and
would normally produce a CIrredEvCan. However, we really do want to
would normally produce a CIrredCan. However, we really do want to
be able to solve (f a) ~R (f a). So, in the representational case only,
we do a reflexivity check.
......@@ -958,7 +954,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~r s2 t2
-- See Note [Decomposing equality], note {4}
can_eq_app ev ReprEq _ _ _ _
= do { traceTcS "failing to decompose representational AppTy equality" (ppr ev)
; continueWith (CIrredEvCan { cc_ev = ev }) }
; continueWith (mkIrredCt ev) }
-- no need to call canEqFailure, because that flattens, and the
-- types involved here are already flat
......@@ -1031,7 +1027,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
-- See Note [Skolem abstract data] (at tyConSkolem)
| tyConSkolem tc1 || tyConSkolem tc2
= do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
; continueWith (CIrredEvCan { cc_ev = ev }) }
; continueWith (mkIrredCt ev) }
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
......@@ -1293,7 +1289,7 @@ canEqFailure ev ReprEq ty1 ty2
vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
`andWhenContinue` \ new_ev ->
continueWith (CIrredEvCan { cc_ev = new_ev }) }
continueWith (mkIrredCt new_ev) }
-- | Call when canonicalizing an equality fails with utterly no hope.
canEqHardFailure :: CtEvidence
......@@ -1304,7 +1300,7 @@ canEqHardFailure ev ty1 ty2
; (s2, co2) <- flatten FM_SubstOnly ev ty2
; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
`andWhenContinue` \ new_ev ->
do { emitInsoluble (mkNonCanonical new_ev)
do { emitInsoluble (mkInsolubleCt new_ev)
; stopWith new_ev "Definitely not equal" }}
{-
......@@ -1481,7 +1477,7 @@ canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
-- kind_ev :: (k1 :: *) ~ (k2 :: *)
; traceTcS "Hetero equality gives rise to derived kind equality" $
ppr ev
; continueWith (CIrredEvCan { cc_ev = ev }) }
; continueWith (mkIrredCt ev) }
where
lhs = mkTyVarTy tv1 `mkCastTy` co1
......@@ -1549,7 +1545,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
`andWhenContinue` \ new_ev ->
if isInsolubleOccursCheck eq_rel tv1 nrhs
then do { emitInsoluble (mkNonCanonical new_ev)
then do { emitInsoluble (mkInsolubleCt new_ev)
-- If we have a ~ [a], it is not canonical, and in particular
-- we don't want to rewrite existing inerts with it, otherwise
-- we'd risk divergence in the constraint solver
......@@ -1563,7 +1559,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
-- canonical, and we might loop if we were to use it in rewriting.
else do { traceTcS "Possibly-soluble occurs check"
(ppr nlhs $$ ppr nrhs)
; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
; continueWith (mkIrredCt new_ev) } }
where
role = eqRelRole eq_rel
......
......@@ -441,11 +441,10 @@ This only matters in instance declarations..
-}
reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
= do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
, text "Insols =" <+> ppr insols
, text "Suppress =" <+> ppr (cec_suppress ctxt)])
; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
; let tidy_cts = bagToList (mapBag (tidyCt env) simples)
; traceTc "rw2" (ppr tidy_cts)
-- First deal with things that are utterly wrong
......@@ -477,7 +476,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
-- report1: ones that should *not* be suppresed by
-- an insoluble somewhere else in the tree
-- It's crucial that anything that is considered insoluble
-- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
-- (see TcRnTypes.insolubleWantedCt) is caught here, otherwise
-- we might suppress its error message, and proceed on past
-- type checking to get a Lint error later
report1 = [ ("custom_error", is_user_type_error,True, mkUserTypeErrorReporter)
......@@ -936,9 +935,9 @@ coercion.
Note [Do not report derived but soluble errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The wc_simples include Derived constraints that have not been solved, but are
not insoluble (in that case they'd be in wc_insols). We do not want to report
these as errors:
The wc_simples include Derived constraints that have not been solved,
but are not insoluble (in that case they'd be reported by 'report1').
We do not want to report these as errors:
* Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
an unsolved [D] Eq a, and we do not want to report that; it's just noise.
......
......@@ -201,16 +201,15 @@ solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
-- The result is not necessarily zonked
solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
= nestTcS $
do { solveSimples simples1
; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
; (implics2, tv_eqs, fun_eqs, others) <- getUnsolvedInerts
; (unif_count, unflattened_eqs) <- reportUnifications $
unflattenWanteds tv_eqs fun_eqs
-- See Note [Unflatten after solving the simple wanteds]
; return ( unif_count
, WC { wc_simple = others `andCts` unflattened_eqs
, wc_insol = insols1 `andCts` insols2
, wc_impl = implics1 `unionBags` implics2 }) }
{- Note [The solveSimpleWanteds loop]
......@@ -270,7 +269,7 @@ runTcPluginsGiven
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
-- main solver.
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
| isEmptyBag simples1
= return (False, wc)
| otherwise
......@@ -284,15 +283,17 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl =
; let (_, _, solved_wanted) = pluginSolvedCts p
(_, unsolved_derived, unsolved_wanted) = pluginInputCts p
new_wanted = pluginNewCts p
insols = pluginBadCts p
-- SLPJ: I'm deeply suspicious of this
-- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
; mapM_ setEv solved_wanted
; return ( notNull (pluginNewCts p)
, WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
`andCts` listToBag unsolved_derived
, wc_insol = listToBag (pluginBadCts p) `andCts` insols1
, WC { wc_simple = listToBag new_wanted `andCts`
listToBag unsolved_wanted `andCts`
listToBag unsolved_derived `andCts`
listToBag insols
, wc_impl = implics1 } ) } }
where
setEv :: (EvTerm,Ct) -> TcS ()
......@@ -493,10 +494,10 @@ interactWithInertsStage wi
= do { inerts <- getTcSInerts
; let ics = inert_cans inerts
; case wi of
CTyEqCan {} -> interactTyVarEq ics wi
CFunEqCan {} -> interactFunEq ics wi
CIrredEvCan {} -> interactIrred ics wi
CDictCan {} -> interactDict ics wi
CTyEqCan {} -> interactTyVarEq ics wi
CFunEqCan {} -> interactFunEq ics wi
CIrredCan {} -> interactIrred ics wi
CDictCan {} -> interactDict ics wi
_ -> pprPanic "interactWithInerts" (ppr wi) }
-- CHoleCan are put straight into inert_frozen, so never get here
-- CNonCanonical have been canonicalised
......@@ -657,7 +658,7 @@ that this chain of events won't happen, but that's very fragile.)
-- mean that (ty1 ~ ty2)
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w })
| let pred = ctEvPred ev_w
(matching_irreds, others)
= partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
......
......@@ -1351,11 +1351,10 @@ zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC wc = zonkWCRec wc
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
= do { simple' <- zonkSimples simple
; implic' <- mapBagM zonkImplication implic
; insol' <- zonkSimples insol
; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
; return (WC { wc_simple = simple', wc_impl = implic' }) }
zonkSimples :: Cts -> TcM Cts
zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
......@@ -1366,10 +1365,12 @@ zonkCt' :: Ct -> TcM Ct
zonkCt' ct = zonkCt ct
{- Note [zonkCt behaviour]
~~~~~~~~~~~~~~~~~~~~~~~~~~
zonkCt tries to maintain the canonical form of a Ct. For example,
- a CDictCan should stay a CDictCan;
- a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
- a CHoleCan should stay a CHoleCan
- a CIrredCan should stay a CIrredCan with its cc_insol flag intact
Why?, for example:
- For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
......@@ -1380,21 +1381,27 @@ Why?, for example:
- For CHoleCan, once we forget that it's a hole, we can never recover that info.
- For CIrredCan we want to see if a constraint is insoluble with insolubleWC
NB: we do not expect to see any CFunEqCans, because zonkCt is only
called on unflattened constraints.
NB: Constraints are always re-flattened etc by the canonicaliser in
@TcCanonical@ even if they come in as CDictCan. Only canonical constraints that
are actually in the inert set carry all the guarantees. So it is okay if zonkCt
creates e.g. a CDictCan where the cc_tyars are /not/ function free.
-}
zonkCt :: Ct -> TcM Ct
zonkCt ct@(CHoleCan { cc_ev = ev })
= do { ev' <- zonkCtEvidence ev
; return $ ct { cc_ev = ev' } }
zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
= do { ev' <- zonkCtEvidence ev
; args' <- mapM zonkTcType args
; return $ ct { cc_ev = ev', cc_tyargs = args' } }
zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
= do { ev' <- zonkCtEvidence ev
; tv_ty' <- zonkTcTyVar tv
......@@ -1404,6 +1411,11 @@ zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
, cc_tyvar = tv'
, cc_rhs = rhs' } }
Nothing -> return (mkNonCanonical ev') }
zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
= do { ev' <- zonkCtEvidence ev
; return (ct { cc_ev = ev' }) }
zonkCt ct
= ASSERT( not (isCFunEqCan ct) )
-- We do not expect to see any CFunEqCans, because zonkCt is only called on
......
......@@ -1589,6 +1589,17 @@ Hence:
- insolublesOnly in tryCaptureConstraints
- emitConstraints in the Left case of captureConstraints
Hover note that fresly-generated constraints like (Int ~ Bool), or
((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as
insoluble. The constraint solver does that. So they'll be discarded.
That's probably ok; but see th/5358 as a not-so-good example:
t1 :: Int
t1 x = x -- Manifestly wrong
foo = $(...raises exception...)
We report the exception, but not the bug in t1. Oh well. Possible
solution: make TcUnify.uType spot manifestly-insoluble constraints.
************************************************************************
* *
......
......@@ -70,12 +70,13 @@ module TcRnTypes(
isEmptyCts, isCTyEqCan, isCFunEqCan,
isPendingScDict, superClassesMightHelp,
isCDictCan_Maybe, isCFunEqCan_maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
isCNonCanonical, isWantedCt, isDerivedCt,
isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
isUserTypeErrorCt, getUserTypeErrorMsg,
ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
mkTcEqPredLikeEv,
mkNonCanonical, mkNonCanonicalCt, mkGivens,
mkIrredCt, mkInsolubleCt,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvTerm, ctEvCoercion, ctEvId,
tyCoVarsOfCt, tyCoVarsOfCts,
......@@ -83,9 +84,9 @@ module TcRnTypes(
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, mkSimpleWC, mkImplicWC,
addInsols, getInsolubles, insolublesOnly, addSimples, addImplics,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
tyCoVarsOfWCList, trulyInsoluble,
addInsols, insolublesOnly, addSimples, addImplics,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt,
isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic,
arisesFromGivens,
......@@ -1619,13 +1620,20 @@ data Ct
-- superclasses as Givens
}
| CIrredEvCan { -- These stand for yet-unusable predicates
cc_ev :: CtEvidence -- See Note [Ct/evidence invariant]
-- The ctev_pred of the evidence is
-- of form (tv xi1 xi2 ... xin)
| CIrredCan { -- These stand for yet-unusable predicates
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_insol :: Bool -- True <=> definitely an error, can never be solved
-- False <=> might be soluble
-- For the might-be-soluble case, the ctev_pred of the evidence is
-- of form (tv xi1 xi2 ... xin) with a tyvar at the head
-- or (tv1 ~ ty2) where the CTyEqCan kind invariant fails
-- or (F tys ~ ty) where the CFunEqCan kind invariant fails
-- See Note [CIrredEvCan constraints]
-- See Note [CIrredCan constraints]
-- The definitely-insoluble case is for things like
-- Int ~ Bool tycons don't match
-- a ~ [a] occurs check
}
| CTyEqCan { -- tv ~ rhs
......@@ -1710,9 +1718,9 @@ distinguished by cc_hole:
e.g. f :: _ -> _
f x = [x,True]
Note [CIrredEvCan constraints]
Note [CIrredCan constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
CIrredEvCan constraints are used for constraints that are "stuck"
CIrredCan constraints are used for constraints that are "stuck"
- we can't solve them (yet)
- we can't use them to solve other constraints
- but they may become soluble if we substitute for some
......@@ -1754,6 +1762,12 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev }
mkNonCanonicalCt :: Ct -> Ct
mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
mkIrredCt :: CtEvidence -> Ct
mkIrredCt ev = CIrredCan { cc_ev = ev, cc_insol = False }
mkInsolubleCt :: CtEvidence -> Ct
mkInsolubleCt ev = CIrredCan { cc_ev = ev, cc_insol = True }
mkGivens :: CtLoc -> [EvId] -> [Ct]
mkGivens loc ev_ids
= map mk ev_ids
......@@ -1806,7 +1820,9 @@ instance Outputable Ct where
CDictCan { cc_pend_sc = pend_sc }
| pend_sc -> text "CDictCan(psc)"
| otherwise -> text "CDictCan"
CIrredEvCan {} -> text "CIrredEvCan"
CIrredCan { cc_insol = insol }
| insol -> text "CIrredCan(insol)"
| otherwise -> text "CIrredCan(sol)"
CHoleCan { cc_hole = hole } -> text "CHoleCan:" <+> ppr hole
{-
......@@ -1838,7 +1854,7 @@ tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
= tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk
`unionFV` tyCoFVsOfType (tyVarKind fsk)
tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys
tyCoFVsOfCt (CIrredEvCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
tyCoFVsOfCt (CIrredCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
tyCoFVsOfCt (CHoleCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
tyCoFVsOfCt (CNonCanonical { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
......@@ -1873,10 +1889,9 @@ tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC
-- computation. See Note [Deterministic FV] in FV.
tyCoFVsOfWC :: WantedConstraints -> FV
-- Only called on *zonked* things, hence no need to worry about flatten-skolems
tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic })
= tyCoFVsOfCts simple `unionFV`
tyCoFVsOfBag tyCoFVsOfImplic implic `unionFV`
tyCoFVsOfCts insol
tyCoFVsOfBag tyCoFVsOfImplic implic
-- | Returns free variables of Implication as a composable FV computation.
-- See Note [Deterministic FV] in FV.
......@@ -1891,6 +1906,13 @@ tyCoFVsOfImplic (Implic { ic_skols = skols
tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
tyCoFVsOfBag tvs_of = foldrBag (unionFV . tvs_of) emptyFV
---------------------------
dropDerivedWC :: WantedConstraints -> WantedConstraints
-- See Note [Dropping derived constraints]
dropDerivedWC wc@(WC { wc_simple = simples })
= wc { wc_simple = dropDerivedSimples simples }
-- The wc_impl implications are already (recursively) filtered
--------------------------
dropDerivedSimples :: Cts -> Cts
-- Drop all Derived constraints, but make [W] back into [WD],
......@@ -1902,10 +1924,13 @@ dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples
dropDerivedCt :: Ct -> Maybe Ct
dropDerivedCt ct
= case ctEvFlavour ev of
Given -> Just ct -- Presumably insoluble; keep
Wanted WOnly -> Just (ct' { cc_ev = ev_wd })
Wanted _ -> Just ct'
_ -> ASSERT( isDerivedCt ct ) Nothing
-- simples are all Wanted or Derived
Derived | isDroppableDerivedLoc (ctLoc ct)
-> Nothing
| otherwise
-> Just ct
where
ev = ctEvidence ct
ev_wd = ev { ctev_nosh = WDeriv }
......@@ -1921,13 +1946,6 @@ we might miss some fundeps. Trac #13662 showed this up.
See Note [The superclass story] in TcCanonical.
-}
dropDerivedInsols :: Cts -> Cts
-- See Note [Dropping derived constraints]
dropDerivedInsols insols
= filterBag (not . isDroppableDerivedCt) insols
-- insols can include Given
isDroppableDerivedCt :: Ct -> Bool
isDroppableDerivedCt ct
| isDerivedCt ct = isDroppableDerivedLoc (ctLoc ct)
......@@ -2030,10 +2048,6 @@ isCDictCan_Maybe :: Ct -> Maybe Class
isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
isCDictCan_Maybe _ = Nothing
isCIrredEvCan :: Ct -> Bool
isCIrredEvCan (CIrredEvCan {}) = True
isCIrredEvCan _ = False
isCFunEqCan_maybe :: Ct -> Maybe (TyCon, [Type])
isCFunEqCan_maybe (CFunEqCan { cc_fun = tc, cc_tyargs = xis }) = Just (tc, xis)
isCFunEqCan_maybe _ = Nothing
......@@ -2226,34 +2240,29 @@ v%************************************************************************
data WantedConstraints
= WC { wc_simple :: Cts -- Unsolved constraints, all wanted
, wc_impl :: Bag Implication
, wc_insol :: Cts -- Insoluble constraints, can be
-- wanted, given, or derived
-- See Note [Insoluble constraints]
}
emptyWC :: WantedConstraints
emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag, wc_insol = emptyBag }
emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag }
mkSimpleWC :: [CtEvidence] -> WantedConstraints
mkSimpleWC cts
= WC { wc_simple = listToBag (map mkNonCanonical cts)
, wc_impl = emptyBag
, wc_insol = emptyBag }
, wc_impl = emptyBag }
mkImplicWC :: Bag Implication -> WantedConstraints
mkImplicWC implic
= WC { wc_simple = emptyBag, wc_impl = implic, wc_insol = emptyBag }
= WC { wc_simple = emptyBag, wc_impl = implic }
isEmptyWC :: WantedConstraints -> Bool
isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_insol = n })
= isEmptyBag f && isEmptyBag i && isEmptyBag n
isEmptyWC (WC { wc_simple = f, wc_impl = i })
= isEmptyBag f && isEmptyBag i
andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
andWC (WC { wc_simple = f1, wc_impl = i1, wc_insol = n1 })
(WC { wc_simple = f2, wc_impl = i2, wc_insol = n2 })
andWC (WC { wc_simple = f1, wc_impl = i1 })
(WC { wc_simple = f2, wc_impl = i2 })
= WC { wc_simple = f1 `unionBags` f2
, wc_impl = i1 `unionBags` i2
, wc_insol = n1 `unionBags` n2 }
, wc_impl = i1 `unionBags` i2 }
unionsWC :: [WantedConstraints] -> WantedConstraints
unionsWC = foldr andWC emptyWC
......@@ -2268,28 +2277,17 @@ addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
addInsols wc cts
= wc { wc_insol = wc_insol wc `unionBags` cts }
getInsolubles :: WantedConstraints -> Cts
getInsolubles = wc_insol
= wc { wc_simple = wc_simple wc `unionBags` cts }
insolublesOnly :: WantedConstraints -> WantedConstraints
-- Keep only the insolubles
insolublesOnly (WC { wc_insol = insols, wc_impl = implics })
= WC { wc_simple = emptyBag
, wc_insol = insols
, wc_impl = mapBag implic_insols_only implics }
-- Keep only the definitely-insoluble constraints
insolublesOnly (WC { wc_simple = simples, wc_impl = implics })
= WC { wc_simple = filterBag insolubleWantedCt simples
, wc_impl = mapBag implic_insols_only implics }
where
implic_insols_only implic
= implic { ic_wanted = insolublesOnly (ic_wanted implic) }
dropDerivedWC :: WantedConstraints -> WantedConstraints
-- See Note [Dropping derived constraints]
dropDerivedWC wc@(WC { wc_simple = simples, wc_insol = insols })
= wc { wc_simple = dropDerivedSimples simples
, wc_insol = dropDerivedInsols insols }
-- The wc_impl implications are already (recursively) filtered
isSolvedStatus :: ImplicStatus -> Bool
isSolvedStatus (IC_Solved {}) = True
isSolvedStatus _ = False
......@@ -2302,30 +2300,40 @@ insolubleImplic :: Implication -> Bool
insolubleImplic ic = isInsolubleStatus (ic_status ic)
insolubleWC :: WantedConstraints -> Bool
insolubleWC (WC { wc_impl = implics, wc_insol = insols })
= anyBag trulyInsoluble insols
insolubleWC (WC { wc_impl = implics, wc_simple = simples })
= anyBag insolubleWantedCt simples
|| anyBag insolubleImplic implics
trulyInsoluble :: Ct -> Bool
-- Constraints in the wc_insol set which ARE NOT
-- treated as truly insoluble:
-- a) type holes, arising from PartialTypeSignatures,
-- b) "true" expression holes arising from TypedHoles
insolubleWantedCt :: Ct -> Bool
-- Definitely insoluble, in particular /excluding/ type-hole constraints
insolubleWantedCt ct
| isGivenCt ct = False -- See Note [Given insolubles]
| isHoleCt ct = isOutOfScopeCt ct -- See Note [Insoluble holes]
| insolubleEqCt ct = True
| otherwise = False
insolubleEqCt :: Ct -> Bool
-- Returns True of /equality/ constraints
-- that are /definitely/ insoluble
-- It won't detect some definite errors like
-- F a ~ T (F a)
-- where F is a type family, which actually has an occurs check
--
-- An "expression hole" or "type hole" constraint isn't really an error
-- at all; it's a report saying "_ :: Int" here. But an out-of-scope
-- variable masquerading as expression holes IS treated as truly
-- insoluble, so that it trumps other errors during error reporting.
-- Yuk!
trulyInsoluble insol
| isHoleCt insol = isOutOfScopeCt insol
| otherwise = not (isGivenCt insol) -- See Note [Given insolubles]
-- The function is tuned for application /after/ constraint solving
-- i.e. assuming canonicalisation has been done
-- E.g. It'll reply True for a ~ [a]
-- but False for [a] ~ a
-- and
-- True for Int ~ F a Int
-- but False for Maybe Int ~ F a Int Int
-- (where F is an arity-1 type function)
insolubleEqCt (CIrredCan { cc_insol = insol }) = insol
insolubleEqCt _ = False
instance Outputable WantedConstraints where
ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
ppr (WC {wc_simple = s, wc_impl = i})
= text "WC" <+> braces (vcat
[ ppr_bag (text "wc_simple") s
, ppr_bag (text "wc_insol") n
, ppr_bag (text "wc_impl") i ])
ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
......@@ -2339,21 +2347,37 @@ ppr_bag doc bag
Consider (Trac #14325, comment:)
class (a~b) => C a b
foo :: C a b => a -> b
foo :: C a c => a -> c
foo x = x
hm3 :: C (f b) b => b -> f b
hm3 x = foo x
From the [G] C (f b) b we get the insoluble [G] f b ~# b. Then we we also
get an unsolved [W] C b (f b). If trulyInsouble is true of this, we'll
set cec_suppress to True, and suppress reports of the [W] C b (f b). But we
In the RHS of hm3, from the [G] C (f b) b we get the insoluble
[G] f b ~# b. Then we also get an unsolved [W] C b (f b).