summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2012-05-09 15:50:54 +0100
committerSimon Peyton Jones <simonpj@microsoft.com>2012-05-09 15:50:54 +0100
commitf7e246b50a33c329e9730296f7a342e03bc3db72 (patch)
tree924efcefc93378a6b922a789a945ceff89a77d37 /compiler
parent4b089dbacd2a14f38a335103cf8ac0779d92f937 (diff)
parentff1061274c6c94ffe7c32f0801879a3619ed99a1 (diff)
downloadhaskell-f7e246b50a33c329e9730296f7a342e03bc3db72.tar.gz
Merge branch 'ghc-new-flavor'
Diffstat (limited to 'compiler')
-rw-r--r--compiler/coreSyn/CoreUtils.lhs10
-rw-r--r--compiler/deSugar/DsBinds.lhs110
-rw-r--r--compiler/typecheck/Inst.lhs72
-rw-r--r--compiler/typecheck/TcCanonical.lhs252
-rw-r--r--compiler/typecheck/TcErrors.lhs48
-rw-r--r--compiler/typecheck/TcEvidence.lhs70
-rw-r--r--compiler/typecheck/TcHsSyn.lhs29
-rw-r--r--compiler/typecheck/TcInstDcls.lhs4
-rw-r--r--compiler/typecheck/TcInteract.lhs369
-rw-r--r--compiler/typecheck/TcMType.lhs29
-rw-r--r--compiler/typecheck/TcRnTypes.lhs173
-rw-r--r--compiler/typecheck/TcSMonad.lhs639
-rw-r--r--compiler/typecheck/TcSimplify.lhs50
-rw-r--r--compiler/typecheck/TcUnify.lhs4
-rw-r--r--compiler/types/Coercion.lhs14
-rw-r--r--compiler/types/Type.lhs15
16 files changed, 1005 insertions, 883 deletions
diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index 8ec132f993..7858b20d54 100644
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -187,15 +187,7 @@ mkCast (Coercion e_co) co
-- The guard here checks that g has a (~#) on both sides,
-- otherwise decomposeCo fails. Can in principle happen
-- with unsafeCoerce
- = Coercion new_co
- where
- -- g :: (s1 ~# s2) ~# (t1 ~# t2)
- -- g1 :: s1 ~# t1
- -- g2 :: s2 ~# t2
- new_co = mkSymCo g1 `mkTransCo` e_co `mkTransCo` g2
- [_reflk, g1, g2] = decomposeCo 3 co
- -- Remember, (~#) :: forall k. k -> k -> *
- -- so it takes *three* arguments, not two
+ = Coercion (mkCoCast e_co co)
mkCast (Cast expr co2) co
= ASSERT(let { Pair from_ty _to_ty = coercionKind co;
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 8fc6bd91f3..eae9530b0e 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -18,7 +18,7 @@ lower levels it is preserved with @let@/@letrec@s).
-- for details
module DsBinds ( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec,
- dsHsWrapper, dsTcEvBinds, dsEvBinds, dsTcCoercion
+ dsHsWrapper, dsTcEvBinds, dsEvBinds
) where
#include "HsVersions.h"
@@ -32,7 +32,6 @@ import DsUtils
import HsSyn -- lots of things
import CoreSyn -- lots of things
-import HscTypes ( MonadThings )
import Literal ( Literal(MachStr) )
import CoreSubst
import MkCore
@@ -40,6 +39,8 @@ import CoreUtils
import CoreArity ( etaExpand )
import CoreUnfold
import CoreFVs
+import UniqSupply
+import Unique( Unique )
import Digraph
@@ -52,7 +53,7 @@ import TysWiredIn ( eqBoxDataCon, tupleCon )
import Id
import Class
import DataCon ( dataConWorkId )
-import Name ( Name, localiseName )
+import Name
import MkId ( seqId )
import Var
import VarSet
@@ -662,7 +663,7 @@ but it seems better to reject the program because it's almost certainly
a mistake. That's what the isDeadBinder call detects.
Note [Constant rule dicts]
-~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~
When the LHS of a specialisation rule, (/\as\ds. f es) has a free dict,
which is presumably in scope at the function definition site, we can quantify
over it too. *Any* dict with that type will do.
@@ -695,23 +696,23 @@ as the old one, but with an Internal name and no IdInfo.
\begin{code}
-dsHsWrapper :: MonadThings m => HsWrapper -> CoreExpr -> m CoreExpr
+dsHsWrapper :: HsWrapper -> CoreExpr -> DsM CoreExpr
dsHsWrapper WpHole e = return e
dsHsWrapper (WpTyApp ty) e = return $ App e (Type ty)
dsHsWrapper (WpLet ev_binds) e = do bs <- dsTcEvBinds ev_binds
return (mkCoreLets bs e)
dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 =<< dsHsWrapper c2 e
-dsHsWrapper (WpCast co) e = return $ dsTcCoercion co (mkCast e)
+dsHsWrapper (WpCast co) e = dsTcCoercion co (mkCast e)
dsHsWrapper (WpEvLam ev) e = return $ Lam ev e
dsHsWrapper (WpTyLam tv) e = return $ Lam tv e
dsHsWrapper (WpEvApp evtrm) e = liftM (App e) (dsEvTerm evtrm)
--------------------------------------
-dsTcEvBinds :: MonadThings m => TcEvBinds -> m [CoreBind]
+dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this
dsTcEvBinds (EvBinds bs) = dsEvBinds bs
-dsEvBinds :: MonadThings m => Bag EvBind -> m [CoreBind]
+dsEvBinds :: Bag EvBind -> DsM [CoreBind]
dsEvBinds bs = mapM ds_scc (sccEvBinds bs)
where
ds_scc (AcyclicSCC (EvBind v r)) = liftM (NonRec v) (dsEvTerm r)
@@ -726,39 +727,51 @@ sccEvBinds bs = stronglyConnCompFromEdgedVertices edges
edges = foldrBag ((:) . mk_node) [] bs
mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
- mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term)
+ mk_node b@(EvBind var term) = (b, var, varSetElems (evVarsOfTerm term))
---------------------------------------
-dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr
+dsEvTerm :: EvTerm -> DsM CoreExpr
dsEvTerm (EvId v) = return (Var v)
-dsEvTerm (EvCast v co)
- = return $ dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
- -- unnecessary to call varToCoreExpr v here.
+dsEvTerm (EvCast tm co)
+ = do { tm' <- dsEvTerm tm
+ ; dsTcCoercion co $ mkCast tm' }
+ -- 'v' is always a lifted evidence variable so it is
+ -- unnecessary to call varToCoreExpr v here.
+
dsEvTerm (EvKindCast v co)
- = return $ dsTcCoercion co $ (\_ -> Var v)
+ = do { v' <- dsEvTerm v
+ ; dsTcCoercion co $ (\_ -> v') }
-dsEvTerm (EvDFunApp df tys vars) = return (Var df `mkTyApps` tys `mkVarApps` vars)
-dsEvTerm (EvCoercion co) = return $ dsTcCoercion co mkEqBox
+dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
+ ; return (Var df `mkTyApps` tys `mkApps` tms') }
+dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox
dsEvTerm (EvTupleSel v n)
- = ASSERT( isTupleTyCon tc )
- return $
- Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')]
- where
- (tc, tys) = splitTyConApp (evVarPred v)
- Just [dc] = tyConDataCons_maybe tc
- v' = v `setVarType` ty_want
- xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after
- (tys_before, ty_want:tys_after) = splitAt n tys
-dsEvTerm (EvTupleMk vs) = return $ Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs
- where dc = tupleCon ConstraintTuple (length vs)
- tys = map varType vs
+ = do { tm' <- dsEvTerm v
+ ; let scrut_ty = exprType tm'
+ (tc, tys) = splitTyConApp scrut_ty
+ Just [dc] = tyConDataCons_maybe tc
+ xs = mkTemplateLocals tys
+ the_x = xs !! n
+ ; ASSERT( isTupleTyCon tc )
+ return $
+ Case tm' (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] }
+
+dsEvTerm (EvTupleMk tms)
+ = do { tms' <- mapM dsEvTerm tms
+ ; let tys = map exprType tms'
+ ; return $ Var (dataConWorkId dc) `mkTyApps` tys `mkApps` tms' }
+ where
+ dc = tupleCon ConstraintTuple (length tms)
+
dsEvTerm (EvSuperClass d n)
- = return $ Var sc_sel_id `mkTyApps` tys `App` Var d
+ = do { d' <- dsEvTerm d
+ ; let (cls, tys) = getClassPredTys (exprType d')
+ sc_sel_id = classSCSelId cls n -- Zero-indexed
+ ; return $ Var sc_sel_id `mkTyApps` tys `App` d' }
where
- sc_sel_id = classSCSelId cls n -- Zero-indexed
- (cls, tys) = getClassPredTys (evVarPred d)
+
dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg]
where
errorId = rUNTIME_ERROR_ID
@@ -770,7 +783,7 @@ dsEvTerm (EvLit l) =
EvStr s -> mkStringExprFS s
---------------------------------------
-dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr
+dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
-- This is the crucial function that moves
-- from TcCoercions to Coercions; see Note [TcCoercions] in Coercion
-- e.g. dsTcCoercion (trans g1 g2) k
@@ -778,22 +791,28 @@ dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr
-- case g2 of EqBox g2# ->
-- k (trans g1# g2#)
dsTcCoercion co thing_inside
- = foldr wrap_in_case result_expr eqvs_covs
- where
- result_expr = thing_inside (ds_tc_coercion subst co)
- result_ty = exprType result_expr
+ = do { us <- newUniqueSupply
+ ; let eqvs_covs :: [(EqVar,CoVar)]
+ eqvs_covs = zipWith mk_co_var (varSetElems (coVarsOfTcCo co))
+ (uniqsFromSupply us)
- -- We use the same uniques for the EqVars and the CoVars, and just change
- -- the type. So the CoVars shadow the EqVars
+ subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
+ result_expr = thing_inside (ds_tc_coercion subst co)
+ result_ty = exprType result_expr
- eqvs_covs :: [(EqVar,CoVar)]
- eqvs_covs = [(eqv, eqv `setIdType` mkCoercionType ty1 ty2)
- | eqv <- varSetElems (coVarsOfTcCo co)
- , let (ty1, ty2) = getEqPredTys (evVarPred eqv)]
- subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
-
- wrap_in_case (eqv, cov) body
+ ; return (foldr (wrap_in_case result_ty) result_expr eqvs_covs) }
+ where
+ mk_co_var :: Id -> Unique -> (Id, Id)
+ mk_co_var eqv uniq = (eqv, mkUserLocal occ uniq ty loc)
+ where
+ eq_nm = idName eqv
+ occ = nameOccName eq_nm
+ loc = nameSrcSpan eq_nm
+ ty = mkCoercionType ty1 ty2
+ (ty1, ty2) = getEqPredTys (evVarPred eqv)
+
+ wrap_in_case result_ty (eqv, cov) body
= Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
ds_tc_coercion :: CvSubst -> TcCoercion -> Coercion
@@ -816,6 +835,7 @@ ds_tc_coercion subst tc_co
go (TcNthCo n co) = mkNthCo n (go co)
go (TcInstCo co ty) = mkInstCo (go co) ty
go (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) co
+ go (TcCastCo co1 co2) = mkCoCast (go co1) (go co2)
go (TcCoVarCo v) = ds_ev_id subst v
ds_co_binds :: TcEvBinds -> CvSubst
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index d8ba828d9a..0b4364b7ee 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -83,10 +83,11 @@ emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
emitWanteds origin theta = mapM (emitWanted origin) theta
emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
-emitWanted origin pred = do { loc <- getCtLoc origin
- ; ev <- newWantedEvVar pred
- ; emitFlat (mkNonCanonical (Wanted loc ev))
- ; return ev }
+emitWanted origin pred
+ = do { loc <- getCtLoc origin
+ ; ev <- newWantedEvVar pred
+ ; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
+ ; return ev }
newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
-- Used when Name is the wired-in name for a wired-in class method,
@@ -530,7 +531,7 @@ tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CIrredEvCan { cc_ty = ty }) = tyVarsOfType ty
-tyVarsOfCt (CNonCanonical { cc_flavor = fl }) = tyVarsOfType (ctFlavPred fl)
+tyVarsOfCt (CNonCanonical { cc_ev = fl }) = tyVarsOfType (ctEvPred fl)
tyVarsOfCDict :: Ct -> TcTyVarSet
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
@@ -564,24 +565,22 @@ tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
---------------- Tidying -------------------------
tidyCt :: TidyEnv -> Ct -> Ct
+-- Used only in error reporting
-- Also converts it to non-canonical
tidyCt env ct
- = CNonCanonical { cc_flavor = tidy_flavor env (cc_flavor ct)
+ = CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
, cc_depth = cc_depth ct }
- where tidy_flavor :: TidyEnv -> CtFlavor -> CtFlavor
- tidy_flavor env (Given { flav_gloc = gloc, flav_evar = evar })
- = Given { flav_gloc = tidyGivenLoc env gloc
- , flav_evar = tidyEvVar env evar }
- tidy_flavor env (Solved { flav_gloc = gloc
- , flav_evar = evar })
- = Solved { flav_gloc = tidyGivenLoc env gloc
- , flav_evar = tidyEvVar env evar }
- tidy_flavor env (Wanted { flav_wloc = wloc
- , flav_evar = evar })
- = Wanted { flav_wloc = wloc -- Interesting: no tidying needed?
- , flav_evar = tidyEvVar env evar }
- tidy_flavor env (Derived { flav_wloc = wloc, flav_der_pty = pty })
- = Derived { flav_wloc = wloc, flav_der_pty = tidyType env pty }
+ where
+ tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence
+ -- NB: we do not tidy the ctev_evtm/var field because we don't
+ -- show it in error messages
+ tidy_flavor env ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
+ = ctev { ctev_gloc = tidyGivenLoc env gloc
+ , ctev_pred = tidyType env pred }
+ tidy_flavor env ctev@(Wanted { ctev_pred = pred })
+ = ctev { ctev_pred = tidyType env pred }
+ tidy_flavor env ctev@(Derived { ctev_pred = pred })
+ = ctev { ctev_pred = tidyType env pred }
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
@@ -604,6 +603,10 @@ tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
tidySkolemInfo _ info = info
---------------- Substitution -------------------------
+-- This is used only in TcSimpify, for substituations that are *also*
+-- reflected in the unification variables. So we don't substitute
+-- in the evidence.
+
substCt :: TvSubst -> Ct -> Ct
-- Conservatively converts it to non-canonical:
-- Postcondition: if the constraint does not get rewritten
@@ -611,9 +614,9 @@ substCt subst ct
| pty <- ctPred ct
, sty <- substTy subst pty
= if sty `eqType` pty then
- ct { cc_flavor = substFlavor subst (cc_flavor ct) }
+ ct { cc_ev = substFlavor subst (cc_ev ct) }
else
- CNonCanonical { cc_flavor = substFlavor subst (cc_flavor ct)
+ CNonCanonical { cc_ev = substFlavor subst (cc_ev ct)
, cc_depth = cc_depth ct }
substWC :: TvSubst -> WantedConstraints -> WantedConstraints
@@ -637,21 +640,16 @@ substImplication subst implic@(Implic { ic_skols = tvs
substEvVar :: TvSubst -> EvVar -> EvVar
substEvVar subst var = setVarType var (substTy subst (varType var))
-substFlavor :: TvSubst -> CtFlavor -> CtFlavor
-substFlavor subst (Given { flav_gloc = gloc, flav_evar = evar })
- = Given { flav_gloc = substGivenLoc subst gloc
- , flav_evar = substEvVar subst evar }
-substFlavor subst (Solved { flav_gloc = gloc, flav_evar = evar })
- = Solved { flav_gloc = substGivenLoc subst gloc
- , flav_evar = substEvVar subst evar }
-
-substFlavor subst (Wanted { flav_wloc = wloc, flav_evar = evar })
- = Wanted { flav_wloc = wloc
- , flav_evar = substEvVar subst evar }
-
-substFlavor subst (Derived { flav_wloc = wloc, flav_der_pty = pty })
- = Derived { flav_wloc = wloc
- , flav_der_pty = substTy subst pty }
+substFlavor :: TvSubst -> CtEvidence -> CtEvidence
+substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
+ = ctev { ctev_gloc = substGivenLoc subst gloc
+ , ctev_pred = substTy subst pred }
+
+substFlavor subst ctev@(Wanted { ctev_pred = pred })
+ = ctev { ctev_pred = substTy subst pred }
+
+substFlavor subst ctev@(Derived { ctev_pred = pty })
+ = ctev { ctev_pred = substTy subst pty }
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt)
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index d293f0ea3b..2e87c9e2f2 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -173,26 +173,26 @@ EvBinds, so we are again good.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canonicalize :: Ct -> TcS StopOrContinue
-canonicalize ct@(CNonCanonical { cc_flavor = fl, cc_depth = d })
+canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth = d })
= do { traceTcS "canonicalize (non-canonical)" (ppr ct)
; {-# SCC "canEvVar" #-}
canEvVar d fl (classifyPredType (ctPred ct)) }
canonicalize (CDictCan { cc_depth = d
- , cc_flavor = fl
+ , cc_ev = fl
, cc_class = cls
, cc_tyargs = xis })
= {-# SCC "canClass" #-}
canClass d fl cls xis -- Do not add any superclasses
canonicalize (CTyEqCan { cc_depth = d
- , cc_flavor = fl
+ , cc_ev = fl
, cc_tyvar = tv
, cc_rhs = xi })
= {-# SCC "canEqLeafTyVarLeftRec" #-}
canEqLeafTyVarLeftRec d fl tv xi
canonicalize (CFunEqCan { cc_depth = d
- , cc_flavor = fl
+ , cc_ev = fl
, cc_fun = fn
, cc_tyargs = xis1
, cc_rhs = xi2 })
@@ -200,18 +200,18 @@ canonicalize (CFunEqCan { cc_depth = d
canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
canonicalize (CIPCan { cc_depth = d
- , cc_flavor = fl
+ , cc_ev = fl
, cc_ip_nm = nm
, cc_ip_ty = xi })
= canIP d fl nm xi
-canonicalize (CIrredEvCan { cc_flavor = fl
+canonicalize (CIrredEvCan { cc_ev = fl
, cc_depth = d
, cc_ty = xi })
= canIrred d fl xi
canEvVar :: SubGoalDepth
- -> CtFlavor
+ -> CtEvidence
-> PredTree
-> TcS StopOrContinue
-- Called only for non-canonical EvVars
@@ -233,15 +233,16 @@ canEvVar d fl pred_classifier
\begin{code}
canTuple :: SubGoalDepth -- Depth
- -> CtFlavor -> [PredType] -> TcS StopOrContinue
+ -> CtEvidence -> [PredType] -> TcS StopOrContinue
canTuple d fl tys
= do { traceTcS "can_pred" (text "TuplePred!")
; let xcomp = EvTupleMk
xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
- ; xCtFlavor fl tys (XEvTerm xcomp xdecomp) what_next }
- where what_next fls = mapM_ add_to_work fls >> return Stop
- add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctFlavPred fl))
-
+ ; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp)
+ ; mapM_ add_to_work ctevs
+ ; return Stop }
+ where
+ add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctEvPred fl))
\end{code}
@@ -253,7 +254,7 @@ canTuple d fl tys
\begin{code}
canIP :: SubGoalDepth -- Depth
- -> CtFlavor
+ -> CtEvidence
-> IPName Name -> Type -> TcS StopOrContinue
-- Precondition: EvVar is implicit parameter evidence
canIP d fl nm ty
@@ -264,7 +265,7 @@ canIP d fl nm ty
; mb <- rewriteCtFlavor fl xi co
; case mb of
Just new_fl -> let IPPred _ xi_in = classifyPredType xi
- in continueWith $ CIPCan { cc_flavor = new_fl
+ in continueWith $ CIPCan { cc_ev = new_fl
, cc_ip_nm = nm, cc_ip_ty = xi_in
, cc_depth = d }
Nothing -> return Stop }
@@ -291,7 +292,7 @@ flattened in the first place to facilitate comparing them.)
\begin{code}
canClass, canClassNC
:: SubGoalDepth -- Depth
- -> CtFlavor
+ -> CtEvidence
-> Class -> [Type] -> TcS StopOrContinue
-- Precondition: EvVar is class evidence
@@ -314,14 +315,14 @@ canClass d fl cls tys
; case mb of
Just new_fl ->
- let (ClassPred cls xis_for_dict) = classifyPredType (ctFlavPred new_fl)
+ let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_fl)
in continueWith $
- CDictCan { cc_flavor = new_fl
+ CDictCan { cc_ev = new_fl
, cc_tyargs = xis_for_dict, cc_class = cls, cc_depth = d }
Nothing -> return Stop }
emitSuperclasses :: Ct -> TcS StopOrContinue
-emitSuperclasses ct@(CDictCan { cc_depth = d, cc_flavor = fl
+emitSuperclasses ct@(CDictCan { cc_depth = d, cc_ev = fl
, cc_tyargs = xis_new, cc_class = cls })
-- Add superclasses of this one here, See Note [Adding superclasses].
-- But only if we are not simplifying the LHS of a rule.
@@ -399,20 +400,19 @@ happen.
\begin{code}
newSCWorkFromFlavored :: SubGoalDepth -- Depth
- -> CtFlavor -> Class -> [Xi] -> TcS ()
+ -> CtEvidence -> Class -> [Xi] -> TcS ()
-- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored d flavor cls xis
| isDerived flavor
= return () -- Deriveds don't yield more superclasses because we will
-- add them transitively in the case of wanteds.
- | isSolved flavor
- = return ()
| isGiven flavor
= do { let sc_theta = immSuperClasses cls xis
xev = XEvTerm { ev_comp = panic "Can't compose for given!"
- , ev_decomp = \x->zipWith (\_ i->EvSuperClass x i) sc_theta [0..] }
- ; xCtFlavor flavor sc_theta xev (emit_sc_flavs d) }
+ , ev_decomp = \x -> zipWith (\_ i -> EvSuperClass x i) sc_theta [0..] }
+ ; ctevs <- xCtFlavor flavor sc_theta xev
+ ; emit_sc_flavs d ctevs }
| isEmptyVarSet (tyVarsOfTypes xis)
= return () -- Wanteds/Derived with no variables yield no deriveds.
@@ -422,15 +422,17 @@ newSCWorkFromFlavored d flavor cls xis
= do { let sc_rec_theta = transSuperClasses cls xis
impr_theta = filter is_improvement_pty sc_rec_theta
xev = panic "Derived's are not supposed to transform evidence!"
- ; xCtFlavor (Derived (flav_wloc flavor) (ctFlavPred flavor)) impr_theta xev $
- emit_sc_flavs d }
+ der_ev = Derived { ctev_wloc = ctev_wloc flavor, ctev_pred = ctev_pred flavor }
+ ; ctevs <- xCtFlavor der_ev impr_theta xev
+ ; emit_sc_flavs d ctevs }
-emit_sc_flavs :: SubGoalDepth -> [CtFlavor] -> TcS ()
+emit_sc_flavs :: SubGoalDepth -> [CtEvidence] -> TcS ()
emit_sc_flavs d fls
= do { traceTcS "newSCWorkFromFlavored" $
text "Emitting superclass work:" <+> ppr sc_cts
; updWorkListTcS $ appendWorkListCt sc_cts }
- where sc_cts = map (\fl -> CNonCanonical { cc_flavor = fl, cc_depth = d }) fls
+ where
+ sc_cts = map (\fl -> CNonCanonical { cc_ev = fl, cc_depth = d }) fls
is_improvement_pty :: PredType -> Bool
-- Either it's an equality, or has some functional dependency
@@ -454,7 +456,7 @@ is_improvement_pty ty = go (classifyPredType ty)
\begin{code}
canIrred :: SubGoalDepth -- Depth
- -> CtFlavor -> TcType -> TcS StopOrContinue
+ -> CtEvidence -> TcType -> TcS StopOrContinue
-- Precondition: ty not a tuple and no other evidence form
canIrred d fl ty
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
@@ -468,9 +470,9 @@ canIrred d fl ty
Just new_fl
| no_flattening
-> continueWith $
- CIrredEvCan { cc_flavor = new_fl, cc_ty = xi, cc_depth = d }
+ CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d }
| otherwise
- -> canEvVar d new_fl (classifyPredType (ctFlavPred new_fl))
+ -> canEvVar d new_fl (classifyPredType (ctEvPred new_fl))
Nothing -> return Stop }
\end{code}
@@ -529,7 +531,7 @@ data FlattenMode = FMSubstOnly
-- Flatten a bunch of types all at once.
flattenMany :: SubGoalDepth -- Depth
-> FlattenMode
- -> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion])
+ -> CtEvidence -> [Type] -> TcS ([Xi], [TcCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
-- NB: The EvVar inside the flavor is unused, we merely want Given/Solved/Derived/Wanted info
@@ -546,7 +548,7 @@ flattenMany d f ctxt tys
-- constraints. See Note [Flattening] for more detail.
flatten :: SubGoalDepth -- Depth
-> FlattenMode
- -> CtFlavor -> TcType -> TcS (Xi, TcCoercion)
+ -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
-- Postcondition: Coercion :: Xi ~ TcType
flatten d f ctxt ty
| Just ty' <- tcView ty
@@ -595,7 +597,8 @@ flatten d f fl (TyConApp tc tys)
do { flat_cache <- getFlatCache
; case lookupTM fam_ty flat_cache of
Just ct
- | cc_flavor ct `canRewrite` fl
+ | let ctev = cc_ev ct
+ , ctev `canRewrite` fl
-> -- 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
@@ -606,42 +609,42 @@ flatten d f fl (TyConApp tc tys)
-- For now I say we don't keep it fully rewritten.
do { traceTcS "flatten/flat-cache hit" $ ppr ct
; let rhs_xi = cc_rhs ct
- ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f (cc_flavor ct) rhs_xi
- ; let final_co = mkTcCoVarCo (ctId ct) `mkTcTransCo` (mkTcSymCo co)
+ ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f ctev rhs_xi
+ ; let final_co = evTermCoercion (ctEvTerm ctev)
+ `mkTcTransCo` mkTcSymCo co
; return (final_co, flat_rhs_xi,[]) }
- _ | isGivenOrSolved fl -- Given or Solved: make new flatten skolem
+ _ | isGiven fl -- Given: make new flatten skolem
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlattenSkolemTy fam_ty
- ; mg <- newGivenEvVar (mkTcEqPred fam_ty rhs_xi_var)
- (EvCoercion (mkTcReflCo fam_ty))
- ; case mg of
- Fresh eqv ->
- do { let new_fl = Given (flav_gloc fl) eqv
- ct = CFunEqCan { cc_flavor = new_fl
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_xi_var
- , cc_depth = d }
- -- Update the flat cache
- ; updFlatCache ct
- ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
- Cached {} -> panic "flatten TyConApp, var must be fresh!" }
+ ; let co = mkTcReflCo fam_ty
+ new_fl = Given { ctev_gloc = ctev_gloc fl
+ , ctev_pred = mkTcEqPred fam_ty rhs_xi_var
+ , ctev_evtm = EvCoercion co }
+ ct = CFunEqCan { cc_ev = new_fl
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_xi_var
+ , cc_depth = d }
+ -- Update the flat cache
+ ; updFlatCache ct
+ ; return (co, rhs_xi_var, [ct]) }
| otherwise -- Wanted or Derived: make new unification variable
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
- ; mw <- newWantedEvVar (mkTcEqPred fam_ty rhs_xi_var)
+ ; let pred = mkTcEqPred fam_ty rhs_xi_var
+ wloc = ctev_wloc fl
+ ; mw <- newWantedEvVar wloc pred
; case mw of
- Fresh eqv ->
- do { let new_fl = Wanted (flav_wloc fl) eqv
- ct = CFunEqCan { cc_flavor = new_fl
+ Fresh ctev ->
+ do { let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_depth = d }
-- Update the flat cache: just an optimisation!
; updFlatCache ct
- ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
+ ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var, [ct]) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
}
-- Emit the flat constraints
@@ -691,7 +694,7 @@ flatten d _f ctxt ty@(ForAllTy {})
\begin{code}
flattenTyVar :: SubGoalDepth
-> FlattenMode
- -> CtFlavor -> TcTyVar -> TcS (Xi, TcCoercion)
+ -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
-- "Flattening" a type variable means to apply the substitution to it
flattenTyVar d f ctxt tv
= do { ieqs <- getInertEqs
@@ -709,13 +712,15 @@ flattenTyVar d f ctxt tv
Just (co,ty) ->
do { (ty_final,co') <- flatten d f ctxt ty
; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }
- where tv_eq_subst subst tv
- | Just ct <- lookupVarEnv subst tv
- , cc_flavor ct `canRewrite` ctxt
- = Just (mkTcCoVarCo (ctId ct),cc_rhs ct)
- -- NB: even if ct is Derived we are not going to
- -- touch the actual coercion so we are fine.
- | otherwise = Nothing
+ where
+ tv_eq_subst subst tv
+ | Just ct <- lookupVarEnv subst tv
+ , let ctev = cc_ev ct
+ , ctev `canRewrite` ctxt
+ = Just (evTermCoercion (ctEvTerm ctev), cc_rhs ct)
+ -- NB: even if ct is Derived we are not going to
+ -- touch the actual coercion so we are fine.
+ | otherwise = Nothing
\end{code}
Note [Non-idempotent inert substitution]
@@ -765,13 +770,13 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
\begin{code}
canEqEvVarsCreated :: SubGoalDepth
- -> [CtFlavor] -> TcS StopOrContinue
+ -> [CtEvidence] -> TcS StopOrContinue
canEqEvVarsCreated _d [] = return Stop
canEqEvVarsCreated d (quad:quads)
= mapM_ (addToWork . do_quad) quads >> do_quad quad
-- Add all but one to the work list
-- and return the first (if any) for futher processing
- where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctFlavPred fl
+ where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctEvPred fl
in canEqNC d fl ty1 ty2
-- Note the "NC": these are fresh equalities so we must be
-- careful to add their kind constraints
@@ -779,7 +784,7 @@ canEqEvVarsCreated d (quad:quads)
-------------------------
canEqNC, canEq
:: SubGoalDepth
- -> CtFlavor
+ -> CtEvidence
-> Type -> Type -> TcS StopOrContinue
canEqNC d fl ty1 ty2
@@ -790,7 +795,7 @@ canEq _d fl ty1 ty2
| eqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
= if isWanted fl then
- setEvBind (flav_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
+ setEvBind (ctev_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
else
return Stop
@@ -823,11 +828,11 @@ canEq d fl ty1 ty2
-- Fail straight away for better error messages
then canEqFailure d fl
else
- let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map mkTcCoVarCo xs))
- xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (mkTcCoVarCo x)) tys1 [0..]
- xev = XEvTerm xcomp xdecomp
- in xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev (canEqEvVarsCreated d)
-
+ do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
+ xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
+ xev = XEvTerm xcomp xdecomp
+ ; ctevs <- xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev
+ ; canEqEvVarsCreated d ctevs }
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
@@ -839,7 +844,7 @@ canEq d fl ty1 ty2 -- e.g. F a b ~ Maybe c
canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2
- , Wanted loc orig_ev <- fl
+ , Wanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl
= do { let (tvs1,body1) = tcSplitForAllTys s1
(tvs2,body2) = tcSplitForAllTys s2
; if not (equalLength tvs1 tvs2) then
@@ -857,12 +862,12 @@ canEq d fl _ _ = canEqFailure d fl
------------------------
-- Type application
canEqAppTy :: SubGoalDepth
- -> CtFlavor
+ -> CtEvidence
-> Type -> Type -> Type -> Type
-> TcS StopOrContinue
canEqAppTy d fl s1 t1 s2 t2
= ASSERT( not (isKind t1) && not (isKind t2) )
- if isGivenOrSolved fl then
+ if isGiven fl then
do { traceTcS "canEq (app case)" $
text "Ommitting decomposition of given equality between: "
<+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
@@ -870,14 +875,14 @@ canEqAppTy d fl s1 t1 s2 t2
-- because we no longer have 'left' and 'right'
; return Stop }
else
- let xevcomp [x,y] = EvCoercion (mkTcAppCo (mkTcCoVarCo x) (mkTcCoVarCo y))
- xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
- xev = XEvTerm { ev_comp = xevcomp
- , ev_decomp = error "canEqAppTy: can't happen" }
- in xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev $
- canEqEvVarsCreated d
-
-canEqFailure :: SubGoalDepth -> CtFlavor -> TcS StopOrContinue
+ do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
+ xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
+ xev = XEvTerm { ev_comp = xevcomp
+ , ev_decomp = error "canEqAppTy: can't happen" }
+ ; ctevs <- xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev
+ ; canEqEvVarsCreated d ctevs }
+
+canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
canEqFailure d fl = emitFrozenError fl d >> return Stop
------------------------
@@ -885,12 +890,12 @@ emitKindConstraint :: Ct -> TcS StopOrContinue
emitKindConstraint ct
= case ct of
CTyEqCan { cc_depth = d
- , cc_flavor = fl, cc_tyvar = tv
+ , cc_ev = fl, cc_tyvar = tv
, cc_rhs = ty }
-> emit_kind_constraint d fl (mkTyVarTy tv) ty
CFunEqCan { cc_depth = d
- , cc_flavor = fl
+ , cc_ev = fl
, cc_fun = fn, cc_tyargs = xis1
, cc_rhs = xi2 }
-> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2
@@ -904,41 +909,43 @@ emitKindConstraint ct
| otherwise
= ASSERT( isKind k1 && isKind k2 )
do { kev <-
- do { mw <- newWantedEvVar (mkEqPred k1 k2)
+ do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2)
; case mw of
- Cached x -> return x
- Fresh x -> addToWork (canEq d (kind_co_fl x) k1 k2) >> return x }
- ; let xcomp [x] = mkEvKindCast x (mkTcCoVarCo kev)
+ Cached ev_tm -> return ev_tm
+ Fresh ctev -> do { addToWork (canEq d ctev k1 k2)
+ ; return (ctEvTerm ctev) } }
+
+ ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev)
xcomp _ = panic "emit_kind_constraint:can't happen"
- xdecomp x = [mkEvKindCast x (mkTcCoVarCo kev)]
+ xdecomp x = [mkEvKindCast x (evTermCoercion kev)]
xev = XEvTerm xcomp xdecomp
- in xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev what_next }
+
+ ; ctevs <- xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev
-- Important: Do not cache original as Solved since we are supposed to
-- solve /exactly/ the same constraint later! Example:
-- (alpha :: kappa0)
-- (T :: *)
-- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but
-- we don't want to say that (alpha ~ T) is now Solved!
- where
- what_next [new_fl] = continueWith (ct { cc_flavor = new_fl })
- what_next _ = return Stop
+ ; case ctevs of
+ [] -> return Stop
+ [new_ctev] -> continueWith (ct { cc_ev = new_ctev })
+ _ -> panic "emitKindConstraint" }
+ where
k1 = typeKind ty1
k2 = typeKind ty2
ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
+
-- Always create a Wanted kind equality even if
-- you are decomposing a given constraint.
-- NB: DV finds this reasonable for now. Maybe we have to revisit.
- kind_co_fl x
- | isGivenOrSolved fl
- = let (CtLoc _sk_info src_span err_ctxt) = flav_gloc fl
- orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
- ctloc = pushErrCtxtSameOrigin ctxt $
- CtLoc orig src_span err_ctxt
- in Wanted ctloc x
- | otherwise
- = Wanted (pushErrCtxtSameOrigin ctxt (flav_wloc fl)) x
-
+ kind_co_wloc = pushErrCtxtSameOrigin ctxt wanted_loc
+ wanted_loc = case fl of
+ Wanted { ctev_wloc = wloc } -> wloc
+ Derived { ctev_wloc = wloc } -> wloc
+ Given { ctev_gloc = gloc } -> setCtLocOrigin gloc orig
+ orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
\end{code}
Note [Combining insoluble constraints]
@@ -1106,7 +1113,7 @@ classify ty | Just ty' <- tcView ty
= OtherCls ty
-- See note [Canonical ordering for equality constraints].
-reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool
+reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool
-- (t1 `reOrient` t2) responds True
-- iff we should flip to (t2~t1)
-- We try to say False if possible, to minimise evidence generation
@@ -1143,7 +1150,7 @@ reOrient _fl (FskCls {}) (OtherCls {}) = False
------------------
canEqLeaf :: SubGoalDepth -- Depth
- -> CtFlavor
+ -> CtEvidence
-> Type -> Type
-> TcS StopOrContinue
-- Canonicalizing "leaf" equality constraints which cannot be
@@ -1156,13 +1163,16 @@ canEqLeaf :: SubGoalDepth -- Depth
canEqLeaf d fl s1 s2
| cls1 `re_orient` cls2
= do { traceTcS "canEqLeaf (reorienting)" $ ppr fl <+> dcolon <+> pprEq s1 s2
- ; let xcomp [x] = EvCoercion (mkTcSymCo (mkTcCoVarCo x))
+ ; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x))
xcomp _ = panic "canEqLeaf: can't happen"
- xdecomp x = [EvCoercion (mkTcSymCo (mkTcCoVarCo x))]
+ xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))]
xev = XEvTerm xcomp xdecomp
- what_next [fl] = canEqLeafOriented d fl s2 s1
- what_next _ = return Stop
- ; xCtFlavor fl [mkTcEqPred s2 s1] xev what_next }
+ ; ctevs <- xCtFlavor fl [mkTcEqPred s2 s1] xev
+ ; case ctevs of
+ [] -> return Stop
+ [ctev] -> canEqLeafOriented d ctev s2 s1
+ _ -> panic "canEqLeaf" }
+
| otherwise
= do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2)
; canEqLeafOriented d fl s1 s2 }
@@ -1172,7 +1182,7 @@ canEqLeaf d fl s1 s2
cls2 = classify s2
canEqLeafOriented :: SubGoalDepth -- Depth
- -> CtFlavor
+ -> CtEvidence
-> TcType -> TcType -> TcS StopOrContinue
-- By now s1 will either be a variable or a type family application
canEqLeafOriented d fl s1 s2
@@ -1184,10 +1194,10 @@ canEqLeafOriented d fl s1 s2
= canEqLeafTyVarLeftRec d fl tv s2
| otherwise
= pprPanic "canEqLeafOriented" $
- text "Non-variable or non-family equality LHS" <+> ppr (ctFlavPred fl)
+ text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred fl)
canEqLeafFunEqLeftRec :: SubGoalDepth
- -> CtFlavor
+ -> CtEvidence
-> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
canEqLeafFunEqLeftRec d fl (fn,tys1) ty2 -- fl :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
@@ -1210,7 +1220,7 @@ canEqLeafFunEqLeftRec d fl (fn,tys1) ty2 -- fl :: F tys1 ~ ty2
canEqLeafFunEqLeft :: SubGoalDepth -- Depth
- -> CtFlavor
+ -> CtEvidence
-> (TyCon,[Xi])
-> TcType -> TcS StopOrContinue
-- Precondition: No more flattening is needed for the LHS
@@ -1232,12 +1242,12 @@ canEqLeafFunEqLeft d fl (fn,xis1) s2
; case mb of
Nothing -> return Stop
Just new_fl -> continueWith $
- CFunEqCan { cc_flavor = new_fl, cc_depth = d
+ CFunEqCan { cc_ev = new_fl, cc_depth = d
, cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } }
canEqLeafTyVarLeftRec :: SubGoalDepth
- -> CtFlavor
+ -> CtEvidence
-> TcTyVar -> TcType -> TcS StopOrContinue
canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
@@ -1262,7 +1272,7 @@ canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
Nothing -> canEq d new_fl xi1 s2 }
canEqLeafTyVarLeft :: SubGoalDepth -- Depth
- -> CtFlavor
+ -> CtEvidence
-> TcTyVar -> TcType -> TcS StopOrContinue
-- Precondition LHS is fully rewritten from inerts (but not RHS)
canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
@@ -1276,7 +1286,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
-- Reflexivity exposed through flattening
; if tv_ty `eqType` xi2 then
- when (isWanted fl) (setEvBind (flav_evar fl) (EvCoercion co2)) >>
+ when (isWanted fl) (setEvBind (ctev_evar fl) (EvCoercion co2)) >>
return Stop
else do
-- Not reflexivity but maybe an occurs error
@@ -1291,7 +1301,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
; case mb of
Just new_fl -> if not_occ_err then
continueWith $
- CTyEqCan { cc_flavor = new_fl, cc_depth = d
+ CTyEqCan { cc_ev = new_fl, cc_depth = d
, cc_tyvar = tv, cc_rhs = xi2' }
else
canEqFailure d new_fl
@@ -1307,7 +1317,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
-- variable, then the same type is returned.
--
-- Precondition: the two types are not equal (looking though synonyms)
-canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
+canOccursCheck :: CtEvidence -> TcTyVar -> Xi -> TcS (Maybe Xi)
canOccursCheck _gw tv xi = return (expandAway tv xi)
\end{code}
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 020d42c1ba..483de071d4 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -158,17 +158,15 @@ reportTidyWanteds ctxt insols flats implics
deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg)
-> Ct -> TcM ()
deferToRuntime ev_binds_var ctxt mk_err_msg ct
- | fl <- cc_flavor ct
- , Wanted loc _ <- fl
+ | Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
= do { err <- setCtLoc loc $
mk_err_msg ctxt ct
- ; let ev_id = ctId ct -- Prec satisfied: Wanted
- err_msg = pprLocErrMsg err
+ ; let err_msg = pprLocErrMsg err
err_fs = mkFastString $ showSDoc $
err_msg $$ text "(deferred type error)"
-- Create the binding
- ; addTcEvBind ev_binds_var ev_id (EvDelayedError (idType ev_id) err_fs)
+ ; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs)
-- And emit a warning
; reportWarning (makeIntoWarning err) }
@@ -231,7 +229,7 @@ type Reporter = [Ct] -> TcM ()
mkReporter :: (Ct -> TcM ErrMsg) -> [Ct] -> TcM ()
-- Reports errors one at a time
-mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_flavor ct) $
+mkReporter mk_err = mapM_ (\ct -> do { err <- setCtFlavorLoc (cc_ev ct) $
mk_err ct;
; reportError err })
@@ -316,15 +314,15 @@ groupErrs mk_err (ct1 : rest)
; reportError err
; groupErrs mk_err others }
where
- flavor = cc_flavor ct1
+ flavor = cc_ev ct1
cts = ct1 : friends
(friends, others) = partition is_friend rest
- is_friend friend = cc_flavor friend `same_group` flavor
+ is_friend friend = cc_ev friend `same_group` flavor
- same_group :: CtFlavor -> CtFlavor -> Bool
- same_group (Given l1 _) (Given l2 _) = same_loc l1 l2
- same_group (Derived l1 _) (Derived l2 _) = same_loc l1 l2
- same_group (Wanted l1 _) (Wanted l2 _) = same_loc l1 l2
+ same_group :: CtEvidence -> CtEvidence -> Bool
+ same_group (Given {ctev_gloc = l1}) (Given {ctev_gloc = l2}) = same_loc l1 l2
+ same_group (Wanted {ctev_wloc = l1}) (Wanted {ctev_wloc = l2}) = same_loc l1 l2
+ same_group (Derived {ctev_wloc = l1}) (Derived {ctev_wloc = l2}) = same_loc l1 l2
same_group _ _ = False
same_loc :: CtLoc o -> CtLoc o -> Bool
@@ -425,7 +423,7 @@ mkEqErr _ [] = panic "mkEqErr"
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
-- Wanted constraints only!
mkEqErr1 ctxt ct
- = if isGivenOrSolved flav then
+ = if isGiven flav then
let ctx2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg flav }
in mkEqErr_help ctx2 ct False ty1 ty2
else
@@ -434,10 +432,11 @@ mkEqErr1 ctxt ct
; mk_err ctxt1 orig' }
where
- flav = cc_flavor ct
+ flav = cc_ev ct
- inaccessible_msg (Given loc _) = hang (ptext (sLit "Inaccessible code in"))
- 2 (ppr (ctLocOrigin loc))
+ inaccessible_msg (Given { ctev_gloc = loc })
+ = hang (ptext (sLit "Inaccessible code in"))
+ 2 (ppr (ctLocOrigin loc))
-- If a Solved then we should not report inaccessible code
inaccessible_msg _ = empty
@@ -571,7 +570,7 @@ misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
misMatchOrCND ctxt ct oriented ty1 ty2
| null givens ||
(isRigid ty1 && isRigid ty2) ||
- isGivenOrSolved (cc_flavor ct)
+ isGiven (cc_ev ct)
-- If the equality is unconditionally insoluble
-- or there is no context, don't report the context
= misMatchMsg oriented ty1 ty2
@@ -1066,7 +1065,7 @@ solverDepthErrorTcS depth stack
| null stack -- Shouldn't happen unless you say -fcontext-stack=0
= failWith msg
| otherwise
- = setCtFlavorLoc (cc_flavor top_item) $
+ = setCtFlavorLoc (cc_ev top_item) $
do { zstack <- mapM zonkCt stack
; env0 <- tcInitTidyEnv
; let zstack_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet zstack
@@ -1079,7 +1078,7 @@ solverDepthErrorTcS depth stack
, ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
{- DV: Changing this because Derived's no longer have ids ... Kind of a corner case ...
- = setCtFlavorLoc (cc_flavor top_item) $
+ = setCtFlavorLoc (cc_ev top_item) $
do { ev_vars <- mapM (zonkEvVar . cc_id) stack
; env0 <- tcInitTidyEnv
; let tidy_env = tidyFreeTyVars env0 (tyVarsOfEvVars ev_vars)
@@ -1092,7 +1091,7 @@ solverDepthErrorTcS depth stack
-}
-flattenForAllErrorTcS :: CtFlavor -> TcType -> TcM a
+flattenForAllErrorTcS :: CtEvidence -> TcType -> TcM a
flattenForAllErrorTcS fl ty
= setCtFlavorLoc fl $
do { env0 <- tcInitTidyEnv
@@ -1109,11 +1108,10 @@ flattenForAllErrorTcS fl ty
%************************************************************************
\begin{code}
-setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a
-setCtFlavorLoc (Wanted loc _) thing = setCtLoc loc thing
-setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing
-setCtFlavorLoc (Given loc _) thing = setCtLoc loc thing
-setCtFlavorLoc (Solved loc _) thing = setCtLoc loc thing
+setCtFlavorLoc :: CtEvidence -> TcM a -> TcM a
+setCtFlavorLoc (Wanted { ctev_wloc = loc }) thing = setCtLoc loc thing
+setCtFlavorLoc (Derived { ctev_wloc = loc }) thing = setCtLoc loc thing
+setCtFlavorLoc (Given { ctev_gloc = loc }) thing = setCtLoc loc thing
\end{code}
%************************************************************************
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 8ec0a5766b..82298a470b 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -17,7 +17,7 @@ module TcEvidence (
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
- EvLit(..),
+ EvLit(..), evTermCoercion,
-- TcCoercion
TcCoercion(..),
@@ -36,7 +36,7 @@ import Var
import PprCore () -- Instance OutputableBndr TyVar
import TypeRep -- Knows type representation
import TcType
-import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )
+import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe, getEqPredTys )
import TysPrim( funTyCon )
import TyCon
import PrelNames
@@ -102,6 +102,7 @@ data TcCoercion
| TcSymCo TcCoercion
| TcTransCo TcCoercion TcCoercion
| TcNthCo Int TcCoercion
+ | TcCastCo TcCoercion TcCoercion -- co1 |> co2
| TcLetCo TcEvBinds TcCoercion
deriving (Data.Data, Data.Typeable)
@@ -199,6 +200,8 @@ tcCoercionKind co = go co
where
go (TcRefl ty) = Pair ty ty
go (TcLetCo _ co) = go co
+ go (TcCastCo _ co) = case getEqPredTys (pSnd (go co)) of
+ (ty1,ty2) -> Pair ty1 ty2
go (TcTyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos)
go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
go (TcForAllCo tv co) = mkForAllTy tv <$> go co
@@ -206,8 +209,8 @@ tcCoercionKind co = go co
go (TcCoVarCo cv) = eqVarKind cv
go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax))
(substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
- go (TcSymCo co) = swap $ go co
- go (TcTransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
+ go (TcSymCo co) = swap (go co)
+ go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2))
go (TcNthCo d co) = tyConAppArgN d <$> go co
-- c.f. Coercion.coercionKind
@@ -219,7 +222,7 @@ eqVarKind cv
| Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
= ASSERT (tc `hasKey` eqTyConKey)
Pair ty1 ty2
- | otherwise = panic "eqVarKind, non coercion variable"
+ | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
coVarsOfTcCo :: TcCoercion -> VarSet
-- Only works on *zonked* coercions, because of TcLetCo
@@ -229,6 +232,7 @@ coVarsOfTcCo tc_co
go (TcRefl _) = emptyVarSet
go (TcTyConAppCo _ cos) = foldr (unionVarSet . go) emptyVarSet cos
go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2
+ go (TcCastCo co1 co2) = go co1 `unionVarSet` go co2
go (TcForAllCo _ co) = go co
go (TcInstCo co _) = go co
go (TcCoVarCo v) = unitVarSet v
@@ -263,7 +267,7 @@ liftTcCoSubstWith tvs cos ty
Nothing -> mkTcReflCo ty
go (AppTy t1 t2) = mkTcAppCo (go t1) (go t2)
go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
- go ty@(LitTy {}) = mkTcReflCo ty
+ go ty@(LitTy {}) = mkTcReflCo ty
go (ForAllTy tv ty) = mkTcForAllCo tv (go ty)
go (FunTy t1 t2) = mkTcFunCo (go t1) (go t2)
\end{code}
@@ -289,6 +293,8 @@ ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $
sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $
pprTcCo co1 <+> ppr_co TyConPrec co2
+ppr_co p (TcCastCo co1 co2) = maybeParen p FunPrec $
+ ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co
ppr_co p (TcInstCo co ty) = maybeParen p TyConPrec $
pprParendTcCo co <> ptext (sLit "@") <> pprType ty
@@ -454,24 +460,24 @@ data EvTerm
| EvCoercion TcCoercion -- (Boxed) coercion bindings
- | EvCast EvVar TcCoercion -- d |> co
+ | EvCast EvTerm TcCoercion -- d |> co
| EvDFunApp DFunId -- Dictionary instance application
- [Type] [EvVar]
+ [Type] [EvTerm]
- | EvTupleSel EvId Int -- n'th component of the tuple
+ | EvTupleSel EvTerm Int -- n'th component of the tuple, 0-indexed
- | EvTupleMk [EvId] -- tuple built from this stuff
+ | EvTupleMk [EvTerm] -- tuple built from this stuff
| EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
-- See Note [Deferring coercion errors to runtime]
-- in TcSimplify
- | EvSuperClass DictId Int -- n'th superclass. Used for both equalities and
+ | EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and
-- dictionaries, even though the former have no
-- selector Id. We count up from _0_
- | EvKindCast EvVar TcCoercion -- See Note [EvKindCast]
+ | EvKindCast EvTerm TcCoercion -- See Note [EvKindCast]
| EvLit EvLit -- Dictionary for class "SingI" for type lits.
-- Note [EvLit]
@@ -555,14 +561,14 @@ and another to make it into "SingI" evidence.
\begin{code}
-mkEvCast :: EvVar -> TcCoercion -> EvTerm
+mkEvCast :: EvTerm -> TcCoercion -> EvTerm
mkEvCast ev lco
- | isTcReflCo lco = EvId ev
+ | isTcReflCo lco = ev
| otherwise = EvCast ev lco
-mkEvKindCast :: EvVar -> TcCoercion -> EvTerm
+mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm
mkEvKindCast ev lco
- | isTcReflCo lco = EvId ev
+ | isTcReflCo lco = ev
| otherwise = EvKindCast ev lco
emptyTcEvBinds :: TcEvBinds
@@ -573,17 +579,27 @@ isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
-evVarsOfTerm :: EvTerm -> [EvVar]
-evVarsOfTerm (EvId v) = [v]
-evVarsOfTerm (EvCoercion co) = varSetElems (coVarsOfTcCo co)
-evVarsOfTerm (EvDFunApp _ _ evs) = evs
-evVarsOfTerm (EvTupleSel v _) = [v]
-evVarsOfTerm (EvSuperClass v _) = [v]
-evVarsOfTerm (EvCast v co) = v : varSetElems (coVarsOfTcCo co)
-evVarsOfTerm (EvTupleMk evs) = evs
-evVarsOfTerm (EvDelayedError _ _) = []
-evVarsOfTerm (EvKindCast v co) = v : varSetElems (coVarsOfTcCo co)
-evVarsOfTerm (EvLit _) = []
+evTermCoercion :: EvTerm -> TcCoercion
+-- Applied only to EvTerms of type (s~t)
+evTermCoercion (EvId v) = mkTcCoVarCo v
+evTermCoercion (EvCoercion co) = co
+evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co
+evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
+
+evVarsOfTerm :: EvTerm -> VarSet
+evVarsOfTerm (EvId v) = unitVarSet v
+evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co
+evVarsOfTerm (EvDFunApp _ _ evs) = evVarsOfTerms evs
+evVarsOfTerm (EvTupleSel v _) = evVarsOfTerm v
+evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
+evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
+evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs
+evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
+evVarsOfTerm (EvKindCast v co) = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v
+evVarsOfTerm (EvLit _) = emptyVarSet
+
+evVarsOfTerms :: [EvTerm] -> VarSet
+evVarsOfTerms = foldr (unionVarSet . evVarsOfTerm) emptyVarSet
\end{code}
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index aec09e914d..9104016938 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -1095,21 +1095,24 @@ zonkEvTerm env (EvId v) = ASSERT2( isId v, ppr v )
return (EvId (zonkIdOcc env v))
zonkEvTerm env (EvCoercion co) = do { co' <- zonkTcLCoToLCo env co
; return (EvCoercion co') }
-zonkEvTerm env (EvCast v co) = ASSERT( isId v)
- do { co' <- zonkTcLCoToLCo env co
- ; return (mkEvCast (zonkIdOcc env v) co') }
-
-zonkEvTerm env (EvKindCast v co) = ASSERT( isId v)
- do { co' <- zonkTcLCoToLCo env co
- ; return (mkEvKindCast (zonkIdOcc env v) co') }
-
-zonkEvTerm env (EvTupleSel v n) = return (EvTupleSel (zonkIdOcc env v) n)
-zonkEvTerm env (EvTupleMk vs) = return (EvTupleMk (map (zonkIdOcc env) vs))
+zonkEvTerm env (EvCast tm co) = do { tm' <- zonkEvTerm env tm
+ ; co' <- zonkTcLCoToLCo env co
+ ; return (mkEvCast tm' co') }
+
+zonkEvTerm env (EvKindCast v co) = do { v' <- zonkEvTerm env v
+ ; co' <- zonkTcLCoToLCo env co
+ ; return (mkEvKindCast v' co') }
+
+zonkEvTerm env (EvTupleSel tm n) = do { tm' <- zonkEvTerm env tm
+ ; return (EvTupleSel tm' n) }
+zonkEvTerm env (EvTupleMk tms) = do { tms' <- mapM (zonkEvTerm env) tms
+ ; return (EvTupleMk tms') }
zonkEvTerm _ (EvLit l) = return (EvLit l)
-zonkEvTerm env (EvSuperClass d n) = return (EvSuperClass (zonkIdOcc env d) n)
+zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
+ ; return (EvSuperClass d' n) }
zonkEvTerm env (EvDFunApp df tys tms)
= do { tys' <- zonkTcTypeToTypes env tys
- ; let tms' = map (zonkEvVarOcc env) tms
+ ; tms' <- mapM (zonkEvTerm env) tms
; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
zonkEvTerm env (EvDelayedError ty msg)
= do { ty' <- zonkTcTypeToType env ty
@@ -1344,6 +1347,8 @@ zonkTcLCoToLCo env co
go (TcAxiomInstCo ax tys) = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax tys') }
go (TcAppCo co1 co2) = do { co1' <- go co1; co2' <- go co2
; return (mkTcAppCo co1' co2') }
+ go (TcCastCo co1 co2) = do { co1' <- go co1; co2' <- go co2
+ ; return (TcCastCo co1' co2') }
go (TcSymCo co) = do { co' <- go co; return (mkTcSymCo co') }
go (TcNthCo n co) = do { co' <- go co; return (mkTcNthCo n co') }
go (TcTransCo co1 co2) = do { co1' <- go co1; co2' <- go co2
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 776689084f..bc217bb041 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -840,7 +840,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
mk_sc_ev_term sc
| null inst_tv_tys
, null dfun_ev_vars = EvId sc
- | otherwise = EvDFunApp sc inst_tv_tys dfun_ev_vars
+ | otherwise = EvDFunApp sc inst_tv_tys (map EvId dfun_ev_vars)
inst_tv_tys = mkTyVarTys inst_tyvars
arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
@@ -1141,7 +1141,7 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
; self_dict <- newDict clas inst_tys
; let self_ev_bind = EvBind self_dict
- (EvDFunApp dfun_id (mkTyVarTys tyvars) dfun_ev_vars)
+ (EvDFunApp dfun_id (mkTyVarTys tyvars) (map EvId dfun_ev_vars))
; (meth_id, local_meth_sig) <- mkMethIds sig_fn clas tyvars dfun_ev_vars
inst_tys sel_id
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 884331dbcc..44d6a8d01f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -31,7 +31,6 @@ import TyCon
import Name
import IParam
-import TysWiredIn ( eqTyCon )
import FunDeps
import TcEvidence
@@ -46,7 +45,6 @@ import Maybes( orElse )
import Bag
import Control.Monad ( foldM )
-import TrieMap
import VarEnv
import qualified Data.Traversable as Traversable
@@ -106,8 +104,11 @@ solveInteractGiven :: GivenLoc -> [EvVar] -> TcS (Bag Implication)
-- if this can happen in practice though.
solveInteractGiven gloc evs
= solveInteractCts (map mk_noncan evs)
- where mk_noncan ev = CNonCanonical { cc_flavor = Given gloc ev
- , cc_depth = 0 }
+ where
+ mk_noncan ev = CNonCanonical { cc_ev = Given { ctev_gloc = gloc
+ , ctev_evtm = EvId ev
+ , ctev_pred = evVarPred ev }
+ , cc_depth = 0 }
-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
@@ -229,13 +230,13 @@ thePipeline = [ ("lookup-in-inerts", lookupInInertsStage)
--------------------------------------------------------------------
lookupInInertsStage :: SimplifierStage
lookupInInertsStage ct
- | isWantedCt ct
+ | Wanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
= do { is <- getTcSInerts
- ; case lookupInInerts is (ctPred ct) of
- Just ct_cached
- | not (isDerivedCt ct_cached)
- -> setEvBind (ctId ct) (EvId (ctId ct_cached)) >>
- return Stop
+ ; case lookupInInerts is pred of
+ Just ctev
+ | not (isDerived ctev)
+ -> do { setEvBind ev_id (ctEvTerm ctev)
+ ; return Stop }
_ -> continueWith ct }
| otherwise -- I could do something like that for givens
-- as well I suppose but it is not a big deal
@@ -246,7 +247,6 @@ lookupInInertsStage ct
----------------------------------------------------------
canonicalizationStage :: SimplifierStage
canonicalizationStage = TcCanonical.canonicalize
-
\end{code}
*********************************************************************************
@@ -321,7 +321,7 @@ kickOutRewritableInerts ct
; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
rewriteInertEqsFromInertEq (cc_tyvar ct,
- ct_coercion,cc_flavor ct) ieqs
+ ct_coercion,cc_ev ct) ieqs
; let upd_eqs is = is { inert_cans = new_ics }
where ics = inert_cans is
new_ics = ics { inert_eqs = new_ieqs }
@@ -336,7 +336,7 @@ kickOutRewritableInerts ct
; traceTcS "Kick out" (ppr ct $$ ppr wl)
; updWorkListTcS (unionWorkList wl) }
-rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution
+rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtEvidence) -- A new substitution
-> TyVarEnv Ct -- All the inert equalities
-> TcS (TyVarEnv Ct) -- The new inert equalities
rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
@@ -366,7 +366,7 @@ rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
| otherwise -- Just keep it there
= return (Just ct)
where
- fl = cc_flavor ct
+ fl = cc_ev ct
kick_out_rewritable :: Ct
-> InertSet
@@ -401,7 +401,7 @@ kick_out_rewritable ct is@(IS { inert_cans =
-- inert_solved, inert_flat_cache and inert_solved_funeqs
-- optimistically. But when we lookup we have to take the
-- subsitution into account
- fl = cc_flavor ct
+ fl = cc_ev ct
tv = cc_tyvar ct
(ips_out, ips_in) = partitionCCanMap rewritable ipmap
@@ -412,7 +412,7 @@ kick_out_rewritable ct is@(IS { inert_cans =
(irs_out, irs_in) = partitionBag rewritable irreds
(fro_out, fro_in) = partitionBag rewritable frozen
- rewritable ct = (fl `canRewrite` cc_flavor ct) &&
+ rewritable ct = (fl `canRewrite` cc_ev ct) &&
(tv `elemVarSet` tyVarsOfCt ct)
-- NB: tyVarsOfCt will return the type
-- variables /and the kind variables/ that are
@@ -461,9 +461,9 @@ data SPSolveResult = SPCantSolve
-- touchable unification variable.
-- See Note [Touchables and givens]
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
-trySpontaneousSolve workItem@(CTyEqCan { cc_flavor = gw
+trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
, cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
- | isGivenOrSolved gw
+ | isGiven gw
= return SPCantSolve
| Just tv2 <- tcGetTyVar_maybe xi
= do { tch1 <- isTouchableMetaTyVar tv1
@@ -488,7 +488,7 @@ trySpontaneousSolve _ = return SPCantSolve
----------------
trySpontaneousEqOneWay :: SubGoalDepth
- -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
+ -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay d gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
@@ -498,7 +498,7 @@ trySpontaneousEqOneWay d gw tv xi
----------------
trySpontaneousEqTwoWay :: SubGoalDepth
- -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
+ -> CtEvidence -> TcTyVar -> TcTyVar -> TcS SPSolveResult
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
trySpontaneousEqTwoWay d gw tv1 tv2
@@ -585,10 +585,10 @@ unification variables as RHS of type family equations: F xis ~ alpha.
----------------
solveWithIdentity :: SubGoalDepth
- -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
+ -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-- Solve with the identity coercion
-- Precondition: kind(xi) is a sub-kind of kind(tv)
--- Precondition: CtFlavor is Wanted or Derived
+-- Precondition: CtEvidence is Wanted or Derived
-- See [New Wanted Superclass Work] to see why solveWithIdentity
-- must work for Derived as well as Wanted
-- Returns: workItem where
@@ -607,17 +607,18 @@ solveWithIdentity d wd tv xi
-- cf TcUnify.uUnboundKVar
; setWantedTyBind tv xi'
- ; let refl_xi = mkTcReflCo xi'
+ ; let refl_evtm = EvCoercion (mkTcReflCo xi')
+ refl_pred = mkTcEqPred tv_ty xi'
; when (isWanted wd) $
- setEvBind (flav_evar wd) (EvCoercion refl_xi)
+ setEvBind (ctev_evar wd) refl_evtm
- ; ev_given <- newGivenEvVar (mkTcEqPred tv_ty xi')
- (EvCoercion refl_xi) >>= (return . mn_thing)
- ; let given_fl = Given (mkGivenLoc (flav_wloc wd) UnkSkol) ev_given
+ ; let given_fl = Given { ctev_gloc = mkGivenLoc (ctev_wloc wd) UnkSkol
+ , ctev_pred = refl_pred
+ , ctev_evtm = refl_evtm }
; return $
- SPSolved (CTyEqCan { cc_flavor = given_fl
+ SPSolved (CTyEqCan { cc_ev = given_fl
, cc_tyvar = tv, cc_rhs = xi', cc_depth = d }) }
\end{code}
@@ -654,7 +655,7 @@ or, equivalently,
then there is no reaction
\begin{code}
--- Interaction result of WorkItem <~> AtomicInert
+-- Interaction result of WorkItem <~> Ct
data InteractResult
= IRWorkItemConsumed { ir_fire :: String }
@@ -715,8 +716,8 @@ interactWithInertsStage wi
doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
doInteractWithInert
- inertItem@(CDictCan { cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
- workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
+ inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 })
+ workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 })
| cls1 == cls2
= do { let pty1 = mkClassPred cls1 tys1
@@ -728,13 +729,13 @@ doInteractWithInert
, text "workItem = " <+> ppr workItem ])
; any_fundeps
- <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
+ <- if isGiven fl1 && isGiven fl2 then return Nothing
-- NB: We don't create fds for given (and even solved), have not seen a useful
-- situation for these and even if we did we'd have to be very careful to only
-- create Derived's and not Wanteds.
else do { let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
- ; wloc <- get_workitem_wloc fl2
+ wloc = getWantedLoc fl2
; rewriteWithFunDeps fd_eqns tys2 wloc }
-- See Note [Efficient Orientation], [When improvement happens]
@@ -745,23 +746,18 @@ doInteractWithInert
| otherwise -> irKeepGoing "NOP"
-- Actual Functional Dependencies
- Just (_rewritten_tys2,_cos2,fd_work)
+ Just (_rewritten_tys2, fd_work)
-- Standard thing: create derived fds and keep on going. Importantly we don't
-- throw workitem back in the worklist because this can cause loops. See #5236.
-> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert
}
- where get_workitem_wloc (Wanted wl _) = return wl
- get_workitem_wloc (Derived wl _) = return wl
- get_workitem_wloc _ = pprPanic "Unexpected given workitem!" $
- vcat [ text "Work item =" <+> ppr workItem
- , text "Inert item=" <+> ppr inertItem]
-
+
-- Two pieces of irreducible evidence: if their types are *exactly identical*
-- we can rewrite them. We can never improve using this:
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
-- mean that (ty1 ~ ty2)
-doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 })
+doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 })
workItem@(CIrredEvCan { cc_ty = ty2 })
| ty1 `eqType` ty2
= solveOneFromTheOther "Irred/Irred" ifl workItem
@@ -771,9 +767,9 @@ doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 })
-- that equates the type (this is "improvement").
-- However, we don't actually need the coercion evidence,
-- so we just generate a fresh coercion variable that isn't used anywhere.
-doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
- workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
- | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
+doInteractWithInert (CIPCan { cc_ev = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
+ workItem@(CIPCan { cc_ev = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
+ | nm1 == nm2 && isGiven wfl && isGiven ifl
= -- See Note [Overriding implicit parameters]
-- Dump the inert item, override totally with the new one
-- Do not require type equality
@@ -786,44 +782,43 @@ doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
| nm1 == nm2
= -- See Note [When improvement happens]
- do { mb_eqv <- newWantedEvVar (mkEqPred ty2 ty1)
+ do { mb_eqv <- newWantedEvVar new_wloc (mkEqPred ty2 ty1)
-- co :: ty2 ~ ty1, see Note [Efficient orientation]
; cv <- case mb_eqv of
Fresh eqv ->
do { updWorkListTcS $ extendWorkListEq $
- CNonCanonical { cc_flavor = Wanted new_wloc eqv
+ CNonCanonical { cc_ev = eqv
, cc_depth = cc_depth workItem }
- ; return eqv }
+ ; return (ctEvTerm eqv) }
Cached eqv -> return eqv
; case wfl of
- Wanted {} ->
- let ip_co = mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv]
- in do { setEvBind (ctId workItem) $
- mkEvCast (flav_evar ifl) (mkTcSymCo ip_co)
+ Wanted { ctev_evar = ev_id } ->
+ let ip_co = mkTcTyConAppCo (ipTyCon nm1) [evTermCoercion cv]
+ in do { setEvBind ev_id $
+ mkEvCast (ctEvTerm ifl) (mkTcSymCo ip_co)
; irWorkItemConsumed "IP/IP (solved by rewriting)" }
_ -> pprPanic "Unexpected IP constraint" (ppr workItem) }
- where new_wloc
- | Wanted wl _ <- wfl = wl
- | Derived wl _ <- wfl = wl
- | Wanted wl _ <- ifl = wl
- | Derived wl _ <- ifl = wl
- | otherwise = panic "Solve IP: no WantedLoc!"
-
+ where
+ new_wloc | isGiven wfl = getWantedLoc ifl
+ | otherwise = getWantedLoc wfl
-doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
+doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
, cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 })
- wi@(CFunEqCan { cc_flavor = fl2, cc_fun = tc2
+ wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
+{- ToDo: Check with Dimitrios
| lhss_match
, isSolved fl1 -- Inert is solved and we can simply ignore it
-- when workitem is given/solved
- , isGivenOrSolved fl2
+ , isGiven fl2
= irInertConsumed "FunEq/FunEq"
| lhss_match
, isSolved fl2 -- Workitem is solved and we can ignore it when
-- the inert is given/solved
- , isGivenOrSolved fl1
+ , isGiven fl1
= irWorkItemConsumed "FunEq/FunEq"
+-}
+
| fl1 `canSolve` fl2 && lhss_match
= do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
@@ -836,10 +831,12 @@ doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
-- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
- ; xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev $ what_next d2
+ ; ctevs <- xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev
-- Why not simply xCtFlavor? See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
+ ; add_to_work d2 ctevs
; irWorkItemConsumed "FunEq/FunEq" }
+
| fl2 `canSolve` fl1 && lhss_match
= do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
@@ -847,25 +844,26 @@ doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
; let xev = XEvTerm xcomp xdecomp
-- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)]
- xcomp [x] = EvCoercion (co2 `mkTcTransCo` mkTcCoVarCo x)
+ xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x)
xcomp _ = panic "No more goals!"
-- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
- xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` mkTcCoVarCo x)]
+ xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
- ; xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev $ what_next d1
+ ; ctevs <- xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev
-- Why not simply xCtFlavor? See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
+ ; add_to_work d1 ctevs
; irInertConsumed "FunEq/FunEq"}
where
+ add_to_work d [ctev] = updWorkListTcS $ extendWorkListEq $
+ CNonCanonical {cc_ev = ctev, cc_depth = d}
+ add_to_work _ _ = return ()
+
lhss_match = tc1 == tc2 && eqTypes args1 args2
- what_next d [new_fl]
- = updWorkListTcS $
- extendWorkListEq (CNonCanonical {cc_flavor=new_fl,cc_depth = d})
- what_next _ _ = return ()
- co1 = mkTcCoVarCo $ flav_evar fl1
- co2 = mkTcCoVarCo $ flav_evar fl2
- mk_sym_co x = mkTcSymCo (mkTcCoVarCo x)
+ co1 = evTermCoercion $ ctEvTerm fl1
+ co2 = evTermCoercion $ ctEvTerm fl2
+ mk_sym_co x = mkTcSymCo (evTermCoercion x)
doInteractWithInert _ _ = irKeepGoing "NOP"
@@ -905,7 +903,7 @@ solving.
\begin{code}
solveOneFromTheOther :: String -- Info
- -> CtFlavor -- Inert
+ -> CtEvidence -- Inert
-> Ct -- WorkItem
-> TcS InteractResult
-- Preconditions:
@@ -920,22 +918,23 @@ solveOneFromTheOther info ifl workItem
-- so it's safe to continue on from this point
= irInertConsumed ("Solved[DI] " ++ info)
- | isSolved ifl, isGivenOrSolved wfl
+{- ToDo: Check with Dimitrios
+ | isSolved ifl, isGiven wfl
-- Same if the inert is a GivenSolved -- just get rid of it
= irInertConsumed ("Solved[SI] " ++ info)
+-}
| otherwise
= ASSERT( ifl `canSolve` wfl )
-- Because of Note [The Solver Invariant], plus Derived dealt with
- do { when (isWanted wfl) $ setEvBind wid (EvId iid)
+ do { case wfl of
+ Wanted { ctev_evar = ev_id } -> setEvBind ev_id (ctEvTerm ifl)
+ _ -> return ()
-- Overwrite the binding, if one exists
-- If both are Given, we already have evidence; no need to duplicate
; irWorkItemConsumed ("Solved " ++ info) }
where
- wfl = cc_flavor workItem
- wid = ctId workItem
- iid = flav_evar ifl
-
+ wfl = cc_ev workItem
\end{code}
Note [Superclasses and recursive dictionaries]
@@ -1305,7 +1304,7 @@ now!).
rewriteWithFunDeps :: [Equation]
-> [Xi]
-> WantedLoc
- -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)]))
+ -> TcS (Maybe ([Xi], [CtEvidence]))
-- Not quite a WantedEvVar unfortunately
-- Because our intention could be to make
-- it derived at the end of the day
@@ -1313,13 +1312,13 @@ rewriteWithFunDeps :: [Equation]
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
rewriteWithFunDeps eqn_pred_locs xis wloc
= do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
- ; let fd_ev_pos :: [(Int,(EqVar,WantedLoc))]
+ ; let fd_ev_pos :: [(Int,CtEvidence)]
fd_ev_pos = concat fd_ev_poss
- (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+ rewritten_xis = rewriteDictParams fd_ev_pos xis
; if null fd_ev_pos then return Nothing
- else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
+ else return (Just (rewritten_xis, map snd fd_ev_pos)) }
-instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
+instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)]
-- Post: Returns the position index as well as the corresponding FunDep equality
instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
@@ -1332,10 +1331,10 @@ instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
= let sty1 = Type.substTy subst ty1
sty2 = Type.substTy subst ty2
in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
- else do { mb_eqv <- newWantedEvVar (mkTcEqPred sty1 sty2)
+ else do { mb_eqv <- newDerived (push_ctx wl) (mkTcEqPred sty1 sty2)
; case mb_eqv of
- Fresh eqv -> return $ (i,(eqv, push_ctx wl)):ievs
- Cached {} -> return ievs }
+ Just ctev -> return $ (i,ctev):ievs
+ Nothing -> return ievs }
-- We are eventually going to emit FD work back in the work list so
-- it is important that we only return the /freshly created/ and not
-- some existing equality!
@@ -1355,34 +1354,30 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
-rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
- -> [Type] -- A sequence of types: tys
- -> [(Type, TcCoercion)] -- Returns: [(ty', co : ty' ~ ty)]
+rewriteDictParams :: [(Int,CtEvidence)] -- A set of coercions : (pos, ty' ~ ty)
+ -> [Type] -- A sequence of types: tys
+ -> [Type]
rewriteDictParams param_eqs tys
= zipWith do_one tys [0..]
where
- do_one :: Type -> Int -> (Type, TcCoercion)
+ do_one :: Type -> Int -> Type
do_one ty n = case lookup n param_eqs of
- Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev))
- Nothing -> (ty, mkTcReflCo ty) -- Identity
+ Just wev -> get_fst_ty wev
+ Nothing -> ty
- get_fst_ty (wev,_wloc)
- | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev )
+ get_fst_ty ctev
+ | Just (ty1, _) <- getEqPredTys_maybe (ctEvPred ctev)
= ty1
| otherwise
= panic "rewriteDictParams: non equality fundep!?"
-emitFDWorkAsDerived :: [(EvVar,WantedLoc)]
+emitFDWorkAsDerived :: [CtEvidence] -- All Derived
-> SubGoalDepth -> TcS ()
emitFDWorkAsDerived evlocs d
- = updWorkListTcS $ appendWorkListEqs fd_cts
- where fd_cts = map mk_fd_ct evlocs
- mk_fd_ct (v,wl)
- = CNonCanonical { cc_flavor = Derived wl (evVarPred v)
- , cc_depth = d }
-
-
+ = updWorkListTcS $ appendWorkListEqs (map mk_fd_ct evlocs)
+ where
+ mk_fd_ct der_ev = CNonCanonical { cc_ev = der_ev, cc_depth = d }
\end{code}
@@ -1432,11 +1427,11 @@ doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
-- Given dictionary
-- See Note [Given constraint that matches an instance declaration]
-doTopReact _inerts (CDictCan { cc_flavor = Given {} })
+doTopReact _inerts (CDictCan { cc_ev = Given {} })
= return NoTopInt -- NB: Superclasses already added since it's canonical
-- Derived dictionary: just look for functional dependencies
-doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
+doTopReact _inerts workItem@(CDictCan { cc_ev = Derived loc _pty
, cc_class = cls, cc_tyargs = xis })
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
@@ -1444,7 +1439,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
; m <- rewriteWithFunDeps fd_eqns xis loc
; case m of
Nothing -> return NoTopInt
- Just (xis',_,fd_work) ->
+ Just (xis', fd_work) ->
let workItem' = workItem { cc_tyargs = xis' }
-- Deriveds are not supposed to have identity
in do { emitFDWorkAsDerived fd_work (cc_depth workItem)
@@ -1454,7 +1449,7 @@ doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc _pty
}
-- Wanted dictionary
-doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id)
+doTopReact inerts workItem@(CDictCan { cc_ev = fl@(Wanted { ctev_wloc = loc, ctev_evar = dict_id })
, cc_class = cls, cc_tyargs = xis
, cc_depth = depth })
-- See Note [MATCHING-SYNONYMS]
@@ -1470,108 +1465,103 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc dict_id)
Nothing ->
do { lkup_inst_res <- matchClassInst inerts cls xis loc
; case lkup_inst_res of
- GenInst wtvs ev_term
- -> let sfl = Solved (mkSolvedLoc loc UnkSkol) dict_id
- in addToSolved (workItem { cc_flavor = sfl }) >>
- doSolveFromInstance wtvs ev_term
- NoInstance
- -> return NoTopInt
+ GenInst wtvs ev_term -> do { addToSolved fl
+ ; doSolveFromInstance wtvs ev_term }
+ NoInstance -> return NoTopInt
}
-- Actual Functional Dependencies
- Just (_xis',_cos,fd_work) ->
+ Just (_xis', fd_work) ->
do { emitFDWorkAsDerived fd_work (cc_depth workItem)
; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
, tir_new_item = ContinueWith workItem } } }
- where doSolveFromInstance :: [EvVar] -> EvTerm -> TcS TopInteractResult
- -- Precondition: evidence term matches the predicate workItem
- doSolveFromInstance evs ev_term
- | null evs
- = do { traceTcS "doTopReact/found nullary instance for" $
- ppr dict_id
- ; setEvBind dict_id ev_term
- ; return $
- SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
- , tir_new_item = Stop } }
- | otherwise
- = do { traceTcS "doTopReact/found non-nullary instance for" $
- ppr dict_id
- ; setEvBind dict_id ev_term
- ; let mk_new_wanted ev
- = CNonCanonical { cc_flavor = fl { flav_evar = ev }
- , cc_depth = depth + 1 }
- ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
- ; return $
- SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
- , tir_new_item = Stop }
- }
+ where
+ doSolveFromInstance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
+ -- Precondition: evidence term matches the predicate workItem
+ doSolveFromInstance evs ev_term
+ | null evs
+ = do { traceTcS "doTopReact/found nullary instance for" $
+ ppr dict_id
+ ; setEvBind dict_id ev_term
+ ; return $
+ SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
+ , tir_new_item = Stop } }
+ | otherwise
+ = do { traceTcS "doTopReact/found non-nullary instance for" $
+ ppr dict_id
+ ; setEvBind dict_id ev_term
+ ; let mk_new_wanted ev
+ = CNonCanonical { cc_ev = ev
+ , cc_depth = depth + 1 }
+ ; updWorkListTcS (appendWorkListCt (map mk_new_wanted evs))
+ ; return $
+ SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
+ , tir_new_item = Stop }
+ }
-- Type functions
-doTopReact _inerts (CFunEqCan { cc_flavor = fl })
+{- ToDo: Check with Dimitrios
+doTopReact _inerts (CFunEqCan { cc_ev = fl })
| isSolved fl
= return NoTopInt -- If Solved, no more interactions should happen
+-}
-- Otherwise, it's a Given, Derived, or Wanted
-doTopReact _inerts workItem@(CFunEqCan { cc_flavor = fl, cc_depth = d
+doTopReact _inerts workItem@(CFunEqCan { cc_ev = fl, cc_depth = d
, cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
= ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
; case match_res of
Nothing -> return NoTopInt
Just (famInst, rep_tys)
- -> do { mb_already_solved <- lkpFunEqCache (mkTyConApp tc args)
+ -> do { mb_already_solved <- lkpSolvedFunEqCache (mkTyConApp tc args)
; traceTcS "doTopReact: Family instance matches" $
vcat [ text "solved-fun-cache" <+> if isJust mb_already_solved then text "hit" else text "miss"
, text "workItem =" <+> ppr workItem ]
; let (coe,rhs_ty)
- | Just cached_ct <- mb_already_solved
- = (mkTcCoVarCo (ctId cached_ct),
- cc_rhs cached_ct)
+ | Just ctev <- mb_already_solved
+ , not (isDerived ctev)
+ = ASSERT( isEqPred (ctEvPred ctev) )
+ (evTermCoercion (ctEvTerm ctev), snd (getEqPredTys (ctEvPred ctev)))
| otherwise
= let coe_ax = famInstAxiom famInst
in (mkTcAxInstCo coe_ax rep_tys,
mkAxInstRHS coe_ax rep_tys)
- xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` mkTcCoVarCo x)]
- xcomp [x] = EvCoercion (coe `mkTcTransCo` mkTcCoVarCo x)
+ xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
+ xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
xcomp _ = panic "No more goals!"
xev = XEvTerm xcomp xdecomp
- ; xCtFlavor fl [mkTcEqPred rhs_ty xi] xev what_next } }
- where what_next [ct_flav]
- = do { updWorkListTcS $
- extendWorkListEq (CNonCanonical { cc_flavor = ct_flav
- , cc_depth = d+1 })
- ; cache_in_solved fl
- ; return $ SomeTopInt { tir_rule = "Fun/Top"
- , tir_new_item = Stop } }
- what_next _ -- No subgoal (because it's cached)
- = do { cache_in_solved fl
- ; return $ SomeTopInt { tir_rule = "Fun/Top"
- , tir_new_item = Stop } }
-
- cache_in_solved (Derived {}) = return ()
- cache_in_solved (Wanted wl ev) =
- let sfl = Solved (mkSolvedLoc wl UnkSkol) ev
- solved = workItem { cc_flavor = sfl }
- in updFunEqCache solved >> addToSolved solved
- cache_in_solved fl =
- let sfl = Solved (flav_gloc fl) (flav_evar fl)
- solved = workItem { cc_flavor = sfl }
- in updFunEqCache solved >> addToSolved solved
+ ; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
+ ; case ctevs of
+ [ctev] -> updWorkListTcS $ extendWorkListEq $
+ CNonCanonical { cc_ev = ctev
+ , cc_depth = d+1 }
+ ctevs -> -- No subgoal (because it's cached)
+ ASSERT( null ctevs) return ()
+
+ ; unless (isDerived fl) $
+ do { addSolvedFunEq fl
+ ; addToSolved fl }
+ ; return $ SomeTopInt { tir_rule = "Fun/Top"
+ , tir_new_item = Stop } } }
-- Any other work item does not react with any top-level equations
doTopReact _inerts _workItem = return NoTopInt
-lkpFunEqCache :: TcType -> TcS (Maybe Ct)
-lkpFunEqCache fam_head
+lkpSolvedFunEqCache :: TcType -> TcS (Maybe CtEvidence)
+lkpSolvedFunEqCache fam_head
= do { (_subst,_inscope) <- getInertEqs
; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
; traceTcS "lkpFunEqCache" $ vcat [ text "fam_head =" <+> ppr fam_head
- , text "funeq cache =" <+> pprCtTypeMap (unCtFamHeadMap fun_cache) ]
- ; rewrite_cached $
- lookupTM fam_head (unCtFamHeadMap fun_cache) }
+ , text "funeq cache =" <+> ppr fun_cache ]
+ ; return (lookupFamHead fun_cache fam_head) }
+
+{- ToDo; talk to Dimitrios. I have no idea what is happening here
+
+ ; rewrite_cached (lookupFamHead fun_cache fam_head) }
-- The two different calls do not seem to make a significant difference in
-- terms of hit/miss rate for many memory-critical/performance tests but the
-- latter blows up the space on the heap somehow ... It maybe the niFixTvSubst.
@@ -1579,11 +1569,10 @@ lkpFunEqCache fam_head
-- lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) }
where rewrite_cached Nothing = return Nothing
- rewrite_cached (Just ct@(CFunEqCan { cc_flavor = fl, cc_depth = d
+ rewrite_cached (Just ct@(CFunEqCan { cc_ev = fl, cc_depth = d
, cc_fun = tc, cc_tyargs = xis
, cc_rhs = xi}))
- = ASSERT (isSolved fl)
- do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis
+ = do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis
-- cos :: xis_subst ~ xis
; (xi_subst,co) <- flatten d FMFullFlatten fl xi
-- co :: xi_subst ~ xi
@@ -1607,27 +1596,14 @@ lkpFunEqCache fam_head
-> return Nothing -- Strange: cached?
Just fl'
-> return $
- Just (CFunEqCan { cc_flavor = fl'
+ Just (CFunEqCan { cc_ev = fl'
, cc_depth = d
, cc_fun = tc
, cc_tyargs = xis_subst
, cc_rhs = xi_subst }) }
rewrite_cached (Just other_ct)
= pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct
-
-updFunEqCache :: Ct -> TcS ()
-updFunEqCache fun_eq@(CFunEqCan { cc_fun = tc, cc_tyargs = xis })
- = modifyInertTcS $ \inert -> ((), upd_inert inert)
- where upd_inert inert
- = let slvd = unCtFamHeadMap (inert_solved_funeqs inert)
- in inert { inert_solved_funeqs =
- CtFamHeadMap (alterTM key upd_funeqs slvd) }
- upd_funeqs Nothing = Just fun_eq
- upd_funeqs (Just _ct) = Just fun_eq
- -- Or _ct? depends on which caches more steps of computation
- key = mkTyConApp tc xis
-updFunEqCache other = pprPanic "updFunEqCache:Non family equation" $ ppr other
-
+-}
\end{code}
@@ -1830,7 +1806,7 @@ NB: The desugarer needs be more clever to deal with equalities
\begin{code}
data LookupInstResult
= NoInstance
- | GenInst [EvVar] EvTerm
+ | GenInst [CtEvidence] EvTerm
matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
@@ -1875,12 +1851,11 @@ matchClassInst inerts clas tys loc
; if null theta then
return (GenInst [] (EvDFunApp dfun_id tys []))
else do
- { evc_vars <- instDFunConstraints theta
- ; let ev_vars = map mn_thing evc_vars
- new_ev_vars = [mn_thing evc | evc <- evc_vars
- , isFresh evc ]
+ { evc_vars <- instDFunConstraints loc theta
+ ; let new_ev_vars = freshGoals evc_vars
-- new_ev_vars are only the real new variables that can be emitted
- ; return $ GenInst new_ev_vars (EvDFunApp dfun_id tys ev_vars) } }
+ dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
+ ; return $ GenInst new_ev_vars dfun_app } }
}
where
givens_for_this_clas :: Cts
@@ -1892,7 +1867,7 @@ matchClassInst inerts clas tys loc
given_overlap untch = anyBag (matchable untch) givens_for_this_clas
matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys
- , cc_flavor = fl })
+ , cc_ev = fl })
| isGiven fl
= ASSERT( clas_g == clas )
case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 3ba80e3b0f..79b6b02950 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -627,29 +627,24 @@ zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
zonkCt :: Ct -> TcM Ct
-- Zonking a Ct conservatively gives back a CNonCanonical
zonkCt ct
- = do { fl' <- zonkFlavor (cc_flavor ct)
+ = do { fl' <- zonkCtEvidence (cc_ev ct)
; return $
- CNonCanonical { cc_flavor = fl'
+ CNonCanonical { cc_ev = fl'
, cc_depth = cc_depth ct } }
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt
-zonkFlavor :: CtFlavor -> TcM CtFlavor
-zonkFlavor (Given loc evar)
+zonkCtEvidence :: CtEvidence -> TcM CtEvidence
+zonkCtEvidence ctev@(Given { ctev_gloc = loc, ctev_pred = pred })
= do { loc' <- zonkGivenLoc loc
- ; evar' <- zonkEvVar evar
- ; return (Given loc' evar') }
-zonkFlavor (Solved loc evar)
- = do { loc' <- zonkGivenLoc loc
- ; evar' <- zonkEvVar evar
- ; return (Solved loc' evar') }
-zonkFlavor (Wanted loc evar)
- = do { evar' <- zonkEvVar evar
- ; return (Wanted loc evar') }
-zonkFlavor (Derived loc pty)
- = do { pty' <- zonkTcType pty
- ; return (Derived loc pty') }
-
+ ; pred' <- zonkTcType pred
+ ; return (ctev { ctev_gloc = loc', ctev_pred = pred'}) }
+zonkCtEvidence ctev@(Wanted { ctev_pred = pred })
+ = do { pred' <- zonkTcType pred
+ ; return (ctev { ctev_pred = pred' }) }
+zonkCtEvidence ctev@(Derived { ctev_pred = pred })
+ = do { pred' <- zonkTcType pred
+ ; return (ctev { ctev_pred = pred' }) }
zonkGivenLoc :: GivenLoc -> TcM GivenLoc
-- GivenLocs may have unification variables inside them!
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 6a79b738fd..d17d3e6a10 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -55,9 +55,9 @@ module TcRnTypes(
singleCt, extendCts, isEmptyCts, isCTyEqCan, isCFunEqCan,
isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
- isGivenCt, isGivenOrSolvedCt,
- ctWantedLoc,
- SubGoalDepth, mkNonCanonical, ctPred, ctFlavPred, ctId, ctFlavId,
+ isGivenCt,
+ ctWantedLoc, ctEvidence,
+ SubGoalDepth, mkNonCanonical, ctPred, ctEvPred, ctEvTerm, ctEvId,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, addFlats, addImplics, mkFlatWC,
@@ -70,9 +70,9 @@ module TcRnTypes(
SkolemInfo(..),
- CtFlavor(..), pprFlavorArising,
- mkSolvedLoc, mkGivenLoc,
- isWanted, isGivenOrSolved, isGiven, isSolved,
+ CtEvidence(..), pprFlavorArising,
+ mkGivenLoc,
+ isWanted, isGiven,
isDerived, getWantedLoc, getGivenLoc, canSolve, canRewrite,
-- Pretty printing
@@ -89,7 +89,7 @@ module TcRnTypes(
import HsSyn
import HscTypes
-import TcEvidence( EvBind, EvBindsVar )
+import TcEvidence
import Type
import Class ( Class )
import TyCon ( TyCon )
@@ -850,7 +850,7 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num xi
- cc_flavor :: CtFlavor,
+ cc_ev :: CtEvidence,
cc_class :: Class,
cc_tyargs :: [Xi],
@@ -860,14 +860,14 @@ data Ct
| CIPCan { -- ?x::tau
-- See note [Canonical implicit parameter constraints].
- cc_flavor :: CtFlavor,
+ cc_ev :: CtEvidence,
cc_ip_nm :: IPName Name,
- cc_ip_ty :: TcTauType, -- Not a Xi! See same not as above
+ cc_ip_ty :: TcTauType, -- Not a Xi! See same not as above
cc_depth :: SubGoalDepth -- See Note [WorkList]
}
| CIrredEvCan { -- These stand for yet-unknown predicates
- cc_flavor :: CtFlavor,
+ cc_ev :: CtEvidence,
cc_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
-- Since, if it were a type constructor application, that'd make the
-- whole constraint a CDictCan, CIPCan, or CTyEqCan. And it can't be
@@ -881,7 +881,7 @@ data Ct
-- * typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
-- * We prefer unification variables on the left *JUST* for efficiency
- cc_flavor :: CtFlavor,
+ cc_ev :: CtEvidence,
cc_tyvar :: TcTyVar,
cc_rhs :: Xi,
@@ -891,7 +891,7 @@ data Ct
| CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) `compatKind` typeKind xi
- cc_flavor :: CtFlavor,
+ cc_ev :: CtEvidence,
cc_fun :: TyCon, -- A type function
cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
cc_rhs :: Xi, -- *never* over-saturated (because if so
@@ -902,18 +902,24 @@ data Ct
}
| CNonCanonical { -- See Note [NonCanonical Semantics]
- cc_flavor :: CtFlavor,
+ cc_ev :: CtEvidence,
cc_depth :: SubGoalDepth
}
\end{code}
\begin{code}
-mkNonCanonical :: CtFlavor -> Ct
-mkNonCanonical flav = CNonCanonical { cc_flavor = flav, cc_depth = 0}
+mkNonCanonical :: CtEvidence -> Ct
+mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0}
+
+ctEvidence :: Ct -> CtEvidence
+ctEvidence = cc_ev
ctPred :: Ct -> PredType
-ctPred (CNonCanonical { cc_flavor = fl }) = ctFlavPred fl
+ctPred ct = ctEvPred (cc_ev ct)
+-- ToDo Check with Dimitrios
+{-
+ctPred (CNonCanonical { cc_ev = fl }) = ctEvPred fl
ctPred (CDictCan { cc_class = cls, cc_tyargs = xis })
= mkClassPred cls xis
ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
@@ -923,18 +929,13 @@ ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
ctPred (CIPCan { cc_ip_nm = nm, cc_ip_ty = xi })
= mkIPPred nm xi
ctPred (CIrredEvCan { cc_ty = xi }) = xi
-
-
-ctId :: Ct -> EvVar
--- Precondition: not a derived!
-ctId ct = ctFlavId (cc_flavor ct)
-
+-}
\end{code}
%************************************************************************
%* *
- CtFlavor
+ CtEvidence
The "flavor" of a canonical constraint
%* *
%************************************************************************
@@ -942,20 +943,17 @@ ctId ct = ctFlavId (cc_flavor ct)
\begin{code}
ctWantedLoc :: Ct -> WantedLoc
-- Only works for Wanted/Derived
-ctWantedLoc ct = ASSERT2( not (isGivenOrSolved (cc_flavor ct)), ppr ct )
- getWantedLoc (cc_flavor ct)
+ctWantedLoc ct = ASSERT2( not (isGiven (cc_ev ct)), ppr ct )
+ getWantedLoc (cc_ev ct)
isWantedCt :: Ct -> Bool
-isWantedCt = isWanted . cc_flavor
+isWantedCt = isWanted . cc_ev
isGivenCt :: Ct -> Bool
-isGivenCt = isGiven . cc_flavor
+isGivenCt = isGiven . cc_ev
isDerivedCt :: Ct -> Bool
-isDerivedCt = isDerived . cc_flavor
-
-isGivenOrSolvedCt :: Ct -> Bool
-isGivenOrSolvedCt = isGivenOrSolved . cc_flavor
+isDerivedCt = isDerived . cc_ev
isCTyEqCan :: Ct -> Bool
isCTyEqCan (CTyEqCan {}) = True
@@ -989,7 +987,7 @@ isCNonCanonical _ = False
\begin{code}
instance Outputable Ct where
- ppr ct = ppr (cc_flavor ct) <+>
+ ppr ct = ppr (cc_ev ct) <+>
braces (ppr (cc_depth ct)) <+> parens (text ct_sort)
where ct_sort = case ct of
CTyEqCan {} -> "CTyEqCan"
@@ -1229,86 +1227,80 @@ pprWantedsWithLocs wcs
%* *
%************************************************************************
+Note [Evidence field of CtEvidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+During constraint solving we never look at the type of ctev_evtm, or
+ctev_evar; instead we look at the cte_pred field. The evtm/evar field
+may be un-zonked.
+
\begin{code}
-data CtFlavor
- = Given { flav_gloc :: GivenLoc, flav_evar :: EvVar }
- -- Trully given, not depending on subgoals
+data CtEvidence -- Rename to CtEvidence
+ = Given { ctev_gloc :: GivenLoc
+ , ctev_pred :: TcPredType
+ , ctev_evtm :: EvTerm } -- See Note [Evidence field of CtEvidence]
+ -- Truly given, not depending on subgoals
-- NB: Spontaneous unifications belong here
-- DV TODOs: (i) Consider caching actual evidence _term_
-- (ii) Revisit Note [Optimizing Spontaneously Solved Coercions]
- | Solved { flav_gloc :: GivenLoc, flav_evar :: EvVar }
- -- Originally wanted, but now we've produced and
- -- bound some partial evidence for this constraint.
- -- NB: Evidence may rely on yet-wanted constraints or other solved or given
-
- | Wanted { flav_wloc :: WantedLoc, flav_evar :: EvVar }
+ | Wanted { ctev_wloc :: WantedLoc
+ , ctev_pred :: TcPredType
+ , ctev_evar :: EvVar } -- See Note [Evidence field of CtEvidence]
-- Wanted goal
- | Derived { flav_wloc :: WantedLoc, flav_der_pty :: TcPredType }
+ | Derived { ctev_wloc :: WantedLoc
+ , ctev_pred :: TcPredType }
-- A goal that we don't really have to solve and can't immediately
- -- rewrite anything other than a derived (there's no evidence variable!)
+ -- rewrite anything other than a derived (there's no evidence!)
-- but if we do manage to solve it may help in solving other goals.
-ctFlavPred :: CtFlavor -> TcPredType
+ctEvPred :: CtEvidence -> TcPredType
-- The predicate of a flavor
-ctFlavPred (Given _ evar) = evVarPred evar
-ctFlavPred (Solved _ evar) = evVarPred evar
-ctFlavPred (Wanted _ evar) = evVarPred evar
-ctFlavPred (Derived { flav_der_pty = pty }) = pty
-
-ctFlavId :: CtFlavor -> EvVar
--- Precondition: can't be derived
-ctFlavId (Derived _ pty)
- = pprPanic "ctFlavId: derived constraint cannot have id" $
- text "pty =" <+> ppr pty
-ctFlavId fl = flav_evar fl
-
-instance Outputable CtFlavor where
+ctEvPred = ctev_pred
+
+ctEvTerm :: CtEvidence -> EvTerm
+ctEvTerm (Given { ctev_evtm = tm }) = tm
+ctEvTerm (Wanted { ctev_evar = ev }) = EvId ev
+ctEvTerm ctev@(Derived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
+ (ppr ctev)
+
+ctEvId :: CtEvidence -> TcId
+ctEvId (Wanted { ctev_evar = ev }) = ev
+ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
+
+instance Outputable CtEvidence where
ppr fl = case fl of
- (Given _ evar) -> ptext (sLit "[G]") <+> ppr evar <+> ppr_pty
- (Solved _ evar) -> ptext (sLit "[S]") <+> ppr evar <+> ppr_pty
- (Wanted _ evar) -> ptext (sLit "[W]") <+> ppr evar <+> ppr_pty
- (Derived {}) -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
- where ppr_pty = dcolon <+> ppr (ctFlavPred fl)
+ Given {} -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty
+ Wanted {} -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty
+ Derived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
+ where ppr_pty = dcolon <+> ppr (ctEvPred fl)
-getWantedLoc :: CtFlavor -> WantedLoc
+getWantedLoc :: CtEvidence -> WantedLoc
-- Precondition: Wanted or Derived
-getWantedLoc fl = flav_wloc fl
+getWantedLoc fl = ctev_wloc fl
-getGivenLoc :: CtFlavor -> GivenLoc
--- Precondition: Given or Solved
-getGivenLoc fl = flav_gloc fl
+getGivenLoc :: CtEvidence -> GivenLoc
+-- Precondition: Given
+getGivenLoc fl = ctev_gloc fl
-pprFlavorArising :: CtFlavor -> SDoc
-pprFlavorArising (Given gl _) = pprArisingAt gl
-pprFlavorArising (Solved gl _) = pprArisingAt gl
-pprFlavorArising (Wanted wl _) = pprArisingAt wl
-pprFlavorArising (Derived wl _) = pprArisingAt wl
+pprFlavorArising :: CtEvidence -> SDoc
+pprFlavorArising (Given { ctev_gloc = gl }) = pprArisingAt gl
+pprFlavorArising ctev = pprArisingAt (ctev_wloc ctev)
-isWanted :: CtFlavor -> Bool
+isWanted :: CtEvidence -> Bool
isWanted (Wanted {}) = True
isWanted _ = False
-isGivenOrSolved :: CtFlavor -> Bool
-isGivenOrSolved (Given {}) = True
-isGivenOrSolved (Solved {}) = True
-isGivenOrSolved _ = False
-
-isSolved :: CtFlavor -> Bool
-isSolved (Solved {}) = True
-isSolved _ = False
-
-isGiven :: CtFlavor -> Bool
-isGiven (Given {}) = True
+isGiven :: CtEvidence -> Bool
+isGiven (Given {}) = True
isGiven _ = False
-isDerived :: CtFlavor -> Bool
+isDerived :: CtEvidence -> Bool
isDerived (Derived {}) = True
isDerived _ = False
-canSolve :: CtFlavor -> CtFlavor -> Bool
+canSolve :: CtEvidence -> CtEvidence -> Bool
-- canSolve 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.
@@ -1325,18 +1317,13 @@ canSolve (Wanted {}) (Wanted {}) = True
canSolve (Derived {}) (Derived {}) = True -- Derived can't solve wanted/given
canSolve _ _ = False -- No evidence for a derived, anyway
-canRewrite :: CtFlavor -> CtFlavor -> Bool
+canRewrite :: CtEvidence -> CtEvidence -> Bool
-- canRewrite ct1 ct2
-- The equality constraint ct1 can be used to rewrite inside ct2
canRewrite = canSolve
-
mkGivenLoc :: WantedLoc -> SkolemInfo -> GivenLoc
mkGivenLoc wl sk = setCtLocOrigin wl sk
-
-mkSolvedLoc :: WantedLoc -> SkolemInfo -> GivenLoc
-mkSolvedLoc wl sk = setCtLocOrigin wl sk
-
\end{code}
%************************************************************************
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index ca7cf88fd1..7d86d157a0 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -24,15 +24,13 @@ module TcSMonad (
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts,
emitFrozenError,
- isWanted, isGivenOrSolved, isDerived,
- isGivenOrSolvedCt, isGivenCt,
- isWantedCt, isDerivedCt, pprFlavorArising,
+ isWanted, isDerived,
+ isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
isFlexiTcsTv,
canRewrite, canSolve,
- mkSolvedLoc, mkGivenLoc,
- ctWantedLoc,
+ mkGivenLoc, ctWantedLoc,
TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
traceFireTcS, bumpStepCountTcS, doWithInert,
@@ -42,16 +40,17 @@ module TcSMonad (
SimplContext(..), isInteractive, performDefaulting,
-- Getting and setting the flattening cache
- getFlatCache, updFlatCache, addToSolved,
+ getFlatCache, updFlatCache, addToSolved, addSolvedFunEq,
deferTcSForAllEq,
setEvBind,
XEvTerm(..),
- MaybeNew (..), isFresh,
- xCtFlavor, -- Transform a CtFlavor during a step
+ MaybeNew (..), isFresh, freshGoals, getEvTerms,
+
+ xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
- newWantedEvVar, newGivenEvVar, instDFunConstraints, newKindConstraint,
+ newWantedEvVar, instDFunConstraints, newKindConstraint,
newDerived,
xCtFlavor_cache, rewriteCtFlavor_cache,
@@ -68,12 +67,14 @@ module TcSMonad (
-- Inerts
InertSet(..), InertCans(..),
getInertEqs, getCtCoercion,
- emptyInert, getTcSInerts, lookupInInerts, updInertSet, extractUnsolved,
+ emptyInert, getTcSInerts, lookupInInerts,
+ extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
getRelevantCts, extractRelevantInerts,
- CCanMap (..), CtTypeMap, CtFamHeadMap(..), CtPredMap(..),
- pprCtTypeMap, partCtFamHeadMap,
+ CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
+ PredMap, FamHeadMap,
+ partCtFamHeadMap, lookupFamHead,
instDFunType, -- Instantiation
@@ -136,14 +137,12 @@ import TcRnTypes
import Unique
import UniqFM
-import Maybes ( orElse )
+import Maybes ( orElse, catMaybes )
-import Control.Monad( when )
+import Control.Monad( when, zipWithM )
import StaticFlags( opt_PprStyle_Debug )
import Data.IORef
-import Data.List ( find )
-import Control.Monad ( zipWithM )
import TrieMap
\end{code}
@@ -298,11 +297,10 @@ emptyCCanMap = CCanMap { cts_given = emptyUFM, cts_derived = emptyUFM, cts_wante
updCCanMap:: Uniquable a => (a,Ct) -> CCanMap a -> CCanMap a
updCCanMap (a,ct) cmap
- = case cc_flavor ct of
+ = case cc_ev ct of
Wanted {} -> cmap { cts_wanted = insert_into (cts_wanted cmap) }
Given {} -> cmap { cts_given = insert_into (cts_given cmap) }
Derived {} -> cmap { cts_derived = insert_into (cts_derived cmap) }
- Solved {} -> panic "updCCanMap update with solved!"
where
insert_into m = addToUFM_C unionBags m a (singleCt ct)
@@ -319,13 +317,24 @@ getRelevantCts a cmap
where
lookup map = lookupUFM map a `orElse` emptyCts
-lookupCCanMap :: Uniquable a => a -> (Ct -> Bool) -> CCanMap a -> Maybe Ct
-lookupCCanMap a p map
- = let possible_cts = lookupUFM (cts_given map) a `orElse`
- lookupUFM (cts_wanted map) a `orElse`
- lookupUFM (cts_derived map) a `orElse` emptyCts
- in find p (bagToList possible_cts)
+lookupCCanMap :: Uniquable a => a -> (CtEvidence -> Bool) -> CCanMap a -> Maybe CtEvidence
+lookupCCanMap a pick_me map
+ = findEvidence pick_me possible_cts
+ where
+ possible_cts = lookupUFM (cts_given map) a `plus` (
+ lookupUFM (cts_wanted map) a `plus` (
+ lookupUFM (cts_derived map) a `plus` emptyCts))
+ plus Nothing cts2 = cts2
+ plus (Just cts1) cts2 = cts1 `unionBags` cts2
+
+findEvidence :: (CtEvidence -> Bool) -> Cts -> Maybe CtEvidence
+findEvidence pick_me cts
+ = foldrBag pick Nothing cts
+ where
+ pick :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
+ pick ct deflt | let ctev = cc_ev ct, pick_me ctev = Just ctev
+ | otherwise = deflt
partitionCCanMap :: (Ct -> Bool) -> CCanMap a -> (Cts,CCanMap a)
-- All constraints that /match/ the predicate go in the bag, the rest remain in the map
@@ -360,27 +369,33 @@ extractUnsolvedCMap cmap =
-- Maps from PredTypes to Constraints
-type CtTypeMap = TypeMap Ct
-newtype CtPredMap =
- CtPredMap { unCtPredMap :: CtTypeMap } -- Indexed by TcPredType
-newtype CtFamHeadMap =
- CtFamHeadMap { unCtFamHeadMap :: CtTypeMap } -- Indexed by family head
+type CtTypeMap = TypeMap Ct
+type CtPredMap = PredMap Ct
+type CtFamHeadMap = FamHeadMap Ct
+
+newtype PredMap a = PredMap { unPredMap :: TypeMap a } -- Indexed by TcPredType
+newtype FamHeadMap a = FamHeadMap { unFamHeadMap :: TypeMap a } -- Indexed by family head
-pprCtTypeMap :: TypeMap Ct -> SDoc
-pprCtTypeMap ctmap = ppr (foldTM (:) ctmap [])
+instance Outputable a => Outputable (PredMap a) where
+ ppr (PredMap m) = ppr (foldTM (:) m [])
+
+instance Outputable a => Outputable (FamHeadMap a) where
+ ppr (FamHeadMap m) = ppr (foldTM (:) m [])
ctTypeMapCts :: TypeMap Ct -> Cts
ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
+lookupFamHead :: FamHeadMap a -> TcType -> Maybe a
+lookupFamHead (FamHeadMap m) key = lookupTM key m
partCtFamHeadMap :: (Ct -> Bool)
-> CtFamHeadMap
-> (Cts, CtFamHeadMap)
partCtFamHeadMap f ctmap
= let (cts,tymap_final) = foldTM upd_acc tymap_inside (emptyBag, tymap_inside)
- in (cts, CtFamHeadMap tymap_final)
+ in (cts, FamHeadMap tymap_final)
where
- tymap_inside = unCtFamHeadMap ctmap
+ tymap_inside = unFamHeadMap ctmap
upd_acc ct (cts,acc_map)
| f ct = (extendCts cts ct, alterTM ct_key (\_ -> Nothing) acc_map)
| otherwise = (cts,acc_map)
@@ -388,8 +403,6 @@ partCtFamHeadMap f ctmap
= ty1
| otherwise
= panic "partCtFamHeadMap, encountered non equality!"
-
-
\end{code}
%************************************************************************
@@ -400,9 +413,7 @@ partCtFamHeadMap f ctmap
%************************************************************************
\begin{code}
-
-
--- All Given (fully known) or Wanted or Derived, never Solved
+-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
data InertCans
= IC { inert_eqs :: TyVarEnv Ct
@@ -467,29 +478,51 @@ The InertCans represents a collection of constraints with the following properti
occurs errors.
9 Given family or dictionary constraints don't mention touchable unification variables
-\begin{code}
+Note [Solved constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When we take a step to simplify a constraint 'c', we call the original constraint "solved".
+For example: Wanted: ev :: [s] ~ [t]
+ New goal: ev1 :: s ~ t
+ Then 'ev' is now "solved".
+
+The reason for all this is simply to avoid re-solving goals we have solved already.
+
+* A solved Wanted may depend on as-yet-unsolved goals, so (for example) we should not
+ use it to rewrite a Given; in that sense the solved goal is still a Wanted
+
+* A solved Given is just given
+
+* A solved Derived is possible; purpose is to avoid creating tons of identical
+ Derived goals.
+
+\begin{code}
-- The Inert Set
data InertSet
= IS { inert_cans :: InertCans
- -- Canonical Given,Wanted,Solved
+ -- Canonical Given, Wanted, Derived (no Solved)
+ -- Sometimes called "the inert set"
+
, inert_frozen :: Cts
-- Frozen errors (as non-canonicals)
- , inert_solved :: CtPredMap
- -- Solved constraints (for caching):
- -- (i) key is by predicate type
- -- (ii) all of 'Solved' flavor, may or may not be canonicals
- -- (iii) we use this field for avoiding creating newEvVars
, inert_flat_cache :: CtFamHeadMap
-- All ``flattening equations'' are kept here.
-- Always canonical CTyFunEqs (Given or Wanted only!)
- -- Key is by family head. We used this field during flattening only
- , inert_solved_funeqs :: CtFamHeadMap
- -- Memoized Solved family equations co :: F xis ~ xi
- -- Stored not necessarily as fully rewritten; we'll do that lazily
- -- when we lookup
+ -- Key is by family head. We use this field during flattening only
+ -- Not necessarily inert wrt top-level equations (or inert_cans)
+
+ , inert_solved_funeqs :: FamHeadMap CtEvidence -- Of form co :: F xis ~ xi
+ , inert_solved :: PredMap CtEvidence -- All others
+ -- These two fields constitute a cache of solved (only!) constraints
+ -- See Note [Solved constraints]
+ -- - Constraints of form (F xis ~ xi) live in inert_solved_funeqs,
+ -- all the others are in inert_solved
+ -- - Used to avoid creating a new EvVar when we have a new goal that we
+ -- have solvedin the past
+ -- - Stored not necessarily as fully rewritten
+ -- (ToDo: rewrite lazily when we lookup)
}
@@ -498,7 +531,7 @@ instance Outputable InertCans where
, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts ics)))
, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips ics)))
, vcat (map ppr (Bag.bagToList $
- ctTypeMapCts (unCtFamHeadMap $ inert_funeqs ics)))
+ ctTypeMapCts (unFamHeadMap $ inert_funeqs ics)))
, vcat (map ppr (Bag.bagToList $ inert_irreds ics))
]
@@ -508,7 +541,7 @@ instance Outputable InertSet where
braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
, text "Solved and cached" <+>
int (foldTypeMap (\_ x -> x+1) 0
- (unCtPredMap $ inert_solved is)) <+>
+ (unPredMap $ inert_solved is)) <+>
text "more constraints" ]
emptyInert :: InertSet
@@ -517,28 +550,27 @@ emptyInert
, inert_eq_tvs = emptyInScopeSet
, inert_dicts = emptyCCanMap
, inert_ips = emptyCCanMap
- , inert_funeqs = CtFamHeadMap emptyTM
+ , inert_funeqs = FamHeadMap emptyTM
, inert_irreds = emptyCts }
, inert_frozen = emptyCts
- , inert_flat_cache = CtFamHeadMap emptyTM
- , inert_solved = CtPredMap emptyTM
- , inert_solved_funeqs = CtFamHeadMap emptyTM }
+ , inert_flat_cache = FamHeadMap emptyTM
+ , inert_solved = PredMap emptyTM
+ , inert_solved_funeqs = FamHeadMap emptyTM }
-type AtomicInert = Ct
-
-updInertSet :: InertSet -> AtomicInert -> InertSet
--- Add a new inert element to the inert set.
-updInertSet is item
- | isSolved (cc_flavor item)
- -- Solved items go in their special place
- = let pty = ctPred item
+updSolvedSet :: InertSet -> CtEvidence -> InertSet
+updSolvedSet is item
+ = let pty = ctEvPred item
upd_solved Nothing = Just item
upd_solved (Just _existing_solved) = Just item
-- .. or Just existing_solved? Is this even possible to happen?
in is { inert_solved =
- CtPredMap $
- alterTM pty upd_solved (unCtPredMap $ inert_solved is) }
+ PredMap $
+ alterTM pty upd_solved (unPredMap $ inert_solved is) }
+
+updInertSet :: InertSet -> Ct -> InertSet
+-- Add a new inert element to the inert set.
+updInertSet is item
| isCNonCanonical item
-- NB: this may happen if we decide to kick some frozen error
-- out to rewrite him. Frozen errors are just NonCanonicals
@@ -548,7 +580,7 @@ updInertSet is item
-- A canonical Given, Wanted, or Derived
= is { inert_cans = upd_inert_cans (inert_cans is) item }
- where upd_inert_cans :: InertCans -> AtomicInert -> InertCans
+ where upd_inert_cans :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
upd_inert_cans ics item
| isCTyEqCan item
@@ -578,14 +610,14 @@ updInertSet is item
upd_funeqs Nothing = Just item
upd_funeqs (Just _already_there)
= panic "updInertSet: item already there!"
- in ics { inert_funeqs = CtFamHeadMap
+ in ics { inert_funeqs = FamHeadMap
(alterTM fam_head upd_funeqs $
- (unCtFamHeadMap $ inert_funeqs ics)) }
+ (unFamHeadMap $ inert_funeqs ics)) }
| otherwise
= pprPanic "upd_inert set: can't happen! Inserting " $
ppr item
-updInertSetTcS :: AtomicInert -> TcS ()
+updInertSetTcS :: Ct -> TcS ()
-- Add a new item in the inerts of the monad
updInertSetTcS item
= do { traceTcS "updInertSetTcs {" $
@@ -596,6 +628,32 @@ updInertSetTcS item
; traceTcS "updInertSetTcs }" $ empty }
+addToSolved :: CtEvidence -> TcS ()
+-- Add a new item in the solved set of the monad
+addToSolved item
+ | isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
+ = return ()
+ | otherwise
+ = do { traceTcS "updSolvedSetTcs {" $
+ text "Trying to insert new solved item:" <+> ppr item
+
+ ; modifyInertTcS (\is -> ((), updSolvedSet is item))
+
+ ; traceTcS "updSolvedSetTcs }" $ empty }
+
+addSolvedFunEq :: CtEvidence -> TcS ()
+addSolvedFunEq fun_eq
+ = modifyInertTcS $ \inert -> ((), upd_inert inert)
+ where
+ upd_inert inert
+ = let slvd = unFamHeadMap (inert_solved_funeqs inert)
+ in inert { inert_solved_funeqs =
+ FamHeadMap (alterTM key upd_funeqs slvd) }
+ upd_funeqs Nothing = Just fun_eq
+ upd_funeqs (Just _ct) = Just fun_eq
+ -- Or _ct? depends on which caches more steps of computation
+ key = ctEvPred fun_eq
+
modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a
-- Modify the inert set with the supplied function
modifyInertTcS upd
@@ -606,20 +664,10 @@ modifyInertTcS upd
; return a }
-addToSolved :: Ct -> TcS ()
--- Don't do any caching for IP preds because of delicate shadowing
-addToSolved ct
- | isIPPred (ctPred ct)
- = return ()
- | otherwise
- = ASSERT ( isSolved (cc_flavor ct) )
- updInertSetTcS ct
-
extractUnsolvedTcS :: TcS (Cts,Cts)
-- Extracts frozen errors and remaining unsolved and sets the
-- inert set to be the remaining!
-extractUnsolvedTcS =
- modifyInertTcS extractUnsolved
+extractUnsolvedTcS = modifyInertTcS extractUnsolved
extractUnsolved :: InertSet -> ((Cts,Cts), InertSet)
-- Postcondition
@@ -660,22 +708,20 @@ extractUnsolved (IS { inert_cans = IC { inert_eqs = eqs
-- At some point, I used to flush all the solved, in
-- fear of evidence loops. But I think we are safe,
-- flushing is why T3064 had become slower
- , inert_solved = solved -- CtPredMap emptyTM
- , inert_flat_cache = flat_cache -- CtFamHeadMap emptyTM
- , inert_solved_funeqs = funeq_cache -- CtFamHeadMap emptyTM
+ , inert_solved = solved -- PredMap emptyTM
+ , inert_flat_cache = flat_cache -- FamHeadMap emptyTM
+ , inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
}
in ((frozen, unsolved), is_solved)
- where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenOrSolvedCt ct) eqs
+ where solved_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
unsolved_eqs = foldVarEnv (\ct cts -> cts `extendCts` ct) emptyCts $
eqs `minusVarEnv` solved_eqs
- (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenOrSolvedCt) irreds
+ (unsolved_irreds, solved_irreds) = Bag.partitionBag (not.isGivenCt) irreds
(unsolved_ips, solved_ips) = extractUnsolvedCMap ips
(unsolved_dicts, solved_dicts) = extractUnsolvedCMap dicts
-
- (unsolved_funeqs, solved_funeqs) =
- partCtFamHeadMap (not . isGivenOrSolved . cc_flavor) funeqs
+ (unsolved_funeqs, solved_funeqs) = partCtFamHeadMap (not . isGivenCt) funeqs
unsolved = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
@@ -697,7 +743,7 @@ extractRelevantInerts wi
in (cts, ics { inert_dicts = dict_map })
extract_ics_relevants ct@(CFunEqCan {}) ics =
let (cts,feqs_map) =
- let funeq_map = unCtFamHeadMap $ inert_funeqs ics
+ let funeq_map = unFamHeadMap $ inert_funeqs ics
fam_head = mkTyConApp (cc_fun ct) (cc_tyargs ct)
lkp = lookupTM fam_head funeq_map
new_funeq_map = alterTM fam_head xtm funeq_map
@@ -706,7 +752,7 @@ extractRelevantInerts wi
in case lkp of
Nothing -> (emptyCts, funeq_map)
Just ct -> (singleCt ct, new_funeq_map)
- in (cts, ics { inert_funeqs = CtFamHeadMap feqs_map })
+ in (cts, ics { inert_funeqs = FamHeadMap feqs_map })
extract_ics_relevants (CIPCan { cc_ip_nm = nm } ) ics =
let (cts, ips_map) = getRelevantCts nm (inert_ips ics)
in (cts, ics { inert_ips = ips_map })
@@ -716,36 +762,40 @@ extractRelevantInerts wi
extract_ics_relevants _ ics = (emptyCts,ics)
-lookupInInerts :: InertSet -> TcPredType -> Maybe Ct
+lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty
= case lookupInSolved solved pty of
- Just ct -> return ct
- Nothing -> lookupInInertCans ics pty
+ Just ctev -> return ctev
+ Nothing -> lookupInInertCans ics pty
-lookupInSolved :: CtPredMap -> TcPredType -> Maybe Ct
+lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
-lookupInSolved tm pty = lookupTM pty $ unCtPredMap tm
+lookupInSolved tm pty = lookupTM pty $ unPredMap tm
-lookupInInertCans :: InertCans -> TcPredType -> Maybe Ct
+lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
-- Returns Just if exactly this pred type exists in the inert canonicals
lookupInInertCans ics pty
- = lkp_ics (classifyPredType pty)
- where lkp_ics (ClassPred cls _)
- = lookupCCanMap cls (\ct -> ctPred ct `eqType` pty) (inert_dicts ics)
- lkp_ics (EqPred ty1 _ty2)
- | Just tv <- getTyVar_maybe ty1
- , Just ct <- lookupVarEnv (inert_eqs ics) tv
- , ctPred ct `eqType` pty
- = Just ct
- lkp_ics (EqPred ty1 _ty2) -- Family equation
- | Just _ <- splitTyConApp_maybe ty1
- , Just ct <- lookupTM ty1 (unCtFamHeadMap $ inert_funeqs ics)
- , ctPred ct `eqType` pty
- = Just ct
- lkp_ics (IrredPred {})
- = find (\ct -> ctPred ct `eqType` pty) (bagToList (inert_irreds ics))
- lkp_ics _ = Nothing -- NB: No caching for IPs
+ = case (classifyPredType pty) of
+ ClassPred cls _
+ -> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)
+
+ EqPred ty1 _ty2
+ | Just tv <- getTyVar_maybe ty1 -- Tyvar equation
+ , Just ct <- lookupVarEnv (inert_eqs ics) tv
+ , let ctev = ctEvidence ct
+ , ctEvPred ctev `eqType` pty
+ -> Just ctev
+
+ | Just _ <- splitTyConApp_maybe ty1 -- Family equation
+ , Just ct <- lookupTM ty1 (unFamHeadMap $ inert_funeqs ics)
+ , let ctev = ctEvidence ct
+ , ctEvPred ctev `eqType` pty
+ -> Just ctev
+
+ IrredPred {} -> findEvidence (\ct -> ctEvPred ct `eqType` pty) (inert_irreds ics)
+
+ _other -> Nothing -- NB: No caching for IPs
\end{code}
@@ -1038,13 +1088,13 @@ emitTcSImplication :: Implication -> TcS ()
emitTcSImplication imp = updTcSImplics (consBag imp)
-emitFrozenError :: CtFlavor -> SubGoalDepth -> TcS ()
+emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
emitFrozenError fl depth
- = do { traceTcS "Emit frozen error" (ppr (ctFlavPred fl))
+ = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
; inert_ref <- getTcSInertsRef
; inerts <- wrapTcS (TcM.readTcRef inert_ref)
- ; let ct = CNonCanonical { cc_flavor = fl
+ ; let ct = CNonCanonical { cc_ev = fl
, cc_depth = depth }
inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct }
; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
@@ -1059,24 +1109,23 @@ getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
getFlatCache :: TcS CtTypeMap
-getFlatCache = getTcSInerts >>= (return . unCtFamHeadMap . inert_flat_cache)
+getFlatCache = getTcSInerts >>= (return . unFamHeadMap . inert_flat_cache)
updFlatCache :: Ct -> TcS ()
-- Pre: constraint is a flat family equation (equal to a flatten skolem)
-updFlatCache flat_eq@(CFunEqCan { cc_flavor = fl, cc_fun = tc, cc_tyargs = xis })
+updFlatCache flat_eq@(CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = xis })
= modifyInertTcS upd_inert_cache
- where upd_inert_cache is = ((), is { inert_flat_cache = CtFamHeadMap new_fc })
+ where upd_inert_cache is = ((), is { inert_flat_cache = FamHeadMap new_fc })
where new_fc = alterTM pred_key upd_cache fc
- fc = unCtFamHeadMap $ inert_flat_cache is
+ fc = unFamHeadMap $ inert_flat_cache is
pred_key = mkTyConApp tc xis
- upd_cache (Just ct) | cc_flavor ct `canSolve` fl = Just ct
+ upd_cache (Just ct) | cc_ev ct `canSolve` fl = Just ct
upd_cache (Just _ct) = Just flat_eq
upd_cache Nothing = Just flat_eq
updFlatCache other_ct = pprPanic "updFlatCache: non-family constraint" $
ppr other_ct
-
getUntouchables :: TcS TcsUntouchables
getUntouchables = TcS (return . tcs_untch)
@@ -1296,142 +1345,193 @@ instFlexiTcSHelper tvname tvkind
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
data XEvTerm =
- XEvTerm { ev_comp :: [EvVar] -> EvTerm
+ XEvTerm { ev_comp :: [EvTerm] -> EvTerm
-- How to compose evidence
- , ev_decomp :: EvVar -> [EvTerm]
+ , ev_decomp :: EvTerm -> [EvTerm]
-- How to decompose evidence
}
-data MaybeNew a = Fresh { mn_thing :: a }
- | Cached { mn_thing :: a }
+data MaybeNew = Fresh CtEvidence | Cached EvTerm
-isFresh :: MaybeNew a -> Bool
+isFresh :: MaybeNew -> Bool
isFresh (Fresh {}) = True
isFresh _ = False
+getEvTerm :: MaybeNew -> EvTerm
+getEvTerm (Fresh ctev) = ctEvTerm ctev
+getEvTerm (Cached tm) = tm
+
+getEvTerms :: [MaybeNew] -> [EvTerm]
+getEvTerms = map getEvTerm
+
+freshGoals :: [MaybeNew] -> [CtEvidence]
+freshGoals mns = [ ctev | Fresh ctev <- mns ]
+
setEvBind :: EvVar -> EvTerm -> TcS ()
-setEvBind ev t
+setEvBind the_ev t
= do { tc_evbinds <- getTcEvBinds
- ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
+ ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev t
- ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr ev
+ ; traceTcS "setEvBind" $ vcat [ text "ev =" <+> ppr the_ev
, text "t =" <+> ppr t ]
#ifndef DEBUG
; return () }
#else
; binds <- getTcEvBindsMap
- ; let cycle = any (reaches binds) (evVarsOfTerm t)
+ ; let cycle = reaches_tm binds t
; when cycle (fail_if_co_loop binds) }
where fail_if_co_loop binds
- = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr ev
+ = do { traceTcS "Cycle in evidence binds" $ vcat [ text "evvar =" <+> ppr the_ev
, ppr (evBindMapBinds binds) ]
- ; when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) }
+ ; when (isEqVar the_ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) }
+
+ reaches_tm :: EvBindMap -> EvTerm -> Bool
+ -- Does any free variable of 'tm' reach 'the_ev'
+ reaches_tm ebm tm = foldVarSet ((||) . reaches ebm) False (evVarsOfTerm tm)
reaches :: EvBindMap -> Var -> Bool
- -- Does this evvar reach ev?
- reaches ebm ev0 = go ev0
- where go ev0
- | ev0 == ev = True
- | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0
- = any go (evVarsOfTerm evtrm)
- | otherwise = False
+ -- Does this evvar reach the_ev?
+ reaches ebm ev
+ | ev == the_ev = True
+ | Just (EvBind _ evtrm) <- lookupEvBind ebm ev = reaches_tm ebm evtrm
+ | otherwise = False
#endif
-newGivenEvVar :: TcPredType -> EvTerm -> TcS (MaybeNew EvVar)
-newGivenEvVar pty evterm
- = do { is <- getTcSInerts
- ; case lookupInInerts is pty of
- Just ct | isGivenOrSolvedCt ct
- -> return (Cached (ctId ct))
- _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
- ; setEvBind new_ev evterm
- ; return (Fresh new_ev) } }
-
-newWantedEvVar :: TcPredType -> TcS (MaybeNew EvVar)
-newWantedEvVar pty
+newGivenEvVar :: GivenLoc -> TcPredType -> EvTerm -> TcS CtEvidence
+-- Make a new variable of the given PredType,
+-- immediately bind it to the given term
+-- and return its CtEvidence
+newGivenEvVar gloc pred rhs
+ = do { new_ev <- wrapTcS $ TcM.newEvVar pred
+ ; setEvBind new_ev rhs
+ ; return (Given { ctev_gloc = gloc, ctev_pred = pred, ctev_evtm = EvId new_ev }) }
+
+newWantedEvVar :: WantedLoc -> TcPredType -> TcS MaybeNew
+newWantedEvVar loc pty
= do { is <- getTcSInerts
; case lookupInInerts is pty of
- Just ct | not (isDerivedCt ct)
- -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ct
- ; return (Cached (ctId ct)) }
+ Just ctev | not (isDerived ctev)
+ -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
+ ; return (Cached (ctEvTerm ctev)) }
_ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
- ; return (Fresh new_ev) } }
-
-newDerived :: TcPredType -> TcS (MaybeNew TcPredType)
-newDerived pty
+ ; let ctev = Wanted { ctev_wloc = loc
+ , ctev_pred = pty
+ , ctev_evar = new_ev }
+ ; return (Fresh ctev) } }
+
+newDerived :: WantedLoc -> TcPredType -> TcS (Maybe CtEvidence)
+-- Returns Nothing if cached,
+-- Just pred if not cached
+newDerived loc pty
= do { is <- getTcSInerts
; case lookupInInerts is pty of
- Just {} -> return (Cached pty)
- _ -> return (Fresh pty) }
+ Just {} -> return Nothing
+ _ -> return (Just Derived { ctev_wloc = loc
+ , ctev_pred = pty }) }
-newKindConstraint :: TcTyVar -> Kind -> TcS (MaybeNew EvVar)
+newKindConstraint :: WantedLoc -> TcTyVar -> Kind -> TcS MaybeNew
-- Create new wanted CoVar that constrains the type to have the specified kind.
-newKindConstraint tv knd
+newKindConstraint loc tv knd
= do { ty_k <- wrapTcS (instFlexiTcSHelper (tyVarName tv) knd)
- ; newWantedEvVar (mkTcEqPred (mkTyVarTy tv) ty_k) }
-
-instDFunConstraints :: TcThetaType -> TcS [MaybeNew EvVar]
-instDFunConstraints = mapM newWantedEvVar
+ ; newWantedEvVar loc (mkTcEqPred (mkTyVarTy tv) ty_k) }
+instDFunConstraints :: WantedLoc -> TcThetaType -> TcS [MaybeNew]
+instDFunConstraints wl = mapM (newWantedEvVar wl)
+\end{code}
-xCtFlavor :: CtFlavor -- Original flavor
+
+Note [xCFlavor]
+~~~~~~~~~~~~~~~
+A call might look like this:
+
+ xCtFlavor ev subgoal-preds evidence-transformer
+
+ ev is Given => use ev_decomp to create new Givens for subgoal-preds,
+ and return them
+
+ ev is Wanted => create new wanteds for subgoal-preds,
+ use ev_comp to bind ev,
+ return fresh wanteds (ie ones not cached in inert_cans or solved)
+
+ ev is Derived => create new deriveds for subgoal-preds
+ (unless cached in inert_cans or solved)
+
+Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
+ Ones that are already cached are not returned
+
+Example
+ ev : Tree a b ~ Tree c d
+ xCtFlavor ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
+ , ev_decomp = \c. [nth 1 c, nth 2 c] })
+ (\fresh-goals. stuff)
+
+\begin{code}
+xCtFlavor :: CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
-> XEvTerm -- Instructions about how to manipulate evidence
- -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals!
- -> TcS a
+ -> TcS [CtEvidence]
xCtFlavor = xCtFlavor_cache True
-
xCtFlavor_cache :: Bool -- True = if wanted add to the solved bag!
- -> CtFlavor -- Original flavor
+ -> CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
-> XEvTerm -- Instructions about how to manipulate evidence
- -> ([CtFlavor] -> TcS a) -- What to do with any remaining /fresh/ goals!
- -> TcS a
-xCtFlavor_cache _ (Given { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with
- = do { let ev_trms = ev_decomp xev evar
- ; new_evars <- zipWithM newGivenEvVar ptys ev_trms
- ; cont_with $
- map (\x -> Given gl (mn_thing x)) (filter isFresh new_evars) }
+ -> TcS [CtEvidence]
+
+xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
+ = ASSERT( equalLength ptys (ev_decomp xev tm) )
+ zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
+ -- For Givens we make new EvVars and bind them immediately. We don't worry
+ -- about caching, but we don't expect complicated calculations among Givens.
+ -- It is important to bind each given:
+ -- class (a~b) => C a b where ....
+ -- f :: C a b => ....
+ -- Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
+ -- But that superclass selector can't (yet) appear in a coercion
+ -- (see evTermCoercion), so the easy thing is to bind it to an Id
-xCtFlavor_cache cache (Wanted { flav_wloc = wl, flav_evar = evar }) ptys xev cont_with
- = do { new_evars <- mapM newWantedEvVar ptys
- ; let evars = map mn_thing new_evars
- evterm = ev_comp xev evars
- ; setEvBind evar evterm
- ; let solved_flav = Solved { flav_gloc = mkSolvedLoc wl UnkSkol
- , flav_evar = evar }
- ; when cache $ addToSolved (mkNonCanonical solved_flav)
- ; cont_with $
- map (\x -> Wanted wl (mn_thing x)) (filter isFresh new_evars) }
-
-xCtFlavor_cache _ (Derived { flav_wloc = wl }) ptys _xev cont_with
- = do { ders <- mapM newDerived ptys
- ; cont_with $
- map (\x -> Derived wl (mn_thing x)) (filter isFresh ders) }
+xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
+ = do { new_evars <- mapM (newWantedEvVar wl) ptys
+ ; setEvBind evar (ev_comp xev (getEvTerms new_evars))
+
+ -- Add the now-solved wanted constraint to the cache
+ ; when cache $ addToSolved ctev
+
+ ; return (freshGoals new_evars) }
- -- I am not sure I actually want to do this (e.g. from recanonicalizing a solved?)
- -- but if we plan to use xCtFlavor for rewriting as well then I might as well add a case
-xCtFlavor_cache _ (Solved { flav_gloc = gl, flav_evar = evar }) ptys xev cont_with
- = do { let ev_trms = ev_decomp xev evar
- ; new_evars <- zipWithM newGivenEvVar ptys ev_trms
- ; cont_with $
- map (\x -> Solved gl (mn_thing x)) (filter isFresh new_evars) }
-
-rewriteCtFlavor :: CtFlavor
+xCtFlavor_cache _ (Derived { ctev_wloc = wl }) ptys _xev
+ = do { ders <- mapM (newDerived wl) ptys
+ ; return (catMaybes ders) }
+
+-----------------------------
+rewriteCtFlavor :: CtEvidence
-> TcPredType -- new predicate
-> TcCoercion -- new ~ old
- -> TcS (Maybe CtFlavor)
--- rewriteCtFlavor old_fl new_pred co
--- Main purpose: create a new identity (flavor) for new_pred;
--- unless new_pred is cached already
--- * Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl
--- * If old_fl was wanted, create a binding for old_fl, in terms of new_fl
--- * If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl
--- * Returns Nothing if new_fl is already cached
+ -> TcS (Maybe CtEvidence)
+{-
+ rewriteCtFlavor old_fl new_pred co
+Main purpose: create a new identity (flavor) for new_pred;
+ unless new_pred is cached already
+* Returns a new_fl : new_pred, with same wanted/given/derived flag as old_fl
+* If old_fl was wanted, create a binding for old_fl, in terms of new_fl
+* If old_fl was given, AND not cached, create a binding for new_fl, in terms of old_fl
+* Returns Nothing if new_fl is already cached
+
+
+ Old evidence New predicate is Return new evidence
+ flavour of same flavor
+ -------------------------------------------------------------------
+ Wanted Already solved or in inert Nothing
+ or Derived Not Just new_evidence
+
+ Given Already in inert Nothing
+ Not Just new_evidence
+
+ Solved NEVER HAPPENS
+-}
rewriteCtFlavor = rewriteCtFlavor_cache True
-- Returns Just new_fl iff either (i) 'co' is reflexivity
@@ -1439,40 +1539,40 @@ rewriteCtFlavor = rewriteCtFlavor_cache True
-- In either case, there is nothing new to do with new_fl
rewriteCtFlavor_cache :: Bool
- -> CtFlavor
+ -> CtEvidence
-> TcPredType -- new predicate
-> TcCoercion -- new ~ old
- -> TcS (Maybe CtFlavor)
+ -> TcS (Maybe CtEvidence)
-- If derived, don't even look at the coercion
-- NB: this allows us to sneak away with ``error'' thunks for
-- coercions that come from derived ids (which don't exist!)
-rewriteCtFlavor_cache _cache (Derived wl _pty_orig) pty_new _co
- = newDerived pty_new >>= from_mn
- where from_mn (Cached {}) = return Nothing
- from_mn (Fresh {}) = return $ Just (Derived wl pty_new)
+rewriteCtFlavor_cache _cache (Derived { ctev_wloc = wl }) pty_new _co
+ = newDerived wl pty_new
-rewriteCtFlavor_cache cache fl pty co
- | isTcReflCo co
- -- If just reflexivity then you may re-use the same variable as optimization
- = if ctFlavPred fl `eqType` pty then
- -- E.g. for type synonyms we want to use the original type
- -- since it's not flattened to report better error messages.
- return $ Just fl
- else
- -- E.g. because we rewrite with a spontaneously solved one
- return (Just $ case fl of
- Derived wl _pty_orig -> Derived wl pty
- Given gl ev -> Given gl (setVarType ev pty)
- Wanted wl ev -> Wanted wl (setVarType ev pty)
- Solved gl ev -> Solved gl (setVarType ev pty))
- | otherwise
- = xCtFlavor_cache cache fl [pty] (XEvTerm ev_comp ev_decomp) cont
- where ev_comp [x] = mkEvCast x co
- ev_comp _ = panic "Coercion can only have one subgoal"
- ev_decomp x = [mkEvCast x (mkTcSymCo co)]
- cont [] = return Nothing
- cont [fl] = return $ Just fl
- cont _ = panic "At most one constraint can be subgoal of coercion!"
+rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
+ = return (Just (Given { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm }))
+ where
+ new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCase optimises ReflCo
+
+rewriteCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = pty_old }) pty_new co
+ | isTcReflCo co -- If just reflexivity then you may re-use the same variable
+ = return (Just (if pty_old `eqType` pty_new
+ then ctev
+ else ctev { ctev_pred = pty_new }))
+ -- If the old and new types compare equal (eqType looks through synonyms)
+ -- then retain the old type, so that error messages come out mentioning synonyms
+
+ | otherwise
+ = do { new_evar <- newWantedEvVar wl pty_new
+ ; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
+
+ -- Add the now-solved wanted constraint to the cache
+ ; when cache $ addToSolved ctev
+
+ ; case new_evar of
+ Fresh ctev -> return (Just ctev)
+ _ -> return Nothing }
+
-- Matching and looking up classes and family instances
@@ -1537,29 +1637,29 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
phi1 = Type.substTy subst1 body1
phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
skol_info = UnifyForAllSkol skol_tvs phi1
- ; mev <- newWantedEvVar (mkTcEqPred phi1 phi2)
- ; let new_fl = Wanted loc (mn_thing mev)
- new_ct = mkNonCanonical new_fl
- new_co = mkTcCoVarCo (mn_thing mev)
- ; coe_inside <- if isFresh mev then
- do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
- ; let ev_binds = TcEvBinds ev_binds_var
- ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv
- ; loc <- wrapTcS $ TcM.getCtLoc skol_info
- ; let wc = WC { wc_flat = singleCt new_ct
- , wc_impl = emptyBag
- , wc_insol = emptyCts }
- imp = Implic { ic_untch = all_untouchables
- , ic_env = lcl_env
- , ic_skols = skol_tvs
- , ic_given = []
- , ic_wanted = wc
- , ic_insol = False
- , ic_binds = ev_binds_var
- , ic_loc = loc }
- ; updTcSImplics (consBag imp)
- ; return (TcLetCo ev_binds new_co) }
- else (return new_co)
+ ; mev <- newWantedEvVar loc (mkTcEqPred phi1 phi2)
+ ; coe_inside <- case mev of
+ Cached ev_tm -> return (evTermCoercion ev_tm)
+ Fresh ctev -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
+ ; let ev_binds = TcEvBinds ev_binds_var
+ new_ct = mkNonCanonical ctev
+ new_co = evTermCoercion (ctEvTerm ctev)
+ ; lcl_env <- wrapTcS $ TcM.getLclTypeEnv
+ ; loc <- wrapTcS $ TcM.getCtLoc skol_info
+ ; let wc = WC { wc_flat = singleCt new_ct
+ , wc_impl = emptyBag
+ , wc_insol = emptyCts }
+ imp = Implic { ic_untch = all_untouchables
+ , ic_env = lcl_env
+ , ic_skols = skol_tvs
+ , ic_given = []
+ , ic_wanted = wc
+ , ic_insol = False
+ , ic_binds = ev_binds_var
+ , ic_loc = loc }
+ ; updTcSImplics (consBag imp)
+ ; return (TcLetCo ev_binds new_co) }
+
; setEvBind orig_ev $
EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs)
}
@@ -1573,7 +1673,6 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
-- Rewriting with respect to the inert equalities
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{code}
-
getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
getInertEqs = do { inert <- getTcSInerts
; let ics = inert_cans inert
@@ -1581,11 +1680,14 @@ getInertEqs = do { inert <- getTcSInerts
getCtCoercion :: EvBindMap -> Ct -> TcCoercion
-- Precondition: A CTyEqCan which is either Wanted or Given, never Derived or Solved!
-getCtCoercion bs ct
+getCtCoercion _bs ct
+ = ASSERT( not (isDerivedCt ct) )
+ evTermCoercion (ctEvTerm (ctEvidence ct))
+{- ToDo: check with Dimitrios that we can dump this stuff
= case lookupEvBind bs cc_id of
-- Given and bound to a coercion term
Just (EvBind _ (EvCoercion co)) -> co
- -- NB: The constraint could have been rewritten due to spontaneous
+ -- NB: The constraint could have been rewritten due to spontaneous
-- unifications but because we are optimizing away mkRefls the evidence
-- variable may still have type (alpha ~ [beta]). The constraint may
-- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
@@ -1596,6 +1698,9 @@ getCtCoercion bs ct
_ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
- where cc_id = ctId ct
-
+ where
+ cc_id = ctId ct
+-}
\end{code}
+
+
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index e6a4fd2f79..f97347a305 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -558,7 +558,7 @@ simplifyRule name lhs_wanted rhs_wanted
-- variables; hence NoUntouchables
; (resid_wanted, _) <- runTcS (SimplInfer doc) untch emptyInert emptyWorkList $
- solveWanteds zonked_all
+ solveWanteds zonked_all
; zonked_lhs <- zonkWC lhs_wanted
@@ -579,7 +579,8 @@ simplifyRule name lhs_wanted rhs_wanted
vcat [ text "zonked_lhs" <+> ppr zonked_lhs
, text "q_cts" <+> ppr q_cts ]
- ; return (map ctId (bagToList q_cts), zonked_lhs { wc_flat = non_q_cts }) }
+ ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
+ , zonked_lhs { wc_flat = non_q_cts }) }
\end{code}
@@ -784,10 +785,11 @@ solveNestedImplications implics
where givens_from_wanteds = foldrBag get_wanted []
get_wanted cc rest_givens
| pushable_wanted cc
- = let fl = cc_flavor cc
- wloc = flav_wloc fl
- gfl = Given (mkGivenLoc wloc UnkSkol) (flav_evar fl)
- this_given = cc { cc_flavor = gfl }
+ = let fl = ctEvidence cc
+ gfl = Given { ctev_gloc = setCtLocOrigin (ctev_wloc fl) UnkSkol
+ , ctev_evtm = EvId (ctev_evar fl)
+ , ctev_pred = ctev_pred fl }
+ this_given = cc { cc_ev = gfl }
in this_given : rest_givens
| otherwise = rest_givens
@@ -1025,20 +1027,20 @@ solveCTyFunEqs cts
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
- solve_one (Wanted _ cv,tv,ty)
+ solve_one (Wanted { ctev_evar = cv }, tv, ty)
= setWantedTyBind tv ty >> setEvBind cv (EvCoercion (mkTcReflCo ty))
solve_one (Derived {}, tv, ty)
= setWantedTyBind tv ty
solve_one arg
= pprPanic "solveCTyFunEqs: can't solve a /given/ family equation!" $ ppr arg
------------
-type FunEqBinds = (TvSubstEnv, [(CtFlavor, TcTyVar, TcType)])
+type FunEqBinds = (TvSubstEnv, [(CtEvidence, TcTyVar, TcType)])
-- The TvSubstEnv is not idempotent, but is loop-free
-- See Note [Non-idempotent substitution] in Unify
emptyFunEqBinds :: FunEqBinds
emptyFunEqBinds = (emptyVarEnv, [])
-extendFunEqBinds :: FunEqBinds -> CtFlavor -> TcTyVar -> TcType -> FunEqBinds
+extendFunEqBinds :: FunEqBinds -> CtEvidence -> TcTyVar -> TcType -> FunEqBinds
extendFunEqBinds (tv_subst, cv_binds) fl tv ty
= (extendVarEnv tv_subst tv ty, (fl, tv, ty):cv_binds)
@@ -1052,7 +1054,7 @@ getSolvableCTyFunEqs untch cts
dflt_funeq :: (Cts, FunEqBinds) -> Ct
-> (Cts, FunEqBinds)
dflt_funeq (cts_in, feb@(tv_subst, _))
- (CFunEqCan { cc_flavor = fl
+ (CFunEqCan { cc_ev = fl
, cc_fun = tc
, cc_tyargs = xis
, cc_rhs = xi })
@@ -1071,7 +1073,7 @@ getSolvableCTyFunEqs untch cts
, not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
-- Occurs check: see Note [Solving Family Equations], Point 2
- = ASSERT ( not (isGivenOrSolved fl) )
+ = ASSERT ( not (isGiven fl) )
(cts_in, extendFunEqBinds feb fl tv (mkTyConApp tc xis))
dflt_funeq (cts_in, fun_eq_binds) ct
@@ -1210,16 +1212,16 @@ defaultTyVar untch the_tv
, not (k `eqKind` default_k)
= tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
do { let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
- ; eqv <- TcSMonad.newKindConstraint the_tv default_k
+ ; eqv <- TcSMonad.newKindConstraint loc the_tv default_k
; case eqv of
Fresh x ->
return $ unitBag $
- CNonCanonical { cc_flavor = Wanted loc x, cc_depth = 0 }
+ CNonCanonical { cc_ev = x, cc_depth = 0 }
Cached _ -> return emptyBag }
{- DELETEME
if isNewEvVar eqv then
return $ unitBag (CNonCanonical { cc_id = evc_the_evvar eqv
- , cc_flavor = fl, cc_depth = 0 })
+ , cc_ev = fl, cc_depth = 0 })
else return emptyBag }
-}
@@ -1300,13 +1302,12 @@ disambigGroup (default_ty:default_tys) group
; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
do { derived_eq <- tryTcS $
-- I need a new tryTcS because we will call solveInteractCts below!
- do { md <- newDerived (mkTcEqPred (mkTyVarTy the_tv) default_ty)
+ do { md <- newDerived (ctev_wloc the_fl)
+ (mkTcEqPred (mkTyVarTy the_tv) default_ty)
+ -- ctev_wloc because constraint is not Given!
; case md of
- Cached _ -> return []
- Fresh pty ->
- -- flav_wloc because constraint is not Given/Solved!
- let dfl = Derived (flav_wloc the_fl) pty
- in return [ CNonCanonical { cc_flavor = dfl, cc_depth = 0 } ] }
+ Nothing -> return []
+ Just ctev -> return [ mkNonCanonical ctev ] }
; traceTcS "disambigGroup (solving) {"
(text "trying to solve constraints along with default equations ...")
@@ -1335,7 +1336,7 @@ disambigGroup (default_ty:default_tys) group
; disambigGroup default_tys group } }
where
((the_ct,the_tv):_) = group
- the_fl = cc_flavor the_ct
+ the_fl = cc_ev the_ct
wanteds = map fst group
\end{code}
@@ -1365,9 +1366,12 @@ newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
newFlatWanteds orig theta
= do { loc <- getCtLoc orig
; mapM (inst_to_wanted loc) theta }
- where inst_to_wanted loc pty
+ where
+ inst_to_wanted loc pty
= do { v <- TcMType.newWantedEvVar pty
; return $
- CNonCanonical { cc_flavor = Wanted loc v
+ CNonCanonical { cc_ev = Wanted { ctev_evar = v
+ , ctev_wloc = loc
+ , ctev_pred = pty }
, cc_depth = 0 } }
\end{code}
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 0b2429842d..c44ce31f2e 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -533,7 +533,9 @@ uType_defer items ty1 ty2
= ASSERT( not (null items) )
do { eqv <- newEq ty1 ty2
; loc <- getCtLoc (TypeEqOrigin (last items))
- ; emitFlat $ mkNonCanonical (Wanted loc eqv)
+ ; let ctev = Wanted { ctev_wloc = loc, ctev_evar = eqv
+ , ctev_pred = mkTcEqPred ty1 ty2 }
+ ; emitFlat $ mkNonCanonical ctev
-- Error trace only
-- NB. do *not* call mkErrInfo unless tracing is on, because
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 1360baca6b..42e54ba47b 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -30,7 +30,7 @@ module Coercion (
-- ** Constructing coercions
mkReflCo, mkCoVarCo,
mkAxInstCo, mkAxInstRHS,
- mkPiCo, mkPiCos,
+ mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkNthCo,
mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
mkForAllCo, mkUnsafeCo,
@@ -672,6 +672,18 @@ mkPiCos vs co = foldr mkPiCo co vs
mkPiCo :: Var -> Coercion -> Coercion
mkPiCo v co | isTyVar v = mkForAllCo v co
| otherwise = mkFunCo (mkReflCo (varType v)) co
+
+mkCoCast :: Coercion -> Coercion -> Coercion
+-- (mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# t1) ~# (s2 ~# t2)
+mkCoCast c g
+ = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
+ where
+ -- g :: (s1 ~# s2) ~# (t1 ~# t2)
+ -- g1 :: s1 ~# t1
+ -- g2 :: s2 ~# t2
+ [_reflk, g1, g2] = decomposeCo 3 g
+ -- Remember, (~#) :: forall k. k -> k -> *
+ -- so it takes *three* arguments, not two
\end{code}
%************************************************************************
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index e0de629da6..f81aebbfcd 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -973,14 +973,17 @@ getClassPredTys_maybe ty = case splitTyConApp_maybe ty of
_ -> Nothing
getEqPredTys :: PredType -> (Type, Type)
-getEqPredTys ty = case getEqPredTys_maybe ty of
- Just (ty1, ty2) -> (ty1, ty2)
- Nothing -> pprPanic "getEqPredTys" (ppr ty)
+getEqPredTys ty
+ = case splitTyConApp_maybe ty of
+ Just (tc, (_ : ty1 : ty2 : tys)) -> ASSERT( tc `hasKey` eqTyConKey && null tys )
+ (ty1, ty2)
+ _ -> pprPanic "getEqPredTys" (ppr ty)
getEqPredTys_maybe :: PredType -> Maybe (Type, Type)
-getEqPredTys_maybe ty = case splitTyConApp_maybe ty of
- Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
- _ -> Nothing
+getEqPredTys_maybe ty
+ = case splitTyConApp_maybe ty of
+ Just (tc, [_, ty1, ty2]) | tc `hasKey` eqTyConKey -> Just (ty1, ty2)
+ _ -> Nothing
getIPPredTy_maybe :: PredType -> Maybe (IPName Name, Type)
getIPPredTy_maybe ty = case splitTyConApp_maybe ty of
View Lorry Controller Status