[Git][ghc/ghc][wip/T24978] Another big increment
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Jul 4 14:20:37 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
d109ecb0 by Simon Peyton Jones at 2024-07-04T15:18:18+01:00
Another big increment
* Combine sfInteractTop, sfInteractInert
* Kill off tryFamFamInjectivity (now happens in improveWantedTopFunEqs)
- - - - -
3 changed files:
- compiler/GHC/Builtin/Types/Literals.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Tc/Solver/Equality.hs
Changes:
=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -142,23 +142,21 @@ tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
-> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam fam fam_tc tys r
= [(BuiltInFamInteract ax_rule, eqn)
- | ax_rule <- sfInteractTop fam
+ | ax_rule <- sfInteract fam
, Just eqn <- [bifint_proves ax_rule [eqn]] ]
where
eqn :: TypeEqn
eqn = Pair (mkTyConApp fam_tc tys) r
tryInteractInertFam :: BuiltInSynFamily -> TyCon
- -> [Type] -> Type -- F tys1 ~ ty1
- -> [Type] -> Type -- F tys2 ~ ty2
+ -> [Type] -> [Type] -- F tys1 ~ F tys2
-> [(CoAxiomRule, TypeEqn)]
-tryInteractInertFam builtin_fam fam_tc tys1 ty1 tys2 ty2
+tryInteractInertFam builtin_fam fam_tc tys1 tys2
= [(BuiltInFamInteract ax_rule, eqn)
- | ax_rule <- sfInteractInert builtin_fam
- , Just eqn <- [bifint_proves ax_rule [eqn1,eqn2]] ]
+ | ax_rule <- sfInteract builtin_fam
+ , Just eqn <- [bifint_proves ax_rule [eqn]] ]
where
- eqn1 = Pair (mkTyConApp fam_tc tys1) ty1
- eqn2 = Pair (mkTyConApp fam_tc tys2) ty2
+ eqn = Pair (mkTyConApp fam_tc tys1) (mkTyConApp fam_tc tys2)
tryMatchFam :: BuiltInSynFamily -> [Type]
-> Maybe (CoAxiomRule, [Type], Type)
@@ -274,41 +272,58 @@ mkTopBinFamDeduction str fam_tc f
; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
; f a b rhs } }
-mkInteractUnaryFamDeduction :: String -> TyCon
- -> (Type -> Type -> -- F x1 ~ r1
- Type -> Type -> -- F x2 ~ r2
- Maybe TypeEqn)
- -> BuiltInFamInteract
-mkInteractUnaryFamDeduction str fam_tc f
- = BIF_Interact
- { bifint_name = fsLit str
- , bifint_arg_roles = [Nominal, Nominal]
- , bifint_res_role = Nominal
- , bifint_proves = \cs -> do { [Pair lhs1 rhs1, Pair lhs2 rhs2] <- return cs
- ; (tc1, [x1]) <- splitTyConApp_maybe lhs1
- ; (tc2, [x2]) <- splitTyConApp_maybe lhs2
- ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
- ; massertPpr (tc2 == fam_tc) (ppr tc2 $$ ppr fam_tc)
- ; f x1 rhs1 x2 rhs2 } }
-
-mkInteractBinFamDeduction :: String -> TyCon
- -> (Type -> Type -> Type -> -- F x1 y1 ~ r1
- Type -> Type -> Type -> -- F x2 y2 ~ r2
- Maybe TypeEqn)
- -> BuiltInFamInteract
-mkInteractBinFamDeduction str fam_tc f
- = BIF_Interact
- { bifint_name = fsLit str
- , bifint_arg_roles = [Nominal, Nominal]
- , bifint_res_role = Nominal
- , bifint_proves = \cs -> do { [Pair lhs1 rhs1, Pair lhs2 rhs2] <- return cs
--- ; same rhs1 rhs2
- ; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs1
- ; (tc2, [x2,y2]) <- splitTyConApp_maybe lhs2
- ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
- ; massertPpr (tc2 == fam_tc) (ppr tc2 $$ ppr fam_tc)
--- ; f x1 y1 x2 y2 } }
- ; f x1 y1 rhs1 x2 y2 rhs2 } }
+mkUnaryBIF :: String -> TyCon -> BuiltInFamInteract
+mkUnaryBIF str fam_tc
+ = BIF_Interact { bifint_name = fsLit str
+ , bifint_arg_roles = [Nominal]
+ , bifint_res_role = Nominal
+ , bifint_proves = proves }
+ where
+ proves cs
+ | [Pair lhs rhs] <- cs -- Expect one coercion argument
+ = do { (tc2, [x2]) <- splitTyConApp_maybe rhs
+ ; guard (tc2 == fam_tc)
+ ; (tc1, [x1]) <- splitTyConApp_maybe lhs
+ ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
+ ; return (Pair x1 x2) }
+ | otherwise
+ = Nothing
+
+mkBinBIF :: String -> TyCon
+ -> WhichArg -> WhichArg
+ -> (Type -> Bool) -- The guard on the equal args, if any
+ -> BuiltInFamInteract
+mkBinBIF str fam_tc eq1 eq2 check_me
+ = BIF_Interact { bifint_name = fsLit str
+ , bifint_arg_roles = [Nominal]
+ , bifint_res_role = Nominal
+ , bifint_proves = proves }
+ where
+ proves cs
+ | [Pair lhs rhs] <- cs -- Expect one coercion argument
+ = do { (tc2, [x2,y2]) <- splitTyConApp_maybe rhs
+ ; guard (tc2 == fam_tc)
+ ; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs
+ ; massertPpr (tc1 == fam_tc) (ppr tc1 $$ ppr fam_tc)
+ ; case (eq1, eq2) of
+ (ArgX,ArgX) -> do_it x1 x2 y1 y2
+ (ArgX,ArgY) -> do_it x1 y2 x2 y1
+ (ArgY,ArgX) -> do_it y1 x2 y2 x1
+ (ArgY,ArgY) -> do_it y1 y2 x1 x2 }
+ | otherwise
+ = Nothing
+
+ do_it a1 a2 b1 b2 = do { same a1 a2; guard (check_me a1); return (Pair b1 b2) }
+
+noGuard :: Type -> Bool
+noGuard _ = True
+
+numGuard :: (Integer -> Bool) -> Type -> Bool
+numGuard pred ty = case isNumLitTy ty of
+ Just n -> pred n
+ Nothing -> False
+
+data WhichArg = ArgX | ArgY
-------------------------------------------------------------------------------
@@ -341,8 +356,7 @@ typeNatTyCons =
tyConAxiomRules :: TyCon -> [CoAxiomRule]
tyConAxiomRules tc
| Just ops <- isBuiltInSynFamTyCon_maybe tc
- = map BuiltInFamInteract (sfInteractTop ops)
- ++ map BuiltInFamInteract (sfInteractInert ops)
+ = map BuiltInFamInteract (sfInteract ops)
++ map BuiltInFamRewrite (sfMatchFam ops)
| otherwise
= []
@@ -361,9 +375,8 @@ typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x)) $
typeNatAddTyCon :: TyCon
typeNatAddTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily
- { sfMatchFam = axAddMatches
- , sfInteractTop = axAddTops
- , sfInteractInert = axAddInteracts
+ { sfMatchFam = axAddMatches
+ , sfInteract = axAddInteracts
}
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "+")
@@ -382,39 +395,31 @@ axAddMatches
where
tc = typeNatAddTyCon
-axAddTops :: [BuiltInFamInteract]
-axAddTops
+axAddInteracts :: [BuiltInFamInteract]
+axAddInteracts
= [ -- (s + t ~ 0) => (s ~ 0)
- mkTopBinFamDeduction "AddT-0L" typeNatAddTyCon $ \ a _b r ->
+ mkTopBinFamDeduction "AddT-0L" tc $ \ a _b r ->
do { _ <- known r (== 0); return (Pair a (num 0)) }
, -- (s + t ~ 0) => (t ~ 0)
- mkTopBinFamDeduction "AddT-0R" typeNatAddTyCon $ \ _a b r ->
+ mkTopBinFamDeduction "AddT-0R" tc $ \ _a b r ->
do { _ <- known r (== 0); return (Pair b (num 0)) }
, -- (5 + t ~ 8) => (t ~ 3)
- mkTopBinFamDeduction "AddT-KKL" typeNatAddTyCon $ \ a b r ->
+ mkTopBinFamDeduction "AddT-KKL" tc $ \ a b r ->
do { na <- isNumLitTy a; nr <- known r (>= na); return (Pair b (num (nr-na))) }
, -- (s + 5 ~ 8) => (s ~ 3)
- mkTopBinFamDeduction "AddT-KKR" typeNatAddTyCon $ \ a b r ->
- do { nb <- isNumLitTy b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) } ]
+ mkTopBinFamDeduction "AddT-KKR" tc $ \ a b r ->
+ do { nb <- isNumLitTy b; nr <- known r (>= nb); return (Pair a (num (nr-nb))) }
-axAddInteracts :: [BuiltInFamInteract]
-axAddInteracts
- = map mk_ax $
- [ ("AddI-xr", \ x1 y1 z1 x2 y2 z2 -> injCheck x1 x2 z1 z2 y1 y2)
- -- (x1+y1~z1, x2+y2~z2) {x1=x2,z1=z2}=> (y1 ~ y2)
- , ("AddI-xr2", \ x1 y1 z1 x2 y2 z2 -> injCheck x2 y1 z1 z2 x1 y2)
- -- (x1+y1~z1, x2+y2~z2) {x2=y1,z1=z2}=> (x1 ~ y2)
- , ("AddI-yr", \ x1 y1 z1 x2 y2 z2 -> injCheck y1 y2 z1 z2 x1 x2)
- -- (x1+y1~z1, x2+y2~z2) {y1=y2,z1=z2}=> (x1 ~ x2)
- , ("AddI-yr2", \ x1 y1 z1 x2 y2 z2 -> injCheck x1 y2 z1 z2 y1 x2)
- -- (x1+y1~z1, x2+y2~z2) {x1=y2,z1=z2}=> (y1 ~ x2)
+ , mkBinBIF "AddI-xx" tc ArgX ArgX noGuard -- x1+y1~x2+y2 {x1=x2}=> (y1 ~ y2)
+ , mkBinBIF "AddI-xy" tc ArgX ArgY noGuard -- x1+y1~x2+y2 {x1=y2}=> (x2 ~ y1)
+ , mkBinBIF "AddI-yx" tc ArgY ArgX noGuard -- x1+y1~x2+y2 {y1=x2}=> (x1 ~ y2)
+ , mkBinBIF "AddI-yy" tc ArgY ArgY noGuard -- x1+y1~x2+y2 {y1=y2}=> (x1 ~ x2)
]
where
- mk_ax (str, fun) = mkInteractBinFamDeduction str typeNatAddTyCon fun
-
+ tc = typeNatAddTyCon
-------------------------------------------------------------------------------
-- Subtraction (-)
@@ -423,9 +428,8 @@ axAddInteracts
typeNatSubTyCon :: TyCon
typeNatSubTyCon = mkTypeNatFunTyCon2 name
BuiltInSynFamily
- { sfMatchFam = axSubMatches
- , sfInteractTop = axSubTops
- , sfInteractInert = axSubInteracts
+ { sfMatchFam = axSubMatches
+ , sfInteract = axSubInteracts
}
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "-")
@@ -439,20 +443,17 @@ axSubMatches
where
tc = typeNatSubTyCon
-axSubTops :: [BuiltInFamInteract]
-axSubTops -- (a - b ~ 5) => (5 + b ~ a)
- = [ mkTopBinFamDeduction "SubT" typeNatSubTyCon $ \ a b r ->
- do { _ <- isNumLitTy r; return (Pair (r .+. b) a) } ]
-
-
axSubInteracts :: [BuiltInFamInteract]
axSubInteracts
- = [ -- (x-y1 ~ z, x-y2 ~ z) => (y1 ~ y2)
- mkInteractBinFamDeduction "SubI-2" typeNatSubTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- injCheck x1 x2 z1 z2 y1 y2
- , -- (x1-y ~ z, x2-y ~ z) => (x1 ~ x2)
- mkInteractBinFamDeduction "SubI-2" typeNatSubTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- injCheck y1 y2 z1 z2 x1 x2 ]
+ = [ -- (a - b ~ 5) => (5 + b ~ a)
+ mkTopBinFamDeduction "SubT" tc $ \ a b r ->
+ do { _ <- isNumLitTy r; return (Pair (r .+. b) a) }
+
+ , mkBinBIF "SubI-xx" tc ArgX ArgX noGuard -- (x-y1 ~ x-y2) => (y1 ~ y2)
+ , mkBinBIF "SubI-yy" tc ArgY ArgY noGuard -- (x1-y ~ x2-y) => (x1 ~ x2)
+ ]
+ where
+ tc = typeNatSubTyCon
{-
Note [Weakened interaction rule for subtraction]
@@ -492,14 +493,11 @@ something more general.
typeNatMulTyCon :: TyCon
typeNatMulTyCon = mkTypeNatFunTyCon2 name
- BuiltInSynFamily
- { sfMatchFam = axMulMatches
- , sfInteractTop = axMulTops
- , sfInteractInert = axMulInteracts
- }
+ BuiltInSynFamily { sfMatchFam = axMulMatches
+ , sfInteract = axMulInteracts }
where
- name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "*")
- typeNatMulTyFamNameKey typeNatMulTyCon
+ name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "*")
+ typeNatMulTyFamNameKey typeNatMulTyCon
axMulMatches :: [BuiltInFamRewrite]
axMulMatches
@@ -512,33 +510,29 @@ axMulMatches
where
tc = typeNatMulTyCon
-axMulTops :: [BuiltInFamInteract]
-axMulTops
+axMulInteracts :: [BuiltInFamInteract]
+axMulInteracts
= [ -- (s * t ~ 1) => (s ~ 1)
- mkTopBinFamDeduction "MulT1" typeNatMulTyCon $ \ s _t r ->
+ mkTopBinFamDeduction "MulT1" tc $ \ s _t r ->
do { _ <- known r (== 1); return (Pair s r) }
, -- (s * t ~ 1) => (t ~ 1)
- mkTopBinFamDeduction "MulT2" typeNatMulTyCon $ \ _s t r ->
+ mkTopBinFamDeduction "MulT2" tc $ \ _s t r ->
do { _ <- known r (== 1); return (Pair t r) }
, -- (3 * t ~ 15) => (t ~ 5)
- mkTopBinFamDeduction "MulT3" typeNatMulTyCon $ \ s t r ->
+ mkTopBinFamDeduction "MulT3" tc $ \ s t r ->
do { ns <- isNumLitTy s; nr <- isNumLitTy r; y <- divide nr ns; return (Pair t (num y)) }
, -- (s * 3 ~ 15) => (s ~ 5)
- mkTopBinFamDeduction "MulT4" typeNatMulTyCon $ \ s t r ->
- do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) } ]
+ mkTopBinFamDeduction "MulT4" tc $ \ s t r ->
+ do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- divide nr nt; return (Pair s (num y)) }
-axMulInteracts :: [BuiltInFamInteract]
-axMulInteracts
- = [ -- (x*y1 ~ z, x*y2 ~ z) => (y1~y2) if x/=0
- mkInteractBinFamDeduction "MulI1" typeNatMulTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { nx1 <- known x1 (/= 0); _ <- known x2 (== nx1); same z1 z2; return (Pair y1 y2) }
-
- , -- (x1*y ~ z, x2*y ~ z) => (x1~x2) if y/0
- mkInteractBinFamDeduction "MulI2" typeNatMulTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { ny1 <- known y1 (/= 0); _ <- known y2 (== ny1); same z1 z2; return (Pair x1 x2) } ]
+ , mkBinBIF "MulI-xx" tc ArgX ArgX (numGuard (/= 0)) -- (x*y1 ~ x*y2) {x/=0}=> (y1 ~ y2)
+ , mkBinBIF "MulI-yy" tc ArgY ArgY (numGuard (/= 0)) -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
+ ]
+ where
+ tc = typeNatMulTyCon
-------------------------------------------------------------------------------
@@ -547,22 +541,16 @@ axMulInteracts
typeNatDivTyCon :: TyCon
typeNatDivTyCon = mkTypeNatFunTyCon2 name
- BuiltInSynFamily
- { sfMatchFam = axDivMatches
- , sfInteractTop = []
- , sfInteractInert = []
- }
+ BuiltInSynFamily { sfMatchFam = axDivMatches
+ , sfInteract = [] }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Div")
typeNatDivTyFamNameKey typeNatDivTyCon
typeNatModTyCon :: TyCon
typeNatModTyCon = mkTypeNatFunTyCon2 name
- BuiltInSynFamily
- { sfMatchFam = axModMatches
- , sfInteractTop = []
- , sfInteractInert = []
- }
+ BuiltInSynFamily { sfMatchFam = axModMatches
+ , sfInteract = [] }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Mod")
typeNatModTyFamNameKey typeNatModTyCon
@@ -589,11 +577,8 @@ axModMatches
typeNatExpTyCon :: TyCon -- Exponentiation
typeNatExpTyCon = mkTypeNatFunTyCon2 name
- BuiltInSynFamily
- { sfMatchFam = axExpMatches
- , sfInteractTop = axExpTops
- , sfInteractInert = axExpInteracts
- }
+ BuiltInSynFamily { sfMatchFam = axExpMatches
+ , sfInteract = axExpInteracts }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "^")
typeNatExpTyFamNameKey typeNatExpTyCon
@@ -608,40 +593,34 @@ axExpMatches
where
tc = typeNatExpTyCon
-axExpTops :: [BuiltInFamInteract]
-axExpTops
+axExpInteracts :: [BuiltInFamInteract]
+axExpInteracts
= [ -- (s ^ t ~ 0) => (s ~ 0)
- mkTopBinFamDeduction "ExpT1" typeNatExpTyCon $ \ s _t r ->
+ mkTopBinFamDeduction "ExpT1" tc $ \ s _t r ->
do { 0 <- isNumLitTy r; return (Pair s r) }
, -- (2 ^ t ~ 8) => (t ~ 3)
- mkTopBinFamDeduction "ExpT2" typeNatExpTyCon $ \ s t r ->
+ mkTopBinFamDeduction "ExpT2" tc $ \ s t r ->
do { ns <- isNumLitTy s; nr <- isNumLitTy r; y <- logExact nr ns; return (Pair t (num y)) }
, -- (s ^ 2 ~ 9) => (s ~ 3)
- mkTopBinFamDeduction "ExpT3" typeNatExpTyCon $ \ s t r ->
- do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) } ]
+ mkTopBinFamDeduction "ExpT3" tc $ \ s t r ->
+ do { nt <- isNumLitTy t; nr <- isNumLitTy r; y <- rootExact nr nt; return (Pair s (num y)) }
-axExpInteracts :: [BuiltInFamInteract]
-axExpInteracts
- = [ -- (x1^y1 ~ z, x2^y2 ~ z) {x1=x2, x1>1}=> (y1~y2)
- mkInteractBinFamDeduction "ExpI1" typeNatExpTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { nx1 <- known x1 (> 1); _ <- known x2 (== nx1); same z1 z2; return (Pair y1 y2) }
+ , mkBinBIF "ExpI-xx" tc ArgX ArgX (numGuard (> 1)) -- (x^y1 ~ x^y2) {x>1}=> (y1 ~ y2)
+ , mkBinBIF "ExpI-yy" tc ArgY ArgY (numGuard (/= 0)) -- (x1*y ~ x2*y) {y/=0}=> (x1 ~ x2)
+ ]
+ where
+ tc = typeNatExpTyCon
- , -- (x1^y1 ~ z, x2^y2 ~ z) {y1=y2, y1>0}=> (x1~x2)
- mkInteractBinFamDeduction "ExpI2" typeNatExpTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- do { ny1 <- known y1 (> 0); _ <- known y2 (== ny1); same z1 z2; return (Pair x1 x2) } ]
-------------------------------------------------------------------------------
-- Logarithm: Log2
-------------------------------------------------------------------------------
typeNatLogTyCon :: TyCon
typeNatLogTyCon = mkTypeNatFunTyCon1 name
- BuiltInSynFamily
- { sfMatchFam = axLogMatches
- , sfInteractTop = []
- , sfInteractInert = []
- }
+ BuiltInSynFamily { sfMatchFam = axLogMatches
+ , sfInteract = [] }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS (fsLit "Log2")
typeNatLogTyFamNameKey typeNatLogTyCon
@@ -670,10 +649,8 @@ typeNatCmpTyCon
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPENATS_INTERNAL (fsLit "CmpNat")
typeNatCmpTyFamNameKey typeNatCmpTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axCmpNatMatches
- , sfInteractTop = axCmpNatTops
- , sfInteractInert = [] }
+ ops = BuiltInSynFamily { sfMatchFam = axCmpNatMatches
+ , sfInteract = axCmpNatInteracts }
axCmpNatMatches :: [BuiltInFamRewrite]
axCmpNatMatches
@@ -683,9 +660,10 @@ axCmpNatMatches
where
tc = typeNatCmpTyCon
-axCmpNatTops :: [BuiltInFamInteract]
-axCmpNatTops
- = [ mkTopBinFamDeduction "CmpNatT3" typeNatCmpTyCon $ \ s t r ->
+axCmpNatInteracts :: [BuiltInFamInteract]
+axCmpNatInteracts
+ = [ -- s `cmp` t ~ EQ ==> s ~ t
+ mkTopBinFamDeduction "CmpNatT3" typeNatCmpTyCon $ \ s t r ->
do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
-------------------------------------------------------------------------------
@@ -705,10 +683,8 @@ typeSymbolCmpTyCon =
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS_INTERNAL (fsLit "CmpSymbol")
typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axSymbolCmpMatches
- , sfInteractTop = axSymbolCmpTops
- , sfInteractInert = [] }
+ ops = BuiltInSynFamily { sfMatchFam = axSymbolCmpMatches
+ , sfInteract = axSymbolCmpInteracts }
ss,ts :: TyVar -- Of kind Symbol
(ss: ts: _) = mkTemplateTyVars (repeat typeSymbolKind)
@@ -721,8 +697,8 @@ axSymbolCmpMatches
where
tc = typeSymbolCmpTyCon
-axSymbolCmpTops :: [BuiltInFamInteract]
-axSymbolCmpTops
+axSymbolCmpInteracts :: [BuiltInFamInteract]
+axSymbolCmpInteracts
= [ mkTopBinFamDeduction "CmpSymbolT" typeSymbolCmpTyCon $ \ s t r ->
do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
@@ -733,10 +709,8 @@ axSymbolCmpTops
typeSymbolAppendTyCon :: TyCon
typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
- BuiltInSynFamily
- { sfMatchFam = axAppendMatches
- , sfInteractTop = axAppendTops
- , sfInteractInert = axAppendInteracts }
+ BuiltInSynFamily { sfMatchFam = axAppendMatches
+ , sfInteract = axAppendInteracts }
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "AppendSymbol")
typeSymbolAppendFamNameKey typeSymbolAppendTyCon
@@ -750,34 +724,31 @@ axAppendMatches
where
tc = typeSymbolAppendTyCon
-axAppendTops :: [BuiltInFamInteract]
-axAppendTops
+axAppendInteracts :: [BuiltInFamInteract]
+axAppendInteracts
= [ -- (AppendSymbol a b ~ "") => (a ~ "")
- mkTopBinFamDeduction "AppendSymbolT1" typeSymbolAppendTyCon $ \ a _b r ->
+ mkTopBinFamDeduction "AppendSymbolT1" tc $ \ a _b r ->
do { rs <- isStrLitTy r; guard (nullFS rs); return (Pair a nullStrLitTy) }
, -- (AppendSymbol a b ~ "") => (b ~ "")
- mkTopBinFamDeduction "AppendSymbolT2" typeSymbolAppendTyCon $ \ _a b r ->
+ mkTopBinFamDeduction "AppendSymbolT2" tc $ \ _a b r ->
do { rs <- isStrLitTy r; guard (nullFS rs); return (Pair b nullStrLitTy) }
, -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
- mkTopBinFamDeduction "AppendSymbolT3" typeSymbolAppendTyCon $ \ a b r ->
+ mkTopBinFamDeduction "AppendSymbolT3" tc $ \ a b r ->
do { as <- isStrLitTyS a; rs <- isStrLitTyS r; guard (as `isPrefixOf` rs)
; return (Pair b (mkStrLitTyS (drop (length as) rs))) }
, -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
- mkTopBinFamDeduction "AppendSymbolT3" typeSymbolAppendTyCon $ \ a b r ->
+ mkTopBinFamDeduction "AppendSymbolT3" tc $ \ a b r ->
do { bs <- isStrLitTyS b; rs <- isStrLitTyS r; guard (bs `isSuffixOf` rs)
- ; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) } ]
+ ; return (Pair a (mkStrLitTyS (take (length rs - length bs) rs))) }
-axAppendInteracts :: [BuiltInFamInteract]
-axAppendInteracts
- = [ -- (AppendSymbol x1 y1 ~ z, AppendSymbol x2 y2 ~ z) {x1=x2}=> (y1 ~ y2)
- mkInteractBinFamDeduction "AppI1" typeSymbolAppendTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- injCheck x1 x2 z1 z2 y1 y2
- , -- (AppendSymbol x1 y1 ~ z, AppendSymbol x2 y2 ~ z) {y1=y2}=> (x1 ~ x2)
- mkInteractBinFamDeduction "AppI2" typeSymbolAppendTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- injCheck y1 y2 z1 z2 x1 x2 ]
+ , mkBinBIF "AppI-xx" tc ArgX ArgX noGuard -- (x++y1 ~ x++y2) => (y1 ~ y2)
+ , mkBinBIF "AppI-yy" tc ArgY ArgY noGuard -- (x1++y ~ x2++y) => (x1 ~ x2)
+ ]
+ where
+ tc = typeSymbolAppendTyCon
-------------------------------------------------------------------------------
-- ConsSymbol
@@ -795,10 +766,8 @@ typeConsSymbolTyCon =
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "ConsSymbol")
typeConsSymbolTyFamNameKey typeConsSymbolTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axConsMatches
- , sfInteractTop = axConsTops
- , sfInteractInert = axConsInteracts }
+ ops = BuiltInSynFamily { sfMatchFam = axConsMatches
+ , sfInteract = axConsInteracts }
axConsMatches :: [BuiltInFamRewrite]
axConsMatches
@@ -807,24 +776,22 @@ axConsMatches
where
tc = typeConsSymbolTyCon
-axConsTops :: [BuiltInFamInteract]
-axConsTops
+axConsInteracts :: [BuiltInFamInteract]
+axConsInteracts
= [ -- ConsSymbol a b ~ "blah" => (a ~ 'b')
- mkTopBinFamDeduction "ConsSymbolT1" typeConsSymbolTyCon $ \ a _b r ->
+ mkTopBinFamDeduction "ConsSymbolT1" tc $ \ a _b r ->
do { rs <- isStrLitTy r; (x,_) <- unconsFS rs; return (Pair a (mkCharLitTy x)) }
, -- ConsSymbol a b ~ "blah" => (b ~ "lah")
- mkTopBinFamDeduction "ConsSymbolT2" typeConsSymbolTyCon $ \ _a b r ->
- do { rs <- isStrLitTy r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) } ]
+ mkTopBinFamDeduction "ConsSymbolT2" tc $ \ _a b r ->
+ do { rs <- isStrLitTy r; (_,xs) <- unconsFS rs; return (Pair b (mkStrLitTy xs)) }
-axConsInteracts :: [BuiltInFamInteract]
-axConsInteracts
- = [ -- (ConsSymbol x1 y1 ~ z, ConsSymbol x2 y2 ~ z) {x1=x2}=> (y1 ~ y2)
- mkInteractBinFamDeduction "AppI1" typeConsSymbolTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- injCheck x1 x2 z1 z2 y1 y2
- , -- (ConsSymbol x1 y1 ~ z, AppendSymbol x2 y2 ~ z) {y1=y2}=> (x1 ~ x2)
- mkInteractBinFamDeduction "AppI1" typeConsSymbolTyCon $ \ x1 y1 z1 x2 y2 z2 ->
- injCheck y1 y2 z1 z2 x1 x2 ]
+
+ , mkBinBIF "ConsI-xx" tc ArgX ArgX noGuard -- (x:y1 ~ x:y2) => (y1 ~ y2)
+ , mkBinBIF "ConsI-yy" tc ArgY ArgY noGuard -- (x1:y ~ x2:y) => (x1 ~ x2)
+ ]
+ where
+ tc = typeConsSymbolTyCon
-------------------------------------------------------------------------------
-- UnconsSymbol
@@ -842,10 +809,8 @@ typeUnconsSymbolTyCon =
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "UnconsSymbol")
typeUnconsSymbolTyFamNameKey typeUnconsSymbolTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axUnconsMatches
- , sfInteractTop = axUnconsTops
- , sfInteractInert = axUnconsInteracts }
+ ops = BuiltInSynFamily { sfMatchFam = axUnconsMatches
+ , sfInteract = axUnconsInteracts }
computeUncons :: FastString -> Type
computeUncons str
@@ -861,25 +826,24 @@ axUnconsMatches
where
tc = typeUnconsSymbolTyCon
-axUnconsTops :: [BuiltInFamInteract]
-axUnconsTops
+axUnconsInteracts :: [BuiltInFamInteract]
+axUnconsInteracts
= [ -- (UnconsSymbol b ~ Nothing) => (b ~ "")
- mkTopUnaryFamDeduction "UnconsSymbolT1" typeUnconsSymbolTyCon $ \b r ->
+ mkTopUnaryFamDeduction "UnconsSymbolT1" tc $ \b r ->
do { Nothing <- isPromotedMaybeTy r; return (Pair b nullStrLitTy) }
, -- (UnconsSymbol b ~ Just ('f',"oobar")) => (b ~ "foobar")
- mkTopUnaryFamDeduction "UnconsSymbolT2" typeUnconsSymbolTyCon $ \b r ->
+ mkTopUnaryFamDeduction "UnconsSymbolT2" tc $ \b r ->
do { Just pr <- isPromotedMaybeTy r
; (c,s) <- isPromotedPairType pr
; chr <- isCharLitTy c
; str <- isStrLitTy s
- ; return (Pair b (mkStrLitTy (consFS chr str))) } ]
+ ; return (Pair b (mkStrLitTy (consFS chr str))) }
-axUnconsInteracts :: [BuiltInFamInteract]
-axUnconsInteracts
- = [ -- (UnconsSymbol x1 ~ z, UnconsSymbol x2 ~ z) => (x1 ~ x2)
- mkInteractUnaryFamDeduction "UnconsI1" typeUnconsSymbolTyCon $ \ x1 z1 x2 z2 ->
- do { same z1 z2; return (Pair x1 x2) } ]
+ , mkUnaryBIF "UnconsI1" tc -- (UnconsSymbol x1 ~ z, UnconsSymbol x2 ~ z) => (x1 ~ x2)
+ ]
+ where
+ tc = typeUnconsSymbolTyCon
-------------------------------------------------------------------------------
-- CharToNat
@@ -897,11 +861,8 @@ typeCharToNatTyCon =
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "CharToNat")
typeCharToNatTyFamNameKey typeCharToNatTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axCharToNatMatches
- , sfInteractTop = axCharToNatTops
- , sfInteractInert = []
- }
+ ops = BuiltInSynFamily { sfMatchFam = axCharToNatMatches
+ , sfInteract = axCharToNatInteracts }
axCharToNatMatches :: [BuiltInFamRewrite]
axCharToNatMatches
@@ -910,8 +871,8 @@ axCharToNatMatches
where
tc = typeCharToNatTyCon
-axCharToNatTops :: [BuiltInFamInteract]
-axCharToNatTops
+axCharToNatInteracts :: [BuiltInFamInteract]
+axCharToNatInteracts
= [ -- (CharToNat c ~ 122) => (c ~ 'z')
mkTopUnaryFamDeduction "CharToNatT1" typeCharToNatTyCon $ \c r ->
do { nr <- isNumLitTy r; chr <- integerToChar nr; return (Pair c (mkCharLitTy chr)) } ]
@@ -932,10 +893,8 @@ typeNatToCharTyCon =
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS (fsLit "NatToChar")
typeNatToCharTyFamNameKey typeNatToCharTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axNatToCharMatches
- , sfInteractTop = axNatToCharTops
- , sfInteractInert = [] }
+ ops = BuiltInSynFamily { sfMatchFam = axNatToCharMatches
+ , sfInteract = axNatToCharInteracts }
axNatToCharMatches :: [BuiltInFamRewrite]
axNatToCharMatches
@@ -944,8 +903,8 @@ axNatToCharMatches
where
tc = typeNatToCharTyCon
-axNatToCharTops :: [BuiltInFamInteract]
-axNatToCharTops
+axNatToCharInteracts :: [BuiltInFamInteract]
+axNatToCharInteracts
= [ -- (NatToChar n ~ 'z') => (n ~ 122)
mkTopUnaryFamDeduction "CharToNatT1" typeNatToCharTyCon $ \n r ->
do { c <- isCharLitTy r; return (Pair n (mkNumLitTy (charToInteger c))) } ]
@@ -967,11 +926,8 @@ typeCharCmpTyCon =
where
name = mkWiredInTyConName UserSyntax gHC_INTERNAL_TYPELITS_INTERNAL (fsLit "CmpChar")
typeCharCmpTyFamNameKey typeCharCmpTyCon
- ops = BuiltInSynFamily
- { sfMatchFam = axCharCmpMatches
- , sfInteractTop = axCharCmpTops
- , sfInteractInert = []
- }
+ ops = BuiltInSynFamily { sfMatchFam = axCharCmpMatches
+ , sfInteract = axCharCmpInteracts }
sc :: TyVar -- Of kind Char
(sc: _) = mkTemplateTyVars (repeat charTy)
@@ -984,8 +940,8 @@ axCharCmpMatches
where
tc = typeCharCmpTyCon
-axCharCmpTops :: [BuiltInFamInteract]
-axCharCmpTops
+axCharCmpInteracts :: [BuiltInFamInteract]
+axCharCmpInteracts
= [ -- (CmpChar s t ~ EQ) => s ~ t
mkTopBinFamDeduction "CmpCharT" typeCharCmpTyCon $ \ s t r ->
do { EQ <- isOrderingLitTy r; return (Pair s t) } ]
@@ -1101,11 +1057,6 @@ mkTypeSymbolFunTyCon2 op tcb =
Nothing
NotInjective
-injCheck :: Type -> Type -> Type -> Type -> Type -> Type -> Maybe TypeEqn
--- If x1=x2 and y1=y2, emit z1=z2
-injCheck x1 x2 y1 y2 z1 z2
- = do { guard (x1 `tcEqType` x2); guard (y1 `tcEqType` y2); return (Pair z1 z2) }
-
same :: Type -> Type -> Maybe ()
same ty1 ty2 = guard (ty1 `tcEqType` ty2)
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -251,7 +251,7 @@ data CoAxBranch
-- cab_tvs and cab_lhs may be eta-reduced; see
-- Note [Eta reduction for data families]
, cab_cvs :: [CoVar]
- -- ^ Bound coercion variables
+ -- ^ Bound coercion variables
-- Always empty, for now.
-- See Note [Constraints in patterns]
-- in GHC.Tc.TyCl
@@ -654,22 +654,14 @@ instance Outputable CoAxiomRule where
data BuiltInSynFamily = BuiltInSynFamily
{ sfMatchFam :: [BuiltInFamRewrite]
- , sfInteractTop :: [BuiltInFamInteract]
+ , sfInteract:: [BuiltInFamInteract]
-- If given these type arguments and RHS, returns the equalities that
-- are guaranteed to hold. That is, if
- -- (ar, Pair s1 s2) is an element ofo (sfInteractTop tys ty)
+ -- (ar, Pair s1 s2) is an element of (sfInteract tys ty)
-- then AxiomRule ar [co :: F tys ~ ty] :: s1~s2
-
- , sfInteractInert :: [BuiltInFamInteract]
- -- If given one set of arguments and result, and another set of arguments
- -- and result, returns the equalities that are guaranteed to hold.
}
-- Provides default implementations that do nothing.
trivialBuiltInFamily :: BuiltInSynFamily
-trivialBuiltInFamily = BuiltInSynFamily
- { sfMatchFam = []
- , sfInteractTop = []
- , sfInteractInert = []
- }
+trivialBuiltInFamily = BuiltInSynFamily { sfMatchFam = [], sfInteract = [] }
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -44,7 +44,6 @@ import GHC.Types.Var.Set( anyVarSet )
import GHC.Types.Name.Reader
import GHC.Types.Basic
-import GHC.Builtin.Types ( anyTypeOfKind )
import GHC.Builtin.Types.Literals ( tryInteractTopFam, tryInteractInertFam )
import GHC.Utils.Outputable
@@ -1716,18 +1715,11 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
then finish_with_swapping
else finish_without_swapping
- | TyFamLHS fun_tc1 fun_args1 <- lhs1
- , TyFamLHS fun_tc2 fun_args2 <- lhs2
+ | TyFamLHS _fun_tc1 fun_args1 <- lhs1
+ , TyFamLHS _fun_tc2 fun_args2 <- lhs2
-- See Note [Decomposing type family applications]
= do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
-
- ; unifications_done <- tryFamFamInjectivity ev eq_rel
- fun_tc1 fun_args1 fun_tc2 fun_args2 mco
- ; if unifications_done
- then -- Go round again, since the unifications affect lhs/rhs
- startAgainWith (mkNonCanonical ev)
- else
- do { tclvl <- getTcLevel
+ ; tclvl <- getTcLevel
; let tvs1 = tyCoVarsOfTypes fun_args1
tvs2 = tyCoVarsOfTypes fun_args2
@@ -1746,7 +1738,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-- if swap_for_rewriting doesn't care either way
; if swap_for_rewriting || (meta_tv_lhs == meta_tv_rhs && swap_for_size)
then finish_with_swapping
- else finish_without_swapping } }
+ else finish_without_swapping }
where
sym_mco = mkSymMCo mco
role = eqRelRole eq_rel
@@ -2945,55 +2937,6 @@ equality with the template on the left. Delicate, but it works.
-}
-tryFamFamInjectivity :: CtEvidence -> EqRel
- -> TyCon -> [TcType] -> TyCon -> [TcType] -> MCoercion
- -> TcS Bool -- True <=> some unification happened
-tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
- | ReprEq <- eq_rel
- = return False -- Injectivity applies only for Nominal equalities
- | fun_tc1 /= fun_tc2
- = return False -- If the families don't match, stop.
-
- -- Is F an injective type family
- | isWanted ev -- Injectivity conditions only work for Wanteds
- , Injective inj <- tyConInjectivityInfo fun_tc1
- = unifyFunDeps ev Nominal $ \uenv ->
- uPairsTcM uenv [ Pair ty1 ty2
- | (ty1,ty2,True) <- zip3 fun_args1 fun_args2 inj ]
-
- -- Built-in synonym families don't have an entry point for this
- -- use case. So, we just use sfInteractInert and pass two equal
- -- RHSs. We *could* add another entry point, but then there would
- -- be a burden to make sure the new entry point and existing ones
- -- were internally consistent. This is slightly distasteful, but
- -- it works well in practice and localises the problem. Ugh.
- --
- -- This path works both Wanteds and Givens
- | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1
- = let tc_kind = tyConKind fun_tc1
- ki1 = piResultTys tc_kind fun_args1
- ki2 | MRefl <- mco
- = ki1 -- just a small optimisation
- | otherwise
- = piResultTys tc_kind fun_args2
-
- fake_rhs1 = anyTypeOfKind ki1
- fake_rhs2 = anyTypeOfKind ki2
-
- eqs :: [TypeEqn]
- eqs = map snd $ tryInteractInertFam ops fun_tc1
- fun_args1 fake_rhs1 fun_args2 fake_rhs2
- in
- do { traceTcS "famfam" (vcat [ppr fun_tc1
- , text "1side" <+> ppr fun_args1 <+> ppr fake_rhs1
- , text "2side" <+> ppr fun_args2 <+> ppr fake_rhs2
- , ppr eqs ])
- ; unifyFunDeps ev Nominal $ \uenv ->
- uPairsTcM uenv eqs }
-
- | otherwise -- ordinary, non-injective type family
- = return False
-
--------------------
tryFunDeps :: EqRel -> EqCt -> SolverStage ()
tryFunDeps eq_rel work_item@(EqCt { eq_lhs = lhs, eq_ev = ev })
@@ -3011,12 +2954,15 @@ tryFunDeps eq_rel work_item@(EqCt { eq_lhs = lhs, eq_ev = ev })
--------------------
improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
+-- TyCon is definitely a type family
-- See Note [FunDep and implicit parameter reactions]
improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs_ty })
| isGiven ev = improveGivenTopFunEqs fam_tc args ev rhs_ty
| otherwise = improveWantedTopFunEqs fam_tc args ev rhs_ty
improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
+-- TyCon is definitely a type family
+-- Work-item is a Given
improveGivenTopFunEqs fam_tc args ev rhs_ty
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
= do { traceTcS "improveGivenTopFunEqs" (ppr fam_tc <+> ppr args $$ ppr ev $$ ppr rhs_ty)
@@ -3026,14 +2972,15 @@ improveGivenTopFunEqs fam_tc args ev rhs_ty
, let new_co = mkAxiomRuleCo ax [given_co] ]
; return False } -- False: no unifications
| otherwise
- = return False -- See Note [No Given/Given fundeps]
+ = return False
where
given_co :: Coercion = ctEvCoercion ev
improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
+-- TyCon is definitely a type family
+-- Work-item is a Wanted
improveWantedTopFunEqs fam_tc args ev rhs_ty
- = do { fam_envs <- getFamInstEnvs
- ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs_ty
+ = do { eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty
; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs_ty
, ppr eqns ])
; unifyFunDeps ev Nominal $ \uenv ->
@@ -3046,83 +2993,86 @@ improveWantedTopFunEqs fam_tc args ev rhs_ty
-- ToDo: this location is wrong; it should be FunDepOrigin2
-- See #14778
-improve_top_fun_eqs :: FamInstEnvs
- -> TyCon -> [TcType] -> Xi
- -> TcS [TypeEqn]
-improve_top_fun_eqs fam_envs fam_tc args rhs_ty
+improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi
+ -> TcS [TypeEqn]
+-- TyCon is definitely a type family
+improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
- = return (map snd $ tryInteractTopFam ops fam_tc args rhs_ty)
-
- -- see Note [Type inference for type families with injectivity]
- | isOpenTypeFamilyTyCon fam_tc
- , Injective injective_args <- tyConInjectivityInfo fam_tc
- , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
- = -- it is possible to have several compatible equations in an open type
- -- family but we only want to derive equalities from one such equation.
- do { let improvs = buildImprovementData fam_insts
- fi_tvs fi_tys fi_rhs (const Nothing)
-
- ; traceTcS "improve_top_fun_eqs2" (ppr improvs)
- ; concatMapM (injImproveEqns injective_args) $
- take 1 improvs }
-
- | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
- , Injective injective_args <- tyConInjectivityInfo fam_tc
- = concatMapM (injImproveEqns injective_args) $
- buildImprovementData (fromBranches (co_ax_branches ax))
- cab_tvs cab_lhs cab_rhs Just
+ = return (map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty)
- | otherwise
+ -- See Note [Type inference for type families with injectivity]
+ | Injective inj_args <- tyConInjectivityInfo fam_tc
+ = do { fam_envs <- getFamInstEnvs
+ ; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
+ ; let local_eqns = improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty
+ ; return (local_eqns ++ top_eqns) }
+
+ | otherwise -- No injectivity
= return []
+improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn]
+-- Interact with top-level instance declarations
+improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
+ = concatMapM do_one branches
where
- in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty)
-
- buildImprovementData
- :: [a] -- axioms for a TF (FamInst or CoAxBranch)
- -> (a -> [TyVar]) -- get bound tyvars of an axiom
- -> (a -> [Type]) -- get LHS of an axiom
- -> (a -> Type) -- get RHS of an axiom
- -> (a -> Maybe CoAxBranch) -- Just => apartness check required
- -> [( [Type], Subst, [TyVar], Maybe CoAxBranch )]
- -- Result:
- -- ( [arguments of a matching axiom]
- -- , RHS-unifying substitution
- -- , axiom variables without substitution
- -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
- buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
- [ (ax_args, subst, unsubstTvs, wrap axiom)
- | axiom <- axioms
- , let ax_args = axiomLHS axiom
- ax_rhs = axiomRHS axiom
- ax_tvs = axiomTVs axiom
- in_scope1 = in_scope `extendInScopeSetList` ax_tvs
- , Just subst <- [tcUnifyTyWithTFs False in_scope1 ax_rhs rhs_ty]
- , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
- unsubstTvs = filter (notInSubst <&&> isTyVar) ax_tvs ]
- -- The order of unsubstTvs is important; it must be
- -- in telescope order e.g. (k:*) (a:k)
-
- injImproveEqns :: [Bool]
- -> ([Type], Subst, [TyCoVar], Maybe CoAxBranch)
- -> TcS [TypeEqn]
- injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
- = do { subst <- instFlexiX subst unsubstTvs
- -- If the current substitution bind [k -> *], and
- -- one of the un-substituted tyvars is (a::k), we'd better
- -- be sure to apply the current substitution to a's kind.
- -- Hence instFlexiX. #13135 was an example.
-
- ; return [ Pair (substTy subst ax_arg) arg
- -- NB: the ax_arg part is on the left
- -- see Note [Improvement orientation]
- | case cabr of
- Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
- _ -> True
- , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
-
-
-improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS Bool
+ branches :: [CoAxBranch]
+ branches | isOpenTypeFamilyTyCon fam_tc
+ , (fam_inst1 : _) <- lookupFamInstEnvByTyCon fam_envs fam_tc
+ = fromBranches (coAxiomBranches (fi_axiom fam_inst1))
+ -- fam_inst1: It is possible to have several compatible equations in an open
+ -- type family but we only want to derive equalities from one such equation.
+
+ | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
+ = fromBranches (coAxiomBranches ax)
+
+ | otherwise
+ = []
+
+ do_one :: CoAxBranch -> TcS [TypeEqn]
+ do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs })
+ | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs
+ , Just subst <- tcUnifyTyWithTFs False in_scope1 branch_rhs rhs_ty
+ = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst
+ unsubstTvs = filterOut inSubst branch_tvs
+ -- The order of unsubstTvs is important; it must be
+ -- in telescope order e.g. (k:*) (a:k)
+
+ ; subst <- instFlexiX subst unsubstTvs
+ -- If the current substitution bind [k -> *], and
+ -- one of the un-substituted tyvars is (a::k), we'd better
+ -- be sure to apply the current substitution to a's kind.
+ -- Hence instFlexiX. #13135 was an example.
+
+ ; if apartnessCheck (substTys subst branch_lhs_tys) branch
+ then return (mkInjectivityEqns inj_args (map (substTy subst) branch_lhs_tys) lhs_tys)
+ -- NB: The fresh unification variables (from unsubstTvs) are on the left
+ -- See Note [Improvement orientation]
+ else return [] }
+ | otherwise
+ = return []
+
+ in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty)
+
+
+improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [TypeEqn]
+-- Interact with itself, specifically F s1 s2 ~ F t1 t2
+improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty
+ | Just (tc, rhs_tys) <- tcSplitTyConApp_maybe rhs_ty
+ , tc == fam_tc
+ = mkInjectivityEqns inj_args lhs_tys rhs_tys
+ | otherwise
+ = []
+
+mkInjectivityEqns :: [Bool] -> [TcType] -> [TcType] -> [TypeEqn]
+-- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True]
+-- return the equations [Pair s1 t1, Pair s3 t3]
+mkInjectivityEqns inj_args lhs_args rhs_args
+ = [ Pair lhs_arg rhs_arg | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]
+
+---------------------------------------------
+improveLocalFunEqs :: InertCans
+ -> TyCon -> [TcType] -> EqCt -- F args ~ rhs
+ -> TcS Bool
-- Emit equalities from interaction between two equalities
improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
| isGiven work_ev = improveGivenLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs
@@ -3138,8 +3088,8 @@ improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
improveGivenLocalFunEqs :: [EqCt] -- Inert items, mixture of Given and Wanted
- -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item
- -> TcS Bool -- True <=> Something was emitted
+ -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Given)
+ -> TcS Bool -- Always False (no unifications)
-- Emit equalities from interaction between two Given type-family equalities
-- e.g. (x+y1~z, x+y2~z) => (y1 ~ y2)
improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
@@ -3152,12 +3102,15 @@ improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
given_co :: Coercion = ctEvCoercion work_ev
do_one :: BuiltInSynFamily -> EqCt -> TcS ()
- do_one ops (EqCt { eq_ev = inert_ev
- , eq_lhs = TyFamLHS _ inert_args
- , eq_rhs = inert_rhs })
- | isGiven inert_ev
+ -- Used only work-item is Given
+ do_one ops EqCt { eq_ev = inert_ev, eq_lhs = inert_lhs, eq_rhs = inert_rhs }
+ | isGiven inert_ev -- Given/Given interaction
+ , TyFamLHS _ inert_args <- inert_lhs -- Inert item is F inert_args ~ inert_rhs
+ , work_rhs `tcEqType` inert_rhs -- Both RHSs are the same
, not (null pairs)
- = do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args
+ = -- So we have work_ev : F work_args ~ rhs
+ -- inert_ev : F inert_args ~ rhs
+ do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args
, text "work_ev" <+> ppr work_ev
, text "inert_ev" <+> ppr inert_ev
, ppr work_rhs
@@ -3167,17 +3120,20 @@ improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
-- fact that it's a combination of Givens, but I don't
-- this that matters.
where
- pairs = [ (Nominal, new_co)
- | (ax, _) <- tryInteractInertFam ops fam_tc
- work_args work_rhs inert_args inert_rhs
- , let new_co = mkAxiomRuleCo ax [given_co, ctEvCoercion inert_ev] ]
+ pairs = [ (Nominal, mkAxiomRuleCo ax [combined_co])
+ | (ax, _) <- tryInteractInertFam ops fam_tc work_args inert_args
+ , let -- given_co :: F work_args ~ rhs
+ -- inert_co :: F inert_args ~ rhs
+ -- the_co :: F work_args ~ F inert_args
+ inert_co = ctEvCoercion inert_ev
+ combined_co = given_co `mkTransCo` mkSymCo inert_co ]
do_one _ _ = return ()
improveWantedLocalFunEqs
:: [EqCt] -- Inert items (Given and Wanted)
- -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (wanted)
- -> TcS Bool
+ -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Wanted)
+ -> TcS Bool -- True <=> some unifications
-- Emit improvement equalities for a Wanted constraint, by comparing
-- the current work item with inert CFunEqs (boh Given and Wanted)
-- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y'
@@ -3212,17 +3168,18 @@ improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs
--------------------
do_one_built_in ops rhs (EqCt { eq_lhs = TyFamLHS _ iargs, eq_rhs = irhs, eq_ev = inert_ev })
- = mk_fd_eqns inert_ev (map snd $ tryInteractInertFam ops fam_tc args rhs iargs irhs)
+ | irhs `tcEqType` rhs
+ = mk_fd_eqns inert_ev (map snd $ tryInteractInertFam ops fam_tc args iargs)
+ | otherwise
+ = []
do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -- TyVarLHS
--------------------
-- See Note [Type inference for type families with injectivity]
do_one_injective inj_args rhs (EqCt { eq_lhs = TyFamLHS _ inert_args
, eq_rhs = irhs, eq_ev = inert_ev })
- | not (isGiven inert_ev && isGiven work_ev) -- See Note [No Given/Given fundeps]
- , rhs `tcEqType` irhs
- = mk_fd_eqns inert_ev $ [ Pair arg iarg
- | (arg, iarg, True) <- zip3 args inert_args inj_args ]
+ | rhs `tcEqType` irhs
+ = mk_fd_eqns inert_ev $ mkInjectivityEqns inj_args args inert_args
| otherwise
= []
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d109ecb026479ffd64b8b227fdebae2db6b2afff
--
This project does not include diff previews in email notifications.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d109ecb026479ffd64b8b227fdebae2db6b2afff
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240704/cbf24d35/attachment-0001.html>
More information about the ghc-commits
mailing list