| ... |
... |
@@ -1627,11 +1627,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 |
|
1627
|
1627
|
kind_loc = mkKindEqLoc xi1 xi2 loc
|
|
1628
|
1628
|
; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co)
|
|
1629
|
1629
|
; emitWorkNC [CtGiven kind_ev]
|
|
1630
|
|
- ; let kind_co = givenCtEvCoercion kind_ev
|
|
1631
|
|
- new_xi2 = mkCastTy ps_xi2 (mk_sym_co kind_co)
|
|
1632
|
|
- ; new_ev <- do_rewrite emptyRewriterSet kind_co
|
|
1633
|
|
- -- In the Given case, `new_ev` is canonical, so carry on
|
|
1634
|
|
- ; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }
|
|
|
1630
|
+ ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) }
|
|
1635
|
1631
|
|
|
1636
|
1632
|
CtWanted {}
|
|
1637
|
1633
|
-> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv ->
|
| ... |
... |
@@ -1646,28 +1642,28 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 |
|
1646
|
1642
|
assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $
|
|
1647
|
1643
|
-- The constraints won't be empty because the two kinds differ, and there
|
|
1648
|
1644
|
-- are no unifications, so we must have emitted one or more constraints
|
|
1649
|
|
- do { new_ev <- do_rewrite (rewriterSetFromCts cts) kind_co
|
|
1650
|
|
- -- The rewritten equality `new_ev` is non-canonical,
|
|
1651
|
|
- -- so put it straight in the Irreds
|
|
1652
|
|
- ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) new_ev } }
|
|
|
1645
|
+ finish (rewriterSetFromCts cts) kind_co }
|
|
1653
|
1646
|
where
|
|
1654
|
1647
|
xi1 = canEqLHSType lhs1
|
|
1655
|
1648
|
role = eqRelRole eq_rel
|
|
1656
|
1649
|
|
|
1657
|
|
- -- Apply mkSymCo when /not/ swapped
|
|
1658
|
|
- mk_sym_co co = case swapped of
|
|
1659
|
|
- NotSwapped -> mkSymCo co
|
|
1660
|
|
- IsSwapped -> co
|
|
1661
|
|
-
|
|
1662
|
|
- do_rewrite rewriters kind_co
|
|
|
1650
|
+ finish rewriters kind_co
|
|
1663
|
1651
|
= do { traceTcS "Hetero equality gives rise to kind equality"
|
|
1664
|
1652
|
(ppr swapped $$
|
|
1665
|
1653
|
ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
|
|
1666
|
|
- ; rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn }
|
|
|
1654
|
+ ; new_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
|
|
|
1655
|
+ ; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }
|
|
|
1656
|
+
|
|
1667
|
1657
|
where
|
|
1668
|
1658
|
-- kind_co :: ki1 ~N ki2
|
|
1669
|
1659
|
lhs_redn = mkReflRedn role ps_xi1
|
|
1670
|
|
- rhs_redn = mkGReflRightRedn role xi2 (mk_sym_co kind_co)
|
|
|
1660
|
+ rhs_redn = mkGReflRightRedn role xi2 sym_kind_co
|
|
|
1661
|
+ new_xi2 = mkCastTy ps_xi2 sym_kind_co
|
|
|
1662
|
+
|
|
|
1663
|
+ -- Apply mkSymCo when /not/ swapped
|
|
|
1664
|
+ sym_kind_co = case swapped of
|
|
|
1665
|
+ NotSwapped -> mkSymCo kind_co
|
|
|
1666
|
+ IsSwapped -> kind_co
|
|
1671
|
1667
|
|
|
1672
|
1668
|
|
|
1673
|
1669
|
canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs
|