Commit e1fc5a33 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Define emitNewWantedEq, and use it

This is just a minor refactoring
parent 9417e579
......@@ -1456,11 +1456,10 @@ homogeniseRhsKind ev eq_rel lhs rhs build_ct
| otherwise -- Wanted and Derived. See Note [No derived kind equalities]
-- evar :: (lhs :: k1) ~ (rhs :: k2)
= do { (kind_ev, kind_co) <- newWantedEq kind_loc Nominal k1 k2
= do { kind_co <- emitNewWantedEq kind_loc Nominal k1 k2
-- kind_ev :: (k1 :: *) ~ (k2 :: *)
; traceTcS "Hetero equality gives rise to wanted kind equality" $
ppr (kind_ev)
; emitWorkNC [kind_ev]
ppr (kind_co)
; let homo_co = mkSymCo kind_co
-- homo_co :: k2 ~ k1
rhs' = mkCastTy rhs homo_co
......@@ -1471,7 +1470,7 @@ homogeniseRhsKind ev eq_rel lhs rhs build_ct
where homo_pred = mkTcEqPredLikeEv ev lhs rhs'
CtWanted { ctev_dest = dest } -> do
{ (type_ev, hole_co) <- newWantedEq loc role lhs rhs'
-- type_ev :: (lhs :: k1) ~ (rhs |> sym kind_ev :: k1)
-- type_ev :: (lhs :: k1) ~ (rhs |> sym kind_co :: k1)
; setWantedEq dest
(hole_co `mkTransCo`
(mkReflCo role rhs
......
......@@ -1416,20 +1416,17 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
| otherwise -- We must not assign ufsk := ...ufsk...!
= do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
; new_ev <- case old_ev of
CtWanted {} -> do { (ev, _) <- newWantedEq loc Nominal alpha_ty rhs_ty
; updWorkListTcS $
extendWorkListEq (mkNonCanonical ev)
; return ev }
; new_co <- case old_ev of
CtWanted {} -> emitNewWantedEq loc Nominal alpha_ty rhs_ty
CtDerived {} -> do { ev <- newDerivedNC loc pred
; updWorkListTcS (extendWorkListDerived loc ev)
; return ev }
where pred = mkPrimEqPred alpha_ty rhs_ty
; return (ctEvCoercion ev) } -- Coercion is bottom
where pred = mkPrimEqPred alpha_ty rhs_ty
_ -> pprPanic "reduce_top_fun_eq" (ppr old_ev)
-- By emitting this as non-canonical, we deal with all
-- flattening, occurs-check, and ufsk := ufsk issues
; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
; let final_co = ax_co `mkTcTransCo` mkTcSymCo new_co
-- ax_co :: fam_tc args ~ rhs_ty
-- ev :: alpha ~ rhs_ty
-- ufsk := alpha
......@@ -1440,7 +1437,7 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
, nest 2 (text ":=") <+>
if isDerived old_ev then text "(derived)"
else ppr final_co
, text "new_ev:" <+> ppr new_ev ]
, text "new_co:" <+> ppr new_co ]
; stopWith old_ev "Fun/Top (wanted)" }
where
loc = ctEvLoc old_ev
......
......@@ -29,7 +29,7 @@ module TcSMonad (
MaybeNew(..), freshGoals, isFresh, getEvTerm,
newTcEvBinds,
newWantedEq,
newWantedEq, emitNewWantedEq,
newWanted, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
newBoundEvVarId,
unifyTyVar, unflattenFmv, reportUnifications,
......@@ -2995,6 +2995,15 @@ newBoundEvVarId pred rhs
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
-- | Emit a new Wanted equality into the work-list
emitNewWantedEq loc role ty1 ty2
| otherwise
= do { (ev, co) <- newWantedEq loc role ty1 ty2
; updWorkListTcS $
extendWorkListEq (mkNonCanonical ev)
; return co }
-- | Make a new equality CtEvidence
newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
newWantedEq loc role ty1 ty2
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment