[Git][ghc/ghc][wip/T24978] 2 commits: Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Jul 12 16:37:46 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
cbd0aa15 by Simon Peyton Jones at 2024-07-12T17:10:12+01:00
Wibbles
- - - - -
493b80a9 by Simon Peyton Jones at 2024-07-12T17:37:12+01:00
Typo in coercionKind
- - - - -
23 changed files:
- compiler/GHC/Builtin/Types/Literals.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/TyCo/Tidy.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Data/Pair.hs
- compiler/GHC/Iface/Rename.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
Changes:
=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -33,7 +33,7 @@ import GHC.Prelude
import GHC.Core.Type
import GHC.Core.Unify ( tcMatchTys )
import GHC.Data.Pair
-import GHC.Core.TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon
+import GHC.Core.TyCon ( TyCon, FamTyConFlav(..), mkFamilyTyCon, tyConArity
, Injectivity(..), isBuiltInSynFamTyCon_maybe )
import GHC.Core.Coercion.Axiom
import GHC.Core.TyCo.Compare ( tcEqType )
@@ -64,7 +64,6 @@ import GHC.Builtin.Names
)
import GHC.Data.FastString
import GHC.Utils.Panic
-import GHC.Utils.Misc
import GHC.Utils.Outputable
import Control.Monad ( guard )
@@ -141,28 +140,28 @@ There are a few steps to adding a built-in type family:
tryInteractTopFam :: BuiltInSynFamily -> TyCon -> [Type] -> Type
-> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam fam fam_tc tys r
- = [(BuiltInFamInteract ax_rule, eqn)
+ = [(BuiltInFamInteract ax_rule, eqn_out)
| ax_rule <- sfInteract fam
- , Just eqn <- [bifint_proves ax_rule [eqn]] ]
+ , Just eqn_out <- [bifint_proves ax_rule eqn_in] ]
where
- eqn :: TypeEqn
- eqn = Pair (mkTyConApp fam_tc tys) r
+ eqn_in :: TypeEqn
+ eqn_in = Pair (mkTyConApp fam_tc tys) r
tryInteractInertFam :: BuiltInSynFamily -> TyCon
-> [Type] -> [Type] -- F tys1 ~ F tys2
-> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam builtin_fam fam_tc tys1 tys2
- = [(BuiltInFamInteract ax_rule, eqn)
+ = [(BuiltInFamInteract ax_rule, eqn_out)
| ax_rule <- sfInteract builtin_fam
- , Just eqn <- [bifint_proves ax_rule [eqn]] ]
+ , Just eqn_out <- [bifint_proves ax_rule eqn_in] ]
where
- eqn = Pair (mkTyConApp fam_tc tys1) (mkTyConApp fam_tc tys2)
+ eqn_in = Pair (mkTyConApp fam_tc tys1) (mkTyConApp fam_tc tys2)
tryMatchFam :: BuiltInSynFamily -> [Type]
-> Maybe (BuiltInFamRewrite, [Type], Type)
-- Does this reduce on the given arguments?
-- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
--- That is: mkAxiomRuleCo ax (zipWith mkReflCo (coAxArgRuleRoles ax) ts)
+-- That is: mkAxiomCo ax (zipWith mkReflCo (coAxArgRuleRoles ax) ts)
-- :: F tys ~r rhs,
tryMatchFam builtin_fam arg_tys
= listToMaybe $ -- Pick first rule to match
@@ -179,11 +178,11 @@ mkUnaryConstFoldAxiom :: TyCon -> String
-> (a -> Maybe Type)
-> BuiltInFamRewrite
-- For the definitional axioms, like (3+4 --> 7)
-mkUnaryConstFoldAxiom tc str isReqTy f
+mkUnaryConstFoldAxiom fam_tc str isReqTy f
= BIF_Rewrite
{ bifrw_name = fsLit str
- , bifrw_arg_roles = [Nominal]
- , bifrw_res_role = Nominal
+ , bifrw_fam_tc = fam_tc
+ , bifrw_arity = 1
, bifrw_match = \ts -> do { [t1] <- return ts
; t1' <- isReqTy t1
; res <- f t1'
@@ -191,7 +190,7 @@ mkUnaryConstFoldAxiom tc str isReqTy f
, bifrw_proves = \cs -> do { [Pair s1 s2] <- return cs
; s2' <- isReqTy s2
; z <- f s2'
- ; return (mkTyConApp tc [s1] === z) }
+ ; return (mkTyConApp fam_tc [s1] === z) }
}
mkBinConstFoldAxiom :: TyCon -> String
@@ -200,11 +199,11 @@ mkBinConstFoldAxiom :: TyCon -> String
-> (a -> b -> Maybe Type)
-> BuiltInFamRewrite
-- For the definitional axioms, like (3+4 --> 7)
-mkBinConstFoldAxiom tc str isReqTy1 isReqTy2 f
+mkBinConstFoldAxiom fam_tc str isReqTy1 isReqTy2 f
= BIF_Rewrite
{ bifrw_name = fsLit str
- , bifrw_arg_roles = [Nominal, Nominal]
- , bifrw_res_role = Nominal
+ , bifrw_fam_tc = fam_tc
+ , bifrw_arity = 2
, bifrw_match = \ts -> do { [t1,t2] <- return ts
; t1' <- isReqTy1 t1
; t2' <- isReqTy2 t2
@@ -214,31 +213,35 @@ mkBinConstFoldAxiom tc str isReqTy1 isReqTy2 f
; s2' <- isReqTy1 s2
; t2' <- isReqTy2 t2
; z <- f s2' t2'
- ; return (mkTyConApp tc [s1,t1] === z) }
+ ; return (mkTyConApp fam_tc [s1,t1] === z) }
}
mkRewriteAxiom :: TyCon -> String
- -> [TyVar] -> [Type] -- LHS
- -> Type -- RHS
+ -> [TyVar] -> [Type] -- LHS of axiom
+ -> Type -- RHS or axiom
-> BuiltInFamRewrite
-mkRewriteAxiom tc str tpl_tvs lhs_tys rhs_ty
- = BIF_Rewrite
- { bifrw_name = fsLit str
- , bifrw_arg_roles = [Nominal | _ <- tpl_tvs]
- , bifrw_res_role = Nominal
- , bifrw_match = match_fn
- , bifrw_proves = inst_fn }
+mkRewriteAxiom fam_tc str tpl_tvs lhs_tys rhs_ty
+ = assertPpr (tyConArity fam_tc == length lhs_tys) (text str <+> ppr lhs_tys) $
+ BIF_Rewrite
+ { bifrw_name = fsLit str
+ , bifrw_fam_tc = fam_tc
+ , bifrw_arity = bif_arity
+ , bifrw_match = match_fn
+ , bifrw_proves = inst_fn }
where
+ bif_arity = length tpl_tvs
+
match_fn :: [Type] -> Maybe ([Type],Type)
match_fn arg_tys
- = case tcMatchTys lhs_tys arg_tys of
+ = assertPpr (tyConArity fam_tc == length arg_tys) (text str <+> ppr arg_tys) $
+ case tcMatchTys lhs_tys arg_tys of
Nothing -> Nothing
Just subst -> Just (substTyVars subst tpl_tvs, substTy subst rhs_ty)
inst_fn :: [TypeEqn] -> Maybe TypeEqn
inst_fn inst_eqns
- = assertPpr (inst_eqns `equalLength` tpl_tvs) (text str $$ ppr inst_eqns) $
- Just (mkTyConApp tc (substTys (zipTCvSubst tpl_tvs tys1) lhs_tys)
+ = assertPpr (length inst_eqns == bif_arity) (text str $$ ppr inst_eqns) $
+ Just (mkTyConApp fam_tc (substTys (zipTCvSubst tpl_tvs tys1) lhs_tys)
===
substTy (zipTCvSubst tpl_tvs tys2) rhs_ty)
where
@@ -251,12 +254,10 @@ mkTopUnaryFamDeduction :: String -> TyCon
mkTopUnaryFamDeduction str fam_tc f
= BIF_Interact
{ bifint_name = fsLit str
- , bifint_arg_roles = [Nominal]
- , bifint_res_role = Nominal
- , bifint_proves = \cs -> do { [Pair lhs rhs] <- return cs
- ; (tc, [a]) <- splitTyConApp_maybe lhs
- ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
- ; f a rhs } }
+ , bifint_proves = \(Pair lhs rhs)
+ -> do { (tc, [a]) <- splitTyConApp_maybe lhs
+ ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
+ ; f a rhs } }
mkTopBinFamDeduction :: String -> TyCon
-> (Type -> Type -> Type -> Maybe TypeEqn)
@@ -265,42 +266,32 @@ mkTopBinFamDeduction :: String -> TyCon
mkTopBinFamDeduction str fam_tc f
= BIF_Interact
{ bifint_name = fsLit str
- , bifint_arg_roles = [Nominal]
- , bifint_res_role = Nominal
- , bifint_proves = \cs -> do { [Pair lhs rhs] <- return cs
- ; (tc, [a,b]) <- splitTyConApp_maybe lhs
- ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
- ; f a b rhs } }
+ , bifint_proves = \(Pair lhs rhs) ->
+ do { (tc, [a,b]) <- splitTyConApp_maybe lhs
+ ; massertPpr (tc == fam_tc) (ppr tc $$ ppr fam_tc)
+ ; f a b rhs } }
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 }
+ = BIF_Interact { bifint_name = fsLit str
+ , bifint_proves = proves }
where
- proves cs
- | [Pair lhs rhs] <- cs -- Expect one coercion argument
+ proves (Pair lhs rhs)
= 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 }
+ = BIF_Interact { bifint_name = fsLit str
+ , bifint_proves = proves }
where
- proves cs
- | [Pair lhs rhs] <- cs -- Expect one coercion argument
+ proves (Pair lhs rhs)
= do { (tc2, [x2,y2]) <- splitTyConApp_maybe rhs
; guard (tc2 == fam_tc)
; (tc1, [x1,y1]) <- splitTyConApp_maybe lhs
@@ -310,8 +301,6 @@ mkBinBIF str fam_tc eq1 eq2 check_me
(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) }
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -45,7 +45,7 @@ module GHC.Core.Coercion (
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkProofIrrelCo,
- downgradeRole, mkAxiomRuleCo,
+ downgradeRole, mkAxiomCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo,
castCoercionKind, castCoercionKind1, castCoercionKind2,
@@ -1029,10 +1029,10 @@ mkAxInstCo :: Role
-- Only called with BranchedAxiom or UnbranchedAxiom
mkAxInstCo role axr tys cos
| arity == n_tys = downgradeRole role ax_role $
- AxiomRuleCo axr (rtys `chkAppend` cos)
+ AxiomCo axr (rtys `chkAppend` cos)
| otherwise = assert (arity < n_tys) $
downgradeRole role ax_role $
- mkAppCos (AxiomRuleCo axr (ax_args `chkAppend` cos))
+ mkAppCos (AxiomCo axr (ax_args `chkAppend` cos))
leftover_args
where
(ax_role, branch) = case coAxiomRuleBranch_maybe axr of
@@ -1045,8 +1045,8 @@ mkAxInstCo role axr tys cos
(ax_args, leftover_args) = splitAt arity rtys
-- worker function
-mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
-mkAxiomRuleCo = AxiomRuleCo
+mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion
+mkAxiomCo = AxiomCo
-- to be used only with unbranched axioms
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
@@ -1452,7 +1452,6 @@ setNominalRole_maybe r co
setNominalRole_maybe_helper co@(UnivCo { uco_prov = prov })
| case prov of PhantomProv {} -> False -- should always be phantom
ProofIrrelProv {} -> True -- it's always safe
- BuiltinProv {} -> True -- always nominal
PluginProv {} -> False -- who knows? This choice is conservative.
= Just $ co { uco_role = Nominal }
setNominalRole_maybe_helper _ = Nothing
@@ -1571,10 +1570,12 @@ promoteCoercion co = case co of
-- We can get Type~Constraint or Constraint~Type
-- from FunCo {} :: (a -> (b::Type)) ~ (a -=> (b'::Constraint))
- CoVarCo {} -> mkKindCo co
- HoleCo {} -> mkKindCo co
- AxiomRuleCo {} -> mkKindCo co
- UnivCo {} -> mkKindCo co
+ CoVarCo {} -> mkKindCo co
+ HoleCo {} -> mkKindCo co
+ AxiomCo {} -> mkKindCo co
+ UnivCo {} -> mkKindCo co -- We could instead return the (single) `uco_deps` coercion in
+ -- the `ProofIrrelProv` and `PhantomProv` cases, but it doesn't
+ -- quite seem worth doing.
SymCo g
-> mkSymCo (promoteCoercion g)
@@ -2383,28 +2384,28 @@ seqMCo MRefl = ()
seqMCo (MCo co) = seqCo co
seqCo :: Coercion -> ()
-seqCo (Refl ty) = seqType ty
-seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco
-seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
-seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
-seqCo (ForAllCo tv visL visR k co) = seqType (varType tv) `seq`
- rnf visL `seq` rnf visR `seq`
- seqCo k `seq` seqCo co
-seqCo (FunCo r af1 af2 w co1 co2) = r `seq` af1 `seq` af2 `seq`
- seqCo w `seq` seqCo co1 `seq` seqCo co2
-seqCo (CoVarCo cv) = cv `seq` ()
-seqCo (HoleCo h) = coHoleCoVar h `seq` ()
+seqCo (Refl ty) = seqType ty
+seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco
+seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
+seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
+seqCo (CoVarCo cv) = cv `seq` ()
+seqCo (HoleCo h) = coHoleCoVar h `seq` ()
+seqCo (SymCo co) = seqCo co
+seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
+seqCo (SelCo n co) = n `seq` seqCo co
+seqCo (LRCo lr co) = lr `seq` seqCo co
+seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
+seqCo (KindCo co) = seqCo co
+seqCo (SubCo co) = seqCo co
+seqCo (AxiomCo _ cs) = seqCos cs
+seqCo (ForAllCo tv visL visR k co)
+ = seqType (varType tv) `seq` rnf visL `seq` rnf visR `seq`
+ seqCo k `seq` seqCo co
+seqCo (FunCo r af1 af2 w co1 co2)
+ = r `seq` af1 `seq` af2 `seq` seqCo w `seq` seqCo co1 `seq` seqCo co2
seqCo (UnivCo { uco_prov = p, uco_role = r
, uco_lty = t1, uco_rty = t2, uco_deps = deps })
= p `seq` r `seq` seqType t1 `seq` seqType t2 `seq` seqCos deps
-seqCo (SymCo co) = seqCo co
-seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
-seqCo (SelCo n co) = n `seq` seqCo co
-seqCo (LRCo lr co) = lr `seq` seqCo co
-seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
-seqCo (KindCo co) = seqCo co
-seqCo (SubCo co) = seqCo co
-seqCo (AxiomRuleCo _ cs) = seqCos cs
seqCos :: [Coercion] -> ()
seqCos [] = ()
@@ -2446,8 +2447,8 @@ coercionRKind co = coercion_lr_kind CRight co
coercion_lr_kind :: HasDebugCallStack => LeftOrRight -> Coercion -> Type
{-# INLINE coercion_lr_kind #-}
-coercion_lr_kind which co
- = go co
+coercion_lr_kind which orig_co
+ = go orig_co
where
go (Refl ty) = ty
go (GRefl _ ty MRefl) = ty
@@ -2463,13 +2464,15 @@ coercion_lr_kind which co
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
go (SelCo d co) = selectFromType d (go co)
- go (AxiomRuleCo ax cos) = go_ax ax cos
+ go (AxiomCo ax cos) = go_ax ax cos
go (UnivCo { uco_lty = lty, uco_rty = rty})
= pickLR which (lty, rty)
- go (FunCo { fco_afl = af, fco_mult = mult, fco_arg = arg, fco_res = res})
+ go (FunCo { fco_afl = afl, fco_afr = afr, fco_mult = mult
+ , fco_arg = arg, fco_res = res})
= -- See Note [FunCo]
- FunTy { ft_af = af, ft_mult = go mult, ft_arg = go arg, ft_res = go res }
+ FunTy { ft_af = pickLR which (afl, afr), ft_mult = go mult
+ , ft_arg = go arg, ft_res = go res }
go co@(ForAllCo { fco_tcv = tv1, fco_visL = visL, fco_visR = visR
, fco_kind = k_co, fco_body = co1 })
@@ -2493,15 +2496,17 @@ coercion_lr_kind which co
go_app co args = piResultTys (go co) args
-------------
- go_ax (BuiltInFamRewrite bif) cos = go_bif (bifrw_proves bif) cos
- go_ax (BuiltInFamInteract bif) cos = go_bif (bifint_proves bif) cos
- go_ax (UnbranchedAxiom ax) cos = go_branch ax (coAxiomSingleBranch ax) cos
- go_ax (BranchedAxiom ax i) cos = go_branch ax (coAxiomNthBranch ax i) cos
+ go_ax (BuiltInFamRewrite bif) cos = check_bif_res (bifrw_proves bif (map coercionKind cos))
+ go_ax (BuiltInFamInteract bif) [co] = check_bif_res (bifint_proves bif (coercionKind co))
+ go_ax (BuiltInFamInteract {}) _ = crash
+ go_ax (UnbranchedAxiom ax) cos = go_branch ax (coAxiomSingleBranch ax) cos
+ go_ax (BranchedAxiom ax i) cos = go_branch ax (coAxiomNthBranch ax i) cos
-------------
- go_bif proves cos = case proves (map coercionKind cos) of
- Nothing -> pprPanic "coercionKind" (ppr cos)
- Just (Pair lty rty) -> pickLR which (lty, rty)
+ check_bif_res (Just (Pair lhs rhs)) = pickLR which (lhs,rhs)
+ check_bif_res Nothing = crash
+
+ crash = pprPanic "coercionKind" (ppr orig_co)
-------------
go_branch :: CoAxiom br -> CoAxBranch -> [Coercion] -> Type
@@ -2569,16 +2574,13 @@ coercion_lr_kind which co
-- when other_co is not a ForAllCo
= substTy subst (go other_co)
-{-
-
-Note [Nested ForAllCos]
-~~~~~~~~~~~~~~~~~~~~~~~
-
-Suppose we need `coercionKind (ForAllCo a1 (ForAllCo a2 ... (ForAllCo an
-co)...) )`. We do not want to perform `n` single-type-variable
-substitutions over the kind of `co`; rather we want to do one substitution
-which substitutes for all of `a1`, `a2` ... simultaneously. If we do one
-at a time we get the performance hole reported in #11735.
+{- Note [Nested ForAllCos]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we need `coercionKind (ForAllCo a1 (ForAllCo a2 ... (ForAllCo an co)...) )`.
+We do not want to perform `n` single-type-variable substitutions over the kind
+of `co`; rather we want to do one substitution which substitutes for all of
+`a1`, `a2` ... simultaneously. If we do one at a time we get the performance
+hole reported in #11735.
Solution: gather up the type variables for nested `ForAllCos`, and
substitute for them all at once. Remarkably, for #11735 this single
@@ -2606,7 +2608,7 @@ coercionRole = go
go (InstCo co _) = go co
go (KindCo {}) = Nominal
go (SubCo _) = Representational
- go (AxiomRuleCo ax _) = coAxiomRuleRole ax
+ go (AxiomCo ax _) = coAxiomRuleRole ax
{-
Note [Nested InstCos]
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -33,7 +33,7 @@ mkNomReflCo :: Type -> Coercion
mkKindCo :: Coercion -> Coercion
mkSubCo :: HasDebugCallStack => Coercion -> Coercion
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
-mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
+mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion
funRole :: Role -> FunSel -> Role
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -81,7 +81,7 @@ axF :: { F [Int] ~ Bool
; forall (k :: *) (a :: k -> *) (b :: k). F (a b) ~ Char
}
-The axiom is used with the AxiomRuleCo constructor of Coercion. If we wish
+The axiom is used with the AxiomCo constructor of Coercion. If we wish
to have a coercion showing that F (Maybe Int) ~ Char, it will look like
axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char
@@ -574,23 +574,23 @@ CoAxiomRules come in two flavours:
(ax1) 3+4 ----> 7
(ax2) s+0 ----> s
The evidence looks like
- AxiomRuleCo ax1 [3,4] :: 3+4 ~ 7
- AxiomRuleCo ax2 [s] :: s+0 ~ s
- The arguments in the AxiomRuleCo are the /instantiating types/, or
- more generally cocerions, see Note [Coercion axioms applied to coercions]
+ AxiomCo ax1 [3,4] :: 3+4 ~ 7
+ AxiomCo ax2 [s] :: s+0 ~ s
+ The arguments in the AxiomCo are the /instantiating types/, or
+ more generally coercions (see Note [Coercion axioms applied to coercions]
in GHC.Core.TyCo.Rep).
* BuiltInFamInteract: provides evidence for the consequences of one or two
other coercions. For example
- (ax3) g1: a+b ~ 0 ---> a~0
- (ax4) g2: a+b ~ 0 ---> b~0
+ (ax3) g1: a+b ~ 0 ---> a~0
+ (ax4) g2: a+b ~ 0 ---> b~0
(ax5) g3: a+b1~r1, g4 : a+b2~r ---> b1~b2
- The arguments to the AxiomRuleCo are the full coercions
+ The arguments to the AxiomCo are the full coercions
(not types, right from the get-go).
So then:
- AxiomRuleCo ax3 [g1] :: a ~ 0
- AxiomRuleCo ax2 [g2] :: b ~ 0
- AxiomRuleCo ax3 [g3,g4] :: b1 ~ b2
+ AxiomCo ax3 [g1] :: a ~ 0
+ AxiomCo ax4 [g2] :: b ~ 0
+ AxiomCo ax5 [g3,g4] :: b1 ~ b2
-}
@@ -609,14 +609,14 @@ instance Eq CoAxiomRule where
_ == _ = False
coAxiomRuleRole :: CoAxiomRule -> Role
-coAxiomRuleRole (BuiltInFamRewrite bif) = bifrw_res_role bif
-coAxiomRuleRole (BuiltInFamInteract bif) = bifint_res_role bif
-coAxiomRuleRole (UnbranchedAxiom ax) = coAxiomRole ax
-coAxiomRuleRole (BranchedAxiom ax _) = coAxiomRole ax
+coAxiomRuleRole (BuiltInFamRewrite {}) = Nominal
+coAxiomRuleRole (BuiltInFamInteract {}) = Nominal
+coAxiomRuleRole (UnbranchedAxiom ax) = coAxiomRole ax
+coAxiomRuleRole (BranchedAxiom ax _) = coAxiomRole ax
coAxiomRuleArgRoles :: CoAxiomRule -> [Role]
-coAxiomRuleArgRoles (BuiltInFamRewrite bif) = bifrw_arg_roles bif
-coAxiomRuleArgRoles (BuiltInFamInteract bif) = bifint_arg_roles bif
+coAxiomRuleArgRoles (BuiltInFamRewrite bif) = replicate (bifrw_arity bif) Nominal
+coAxiomRuleArgRoles (BuiltInFamInteract {}) = [Nominal]
coAxiomRuleArgRoles (UnbranchedAxiom ax) = coAxBranchRoles (coAxiomSingleBranch ax)
coAxiomRuleArgRoles (BranchedAxiom ax i) = coAxBranchRoles (coAxiomNthBranch ax i)
@@ -636,11 +636,6 @@ instance Data.Data CoAxiomRule where
gunfold _ _ = error "gunfold"
dataTypeOf _ = mkNoRepType "CoAxiomRule"
---instance Ord CoAxiomRule where
--- -- we compare lexically to avoid non-deterministic output when sets of rules
--- -- are printed
--- compare x y = lexicalCompareFS (coaxrName x) (coaxrName y)
-
instance Outputable CoAxiomRule where
ppr (BuiltInFamRewrite bif) = ppr (bifrw_name bif)
ppr (BuiltInFamInteract bif) = ppr (bifint_name bif)
@@ -659,40 +654,47 @@ type TypeEqn = Pair Type
-- Type checking of built-in families
data BuiltInSynFamily = BuiltInSynFamily
- { sfMatchFam :: [BuiltInFamRewrite]
-
- , sfInteract:: [BuiltInFamInteract]
+ { sfMatchFam :: [BuiltInFamRewrite]
+ , 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 of (sfInteract tys ty)
-- then AxiomRule ar [co :: F tys ~ ty] :: s1~s2
}
-data BuiltInFamInteract
+data BuiltInFamInteract -- Argument and result role are always Nominal
= BIF_Interact
- { bifint_name :: FastString
- , bifint_arg_roles :: [Role] -- roles of parameter equations
- , bifint_res_role :: Role -- role of resulting equation
- , bifint_proves :: [TypeEqn] -> Maybe TypeEqn
+ { bifint_name :: FastString
+ , bifint_proves :: TypeEqn -> Maybe TypeEqn
-- ^ Returns @Nothing@ when it doesn't like
-- the supplied arguments. When this happens in a coercion
-- that means that the coercion is ill-formed, and Core Lint
-- checks for that.
}
-data BuiltInFamRewrite
+data BuiltInFamRewrite -- Argument roles and result role are always Nominal
= BIF_Rewrite
- { bifrw_name :: FastString
- , bifrw_arg_roles :: [Role] -- roles of parameter equations
- , bifrw_res_role :: Role -- role of resulting equation
+ { bifrw_name :: FastString
+ , bifrw_fam_tc :: TyCon -- Needed for tyConsOfType
+
+ , bifrw_arity :: Arity -- Number of type arguments needed
+ -- to instantiate this axiom
- , bifrw_match :: [Type] -> Maybe ([Type], Type) -- Instantiating types and result type
+ , bifrw_match :: [Type] -> Maybe ([Type], Type)
-- coaxrMatch: does this reduce on the given arguments?
- -- If it does, returns (CoAxiomRule, types to instantiate the rule at, rhs type)
- -- That is: mkAxiomRuleCo ax (zipWith mkReflCo coAxiomRuleArgRoles ts)
- -- :: F tys ~coaxrRole rhs,
+ -- If it does, returns (types to instantiate the rule at, rhs type)
+ -- That is: mkAxiomCo ax (zipWith mkReflCo coAxiomRuleArgRoles ts)
+ -- :: F tys ~N rhs,
, bifrw_proves :: [TypeEqn] -> Maybe TypeEqn }
+ -- length(inst_tys) = bifrw_arity
+
+ -- INVARIANT: bifrw_match and bifrw_proves are related as follows:
+ -- If Just (inst_tys, res_ty) = bifrw_match ax arg_tys
+ -- then * length arg_tys = tyConArity fam_tc
+ -- * length inst_tys = bifrw_arity
+ -- * bifrw_proves (map mkNomReflCo inst_tys) = Just (mkNomReflCo res_ty)
+
-- Provides default implementations that do nothing.
trivialBuiltInFamily :: BuiltInSynFamily
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -355,7 +355,7 @@ opt_co4 env sym rep r (CoVarCo cv)
opt_co4 _ _ _ _ (HoleCo h)
= pprPanic "opt_univ fell into a hole" (ppr h)
-opt_co4 env sym rep r (AxiomRuleCo con cos)
+opt_co4 env sym rep r (AxiomCo con cos)
-- Do *not* push sym inside top-level axioms
-- e.g. if g is a top-level axiom
-- g a : f a ~ a
@@ -365,9 +365,9 @@ opt_co4 env sym rep r (AxiomRuleCo con cos)
wrapSym sym $
-- some sub-cos might be P: use opt_co2
-- See Note [Optimising coercion optimisation]
- AxiomRuleCo con (zipWith (opt_co2 env False)
- (coAxiomRuleArgRoles con)
- cos)
+ AxiomCo con (zipWith (opt_co2 env False)
+ (coAxiomRuleArgRoles con)
+ cos)
-- Note that the_co does *not* have sym pushed into it
opt_co4 env sym rep r (UnivCo { uco_prov = prov, uco_lty = t1
@@ -833,8 +833,8 @@ opt_trans_rule is co1 co2
-- If we put TrPushSymAxR first, we'll get
-- (axN ty ; sym (axN ty)) :: N ty ~ N ty -- Obviously Refl
-- --> axN (sym (axN ty)) :: N ty ~ N ty -- Very stupid
- | Just (sym1, axr1, cos1) <- isAxiomRuleCo_maybe co1
- , Just (sym2, axr2, cos2) <- isAxiomRuleCo_maybe co2
+ | Just (sym1, axr1, cos1) <- isAxiomCo_maybe co1
+ , Just (sym2, axr2, cos2) <- isAxiomCo_maybe co2
, axr1 == axr2
, sym1 == not sym2
, Just (tc, role, branch) <- coAxiomRuleBranch_maybe axr1
@@ -853,31 +853,31 @@ opt_trans_rule is co1 co2
-- See Note [Push transitivity inside axioms] and
-- Note [Push transitivity inside newtype axioms only]
-- TrPushSymAxR
- | Just (sym, axr, cos1) <- isAxiomRuleCo_maybe co1
+ | Just (sym, axr, cos1) <- isAxiomCo_maybe co1
, True <- sym
, Just cos2 <- matchNewtypeBranch sym axr co2
- , let newAxInst = AxiomRuleCo axr (opt_transList is (map mkSymCo cos2) cos1)
+ , let newAxInst = AxiomCo axr (opt_transList is (map mkSymCo cos2) cos1)
= fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
-- TrPushAxR
- | Just (sym, axr, cos1) <- isAxiomRuleCo_maybe co1
+ | Just (sym, axr, cos1) <- isAxiomCo_maybe co1
, False <- sym
, Just cos2 <- matchNewtypeBranch sym axr co2
- , let newAxInst = AxiomRuleCo axr (opt_transList is cos1 cos2)
+ , let newAxInst = AxiomCo axr (opt_transList is cos1 cos2)
= fireTransRule "TrPushAxR" co1 co2 newAxInst
-- TrPushSymAxL
- | Just (sym, axr, cos2) <- isAxiomRuleCo_maybe co2
+ | Just (sym, axr, cos2) <- isAxiomCo_maybe co2
, True <- sym
, Just cos1 <- matchNewtypeBranch (not sym) axr co1
- , let newAxInst = AxiomRuleCo axr (opt_transList is cos2 (map mkSymCo cos1))
+ , let newAxInst = AxiomCo axr (opt_transList is cos2 (map mkSymCo cos1))
= fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
-- TrPushAxL
- | Just (sym, axr, cos2) <- isAxiomRuleCo_maybe co2
+ | Just (sym, axr, cos2) <- isAxiomCo_maybe co2
, False <- sym
, Just cos1 <- matchNewtypeBranch (not sym) axr co1
- , let newAxInst = AxiomRuleCo axr (opt_transList is cos1 cos2)
+ , let newAxInst = AxiomCo axr (opt_transList is cos1 cos2)
= fireTransRule "TrPushAxL" co1 co2 newAxInst
@@ -1132,13 +1132,13 @@ chooseRole True _ = Representational
chooseRole _ r = r
-----------
-isAxiomRuleCo_maybe :: Coercion -> Maybe (SymFlag, CoAxiomRule, [Coercion])
+isAxiomCo_maybe :: Coercion -> Maybe (SymFlag, CoAxiomRule, [Coercion])
-- We don't expect to see nested SymCo; and that lets us write a simple,
-- non-recursive function. (If we see a nested SymCo we'll just fail,
-- which is ok.)
-isAxiomRuleCo_maybe (SymCo (AxiomRuleCo ax cos)) = Just (True, ax, cos)
-isAxiomRuleCo_maybe (AxiomRuleCo ax cos) = Just (False, ax, cos)
-isAxiomRuleCo_maybe _ = Nothing
+isAxiomCo_maybe (SymCo (AxiomCo ax cos)) = Just (True, ax, cos)
+isAxiomCo_maybe (AxiomCo ax cos) = Just (False, ax, cos)
+isAxiomCo_maybe _ = Nothing
matchNewtypeBranch :: Bool -- True = match LHS, False = match RHS
-> CoAxiomRule
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -394,9 +394,10 @@ orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
`unionNameSet` orphNamesOfCo co1
`unionNameSet` orphNamesOfCo co2
orphNamesOfCo (CoVarCo _) = emptyNameSet
-orphNamesOfCo (AxiomRuleCo con cos) = orphNamesOfAxRule con `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (UnivCo { uco_lty = t1, uco_rty = t2 })
+orphNamesOfCo (AxiomCo con cos) = orphNamesOfAxRule con `unionNameSet` orphNamesOfCos cos
+orphNamesOfCo (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = cos })
= orphNamesOfType t1 `unionNameSet` orphNamesOfType t2
+ `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (SymCo co) = orphNamesOfCo co
orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (SelCo _ co) = orphNamesOfCo co
@@ -410,8 +411,8 @@ orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo
orphNamesOfAxRule :: CoAxiomRule -> NameSet
-orphNamesOfAxRule (BuiltInFamRewrite {}) = emptyNameSet
-orphNamesOfAxRule (BuiltInFamInteract {}) = emptyNameSet
+orphNamesOfAxRule (BuiltInFamRewrite bif) = unitNameSet (tyConName (bifrw_fam_tc bif))
+orphNamesOfAxRule (BuiltInFamInteract {}) = emptyNameSet -- A free-floating axiom
orphNamesOfAxRule (UnbranchedAxiom ax) = orphNamesOfCoAx ax
orphNamesOfAxRule (BranchedAxiom ax _) = orphNamesOfCoAx ax
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -1198,9 +1198,7 @@ reduceTyFamApp_maybe envs role tc tys
| Just builtin_fam <- isBuiltInSynFamTyCon_maybe tc
, Just (rewrite,ts,ty) <- tryMatchFam builtin_fam tys
- , role == bifrw_res_role rewrite
- = let co = mkAxiomRuleCo (BuiltInFamRewrite rewrite)
- (zipWith mkReflCo (bifrw_arg_roles rewrite) ts)
+ = let co = mkAxiomCo (BuiltInFamRewrite rewrite) (map mkNomReflCo ts)
in Just $ mkReduction co ty
| otherwise
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2611,18 +2611,21 @@ lintCoercion (InstCo co arg)
; _ -> failWithL (text "Bad argument of inst") }}}
-lintCoercion this_co@(AxiomRuleCo ax cos)
+lintCoercion this_co@(AxiomCo ax cos)
= do { cos' <- mapM lintCoercion cos
; let arg_kinds :: [Pair Type] = map coercionKind cos'
; lint_roles 0 (coAxiomRuleArgRoles ax) cos'
; lint_ax ax arg_kinds
- ; return (AxiomRuleCo ax cos') }
+ ; return (AxiomCo ax cos') }
where
lint_ax :: CoAxiomRule -> [Pair Type] -> LintM ()
lint_ax (BuiltInFamRewrite bif) prs
= checkL (isJust (bifrw_proves bif prs)) bad_bif
lint_ax (BuiltInFamInteract bif) prs
- = checkL (isJust (bifint_proves bif prs)) bad_bif
+ = checkL (case prs of
+ [pr] -> isJust (bifint_proves bif pr)
+ _ -> False)
+ bad_bif
lint_ax (UnbranchedAxiom ax) prs
= lintBranch this_co (coAxiomTyCon ax) (coAxiomSingleBranch ax) prs
lint_ax (BranchedAxiom ax ind) prs
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -62,7 +62,7 @@ import GHC.Builtin.Types.Prim( funTyFlagTyCon )
import Data.Monoid as DM ( Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
-import GHC.Core.Coercion.Axiom( CoAxiomRule(..), coAxiomTyCon )
+import GHC.Core.Coercion.Axiom( CoAxiomRule(..), BuiltInFamRewrite(..), coAxiomTyCon )
import GHC.Utils.FV
import GHC.Types.Var
@@ -668,7 +668,7 @@ tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
= tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
-- See Note [CoercionHoles and coercion free variables]
-tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
+tyCoFVsOfCo (AxiomCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
tyCoFVsOfCo (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps}) fv_cand in_scope acc
= (tyCoFVsOfCos deps `unionFV` tyCoFVsOfType t1
`unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
@@ -716,7 +716,7 @@ almost_devoid_co_var_of_co (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }
&& almost_devoid_co_var_of_co co2 cv
almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv
almost_devoid_co_var_of_co (HoleCo h) cv = (coHoleCoVar h) /= cv
-almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
+almost_devoid_co_var_of_co (AxiomCo _ cs) cv
= almost_devoid_co_var_of_cos cs cv
almost_devoid_co_var_of_co (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps }) cv
= almost_devoid_co_var_of_cos deps cv
@@ -1126,8 +1126,9 @@ tyConsOfType ty
= go_co kind_co `unionUniqSets` go_co co
go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r })
= go_co m `unionUniqSets` go_co a `unionUniqSets` go_co r
- go_co (AxiomRuleCo ax args) = go_ax ax `unionUniqSets` go_cos args
- go_co (UnivCo { uco_lty = t1, uco_rty = t2 }) = go t1 `unionUniqSets` go t2
+ go_co (AxiomCo ax args) = go_ax ax `unionUniqSets` go_cos args
+ go_co (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = cos })
+ = go t1 `unionUniqSets` go t2 `unionUniqSets` go_cos cos
go_co (CoVarCo {}) = emptyUniqSet
go_co (HoleCo {}) = emptyUniqSet
go_co (SymCo co) = go_co co
@@ -1145,10 +1146,10 @@ tyConsOfType ty
go_tc tc = unitUniqSet tc
- go_ax (UnbranchedAxiom ax) = go_tc $ coAxiomTyCon ax
- go_ax (BranchedAxiom ax _) = go_tc $ coAxiomTyCon ax
- go_ax (BuiltInFamRewrite {}) = emptyUniqSet
- go_ax (BuiltInFamInteract {}) = emptyUniqSet
+ go_ax (UnbranchedAxiom ax) = go_tc $ coAxiomTyCon ax
+ go_ax (BranchedAxiom ax _) = go_tc $ coAxiomTyCon ax
+ go_ax (BuiltInFamRewrite bif) = go_tc $ bifrw_fam_tc bif
+ go_ax (BuiltInFamInteract {}) = emptyUniqSet -- A free-floating axiom
tyConsOfTypes :: [Type] -> UniqSet TyCon
tyConsOfTypes tys = foldr (unionUniqSets . tyConsOfType) emptyUniqSet tys
@@ -1303,6 +1304,23 @@ occCheckExpand vs_to_avoid ty
go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
; arg' <- go_co cxt arg
; return (AppCo co' arg') }
+ go_co cxt (SymCo co) = do { co' <- go_co cxt co
+ ; return (SymCo co') }
+ go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
+ ; co2' <- go_co cxt co2
+ ; return (TransCo co1' co2') }
+ go_co cxt (SelCo n co) = do { co' <- go_co cxt co
+ ; return (SelCo n co') }
+ go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
+ ; return (LRCo lr co') }
+ go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
+ ; arg' <- go_co cxt arg
+ ; return (InstCo co' arg') }
+ go_co cxt (KindCo co) = do { co' <- go_co cxt co
+ ; return (KindCo co') }
+ go_co cxt (SubCo co) = do { co' <- go_co cxt co
+ ; return (SubCo co') }
+
go_co cxt@(as, env) co@(ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = body_co })
= do { kind_co' <- go_co cxt kind_co
; let tv' = setVarType tv $
@@ -1311,6 +1329,7 @@ occCheckExpand vs_to_avoid ty
as' = as `delVarSet` tv
; body' <- go_co (as', env') body_co
; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) }
+
go_co cxt co@(FunCo { fco_mult = w, fco_arg = co1 ,fco_res = co2 })
= do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
@@ -1326,26 +1345,11 @@ occCheckExpand vs_to_avoid ty
| bad_var_occ as (ch_co_var h) = Nothing
| otherwise = return co
- go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
- ; return (AxiomRuleCo ax cs') }
- go_co cxt co@(UnivCo { uco_lty = ty1, uco_rty = ty2 })
- = do { ty1' <- go cxt ty1
- ; ty2' <- go cxt ty2
- ; return (co { uco_lty = ty1', uco_rty = ty2' }) }
- go_co cxt (SymCo co) = do { co' <- go_co cxt co
- ; return (SymCo co') }
- go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
- ; co2' <- go_co cxt co2
- ; return (TransCo co1' co2') }
- go_co cxt (SelCo n co) = do { co' <- go_co cxt co
- ; return (SelCo n co') }
- go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
- ; return (LRCo lr co') }
- go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
- ; arg' <- go_co cxt arg
- ; return (InstCo co' arg') }
- go_co cxt (KindCo co) = do { co' <- go_co cxt co
- ; return (KindCo co') }
- go_co cxt (SubCo co) = do { co' <- go_co cxt co
- ; return (SubCo co') }
+ go_co cxt (AxiomCo ax cs) = do { cs' <- mapM (go_co cxt) cs
+ ; return (AxiomCo ax cs') }
+ go_co cxt co@(UnivCo { uco_lty = ty1, uco_rty = ty2, uco_deps = cos })
+ = do { ty1' <- go cxt ty1
+ ; ty2' <- go cxt ty2
+ ; cos' <- mapM (go_co cxt) cos
+ ; return (co { uco_lty = ty1', uco_rty = ty2', uco_deps = cos' }) }
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -907,7 +907,7 @@ data Coercion
| CoVarCo CoVar -- :: _ -> (N or R)
-- result role depends on the tycon of the variable's type
- | AxiomRuleCo CoAxiomRule [Coercion]
+ | AxiomCo CoAxiomRule [Coercion]
-- The coercion arguments always *precisely* saturate
-- arity of (that branch of) the CoAxiom. If there are
-- any left over, we use AppCo.
@@ -1533,7 +1533,7 @@ is entirely separate, but they all share the need to represent these fields:
, uco_deps :: [Coercion] -- Coercions on which it depends
Here,
- * uco_role, uco_lty, uco_rty express the type of the coercoin
+ * uco_role, uco_lty, uco_rty express the type of the coercion
* uco_prov says where it came from
* uco_deps specifies the coercions on which this proof (which is not
explicity given) depends. See
@@ -1560,15 +1560,10 @@ data UnivCoProvenance
-- ^ From a plugin, which asserts that this coercion is sound.
-- The string and the variable set are for the use by the plugin.
- | BuiltinProv -- The proof comes form GHC's knowledge of arithmetic
- -- or strings; e.g. from (co : a+b ~ 0) we can deduce that
- -- (a ~ 0) and (b ~ 0), with a BuiltinProv proof.
-
deriving (Eq, Ord, Data.Data)
-- Why Ord? See Note [Ord instance of IfaceType] in GHC.Iface.Type
instance Outputable UnivCoProvenance where
- ppr BuiltinProv = text "(builtin)"
ppr PhantomProv = text "(phantom)"
ppr ProofIrrelProv = text "(proof irrel)"
ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
@@ -1577,17 +1572,15 @@ instance NFData UnivCoProvenance where
rnf p = p `seq` ()
instance Binary UnivCoProvenance where
- put_ bh BuiltinProv = putByte bh 1
- put_ bh PhantomProv = putByte bh 2
- put_ bh ProofIrrelProv = putByte bh 3
- put_ bh (PluginProv a) = putByte bh 4 >> put_ bh a
+ put_ bh PhantomProv = putByte bh 1
+ put_ bh ProofIrrelProv = putByte bh 2
+ put_ bh (PluginProv a) = putByte bh 3 >> put_ bh a
get bh = do
tag <- getByte bh
case tag of
- 1 -> return BuiltinProv
- 2 -> return PhantomProv
- 3 -> return ProofIrrelProv
- 4 -> do a <- get bh
+ 1 -> return PhantomProv
+ 2 -> return ProofIrrelProv
+ 3 -> do a <- get bh
return $ PluginProv a
_ -> panic ("get UnivCoProvenance " ++ show tag)
@@ -1614,7 +1607,7 @@ A ProofIrrelProv is a coercion between coercions. For example:
In core, we get
G :: * -> *
- MkG :: forall (a :: *). (a ~ Bool) -> G a
+ MkG :: forall (a :: *). (a ~# Bool) -> G a
Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be
@@ -1631,8 +1624,8 @@ Note that
Here,
co3 = UnivCo ProofIrrelProv Nominal (CoercionTy co1) (CoercionTy co2) [co5]
where
- co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
- co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
+ co5 :: (a1 ~# Bool) ~# (a2 ~# Bool)
+ co5 = TyConAppCo Nominal (~#) [<Consraint#>, <Constraint#>, co4, <Bool>]
Note [The importance of tracking UnivCo dependencies]
@@ -1961,7 +1954,7 @@ foldTyCo (TyCoFolder { tcf_view = view
go_co env (TyConAppCo _ _ args) = go_cos env args
go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2
go_co env (CoVarCo cv) = covar env cv
- go_co env (AxiomRuleCo _ cos) = go_cos env cos
+ go_co env (AxiomCo _ cos) = go_cos env cos
go_co env (HoleCo hole) = cohole env hole
go_co env (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps })
= go_ty env t1 `mappend` go_ty env t2
@@ -2033,7 +2026,7 @@ coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2
+ coercionSize w
coercionSize (CoVarCo _) = 1
coercionSize (HoleCo _) = 1
-coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs)
+coercionSize (AxiomCo _ cs) = 1 + sum (map coercionSize cs)
coercionSize (UnivCo { uco_lty = t1, uco_rty = t2 }) = 1 + typeSize t1 + typeSize t2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -57,7 +57,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
( mkCoVarCo, mkKindCo, mkSelCo, mkTransCo
, mkNomReflCo, mkSubCo, mkSymCo
, mkFunCo2, mkForAllCo, mkUnivCo
- , mkAxiomRuleCo, mkAppCo, mkGReflCo
+ , mkAxiomCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
, coercionKind, coercionLKind, coVarTypesRole )
@@ -879,7 +879,7 @@ subst_co subst co
go (Refl ty) = mkNomReflCo $! (go_ty ty)
go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
go (TyConAppCo r tc args)= mkTyConAppCo r tc $! go_cos args
- go (AxiomRuleCo con cos) = mkAxiomRuleCo con $! go_cos cos
+ go (AxiomCo con cos) = mkAxiomCo con $! go_cos cos
go (AppCo co arg) = (mkAppCo $! go co) $! go arg
go (ForAllCo tv visL visR kind_co co)
= case substForAllCoBndrUnchecked subst tv kind_co of
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -342,7 +342,7 @@ tidyCo env co
go (FunCo r afl afr w co1 co2) = ((FunCo r afl afr $! go w) $! go co1) $! go co2
go (CoVarCo cv) = CoVarCo $! go_cv cv
go (HoleCo h) = HoleCo $! go_hole h
- go (AxiomRuleCo ax cos) = AxiomRuleCo ax $ strictMap go cos
+ go (AxiomCo ax cos) = AxiomCo ax $ strictMap go cos
go co@(UnivCo { uco_lty = t1, uco_rty = t2 })
= co { uco_lty = tidyType env t1, uco_rty = tidyType env t2 }
-- Don't bother to tidy the uco_deps field
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -274,7 +274,7 @@ import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Core.Coercion
( mkNomReflCo, mkGReflCo, mkReflCo
, mkTyConAppCo, mkAppCo
- , mkForAllCo, mkFunCo2, mkAxiomRuleCo, mkUnivCo
+ , mkForAllCo, mkFunCo2, mkAxiomCo, mkUnivCo
, mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
, mkKindCo, mkSubCo, mkFunCo, funRole
, decomposePiCos, coercionKind
@@ -556,8 +556,8 @@ expandTypeSynonyms ty
= mkFunCo2 r afl afr (go_co subst w) (go_co subst co1) (go_co subst co2)
go_co subst (CoVarCo cv)
= substCoVar subst cv
- go_co subst (AxiomRuleCo ax cs)
- = mkAxiomRuleCo ax (map (go_co subst) cs)
+ go_co subst (AxiomCo ax cs)
+ = mkAxiomCo ax (map (go_co subst) cs)
go_co subst co@(UnivCo { uco_lty = lty, uco_rty = rty })
= co { uco_lty = go subst lty, uco_rty = go subst rty }
go_co subst (SymCo co)
@@ -974,7 +974,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
<*> go_ty env t1 <*> go_ty env t2
go_co !env (SymCo co) = mkSymCo <$> go_co env co
go_co !env (TransCo c1 c2) = mkTransCo <$> go_co env c1 <*> go_co env c2
- go_co !env (AxiomRuleCo r cos) = mkAxiomRuleCo r <$> go_cos env cos
+ go_co !env (AxiomCo r cos) = mkAxiomCo r <$> go_cos env cos
go_co !env (SelCo i co) = mkSelCo i <$> go_co env co
go_co !env (LRCo lr co) = mkLRCo lr <$> go_co env co
go_co !env (InstCo co arg) = mkInstCo <$> go_co env co <*> go_co env arg
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -284,19 +284,19 @@ toIfaceCoercionX fr co
go (GRefl r ty mco) = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco)
go (CoVarCo cv)
-- See Note [Free TyVars and CoVars in IfaceType] in GHC.Iface.Type
- | cv `elemVarSet` fr = IfaceFreeCoVar cv
- | otherwise = IfaceCoVarCo (toIfaceCoVar cv)
- go (HoleCo h) = IfaceHoleCo (coHoleCoVar h)
-
- go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2)
- go (SymCo co) = IfaceSymCo (go co)
- go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
- go (SelCo d co) = IfaceSelCo d (go co)
- go (LRCo lr co) = IfaceLRCo lr (go co)
- go (InstCo co arg) = IfaceInstCo (go co) (go arg)
- go (KindCo c) = IfaceKindCo (go c)
- go (SubCo co) = IfaceSubCo (go co)
- go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (toIfaceAxiomRule co) (map go cs)
+ | cv `elemVarSet` fr = IfaceFreeCoVar cv
+ | otherwise = IfaceCoVarCo (toIfaceCoVar cv)
+ go (HoleCo h) = IfaceHoleCo (coHoleCoVar h)
+
+ go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2)
+ go (SymCo co) = IfaceSymCo (go co)
+ go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
+ go (SelCo d co) = IfaceSelCo d (go co)
+ go (LRCo lr co) = IfaceLRCo lr (go co)
+ go (InstCo co arg) = IfaceInstCo (go co) (go arg)
+ go (KindCo c) = IfaceKindCo (go c)
+ go (SubCo co) = IfaceSubCo (go co)
+ go (AxiomCo ax cs) = IfaceAxiomCo (toIfaceAxiomRule ax) (map go cs)
go (UnivCo { uco_prov = p, uco_role = r, uco_lty = t1, uco_rty = t2, uco_deps = deps })
= IfaceUnivCo p r (toIfaceTypeX fr t1) (toIfaceTypeX fr t2) (map go deps)
=====================================
compiler/GHC/Data/Pair.hs
=====================================
@@ -64,3 +64,5 @@ unzipPairs [] = ([], [])
unzipPairs (Pair a b : prs) = (a:as, b:bs)
where
!(as,bs) = unzipPairs prs
+ -- This makes the unzip work eagerly, building no thunks at
+ -- the cost of doing all the work up-front.
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -675,15 +675,13 @@ rnIfaceCo (IfaceInstCo c1 c2) = IfaceInstCo <$> rnIfaceCo c1 <*> rnIfa
rnIfaceCo (IfaceSelCo d c) = IfaceSelCo d <$> rnIfaceCo c
rnIfaceCo (IfaceLRCo lr c) = IfaceLRCo lr <$> rnIfaceCo c
rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c
-rnIfaceCo (IfaceAxiomRuleCo ax cos) = IfaceAxiomRuleCo ax <$> mapM rnIfaceCo cos
+rnIfaceCo (IfaceAxiomCo ax cos) = IfaceAxiomCo ax <$> mapM rnIfaceCo cos
rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
rnIfaceCo (IfaceForAllCo bndr visL visR co1 co2)
= (\bndr' co1' co2' -> IfaceForAllCo bndr' visL visR co1' co2')
<$> rnIfaceBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceUnivCo s r t1 t2 deps)
= IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2 <*> mapM rnIfaceCo deps
- -- Renaming affects only type constructors, not coercion variables,
- -- so no need to recurse into the free-var fields
rnIfaceTyCon :: Rename IfaceTyCon
rnIfaceTyCon (IfaceTyCon n info)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1781,10 +1781,8 @@ freeNamesIfCoercion (IfaceForAllCo _tcv _visL _visR kind_co co)
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
-freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2 _)
- = freeNamesIfType t1 &&& freeNamesIfType t2
- -- Ignoring uco_deps field, which are all local,
- -- and don't contribute to dependency analysis
+freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2 cos)
+ = freeNamesIfType t1 &&& freeNamesIfType t2 &&& fnList freeNamesIfCoercion cos
freeNamesIfCoercion (IfaceSymCo c)
= freeNamesIfCoercion c
freeNamesIfCoercion (IfaceTransCo c1 c2)
@@ -1799,7 +1797,7 @@ freeNamesIfCoercion (IfaceKindCo c)
= freeNamesIfCoercion c
freeNamesIfCoercion (IfaceSubCo co)
= freeNamesIfCoercion co
-freeNamesIfCoercion (IfaceAxiomRuleCo ax cos)
+freeNamesIfCoercion (IfaceAxiomCo ax cos)
= fnAxRule ax &&& fnList freeNamesIfCoercion cos
fnAxRule :: IfaceAxiomRule -> NameSet
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -476,7 +476,7 @@ data IfaceCoercion
| IfaceAppCo IfaceCoercion IfaceCoercion
| IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceCoercion IfaceCoercion
| IfaceCoVarCo IfLclName
- | IfaceAxiomRuleCo IfaceAxiomRule [IfaceCoercion]
+ | IfaceAxiomCo IfaceAxiomRule [IfaceCoercion]
-- ^ There are only a fixed number of CoAxiomRules, so it suffices
-- to use an IfaceLclName to distinguish them.
-- See Note [Adding built-in type families] in GHC.Builtin.Types.Literals
@@ -711,7 +711,7 @@ substIfaceType env ty
go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2)
go_co (IfaceKindCo co) = IfaceKindCo (go_co co)
go_co (IfaceSubCo co) = IfaceSubCo (go_co co)
- go_co (IfaceAxiomRuleCo n cos) = IfaceAxiomRuleCo n (go_cos cos)
+ go_co (IfaceAxiomCo n cos) = IfaceAxiomCo n (go_cos cos)
go_cos = map go_co
@@ -2013,7 +2013,7 @@ ppr_co ctxt_prec (IfaceInstCo co ty)
text "Inst" <+> sep [ pprParendIfaceCoercion co
, pprParendIfaceCoercion ty ]
-ppr_co ctxt_prec (IfaceAxiomRuleCo ax cos)
+ppr_co ctxt_prec (IfaceAxiomCo ax cos)
= ppr_special_co ctxt_prec (pprIfAxRule ax) cos
ppr_co ctxt_prec (IfaceSymCo co)
= ppr_special_co ctxt_prec (text "Sym") [co]
@@ -2399,7 +2399,7 @@ instance Binary IfaceCoercion where
put_ bh (IfaceSubCo a) = do
putByte bh 16
put_ bh a
- put_ bh (IfaceAxiomRuleCo a b) = do
+ put_ bh (IfaceAxiomCo a b) = do
putByte bh 17
put_ bh a
put_ bh b
@@ -2465,7 +2465,7 @@ instance Binary IfaceCoercion where
return $ IfaceSubCo a
17-> do a <- get bh
b <- get bh
- return $ IfaceAxiomRuleCo a b
+ return $ IfaceAxiomCo a b
_ -> panic ("get IfaceCoercion " ++ show tag)
instance Binary IfaceAxiomRule where
@@ -2516,7 +2516,7 @@ instance NFData IfaceCoercion where
IfaceAppCo f1 f2 -> rnf f1 `seq` rnf f2
IfaceForAllCo f1 f2 f3 f4 f5 -> rnf f1 `seq` rnf f2 `seq` rnf f3 `seq` rnf f4 `seq` rnf f5
IfaceCoVarCo f1 -> rnf f1
- IfaceAxiomRuleCo f1 f2 -> rnf f1 `seq` rnf f2
+ IfaceAxiomCo f1 f2 -> rnf f1 `seq` rnf f2
IfaceUnivCo f1 f2 f3 f4 deps -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4 `seq` rnf deps
IfaceSymCo f1 -> rnf f1
IfaceTransCo f1 f2 -> rnf f1 `seq` rnf f2
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1485,8 +1485,8 @@ tcIfaceCo = go
go (IfaceLRCo lr c) = LRCo lr <$> go c
go (IfaceKindCo c) = KindCo <$> go c
go (IfaceSubCo c) = SubCo <$> go c
- go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> tcIfaceCoAxiomRule ax
- <*> mapM go cos
+ go (IfaceAxiomCo ax cos) = AxiomCo <$> tcIfaceAxiomRule ax
+ <*> mapM go cos
go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c)
go (IfaceHoleCo c) = pprPanic "tcIfaceCo:IfaceHoleCo" (ppr c)
@@ -2020,18 +2020,18 @@ tcIfaceTyCon (IfaceTyCon name _info)
AConLike (RealDataCon dc) -> return (promoteDataCon dc)
_ -> pprPanic "tcIfaceTyCon" (ppr thing) }
-tcIfaceCoAxiomRule :: IfaceAxiomRule -> IfL CoAxiomRule
+tcIfaceAxiomRule :: IfaceAxiomRule -> IfL CoAxiomRule
-- Unlike CoAxioms, which arise from user 'type instance' declarations,
-- there are a fixed set of CoAxiomRules:
-- - axioms for type-level literals (Nat and Symbol),
-- enumerated in typeNatCoAxiomRules
-tcIfaceCoAxiomRule (IfaceAR_X n)
+tcIfaceAxiomRule (IfaceAR_X n)
| Just axr <- lookupUFM typeNatCoAxiomRules (ifLclNameFS n)
= return axr
| otherwise
- = pprPanic "tcIfaceCoAxiomRule" (ppr n)
-tcIfaceCoAxiomRule (IfaceAR_U name) = do { ax <- tcIfaceUnbranchedAxiom name; return (UnbranchedAxiom ax) }
-tcIfaceCoAxiomRule (IfaceAR_B name i) = do { ax <- tcIfaceBranchedAxiom name; return (BranchedAxiom ax i) }
+ = pprPanic "tcIfaceAxiomRule" (ppr n)
+tcIfaceAxiomRule (IfaceAR_U name) = do { ax <- tcIfaceUnbranchedAxiom name; return (UnbranchedAxiom ax) }
+tcIfaceAxiomRule (IfaceAR_B name i) = do { ax <- tcIfaceBranchedAxiom name; return (BranchedAxiom ax i) }
tcIfaceUnbranchedAxiom :: IfExtName -> IfL (CoAxiom Unbranched)
tcIfaceUnbranchedAxiom name
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -1405,7 +1405,7 @@ parameters, is that we simply produce new Wanted equalities. So for example
where 'cv' is currently unused. However, this new item can perhaps be
spontaneously solved to become given and react with d2,
discharging it in favour of a new constraint d2' thus:
- [W[ d2' : D Int Bool
+ [W] d2' : D Int Bool
d2 := d2' |> D Int cv
Now d2' can be discharged from d1
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2969,7 +2969,7 @@ improveGivenTopFunEqs fam_tc args ev rhs_ty
; emitNewGivens (ctEvLoc ev) $
[ (Nominal, new_co)
| (ax, _) <- tryInteractTopFam ops fam_tc args rhs_ty
- , let new_co = mkAxiomRuleCo ax [given_co] ]
+ , let new_co = mkAxiomCo ax [given_co] ]
; return False } -- False: no unifications
| otherwise
= return False
@@ -3124,7 +3124,7 @@ improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs
-- this that matters.
where
inert_co = ctEvCoercion inert_ev
- mk_ax_co (ax,_) = (Nominal, mkAxiomRuleCo ax [combined_co])
+ mk_ax_co (ax,_) = (Nominal, mkAxiomCo ax [combined_co])
where
combined_co = given_co `mkTransCo` mkSymCo inert_co
-- given_co :: F work_args ~ rhs
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -142,7 +142,7 @@ synonymTyConsOfType ty
= go_co m `plusNameEnv` go_co a `plusNameEnv` go_co r
go_co (CoVarCo _) = emptyNameEnv
go_co (HoleCo {}) = emptyNameEnv
- go_co (AxiomRuleCo _ cs) = go_co_s cs
+ go_co (AxiomCo _ cs) = go_co_s cs
go_co (UnivCo { uco_lty = t1, uco_rty = t2})
= go t1 `plusNameEnv` go t2
go_co (SymCo co) = go_co co
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1563,7 +1563,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos
go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2]
go_co dv (FunCo _ _ _ w co1 co2) = foldlM go_co dv [w, co1, co2]
- go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos
+ go_co dv (AxiomCo _ cos) = foldlM go_co dv cos
go_co dv (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps })
= do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv t1
; dv2 <- collect_cand_qtvs orig_ty True cur_lvl bound dv1 t2
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/51db59f2f029cfc526b6ee6d7668c30ec10f7d74...493b80a991313bd3bf7c86d6831a06766cd58dc7
--
This project does not include diff previews in email notifications.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/51db59f2f029cfc526b6ee6d7668c30ec10f7d74...493b80a991313bd3bf7c86d6831a06766cd58dc7
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/20240712/a138dc5d/attachment-0001.html>
More information about the ghc-commits
mailing list