summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Solver/Canonical.hs
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Solver/Canonical.hs')
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs145
1 files changed, 70 insertions, 75 deletions
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 162ef60cbc..e8c4ee82e2 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -29,6 +29,7 @@ import GHC.Core.Multiplicity
import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness checking
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
+import GHC.Core.Reduction
import GHC.Core
import GHC.Types.Id( mkTemplateLocals )
import GHC.Core.FamInstEnv ( FamInstEnvs )
@@ -209,15 +210,15 @@ canClass :: CtEvidence
canClass ev cls tys pend_sc fds
= -- all classes do *nominal* matching
assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
- do { (xis, cos) <- rewriteArgsNom ev cls_tc tys
- ; let co = mkTcTyConAppCo Nominal cls_tc cos
- xi = mkClassPred cls xis
+ do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc tys
+ ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns
mk_ct new_ev = CDictCan { cc_ev = new_ev
, cc_tyargs = xis
, cc_class = cls
, cc_pend_sc = pend_sc
, cc_fundeps = fds }
- ; mb <- rewriteEvidence ev xi co
+ ; mb <- rewriteEvidence ev redn
+
; traceTcS "canClass" (vcat [ ppr ev
, ppr xi, ppr mb ])
; return (fmap mk_ct mb) }
@@ -709,8 +710,8 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
canIrred ev
= do { let pred = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
- ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
- ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+ ; redn <- rewrite ev pred
+ ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
do { -- Re-classify, in case rewriting has improved its shape
-- Code is like the canNC, except
@@ -824,8 +825,8 @@ canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
canForAll ev pend_sc
= do { -- First rewrite it to apply the current substitution
let pred = ctEvPred ev
- ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
- ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+ ; redn <- rewrite ev pred
+ ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
do { -- Now decompose into its pieces and solve it
-- (It takes a lot less code to rewrite before decomposing.)
@@ -1058,9 +1059,9 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
-- No similarity in type structure detected. Rewrite and try again.
can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
- = do { (xi1, co1) <- rewrite ev ps_ty1
- ; (xi2, co2) <- rewrite ev ps_ty2
- ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+ = do { redn1@(Reduction _ xi1) <- rewrite ev ps_ty1
+ ; redn2@(Reduction _ xi2) <- rewrite ev ps_ty2
+ ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
----------------------------
@@ -1459,9 +1460,9 @@ can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2
-> TcType -- ^ ty2
-> TcType -- ^ ty2, with type synonyms
-> TcS (StopOrContinue Ct)
-can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
+can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
= do { traceTcS "can_eq_newtype_nc" $
- vcat [ ppr ev, ppr swapped, ppr co, ppr gres, ppr ty1', ppr ty2 ]
+ vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]
-- check for blowing our stack:
-- See Note [Newtypes can blow the stack]
@@ -1477,8 +1478,11 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
-- module, don't warn about it being unused.
-- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.
- ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2
- (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
+ ; let redn1 = mkReduction co1 ty1'
+
+ ; new_ev <- rewriteEqEvidence ev swapped
+ redn1
+ (mkReflRedn Representational ps_ty2)
; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
where
gre_list = bagToList gres
@@ -1553,9 +1557,9 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
= do { traceTcS "Decomposing cast" (vcat [ ppr ev
, ppr ty1 <+> text "|>" <+> ppr co1
, ppr ps_ty2 ])
- ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
- (mkTcGReflRightCo role ty1 co1)
- (mkTcReflCo role ps_ty2)
+ ; new_ev <- rewriteEqEvidence ev swapped
+ (mkGReflLeftRedn role ty1 co1)
+ (mkReflRedn role ps_ty2)
; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
where
role = eqRelRole eq_rel
@@ -1912,14 +1916,14 @@ canEqFailure :: CtEvidence -> EqRel
canEqFailure ev NomEq ty1 ty2
= canEqHardFailure ev ty1 ty2
canEqFailure ev ReprEq ty1 ty2
- = do { (xi1, co1) <- rewrite ev ty1
- ; (xi2, co2) <- rewrite ev ty2
+ = do { redn1 <- rewrite ev ty1
+ ; redn2 <- rewrite ev ty2
-- We must rewrite the types before putting them in the
-- inert set, so that we are sure to kick them out when
-- new equalities become available
; traceTcS "canEqFailure with ReprEq" $
- vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
- ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+ vcat [ ppr ev, ppr redn1, ppr redn2 ]
+ ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
; continueWith (mkIrredCt ReprEqReason new_ev) }
-- | Call when canonicalizing an equality fails with utterly no hope.
@@ -1928,9 +1932,9 @@ canEqHardFailure :: CtEvidence
-- See Note [Make sure that insolubles are fully rewritten]
canEqHardFailure ev ty1 ty2
= do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
- ; (s1, co1) <- rewrite ev ty1
- ; (s2, co2) <- rewrite ev ty2
- ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
+ ; redn1 <- rewrite ev ty1
+ ; redn2 <- rewrite ev ty2
+ ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
{-
@@ -2067,7 +2071,7 @@ Ticket #12526 is another good example of this in action.
-}
---------------------
-canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs
+canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs
-> EqRel -> SwapFlag
-> CanEqLHS -- lhs (or, if swapped, rhs)
-> TcType -- lhs: pretty lhs, already rewritten
@@ -2097,16 +2101,15 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
; let -- kind_co :: (ki2 :: *) ~N (ki1 :: *) (whether swapped or not)
-- co1 :: kind(tv1) ~N ki1
- rhs' = xi2 `mkCastTy` kind_co -- :: ki1
ps_rhs' = ps_xi2 `mkCastTy` kind_co -- :: ki1
- rhs_co = mkTcGReflLeftCo role xi2 kind_co
- -- rhs_co :: (xi2 |> kind_co) ~ xi2
- lhs_co = mkTcReflCo role xi1
+ lhs_redn = mkReflRedn role xi1
+ rhs_redn@(Reduction _ rhs')
+ = mkGReflRightRedn role xi2 kind_co
; traceTcS "Hetero equality gives rise to kind equality"
(ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
- ; type_ev <- rewriteEqEvidence ev swapped xi1 rhs' lhs_co rhs_co
+ ; type_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn
-- rewriteEqEvidence carries out the swap, so we're NotSwapped any more
; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 rhs' ps_rhs' }
@@ -2305,8 +2308,8 @@ canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
-- want to rewrite the LHS to (as per e.g. swapOverTyVars)
canEqCanLHSFinish :: CtEvidence
-> EqRel -> SwapFlag
- -> CanEqLHS -- lhs (or, if swapped, rhs)
- -> TcType -- rhs, pretty rhs
+ -> CanEqLHS -- lhs (or, if swapped, rhs)
+ -> TcType -- rhs (or, if swapped, lhs)
-> TcS (StopOrContinue Ct)
canEqCanLHSFinish ev eq_rel swapped lhs rhs
-- RHS is fully rewritten, but with type synonyms
@@ -2315,7 +2318,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
-- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2
= do { dflags <- getDynFlags
- ; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs rewrite_co1 rewrite_co2
+ ; new_ev <- rewriteEqEvidence ev swapped
+ (mkReflRedn role lhs_ty)
+ (mkReflRedn role rhs)
-- by now, (TyEq:K) is already satisfied
; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs)
@@ -2356,7 +2361,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
do { traceTcS "canEqCanLHSFinish can't make a canonical"
(ppr lhs $$ ppr rhs)
; continueWith (mkIrredCt reason new_ev) }
- ; Just (lhs_tv, co, new_rhs) ->
+ ; Just (lhs_tv, rhs_redn@(Reduction _ new_rhs)) ->
do { traceTcS "canEqCanLHSFinish breaking a cycle" $
ppr lhs $$ ppr rhs
; traceTcS "new RHS:" (ppr new_rhs)
@@ -2370,8 +2375,8 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
else do { -- See Detail (6) of Note [Type variable cycles]
new_new_ev <- rewriteEqEvidence new_ev NotSwapped
- lhs_ty new_rhs
- (mkTcNomReflCo lhs_ty) co
+ (mkReflRedn Nominal lhs_ty)
+ rhs_redn
; continueWith (CEqCan { cc_ev = new_new_ev
, cc_lhs = lhs
@@ -2382,9 +2387,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
lhs_ty = canEqLHSType lhs
- rewrite_co1 = mkTcReflCo role lhs_ty
- rewrite_co2 = mkTcReflCo role rhs
-
-- This is about (TyEq:N)
bad_newtype | ReprEq <- eq_rel
, Just tc <- tyConAppTyCon_maybe rhs
@@ -2410,13 +2412,10 @@ rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco
-> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs
-- result is independent of SwapFlag
rewriteCastedEquality ev eq_rel swapped lhs rhs mco
- = rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
+ = rewriteEqEvidence ev swapped lhs_redn rhs_redn
where
- new_lhs = lhs `mkCastTyMCo` sym_mco
- lhs_co = mkTcGReflLeftMCo role lhs sym_mco
-
- new_rhs = rhs
- rhs_co = mkTcGReflRightMCo role rhs mco
+ lhs_redn = mkGReflRightMRedn role lhs sym_mco
+ rhs_redn = mkGReflLeftMRedn role rhs mco
sym_mco = mkTcSymMCo mco
role = eqRelRole eq_rel
@@ -2945,9 +2944,8 @@ andWhenContinue tcs1 tcs2
ContinueWith ct -> tcs2 ct }
infixr 0 `andWhenContinue` -- allow chaining with ($)
-rewriteEvidence :: CtEvidence -- old evidence
- -> TcPredType -- new predicate
- -> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
+rewriteEvidence :: CtEvidence -- ^ old evidence
+ -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
-> TcS (StopOrContinue CtEvidence)
-- Returns Just new_ev iff either (i) 'co' is reflexivity
-- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
@@ -2983,7 +2981,7 @@ as well as in old_pred; that is important for good error messages.
-}
-rewriteEvidence old_ev@(CtDerived {}) new_pred _co
+rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred)
= -- If derived, don't even look at the coercion.
-- This is very important, DO NOT re-order the equations for
-- rewriteEvidence to put the isTcReflCo test first!
@@ -2993,30 +2991,28 @@ rewriteEvidence old_ev@(CtDerived {}) new_pred _co
-- (Getting this wrong caused #7384.)
continueWith (old_ev { ctev_pred = new_pred })
-rewriteEvidence old_ev new_pred co
+rewriteEvidence old_ev (Reduction co new_pred)
| isTcReflCo co -- See Note [Rewriting with Refl]
= continueWith (old_ev { ctev_pred = new_pred })
-rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
+rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred)
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
; continueWith new_ev }
where
-- mkEvCast optimises ReflCo
- new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational
- (ctEvRole ev)
- (mkTcSymCo co))
+ new_tm = mkEvCast (evId old_evar)
+ (tcDowngradeRole Representational (ctEvRole ev) co)
rewriteEvidence ev@(CtWanted { ctev_dest = dest
, ctev_nosh = si
- , ctev_loc = loc }) new_pred co
+ , ctev_loc = loc }) (Reduction co new_pred)
= do { mb_new_ev <- newWanted_SI si loc new_pred
-- The "_SI" variant ensures that we make a new Wanted
- -- with the same shadow-info as the existing one
-- with the same shadow-info as the existing one (#16735)
; massert (tcCoercionRole co == ctEvRole ev)
; setWantedEvTerm dest
(mkEvCast (getEvExpr mb_new_ev)
- (tcDowngradeRole Representational (ctEvRole ev) co))
+ (tcDowngradeRole Representational (ctEvRole ev) (mkSymCo co)))
; case mb_new_ev of
Fresh new_ev -> continueWith new_ev
Cached _ -> stopWith ev "Cached wanted" }
@@ -3025,26 +3021,25 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
-- or orhs ~ olhs (swapped)
-> SwapFlag
- -> TcType -> TcType -- New predicate nlhs ~ nrhs
- -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
- -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
+ -> Reduction -- lhs_co :: olhs ~ nlhs
+ -> Reduction -- rhs_co :: orhs ~ nrhs
-> TcS CtEvidence -- Of type nlhs ~ nrhs
--- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
--- we generate
+-- With reductions (Reduction lhs_co nlhs) (Reduction rhs_co nrhs),
+-- rewriteEqEvidence yields, for a given equality (Given g olhs orhs):
-- If not swapped
--- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
--- If 'swapped'
--- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
+-- g1 : nlhs ~ nrhs = sym lhs_co ; g ; rhs_co
+-- If swapped
+-- g1 : nlhs ~ nrhs = sym lhs_co ; Sym g ; rhs_co
--
--- For (Wanted w) we do the dual thing.
+-- For a wanted equality (Wanted w), we do the dual thing:
-- New w1 : nlhs ~ nrhs
-- If not swapped
--- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
+-- w : olhs ~ orhs = lhs_co ; w1 ; sym rhs_co
-- If swapped
--- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
+-- w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co
--
--- It's all a form of rewwriteEvidence, specialised for equalities
-rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
+-- It's all a form of rewriteEvidence, specialised for equalities
+rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs)
| CtDerived {} <- old_ev -- Don't force the evidence for a Derived
= return (old_ev { ctev_pred = new_pred })
@@ -3054,9 +3049,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
= return (old_ev { ctev_pred = new_pred })
| CtGiven { ctev_evar = old_evar } <- old_ev
- = do { let new_tm = evCoercion (lhs_co
+ = do { let new_tm = evCoercion ( mkTcSymCo lhs_co
`mkTcTransCo` maybeTcSymCo swapped (mkTcCoVarCo old_evar)
- `mkTcTransCo` mkTcSymCo rhs_co)
+ `mkTcTransCo` rhs_co)
; newGivenEvVar loc' (new_pred, new_tm) }
| CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev
@@ -3065,9 +3060,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
-- The "_SI" variant ensures that we make a new Wanted
-- with the same shadow-info as the existing one (#16735)
; let co = maybeTcSymCo swapped $
- mkSymCo lhs_co
+ lhs_co
`mkTransCo` hole_co
- `mkTransCo` rhs_co
+ `mkTransCo` mkTcSymCo rhs_co
; setWantedEq dest co
; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
; return new_ev }