Commit 06aac68d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Refactor the constraint solver (again!)

There are three core changes here:

a) In the constraint-solver pipeline.
   Given a work-item 'wi', the old scheme was:
      let relevant = getRelevantInerts wi
      interact 'wi' with each constraint in 'relevant'
   Bu now we have a single step
      interact 'wi' with the inert-set

   This turns out to avoid duplication, between getRelevantInerts
   (which needs to know which are relevant) and the interact step.
   Simpler, cleaner.

   This in turn made it sensible to combine the 'spontaneous solve'
   stage into the 'interact with inerts' stage.

b) Wanteds are no longer used to rewrite wanteds.  See Trac #8450.
   This in turn means that the inert set may have
     - many CFunEqCans with the same LHS
     - many CTyEqCans  with the same LHS
   Hence the EqualCtList in teh domain of inert_eqs and inert_funeqs

c) Some refactoring of the representation of the inert set,
   Notably inert_dicts and inert_funeqs are indexed by Class and TyCon
   respectively, so we can easily get all the constraints relevant to
   that class or tycon

There are many knock on effects!  This started as a small job but I
ended up doing qite a lot.  Some error messages in the test suite
really did improve as a result of (b)
parent 706552a2
......@@ -246,7 +246,7 @@ canClassNC d ev cls tys
`andWhenContinue` emitSuperclasses
canClass d ev cls tys
= do { (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
= do { (xis, cos) <- flattenMany d FMFullFlatten ev tys
; let co = mkTcTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
; mb <- rewriteCtFlavor ev xi co
......@@ -387,7 +387,7 @@ canIrred :: CtLoc -> CtEvidence -> TcS StopOrContinue
canIrred d ev
= do { let ty = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty
; (xi,co) <- flatten d FMFullFlatten ev ty -- co :: xi ~ ty
; let no_flattening = xi `eqType` ty
-- We can't use isTcReflCo, because even if the coercion is
-- Refl, the output type might have had a substitution
......@@ -405,7 +405,7 @@ canIrred d ev
canHole :: CtLoc -> CtEvidence -> OccName -> TcS StopOrContinue
canHole d ev occ
= do { let ty = ctEvPred ev
; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty
; (xi,co) <- flatten d FMFullFlatten ev ty -- co :: xi ~ ty
; mb <- rewriteCtFlavor ev xi co
; case mb of
Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_loc = d, cc_occ = occ })
......@@ -465,7 +465,8 @@ data FlattenMode = FMSubstOnly | FMFullFlatten
-- Flatten a bunch of types all at once.
flattenMany :: CtLoc -> FlattenMode
-> CtFlavour -> [Type] -> TcS ([Xi], [TcCoercion])
-> CtEvidence
-> [Type] -> TcS ([Xi], [TcCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
-- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused,
......@@ -483,7 +484,7 @@ flattenMany d f ctxt tys
-- the new type-function-free type, and a collection of new equality
-- constraints. See Note [Flattening] for more detail.
flatten :: CtLoc -> FlattenMode
-> CtFlavour -> TcType -> TcS (Xi, TcCoercion)
-> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
-- Postcondition: Coercion :: Xi ~ TcType
flatten loc f ctxt ty
| Just ty' <- tcView ty
......@@ -525,31 +526,30 @@ flatten loc f ctxt (TyConApp tc tys)
-- in which case the remaining arguments should
-- be dealt with by AppTys
fam_ty = mkTyConApp tc xi_args
; (ret_co, rhs_xi) <-
case f of
FMSubstOnly ->
case f of
FMSubstOnly ->
return (mkTcReflCo fam_ty, fam_ty)
FMFullFlatten ->
do { mb_ct <- lookupFlatEqn fam_ty
FMFullFlatten ->
do { mb_ct <- lookupFlatEqn tc xi_args
; case mb_ct of
Just (ctev, rhs_ty)
| let flav = ctEvFlavour ctev
, flav `canRewrite` ctxt
-> -- You may think that we can just return (cc_rhs ct) but not so.
-- return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
-- The cached constraint resides in the cache so we have to flatten
| ctev `canRewriteOrSame `ctxt -- Must allows [W]/[W]
-> -- You may think that we can just return (cc_rhs ct) but not so.
-- return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
-- The cached constraint resides in the cache so we have to flatten
-- the rhs to make sure we have applied any inert substitution to it.
-- Alternatively we could be applying the inert substitution to the
-- cache as well when we interact an equality with the inert.
-- Alternatively we could be applying the inert substitution to the
-- cache as well when we interact an equality with the inert.
-- The design choice is: do we keep the flat cache rewritten or not?
-- For now I say we don't keep it fully rewritten.
do { (rhs_xi,co) <- flatten loc f flav rhs_ty
do { (rhs_xi,co) <- flatten loc f ctev rhs_ty
; let final_co = evTermCoercion (ctEvTerm ctev)
`mkTcTransCo` mkTcSymCo co
; traceTcS "flatten/flat-cache hit" $ (ppr ctev $$ ppr rhs_xi $$ ppr final_co)
; return (final_co, rhs_xi) }
_ -> do { (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
; let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
......@@ -565,14 +565,14 @@ flatten loc f ctxt (TyConApp tc tys)
-- cf Trac #5655
, mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args) $
cos_rest
)
)
}
flatten loc _f ctxt ty@(ForAllTy {})
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
= do { let (tvs, rho) = splitForAllTys ty
; (rho', co) <- flatten loc FMSubstOnly ctxt rho
; (rho', co) <- flatten loc FMSubstOnly ctxt rho
-- Substitute only under a forall
-- See Note [Flattening under a forall]
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
......@@ -598,7 +598,7 @@ and we have not begun to think about how to make that work!
\begin{code}
flattenTyVar, flattenFinalTyVar
:: CtLoc -> FlattenMode
-> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
-> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
-- "Flattening" a type variable means to apply the substitution to it
-- The substitution is actually the union of the substitution in the TyBinds
-- for the unification variables that have been unified already with the inert
......@@ -640,10 +640,10 @@ flattenTyVar loc f ctxt tv
} } } } } }
where
tv_eq_subst subst tv
| Just ct <- lookupVarEnv subst tv
, let ctev = cc_ev ct
| Just (ct:_) <- lookupVarEnv subst tv -- If the first doesn't work, the
, let ctev = cc_ev ct -- subsequent ones won't either
rhs = cc_rhs ct
, ctEvFlavour ctev `canRewrite` ctxt
, ctev `canRewrite` ctxt
= Just (evTermCoercion (ctEvTerm ctev), rhs)
-- NB: even if ct is Derived we are not going to
-- touch the actual coercion so we are fine.
......@@ -766,9 +766,8 @@ canEqNC loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
canEqNC loc ev ty1 ty2
= do { let flav = ctEvFlavour ev
; (s1, co1) <- flatten loc FMSubstOnly flav ty1
; (s2, co2) <- flatten loc FMSubstOnly flav ty2
= do { (s1, co1) <- flatten loc FMSubstOnly ev ty1
; (s2, co2) <- flatten loc FMSubstOnly ev ty2
; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2) (mkHdEqPred s2 co1 co2)
; case mb_ct of
Nothing -> return Stop
......@@ -812,9 +811,8 @@ canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
canEqFailure :: CtLoc -> CtEvidence -> TcType -> TcType -> TcS StopOrContinue
-- See Note [Make sure that insolubles are fully rewritten]
canEqFailure loc ev ty1 ty2
= do { let flav = ctEvFlavour ev
; (s1, co1) <- flatten loc FMSubstOnly flav ty1
; (s2, co2) <- flatten loc FMSubstOnly flav ty2
= do { (s1, co1) <- flatten loc FMSubstOnly ev ty1
; (s2, co2) <- flatten loc FMSubstOnly ev ty2
; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2)
(mkHdEqPred s2 co1 co2)
; case mb_ct of
......@@ -1076,13 +1074,12 @@ canEqLeafFun :: CtLoc -> CtEvidence
-> TyCon -> [TcType] -> TcType -> TcS StopOrContinue
canEqLeafFun loc ev fn tys1 ty2 -- ev :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFun" $ pprEq (mkTyConApp fn tys1) ty2
; let flav = ctEvFlavour ev
-- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
-- co2 :: xi2 ~ ty2
; (xis1,cos1) <- flattenMany loc FMFullFlatten flav tys1
; (xi2, co2) <- flatten loc FMFullFlatten flav ty2
; (xis1,cos1) <- flattenMany loc FMFullFlatten ev tys1
; (xi2, co2) <- flatten loc FMFullFlatten ev ty2
-- Fancy higher-dimensional coercion between equalities!
-- SPJ asks why? Why not just co : F xis1 ~ F tys1?
......@@ -1104,9 +1101,8 @@ canEqLeafTyVar :: CtLoc -> CtEvidence
-> TcTyVar -> TcType -> TcS StopOrContinue
canEqLeafTyVar loc ev tv s2 -- ev :: tv ~ s2
= do { traceTcS "canEqLeafTyVar 1" $ pprEq (mkTyVarTy tv) s2
; let flav = ctEvFlavour ev
; (xi1,co1) <- flattenTyVar loc FMFullFlatten flav tv -- co1 :: xi1 ~ tv
; (xi2,co2) <- flatten loc FMFullFlatten flav s2 -- co2 :: xi2 ~ s2
; (xi1,co1) <- flattenTyVar loc FMFullFlatten ev tv -- co1 :: xi1 ~ tv
; (xi2,co2) <- flatten loc FMFullFlatten ev s2 -- co2 :: xi2 ~ s2
; let co = mkHdEqPred s2 co1 co2
-- co :: (xi1 ~ xi2) ~ (tv ~ s2)
......
......@@ -45,6 +45,7 @@ import FastString
import Outputable
import SrcLoc
import DynFlags
import ListSetOps ( equivClasses )
import Data.List ( partition, mapAccumL, zip4 )
\end{code}
......@@ -225,40 +226,64 @@ reportWanteds ctxt wanted@(WC { wc_flat = flats, wc_insol = insols, wc_impl = im
reportFlats :: ReportErrCtxt -> Cts -> TcM ()
reportFlats ctxt flats -- Here 'flats' includes insolble goals
= traceTc "reportFlats" (vcat [ ptext (sLit "Flats =") <+> ppr flats
, ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)]) >>
tryReporters
= traceTc "reportFlats" (vcat [ ptext (sLit "Flats =") <+> ppr flats
, ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)])
>> tryReporters
[ -- First deal with things that are utterly wrong
-- Like Int ~ Bool (incl nullary TyCons)
-- or Int ~ t a (AppTy on one side)
("Utterly wrong", utterly_wrong, mkGroupReporter mkEqErr)
, ("Holes", is_hole, mkUniReporter mkHoleError)
("Utterly wrong", utterly_wrong, True, mkGroupReporter mkEqErr)
, ("Holes", is_hole, True, mkUniReporter mkHoleError)
-- Report equalities of form (a~ty). They are usually
-- skolem-equalities, and they cause confusing knock-on
-- skolem-equalities, and they cause confusing knock-on
-- effects in other errors; see test T4093b.
, ("Skolem equalities", skolem_eq, mkUniReporter mkEqErr1) ]
reportFlatErrs
ctxt (bagToList flats)
, ("Skolem equalities", skolem_eq, True, mkSkolReporter)
-- Other equalities; also confusing knock on effects
, ("Equalities", is_equality, True, mkGroupReporter mkEqErr)
, ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
, ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
, ("Dicts", is_dict, False, mkGroupReporter mkDictErr)
]
panicReporter ctxt (bagToList flats)
-- TuplePreds should have been expanded away by the constraint
-- simplifier, so they shouldn't show up at this point
where
utterly_wrong, skolem_eq :: Ct -> PredTree -> Bool
utterly_wrong _ (EqPred ty1 ty2) = isRigid ty1 && isRigid ty2
utterly_wrong, skolem_eq, is_hole, is_dict,
is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
utterly_wrong _ (EqPred ty1 ty2) = isRigid ty1 && isRigid ty2
utterly_wrong _ _ = False
is_hole ct _ = isHoleCt ct
skolem_eq _ (EqPred ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2
skolem_eq _ (EqPred ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2
skolem_eq _ _ = False
is_equality _ (EqPred {}) = True
is_equality _ _ = False
is_dict _ (ClassPred {}) = True
is_dict _ _ = False
is_ip _ (ClassPred cls _) = isIPClass cls
is_ip _ _ = False
is_irred _ (IrredPred {}) = True
is_irred _ _ = False
---------------
isRigid, isRigidOrSkol :: Type -> Bool
isRigid ty
isRigid ty
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isDecomposableTyCon tc
| Just {} <- tcSplitAppTy_maybe ty = True
| isForAllTy ty = True
| otherwise = False
isRigidOrSkol ty
isRigidOrSkol ty
| Just tv <- getTyVar_maybe ty = isSkolemTyVar tv
| otherwise = isRigid ty
......@@ -267,48 +292,38 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
Just (tc,_) | isSynFamilyTyCon tc -> Just tc
_ -> Nothing
-----------------
reportFlatErrs :: Reporter
-- Called once for non-ambigs, once for ambigs
-- Report equality errors, and others only if we've done all
-- the equalities. The equality errors are more basic, and
-- can lead to knock on type-class errors
reportFlatErrs
= tryReporters
[ ("Equalities", is_equality, mkGroupReporter mkEqErr) ]
(\ctxt cts -> do { let (dicts, ips, irreds) = go cts [] [] []
; mkGroupReporter mkIPErr ctxt ips
; mkGroupReporter mkIrredErr ctxt irreds
; mkGroupReporter mkDictErr ctxt dicts })
where
is_equality _ (EqPred {}) = True
is_equality _ _ = False
go [] dicts ips irreds
= (dicts, ips, irreds)
go (ct:cts) dicts ips irreds
| isIPPred (ctPred ct)
= go cts dicts (ct:ips) irreds
| otherwise
= case classifyPredType (ctPred ct) of
ClassPred {} -> go cts (ct:dicts) ips irreds
IrredPred {} -> go cts dicts ips (ct:irreds)
_ -> panic "reportFlatErrs"
-- TuplePreds should have been expanded away by the constraint
-- simplifier, so they shouldn't show up at this point
-- And EqPreds are dealt with by the is_equality test
--------------------------------------------
-- Reporters
--------------------------------------------
type Reporter = ReportErrCtxt -> [Ct] -> TcM ()
type Reporter
= ReportErrCtxt -> [Ct] -> TcM ()
type ReporterSpec
= ( String -- Name
, Ct -> PredTree -> Bool -- Pick these ones
, Bool -- True <=> suppress subsequent reporters
, Reporter) -- The reporter itself
panicReporter :: Reporter
panicReporter _ cts
| null cts = return ()
| otherwise = pprPanic "reportFlats" (ppr cts)
mkSkolReporter :: Reporter
-- Suppress duplicates with the same LHS
mkSkolReporter ctxt cts
= mapM_ (reportGroup mkEqErr ctxt) (equivClasses cmp_lhs_type cts)
where
cmp_lhs_type ct1 ct2
= case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
(EqPred ty1 _, EqPred ty2 _) -> ty1 `cmpType` ty2
_ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
mkUniReporter :: (ReportErrCtxt -> Ct -> TcM ErrMsg) -> Reporter
-- Reports errors one at a time
mkUniReporter mk_err ctxt
= mapM_ $ \ct ->
mkUniReporter mk_err ctxt
= mapM_ $ \ct ->
do { err <- mk_err ctxt ct
; maybeReportError ctxt err
; maybeAddDeferredBinding ctxt err ct }
......@@ -316,26 +331,21 @@ mkUniReporter mk_err ctxt
mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
-- Make error message for a group
-> Reporter -- Deal with lots of constraints
-- Group together insts from same location
-- We want to report them together in error messages
-- Group together errors from same location,
-- and report only the first (to avoid a cascade)
mkGroupReporter mk_err ctxt cts
= mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
where
cmp_loc ct1 ct2 = ctLocSpan (cc_loc ct1) `compare` ctLocSpan (cc_loc ct2)
mkGroupReporter _ _ []
= return ()
mkGroupReporter mk_err ctxt (ct1 : rest)
= do { err <- mk_err ctxt first_group
reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
-> [Ct] -> TcM ()
reportGroup mk_err ctxt cts
= do { err <- mk_err ctxt cts
; maybeReportError ctxt err
; mapM_ (maybeAddDeferredBinding ctxt err) first_group
; mapM_ (maybeAddDeferredBinding ctxt err) cts }
-- Add deferred bindings for all
-- But see Note [Always warn with -fdefer-type-errors]
; mkGroupReporter mk_err ctxt others }
where
loc = cc_loc ct1
first_group = ct1 : friends
(friends, others) = partition is_friend rest
is_friend friend = cc_loc friend `same_loc` loc
same_loc :: CtLoc -> CtLoc -> Bool
same_loc l1 l2 = ctLocSpan l1 == ctLocSpan l2
maybeReportError :: ReportErrCtxt -> ErrMsg -> TcM ()
-- Report the error and/or make a deferred binding for it
......@@ -363,25 +373,25 @@ maybeAddDeferredBinding ctxt err ct
; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs) }
| otherwise -- Do not set any evidence for Given/Derived
= return ()
= return ()
tryReporters :: [(String, Ct -> PredTree -> Bool, Reporter)]
-> Reporter -> Reporter
tryReporters :: [ReporterSpec] -> Reporter -> Reporter
-- Use the first reporter in the list whose predicate says True
tryReporters reporters deflt ctxt cts
= do { traceTc "tryReporters {" (ppr cts)
= do { traceTc "tryReporters {" (ppr cts)
; go ctxt reporters cts
; traceTc "tryReporters }" empty }
where
go ctxt [] cts = deflt ctxt cts
go ctxt ((str, pred, reporter) : rs) cts
go ctxt [] cts = deflt ctxt cts
go ctxt ((str, pred, suppress_after, reporter) : rs) cts
| null yeses = do { traceTc "tryReporters: no" (text str)
; go ctxt rs cts }
| otherwise = do { traceTc "tryReporters: yes" (text str <+> ppr yeses)
; reporter ctxt yeses :: TcM ()
; go (ctxt { cec_suppress = True }) rs nos }
; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
; go ctxt' rs nos }
-- Carry on with the rest, because we must make
-- deferred bindings for them if we have
-- deferred bindings for them if we have
-- -fdefer-type-errors
-- But suppress their error messages
where
......@@ -914,13 +924,15 @@ mkDictErr ctxt cts
; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
; mkErrorMsg ctxt ct1 err }
where
ct1:_ = cts
ct1:_ = elim_superclasses cts
no_givens = null (getUserGivens ctxt)
is_no_inst (ct, (matches, unifiers, _))
= no_givens
&& null matches
= no_givens
&& null matches
&& (null unifiers || all (not . isAmbiguousTyVar) (varSetElems (tyVarsOfCt ct)))
lookup_cls_inst inst_envs ct
= do { tys_flat <- mapM quickFlattenTy tys
-- Note [Flattening in error message generation]
......@@ -928,6 +940,15 @@ mkDictErr ctxt cts
where
(clas, tys) = getClassPredTys (ctPred ct)
-- When simplifying [W] Ord (Set a), we need
-- [W] Eq a, [W] Ord a
-- but we really only want to report the latter
elim_superclasses cts
= filter (\ct -> any (eqPred (ctPred ct)) min_preds) cts
where
min_preds = mkMinimalBySCs (map ctPred cts)
mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
-> TcM (ReportErrCtxt, SDoc)
-- Report an overlap error if this class constraint results
......
This diff is collapsed.
......@@ -43,7 +43,8 @@ module TcRnTypes(
-- Canonical constraints
Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, dropDerivedWC,
singleCt, extendCts, isEmptyCts, isCTyEqCan, isCFunEqCan,
singleCt, listToCts, ctsElts, extendCts, extendCtsList,
isEmptyCts, isCTyEqCan, isCFunEqCan,
isCDictCan_Maybe, isCFunEqCan_maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
isGivenCt, isHoleCt,
......@@ -65,9 +66,8 @@ module TcRnTypes(
CtEvidence(..),
mkGivenLoc,
isWanted, isGiven,
isDerived, canRewrite,
CtFlavour(..), ctEvFlavour, ctFlavour,
isWanted, isGiven, isDerived,
canRewrite, canRewriteOrSame,
-- Pretty printing
pprEvVarTheta, pprWantedsWithLocs,
......@@ -1142,9 +1142,19 @@ singleCt = unitBag
andCts :: Cts -> Cts -> Cts
andCts = unionBags
listToCts :: [Ct] -> Cts
listToCts = listToBag
ctsElts :: Cts -> [Ct]
ctsElts = bagToList
extendCts :: Cts -> Ct -> Cts
extendCts = snocBag
extendCtsList :: Cts -> [Ct] -> Cts
extendCtsList cts xs | null xs = cts
| otherwise = cts `unionBags` listToBag xs
andManyCts :: [Cts] -> Cts
andManyCts = unionManyBags
......@@ -1381,15 +1391,6 @@ data CtEvidence
-- rewrite anything other than a derived (there's no evidence!)
-- but if we do manage to solve it may help in solving other goals.
data CtFlavour = Given | Wanted | Derived
ctFlavour :: Ct -> CtFlavour
ctFlavour ct = ctEvFlavour (cc_ev ct)
ctEvFlavour :: CtEvidence -> CtFlavour
ctEvFlavour (CtGiven {}) = Given
ctEvFlavour (CtWanted {}) = Wanted
ctEvFlavour (CtDerived {}) = Derived
ctEvPred :: CtEvidence -> TcPredType
-- The predicate of a flavor
......@@ -1405,11 +1406,6 @@ ctEvId :: CtEvidence -> TcId
ctEvId (CtWanted { ctev_evar = ev }) = ev
ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
instance Outputable CtFlavour where
ppr Given = ptext (sLit "[G]")
ppr Wanted = ptext (sLit "[W]")
ppr Derived = ptext (sLit "[D]")
instance Outputable CtEvidence where
ppr fl = case fl of
CtGiven {} -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty
......@@ -1429,24 +1425,50 @@ isDerived :: CtEvidence -> Bool
isDerived (CtDerived {}) = True
isDerived _ = False
canRewrite :: CtFlavour -> CtFlavour -> Bool
-- canRewrite ctid1 ctid2
-- The constraint ctid1 can be used to solve ctid2
-- "to solve" means a reaction where the active parts of the two constraints match.
-- active(F xis ~ xi) = F xis
-- active(tv ~ xi) = tv
-- active(D xis) = D xis
-- active(IP nm ty) = nm
--
-- NB: either (a `canRewrite` b) or (b `canRewrite` a) must hold
-----------------------------------------
canRewrite Given _ = True
canRewrite Wanted Derived = True
canRewrite Wanted Wanted = True
canRewrite Derived Derived = True -- Derived can't solve wanted/given
canRewrite :: CtEvidence -> CtEvidence -> Bool
-- Very important function!
-- See Note [canRewrite and canRewriteOrSame]
canRewrite (CtGiven {}) _ = True
canRewrite (CtWanted {}) (CtDerived {}) = True
canRewrite (CtDerived {}) (CtDerived {}) = True -- Derived can't solve wanted/given
canRewrite _ _ = False -- No evidence for a derived, anyway
canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool
canRewriteOrSame (CtGiven {}) _ = True
canRewriteOrSame (CtWanted {}) (CtWanted {}) = True
canRewriteOrSame (CtWanted {}) (CtDerived {}) = True
canRewriteOrSame (CtDerived {}) (CtDerived {}) = True
canRewriteOrSame _ _ = False
\end{code}
See Note [canRewrite and canRewriteOrSame]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(canRewrite ct1 ct2) holds if the constraint ct1 can be used to solve ct2.
"To solve" means a reaction where the active parts of the two constraints match.
active(F xis ~ xi) = F xis
active(tv ~ xi) = tv
active(D xis) = D xis
active(IP nm ty) = nm
At the moment we don't allow Wanteds to rewrite Wanteds, because that can give
rise to very confusing type error messages. A good example is Trac #8450.
Here's another
f :: a -> Bool
f x = ( [x,'c'], [x,True] ) `seq` True
Here we get
[W] a ~ Char
[W] a ~ Bool
but we do not want to complain about Bool ~ Char!
NB: either (a `canRewrite` b) or (b `canRewrite` a)
or a==b
must hold
canRewriteOrSame is similar but returns True for Wanted/Wanted.
See the call sites for explanations.
%************************************************************************
%* *
CtLoc
......
This diff is collapsed.
Cabal @ e3e3702a
Subproject commit a8b7cdf4ed6b8cd2dd6494b1b3f94d0bc3e53ffe
Subproject commit e3e3702a6997f9a431ca562156cf667c93bd0e5e
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