| ... |
... |
@@ -1618,14 +1618,17 @@ canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 |
|
1618
|
1618
|
k2 = typeKind xi2
|
|
1619
|
1619
|
|
|
1620
|
1620
|
|
|
1621
|
|
-{-
|
|
1622
|
|
-Note [Kind Equality Orientation]
|
|
1623
|
|
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
1621
|
+{- Historical Note [Kind Equality Orientation]
|
|
|
1622
|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
1623
|
+This Note describes a solution to a problem that no longer exists;
|
|
|
1624
|
+it used to apply to `canEqCanLHSHetero`.
|
|
|
1625
|
+
|
|
1624
|
1626
|
While in theory [W] x ~ y and [W] y ~ x ought to give us the same behaviour, in
|
|
1625
|
|
-practice it does not. See Historical Note [Fundeps with instances, and equality
|
|
1626
|
|
-orientation] where this is discussed at length. As a rule of thumb: we keep
|
|
1627
|
|
-the newest unification variables on the left of the equality. See also
|
|
1628
|
|
-Note [Improvement orientation].
|
|
|
1627
|
+the past it did not. See Historical Note [Fundeps with instances, and equality
|
|
|
1628
|
+orientation] in GHC.Tc.Solver.FunDeps, where this is discussed at length.
|
|
|
1629
|
+
|
|
|
1630
|
+As a rule of thumb: we keep the newest unification variables on the
|
|
|
1631
|
+left of the equality. See also Note [Improvement orientation].
|
|
1629
|
1632
|
|
|
1630
|
1633
|
In particular, `canEqCanLHSHetero` produces the following constraint equalities
|
|
1631
|
1634
|
|
| ... |
... |
@@ -1657,24 +1660,20 @@ canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2) |
|
1657
|
1660
|
-> TcS (StopOrContinue (Either IrredCt EqCt))
|
|
1658
|
1661
|
canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
|
|
1659
|
1662
|
-- See Note [Equalities with heterogeneous kinds]
|
|
1660
|
|
--- See Note [Kind Equality Orientation]
|
|
1661
|
|
-
|
|
1662
|
|
--- NB: preserve left-to-right orientation!! See wrinkle (W2) in
|
|
1663
|
|
--- Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Dict
|
|
1664
|
1663
|
-- NotSwapped:
|
|
1665
|
1664
|
-- ev :: (lhs1:ki1) ~r# (xi2:ki2)
|
|
1666
|
|
--- kind_co :: k11 ~# ki2 -- Same orientation as ev
|
|
1667
|
|
--- new_ev :: lhs1 ~r# (xi2 |> sym kind_co)
|
|
|
1665
|
+-- kind_co :: ki2 ~# ki1
|
|
|
1666
|
+-- new_ev :: lhs1 ~r# (xi2 |> kind_co)
|
|
1668
|
1667
|
-- Swapped
|
|
1669
|
1668
|
-- ev :: (xi2:ki2) ~r# (lhs1:ki1)
|
|
1670
|
|
--- kind_co :: ki2 ~# ki1 -- Same orientation as ev
|
|
|
1669
|
+-- kind_co :: ki2 ~# ki1
|
|
1671
|
1670
|
-- new_ev :: (xi2 |> kind_co) ~r# lhs1
|
|
1672
|
|
--- Note that we need the `sym` when we are /not/ swapped; hence `mk_sym_co`
|
|
1673
|
1671
|
|
|
1674
|
1672
|
= case ev of
|
|
1675
|
1673
|
CtGiven (GivenCt { ctev_evar = evar, ctev_loc = loc })
|
|
1676
|
|
- -> do { let kind_co = mkKindCo (mkCoVarCo evar)
|
|
1677
|
|
- pred_ty = unSwap swapped mkNomEqPred ki1 ki2
|
|
|
1674
|
+ -> do { let kind_co = maybeSymCo (flipSwap swapped) $
|
|
|
1675
|
+ mkKindCo (mkCoVarCo evar)
|
|
|
1676
|
+ pred_ty = mkNomEqPred ki2 ki1
|
|
1678
|
1677
|
kind_loc = mkKindEqLoc xi1 xi2 loc
|
|
1679
|
1678
|
; kind_ev <- newGivenEv kind_loc (pred_ty, evCoercion kind_co)
|
|
1680
|
1679
|
; emitWorkNC [CtGiven kind_ev]
|
| ... |
... |
@@ -1684,7 +1683,8 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 |
|
1684
|
1683
|
-> do { (unifs, (kind_co, eqs)) <- reportFineGrainUnifications $
|
|
1685
|
1684
|
wrapUnifier ev Nominal $ \uenv ->
|
|
1686
|
1685
|
let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
|
|
1687
|
|
- in unSwap swapped (uType uenv') ki1 ki2
|
|
|
1686
|
+ in uType uenv' ki2 ki1
|
|
|
1687
|
+ -- kind_co :: ki2 ~N ki1
|
|
1688
|
1688
|
-- mkKindEqLoc: any new constraints, arising from the kind
|
|
1689
|
1689
|
-- unification, say they thay come from unifying xi1~xi2
|
|
1690
|
1690
|
|
| ... |
... |
@@ -1728,16 +1728,10 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 |
|
1728
|
1728
|
; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }
|
|
1729
|
1729
|
|
|
1730
|
1730
|
where
|
|
1731
|
|
- -- kind_co :: ki1 ~N ki2
|
|
|
1731
|
+ -- kind_co :: ki2 ~N ki1
|
|
1732
|
1732
|
lhs_redn = mkReflRedn role ps_xi1
|
|
1733
|
|
- rhs_redn = mkGReflRightRedn role xi2 sym_kind_co
|
|
1734
|
|
- new_xi2 = mkCastTy ps_xi2 sym_kind_co
|
|
1735
|
|
-
|
|
1736
|
|
- -- Apply mkSymCo when /not/ swapped
|
|
1737
|
|
- sym_kind_co = case swapped of
|
|
1738
|
|
- NotSwapped -> mkSymCo kind_co
|
|
1739
|
|
- IsSwapped -> kind_co
|
|
1740
|
|
-
|
|
|
1733
|
+ rhs_redn = mkGReflRightRedn role xi2 kind_co
|
|
|
1734
|
+ new_xi2 = mkCastTy ps_xi2 kind_co
|
|
1741
|
1735
|
|
|
1742
|
1736
|
canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs
|
|
1743
|
1737
|
-- or, if swapped: rhs ~ lhs
|