Skip to content

Commit

Permalink
Make the evidence in a CtGiven into an EvId
Browse files Browse the repository at this point in the history
Note [Bind new Givens immediately] in TcRnTypes

We were never using the generality.  Result: less code, more efficient.
Cake for everyone.
  • Loading branch information
Simon Peyton Jones committed Apr 9, 2015
1 parent 702fc77 commit fa46c59
Show file tree
Hide file tree
Showing 9 changed files with 85 additions and 95 deletions.
14 changes: 4 additions & 10 deletions compiler/deSugar/DsBinds.hs
Expand Up @@ -849,27 +849,22 @@ dsEvTerm (EvCast tm co)
-- 'v' is always a lifted evidence variable so it is -- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here. -- unnecessary to call varToCoreExpr v here.


dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms dsEvTerm (EvDFunApp df tys tms) = return (Var df `mkTyApps` tys `mkApps` (map Var tms))
; return (Var df `mkTyApps` tys `mkApps` tms') }

dsEvTerm (EvCoercion (TcCoVarCo v)) = return (Var v) -- See Note [Simple coercions] dsEvTerm (EvCoercion (TcCoVarCo v)) = return (Var v) -- See Note [Simple coercions]
dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox


dsEvTerm (EvTupleSel v n) dsEvTerm (EvTupleSel v n)
= do { tm' <- dsEvTerm v = do { let scrut_ty = idType v
; let scrut_ty = exprType tm'
(tc, tys) = splitTyConApp scrut_ty (tc, tys) = splitTyConApp scrut_ty
Just [dc] = tyConDataCons_maybe tc Just [dc] = tyConDataCons_maybe tc
xs = mkTemplateLocals tys xs = mkTemplateLocals tys
the_x = getNth xs n the_x = getNth xs n
; ASSERT( isTupleTyCon tc ) ; ASSERT( isTupleTyCon tc )
return $ return $
Case tm' (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] } Case (Var v) (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] }


dsEvTerm (EvTupleMk tms) dsEvTerm (EvTupleMk tms)
= do { tms' <- mapM dsEvTerm tms = return (Var (dataConWorkId dc) `mkTyApps` map idType tms `mkApps` map Var tms)
; let tys = map exprType tms'
; return $ Var (dataConWorkId dc) `mkTyApps` tys `mkApps` tms' }
where where
dc = tupleCon ConstraintTuple (length tms) dc = tupleCon ConstraintTuple (length tms)


Expand All @@ -878,7 +873,6 @@ dsEvTerm (EvSuperClass d n)
; let (cls, tys) = getClassPredTys (exprType d') ; let (cls, tys) = getClassPredTys (exprType d')
sc_sel_id = classSCSelId cls n -- Zero-indexed sc_sel_id = classSCSelId cls n -- Zero-indexed
; return $ Var sc_sel_id `mkTyApps` tys `App` d' } ; return $ Var sc_sel_id `mkTyApps` tys `App` d' }
where


dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg] dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg]
where where
Expand Down
50 changes: 16 additions & 34 deletions compiler/typecheck/TcCanonical.hs
Expand Up @@ -189,13 +189,13 @@ canTuple :: CtEvidence -> [PredType] -> TcS (StopOrContinue Ct)
canTuple ev preds canTuple ev preds
| CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
= do { new_evars <- mapM (newWantedEvVar loc) preds = do { new_evars <- mapM (newWantedEvVar loc) preds
; setWantedEvBind evar (EvTupleMk (map (ctEvTerm . fst) new_evars)) ; setWantedEvBind evar (EvTupleMk (map (ctEvId . fst) new_evars))
; emitWorkNC (freshGoals new_evars) ; emitWorkNC (freshGoals new_evars)
-- Note the "NC": these are fresh goals, not necessarily canonical -- Note the "NC": these are fresh goals, not necessarily canonical
; stopWith ev "Decomposed tuple constraint" } ; stopWith ev "Decomposed tuple constraint" }


| CtGiven { ctev_evtm = tm, ctev_loc = loc } <- ev | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
= do { let mk_pr pred i = (pred, EvTupleSel tm i) = do { let mk_pr pred i = (pred, EvTupleSel evar i)
; given_evs <- newGivenEvVars loc (zipWith mk_pr preds [0..]) ; given_evs <- newGivenEvVars loc (zipWith mk_pr preds [0..])
; emitWorkNC given_evs ; emitWorkNC given_evs
; stopWith ev "Decomposed tuple constraint" } ; stopWith ev "Decomposed tuple constraint" }
Expand Down Expand Up @@ -353,9 +353,9 @@ newSCWorkFromFlavored flavor cls xis
= return () -- Deriveds don't yield more superclasses because we will = return () -- Deriveds don't yield more superclasses because we will
-- add them transitively in the case of wanteds. -- add them transitively in the case of wanteds.


| CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- flavor | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
= do { let sc_theta = immSuperClasses cls xis = do { let sc_theta = immSuperClasses cls xis
mk_pr sc_pred i = (sc_pred, EvSuperClass ev_tm i) mk_pr sc_pred i = (sc_pred, EvSuperClass (EvId evar) i)
; given_evs <- newGivenEvVars loc (zipWith mk_pr sc_theta [0..]) ; given_evs <- newGivenEvVars loc (zipWith mk_pr sc_theta [0..])
; emitWorkNC given_evs } ; emitWorkNC given_evs }


Expand Down Expand Up @@ -666,8 +666,8 @@ can_eq_app ev s1 t1 s2 t2
; let co = mkTcAppCo (ctEvCoercion ev_s) co_t ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
; setWantedEvBind evar (EvCoercion co) ; setWantedEvBind evar (EvCoercion co)
; canEqNC ev_s NomEq s1 s2 } ; canEqNC ev_s NomEq s1 s2 }
| CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
= do { let co = evTermCoercion ev_tm = do { let co = mkTcCoVarCo evar
co_s = mkTcLRCo CLeft co co_s = mkTcLRCo CLeft co
co_t = mkTcLRCo CRight co co_t = mkTcLRCo CRight co
; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s) ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s)
Expand Down Expand Up @@ -730,8 +730,8 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2 -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2
; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) } ; setWantedEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) }


CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } CtGiven { ctev_evar = evar, ctev_loc = loc }
-> do { let ev_co = evTermCoercion ev_tm -> do { let ev_co = mkTcCoVarCo evar
; given_evs <- newGivenEvVars loc $ ; given_evs <- newGivenEvVars loc $
[ ( mkTcEqPredRole r ty1 ty2 [ ( mkTcEqPredRole r ty1 ty2
, EvCoercion (mkTcNthCo i ev_co) ) , EvCoercion (mkTcNthCo i ev_co) )
Expand Down Expand Up @@ -1227,23 +1227,6 @@ as possible. Hence the ps_ty1, ps_ty2 argument passed to canEqTyVar.
************************************************************************ ************************************************************************
-} -}


{-
Note [Bind new Givens immediately]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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.
See Note [Coercion evidence terms] in TcEvidence.
-}


-----------------------------
data StopOrContinue a data StopOrContinue a
= ContinueWith a -- The constraint was not solved, although it may have = ContinueWith a -- The constraint was not solved, although it may have
-- been rewritten -- been rewritten
Expand Down Expand Up @@ -1331,14 +1314,14 @@ rewriteEvidence old_ev new_pred co
| isTcReflCo co -- See Note [Rewriting with Refl] | isTcReflCo co -- See Note [Rewriting with Refl]
= return (ContinueWith (old_ev { ctev_pred = new_pred })) = return (ContinueWith (old_ev { ctev_pred = new_pred }))


rewriteEvidence ev@(CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately] = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
; return (ContinueWith new_ev) } ; return (ContinueWith new_ev) }
where where
-- mkEvCast optimises ReflCo -- mkEvCast optimises ReflCo
new_tm = mkEvCast old_tm (tcDowngradeRole Representational new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
(ctEvRole ev) (ctEvRole ev)
(mkTcSymCo co)) (mkTcSymCo co))


rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
= do { (new_ev, freshness) <- newWantedEvVar loc new_pred = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
Expand Down Expand Up @@ -1386,12 +1369,11 @@ rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co
Just new_ev -> continueWith new_ev Just new_ev -> continueWith new_ev
Nothing -> stopWith old_ev "Cached derived" } Nothing -> stopWith old_ev "Cached derived" }


| CtGiven { ctev_evtm = old_tm } <- old_ev | CtGiven { ctev_evar = old_evar } <- old_ev
= do { let new_tm = EvCoercion (lhs_co = do { let new_tm = EvCoercion (lhs_co
`mkTcTransCo` maybeSym swapped (evTermCoercion old_tm) `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
`mkTcTransCo` mkTcSymCo rhs_co) `mkTcTransCo` mkTcSymCo rhs_co)
; new_ev <- newGivenEvVar loc' (new_pred, new_tm) ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
-- See Note [Bind new Givens immediately]
; return (ContinueWith new_ev) } ; return (ContinueWith new_ev) }


| CtWanted { ctev_evar = evar } <- old_ev | CtWanted { ctev_evar = evar } <- old_ev
Expand Down
30 changes: 15 additions & 15 deletions compiler/typecheck/TcEvidence.hs
Expand Up @@ -709,11 +709,11 @@ data EvTerm
| EvCast EvTerm TcCoercion -- d |> co, the coercion being at role representational | EvCast EvTerm TcCoercion -- d |> co, the coercion being at role representational


| EvDFunApp DFunId -- Dictionary instance application | EvDFunApp DFunId -- Dictionary instance application
[Type] [EvTerm] [Type] [EvId]


| EvTupleSel EvTerm Int -- n'th component of the tuple, 0-indexed | EvTupleSel EvId Int -- n'th component of the tuple, 0-indexed


| EvTupleMk [EvTerm] -- tuple built from this stuff | EvTupleMk [EvId] -- tuple built from this stuff


| EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
-- See Note [Deferring coercion errors to runtime] -- See Note [Deferring coercion errors to runtime]
Expand Down Expand Up @@ -787,7 +787,7 @@ Instead we make a binding
g1 :: a~Bool = g |> ax7 a g1 :: a~Bool = g |> ax7 a
and the constraint and the constraint
[G] g1 :: a~Bool [G] g1 :: a~Bool
See Trac [7238] and Note [Bind new Givens immediately] in TcSMonad See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
Note [EvBinds/EvTerm] Note [EvBinds/EvTerm]
~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~
Expand Down Expand Up @@ -993,11 +993,11 @@ evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
evVarsOfTerm :: EvTerm -> VarSet evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvId v) = unitVarSet v evVarsOfTerm (EvId v) = unitVarSet v
evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co
evVarsOfTerm (EvDFunApp _ _ evs) = evVarsOfTerms evs evVarsOfTerm (EvDFunApp _ _ evs) = mkVarSet evs
evVarsOfTerm (EvTupleSel v _) = evVarsOfTerm v evVarsOfTerm (EvTupleSel v _) = unitVarSet v
evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs evVarsOfTerm (EvTupleMk evs) = mkVarSet evs
evVarsOfTerm (EvDelayedError _ _) = emptyVarSet evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
evVarsOfTerm (EvLit _) = emptyVarSet evVarsOfTerm (EvLit _) = emptyVarSet
evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
Expand Down Expand Up @@ -1074,15 +1074,15 @@ instance Outputable EvBind where
-- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing


instance Outputable EvTerm where instance Outputable EvTerm where
ppr (EvId v) = ppr v ppr (EvId v) = ppr v
ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n)) ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n))
ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs
ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n)) ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ] ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
ppr (EvLit l) = ppr l ppr (EvLit l) = ppr l
ppr (EvCallStack cs) = ppr cs ppr (EvCallStack cs) = ppr cs
ppr (EvDelayedError ty msg) = ptext (sLit "error") ppr (EvDelayedError ty msg) = ptext (sLit "error")
<+> sep [ char '@' <> ppr ty, ppr msg ] <+> sep [ char '@' <> ppr ty, ppr msg ]
ppr (EvTypeable ev) = ppr ev ppr (EvTypeable ev) = ppr ev
Expand Down
9 changes: 3 additions & 6 deletions compiler/typecheck/TcHsSyn.hs
Expand Up @@ -1247,10 +1247,8 @@ zonkEvTerm env (EvCoercion co) = do { co' <- zonkTcCoToCo env co
zonkEvTerm env (EvCast tm co) = do { tm' <- zonkEvTerm env tm zonkEvTerm env (EvCast tm co) = do { tm' <- zonkEvTerm env tm
; co' <- zonkTcCoToCo env co ; co' <- zonkTcCoToCo env co
; return (mkEvCast tm' co') } ; return (mkEvCast tm' co') }
zonkEvTerm env (EvTupleSel tm n) = do { tm' <- zonkEvTerm env tm zonkEvTerm env (EvTupleSel tm n) = return (EvTupleSel (zonkIdOcc env tm) n)
; return (EvTupleSel tm' n) } zonkEvTerm env (EvTupleMk tms) = return (EvTupleMk (zonkIdOccs env tms))
zonkEvTerm env (EvTupleMk tms) = do { tms' <- mapM (zonkEvTerm env) tms
; return (EvTupleMk tms') }
zonkEvTerm _ (EvLit l) = return (EvLit l) zonkEvTerm _ (EvLit l) = return (EvLit l)


zonkEvTerm env (EvTypeable ev) = zonkEvTerm env (EvTypeable ev) =
Expand All @@ -1277,8 +1275,7 @@ zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
; return (EvSuperClass d' n) } ; return (EvSuperClass d' n) }
zonkEvTerm env (EvDFunApp df tys tms) zonkEvTerm env (EvDFunApp df tys tms)
= do { tys' <- zonkTcTypeToTypes env tys = do { tys' <- zonkTcTypeToTypes env tys
; tms' <- mapM (zonkEvTerm env) tms ; return (EvDFunApp (zonkIdOcc env df) tys' (zonkIdOccs env tms)) }
; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
zonkEvTerm env (EvDelayedError ty msg) zonkEvTerm env (EvDelayedError ty msg)
= do { ty' <- zonkTcTypeToType env ty = do { ty' <- zonkTcTypeToType env ty
; return (EvDelayedError ty' msg) } ; return (EvDelayedError ty' msg) }
Expand Down
8 changes: 4 additions & 4 deletions compiler/typecheck/TcInstDcls.hs
Expand Up @@ -1066,8 +1066,8 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
-- sc_co :: sc_pred ~ norm_sc_pred -- sc_co :: sc_pred ~ norm_sc_pred
, ClassPred cls tys <- classifyPredType norm_sc_pred , ClassPred cls tys <- classifyPredType norm_sc_pred
, className cls /= typeableClassName , className cls /= typeableClassName
-- `Typeable` has custom solving rules, which is why we exlucde it -- `Typeable` has custom solving rules, which is why we exclude it
-- from the short cut, and fall throught to calling the solver. -- from the short cut, and fall through to calling the solver.


= do { sc_ev_tm <- emit_sc_cls_pred norm_sc_pred cls tys = do { sc_ev_tm <- emit_sc_cls_pred norm_sc_pred cls tys
; sc_ev_id <- newEvVar sc_pred ; sc_ev_id <- newEvVar sc_pred
Expand Down Expand Up @@ -1097,7 +1097,7 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
-> do { let dfun_id = instanceDFunId ispec -> do { let dfun_id = instanceDFunId ispec
; (inst_tys, inst_theta) <- instDFunType dfun_id dfun_inst_tys ; (inst_tys, inst_theta) <- instDFunType dfun_id dfun_inst_tys
; arg_evs <- emitWanteds ScOrigin inst_theta ; arg_evs <- emitWanteds ScOrigin inst_theta
; let dict_app = EvDFunApp dfun_id inst_tys (map EvId arg_evs) ; let dict_app = EvDFunApp dfun_id inst_tys arg_evs
; traceTc "tcSuperClass 2" (ppr sc_pred $$ ppr dict_app) ; traceTc "tcSuperClass 2" (ppr sc_pred $$ ppr dict_app)
; return dict_app } ; return dict_app }


Expand Down Expand Up @@ -1379,7 +1379,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys


; self_dict <- newDict clas inst_tys ; self_dict <- newDict clas inst_tys
; let self_ev_bind = mkWantedEvBind self_dict ; let self_ev_bind = mkWantedEvBind self_dict
(EvDFunApp dfun_id (mkTyVarTys tyvars) (map EvId dfun_ev_vars)) (EvDFunApp dfun_id (mkTyVarTys tyvars) dfun_ev_vars)


; (meth_id, local_meth_sig, hs_wrap) ; (meth_id, local_meth_sig, hs_wrap)
<- mkMethIds hs_sig_fn clas tyvars dfun_ev_vars inst_tys sel_id <- mkMethIds hs_sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
Expand Down
12 changes: 5 additions & 7 deletions compiler/typecheck/TcInteract.hs
Expand Up @@ -131,7 +131,7 @@ solveSimpleGivens loc givens
| otherwise | otherwise
= go (map mk_given_ct givens) = go (map mk_given_ct givens)
where where
mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evtm = EvId ev_id mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
, ctev_pred = evVarPred ev_id , ctev_pred = evVarPred ev_id
, ctev_loc = loc }) , ctev_loc = loc })
go givens = do { solveSimples (listToBag givens) go givens = do { solveSimples (listToBag givens)
Expand Down Expand Up @@ -504,9 +504,7 @@ solveOneFromTheOther ev_i ev_w
lvl_i = ctLocLevel loc_i lvl_i = ctLocLevel loc_i
lvl_w = ctLocLevel loc_w lvl_w = ctLocLevel loc_w


has_binding binds ev has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
| EvId v <- ctEvTerm ev = isJust (lookupEvBind binds v)
| otherwise = True


use_replacement use_replacement
| isIPPred pred = lvl_w > lvl_i | isIPPred pred = lvl_w > lvl_i
Expand Down Expand Up @@ -806,8 +804,8 @@ lookupFlattenTyVar inert_eqs ftv
reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1
-> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2
-> TcS () -> TcS ()
reactFunEq from_this fsk1 (CtGiven { ctev_evtm = tm, ctev_loc = loc }) fsk2 reactFunEq from_this fsk1 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2
= do { let fsk_eq_co = mkTcSymCo (evTermCoercion tm) = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar)
`mkTcTransCo` ctEvCoercion from_this `mkTcTransCo` ctEvCoercion from_this
-- :: fsk2 ~ fsk1 -- :: fsk2 ~ fsk1
fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1) fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
Expand Down Expand Up @@ -1742,7 +1740,7 @@ matchClassInst inerts clas tys loc
; evc_vars <- mapM (newWantedEvVar loc) theta ; evc_vars <- mapM (newWantedEvVar loc) theta
; let new_ev_vars = freshGoals evc_vars ; let new_ev_vars = freshGoals evc_vars
-- new_ev_vars are only the real new variables that can be emitted -- new_ev_vars are only the real new variables that can be emitted
dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars) dfun_app = EvDFunApp dfun_id tys (map (ctEvId . fst) evc_vars)
; return $ GenInst new_ev_vars dfun_app } ; return $ GenInst new_ev_vars dfun_app }


unifiable_givens :: Cts unifiable_givens :: Cts
Expand Down
2 changes: 1 addition & 1 deletion compiler/typecheck/TcMType.hs
Expand Up @@ -935,7 +935,7 @@ tidyCt env ct
_ -> mkNonCanonical (tidy_ev env (ctEvidence ct)) _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
where where
tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evtm/var field because we don't -- NB: we do not tidy the ctev_evar field because we don't
-- show it in error messages -- show it in error messages
tidy_ev env ctev@(CtGiven { ctev_pred = pred }) tidy_ev env ctev@(CtGiven { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred } = ctev { ctev_pred = tidyType env pred }
Expand Down
47 changes: 33 additions & 14 deletions compiler/typecheck/TcRnTypes.hs
Expand Up @@ -1646,14 +1646,39 @@ pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
Note [Evidence field of CtEvidence] Note [Evidence field of CtEvidence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During constraint solving we never look at the type of ctev_evtm, or During constraint solving we never look at the type of ctev_evar;
ctev_evar; instead we look at the cte_pred field. The evtm/evar field instead we look at the cte_pred field. The evtm/evar field
may be un-zonked. may be un-zonked.
Note [Bind new Givens immediately]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For Givens we make new EvVars and bind them immediately. Two main reasons:
* Gain sharing. E.g. suppose we start with g :: C a b, where
class D a => C a b
class (E a, F a) => D a
If we generate all g's superclasses as separate EvTerms we might
get selD1 (selC1 g) :: E a
selD2 (selC1 g) :: F a
selC1 g :: D a
which we could do more economically as:
g1 :: D a = selC1 g
g2 :: E a = selD1 g1
g3 :: F a = selD2 g1
* For *coercion* evidence we *must* 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.
So a Given has EvVar inside it rather that (as previously) an EvTerm.
-} -}



data CtEvidence data CtEvidence
= CtGiven { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] = CtGiven { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
, ctev_evtm :: EvTerm -- See Note [Evidence field of CtEvidence] , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence]
, ctev_loc :: CtLoc } , ctev_loc :: CtLoc }
-- Truly given, not depending on subgoals -- Truly given, not depending on subgoals
-- NB: Spontaneous unifications belong here -- NB: Spontaneous unifications belong here
Expand Down Expand Up @@ -1685,25 +1710,19 @@ ctEvRole :: CtEvidence -> Role
ctEvRole = eqRelRole . ctEvEqRel ctEvRole = eqRelRole . ctEvEqRel


ctEvTerm :: CtEvidence -> EvTerm ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm (CtGiven { ctev_evtm = tm }) = tm ctEvTerm ev = EvId (ctEvId ev)
ctEvTerm (CtWanted { ctev_evar = ev }) = EvId ev
ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
(ppr ctev)


ctEvCoercion :: CtEvidence -> TcCoercion ctEvCoercion :: CtEvidence -> TcCoercion
-- ctEvCoercion ev = evTermCoercion (ctEvTerm ev) ctEvCoercion ev = mkTcCoVarCo (ctEvId ev)
ctEvCoercion (CtGiven { ctev_evtm = tm }) = evTermCoercion tm
ctEvCoercion (CtWanted { ctev_evar = v }) = mkTcCoVarCo v
ctEvCoercion ctev@(CtDerived {}) = pprPanic "ctEvCoercion: derived constraint cannot have id"
(ppr ctev)


ctEvId :: CtEvidence -> TcId ctEvId :: CtEvidence -> TcId
ctEvId (CtWanted { ctev_evar = ev }) = ev ctEvId (CtWanted { ctev_evar = ev }) = ev
ctEvId (CtGiven { ctev_evar = ev }) = ev
ctEvId ctev = pprPanic "ctEvId:" (ppr ctev) ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)


instance Outputable CtEvidence where instance Outputable CtEvidence where
ppr fl = case fl of ppr fl = case fl of
CtGiven {} -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty CtGiven {} -> ptext (sLit "[G]") <+> ppr (ctev_evar fl) <+> ppr_pty
CtWanted {} -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty CtWanted {} -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty
CtDerived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty CtDerived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
where ppr_pty = dcolon <+> ppr (ctEvPred fl) where ppr_pty = dcolon <+> ppr (ctEvPred fl)
Expand Down

0 comments on commit fa46c59

Please sign in to comment.