[Git][ghc/ghc][wip/T24978] Big refacor, combining AxInstCo and AxRuleCo
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Jul 5 14:27:45 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
03beee71 by Simon Peyton Jones at 2024-07-05T15:26:51+01:00
Big refacor, combining AxInstCo and AxRuleCo
- - - - -
21 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/TyCon.hs-boot
- compiler/GHC/Core/Type.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Iface/Rename.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
Changes:
=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -159,14 +159,14 @@ tryInteractInertFam builtin_fam fam_tc tys1 tys2
eqn = Pair (mkTyConApp fam_tc tys1) (mkTyConApp fam_tc tys2)
tryMatchFam :: BuiltInSynFamily -> [Type]
- -> Maybe (CoAxiomRule, [Type], 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 coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
+-- That is: mkAxiomRuleCo ax (zipWith mkReflCo (coAxArgRuleRoles ax) ts)
-- :: F tys ~r rhs,
tryMatchFam builtin_fam arg_tys
= listToMaybe $ -- Pick first rule to match
- [ (BuiltInFamRewrite rw_ax, inst_tys, res_ty)
+ [ (rw_ax, inst_tys, res_ty)
| rw_ax <- sfMatchFam builtin_fam
, Just (inst_tys,res_ty) <- [bifrw_match rw_ax arg_tys] ]
@@ -353,20 +353,16 @@ typeNatTyCons =
]
-tyConAxiomRules :: TyCon -> [CoAxiomRule]
-tyConAxiomRules tc
- | Just ops <- isBuiltInSynFamTyCon_maybe tc
- = map BuiltInFamInteract (sfInteract ops)
- ++ map BuiltInFamRewrite (sfMatchFam ops)
- | otherwise
- = []
-
-- The list of built-in type family axioms that GHC uses.
-- If you define new axioms, make sure to include them in this list.
-- See Note [Adding built-in type families]
typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
-typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x)) $
- concatMap tyConAxiomRules typeNatTyCons
+typeNatCoAxiomRules
+ = listToUFM $
+ [ pr | tc <- typeNatTyCons
+ , Just ops <- [isBuiltInSynFamTyCon_maybe tc]
+ , pr <- [ (bifint_name bif, BuiltInFamInteract bif) | bif <- sfInteract ops ]
+ ++ [ (bifrw_name bif, BuiltInFamRewrite bif) | bif <- sfMatchFam ops ] ]
-------------------------------------------------------------------------------
-- Addition (+)
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -44,7 +44,7 @@ module GHC.Core.Coercion (
mkNakedForAllCo, mkForAllCo, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
- mkAxiomInstCo, mkProofIrrelCo,
+ mkProofIrrelCo,
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo,
@@ -1022,41 +1022,39 @@ it's a relatively expensive test and perhaps better done in
optCoercion. Not a big deal either way.
-}
-mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
+mkAxInstCo :: Role
+ -> CoAxiomRule -- Always BranchedAxiom or UnbranchedAxiom
+ -> [Type] -> [Coercion]
-> Coercion
-- mkAxInstCo can legitimately be called over-saturated;
-- i.e. with more type arguments than the coercion requires
-mkAxInstCo role ax index tys cos
+-- Only called with BranchedAxiom or UnbranchedAxiom
+mkAxInstCo role axr tys cos
| arity == n_tys = downgradeRole role ax_role $
- mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
+ AxiomRuleCo axr (rtys `chkAppend` cos)
| otherwise = assert (arity < n_tys) $
downgradeRole role ax_role $
- mkAppCos (mkAxiomInstCo ax_br index
- (ax_args `chkAppend` cos))
+ mkAppCos (AxiomRuleCo axr (ax_args `chkAppend` cos))
leftover_args
where
- n_tys = length tys
- ax_br = toBranchedAxiom ax
- branch = coAxiomNthBranch ax_br index
- tvs = coAxBranchTyVars branch
- arity = length tvs
- arg_roles = coAxBranchRoles branch
- rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
- (ax_args, leftover_args)
- = splitAt arity rtys
- ax_role = coAxiomRole ax
+ (ax_role, branch) = case coAxiomRuleBranch_maybe axr of
+ Just (_tc, ax_role, branch) -> (ax_role, branch)
+ Nothing -> pprPanic "mkAxInstCo" (ppr axr)
+ n_tys = length tys
+ arity = length (coAxBranchTyVars branch)
+ arg_roles = coAxBranchRoles branch
+ rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
+ (ax_args, leftover_args) = splitAt arity rtys
-- worker function
-mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
-mkAxiomInstCo ax index args
- = assert (args `lengthIs` coAxiomArity ax index) $
- AxiomInstCo ax index args
+mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
+mkAxiomRuleCo = AxiomRuleCo
-- to be used only with unbranched axioms
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
-> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo role ax tys cos
- = mkAxInstCo role ax 0 tys cos
+ = mkAxInstCo role (UnbranchedAxiom ax) tys cos
mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
-- Instantiate the axiom with specified types,
@@ -1386,9 +1384,6 @@ downgradeRole r1 r2 co
Just co' -> co'
Nothing -> pprPanic "downgradeRole" (ppr co)
-mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
-mkAxiomRuleCo = AxiomRuleCo
-
-- | Make a "coercion between coercions".
mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
-> CoercionN -- ^ :: phi1 ~N phi2
@@ -1580,7 +1575,6 @@ promoteCoercion co = case co of
CoVarCo {} -> mkKindCo co
HoleCo {} -> mkKindCo co
- AxiomInstCo {} -> mkKindCo co
AxiomRuleCo {} -> mkKindCo co
UnivCo {} -> mkKindCo co
@@ -2402,7 +2396,6 @@ 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 (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
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
@@ -2472,22 +2465,7 @@ coercionLKind co
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
go (SelCo d co) = selectFromType d (go co)
- go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
- go (AxiomRuleCo ax cos) = pFst $ expectJust "coercionKind" $
- coaxrProves ax $ map coercionKind cos
-
- go_ax_inst ax ind tys
- | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
- , cab_lhs = lhs } <- coAxiomNthBranch ax ind
- , let (tys1, cotys1) = splitAtList tvs tys
- cos1 = map stripCoercionTy cotys1
- = assert (tys `equalLength` (tvs ++ cvs)) $
- -- Invariant of AxiomInstCo: cos should
- -- exactly saturate the axiom branch
- substTyWith tvs tys1 $
- substTyWithCoVars cvs cos1 $
- mkTyConApp (coAxiomTyCon ax) lhs
-
+ go (AxiomRuleCo ax cos) = pFst (coAxRuleKind ax (map coercionKind cos))
go_app :: Coercion -> [Type] -> Type
-- Collect up all the arguments and apply all at once
-- See Note [Nested InstCos]
@@ -2516,9 +2494,7 @@ coercionRKind co
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
go (SelCo d co) = selectFromType d (go co)
- go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
- go (AxiomRuleCo ax cos) = pSnd $ expectJust "coercionKind" $
- coaxrProves ax $ map coercionKind cos
+ go (AxiomRuleCo ax cos) = pSnd (coAxRuleKind ax (map coercionKind cos))
go co@(ForAllCo { fco_tcv = tv1, fco_visR = visR
, fco_kind = k_co, fco_body = co1 }) -- works for both tyvar and covar
@@ -2528,17 +2504,6 @@ coercionRKind co
where
empty_subst = mkEmptySubst (mkInScopeSet $ tyCoVarsOfCo co)
- go_ax_inst ax ind tys
- | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
- , cab_rhs = rhs } <- coAxiomNthBranch ax ind
- , let (tys2, cotys2) = splitAtList tvs tys
- cos2 = map stripCoercionTy cotys2
- = assert (tys `equalLength` (tvs ++ cvs)) $
- -- Invariant of AxiomInstCo: cos should
- -- exactly saturate the axiom branch
- substTyWith tvs tys2 $
- substTyWithCoVars cvs cos2 rhs
-
go_app :: Coercion -> [Type] -> Type
-- Collect up all the arguments and apply all at once
-- See Note [Nested InstCos]
@@ -2588,6 +2553,26 @@ coercionRKind co
-- when other_co is not a ForAllCo
= substTy subst (go other_co)
+coAxRuleKind :: CoAxiomRule -> [Pair Type] -> Pair Type
+coAxRuleKind ax prs
+ = case ax of
+ BuiltInFamRewrite bif -> expectJust "coAxRuleKind" (bifrw_proves bif prs)
+ BuiltInFamInteract bif -> expectJust "coAxRuleKind" (bifint_proves bif prs)
+ UnbranchedAxiom ax -> go_branch ax (coAxiomSingleBranch ax)
+ BranchedAxiom ax i -> go_branch ax (coAxiomNthBranch ax i)
+ where
+ go_branch :: CoAxiom br -> CoAxBranch -> Pair Type
+ go_branch ax (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty })
+ = assert (prs `equalLength` tcvs) $
+ -- Invariant of AxiomRuleCo: cos should
+ -- exactly saturate the axiom branch
+ Pair (substTy (zipTCvSubst tcvs ltys) (mkTyConApp tc lhs_tys))
+ (substTy (zipTCvSubst tcvs rtys) rhs_ty)
+ where
+ (ltys, rtys) = unzipPairs prs
+ tc = coAxiomTyCon ax
+ tcvs = tvs ++ cvs
+
{-
Note [Nested ForAllCos]
@@ -2617,7 +2602,6 @@ coercionRole = go
go (FunCo { fco_role = r }) = r
go (CoVarCo cv) = coVarRole cv
go (HoleCo h) = coVarRole (coHoleCoVar h)
- go (AxiomInstCo ax _ _) = coAxiomRole ax
go (UnivCo { uco_role = r }) = r
go (SymCo co) = go co
go (TransCo co1 _co2) = go co1
@@ -2626,7 +2610,7 @@ coercionRole = go
go (InstCo co _) = go co
go (KindCo {}) = Nominal
go (SubCo _) = Representational
- go (AxiomRuleCo ax _) = coaxrRole ax
+ go (AxiomRuleCo ax _) = coAxiomRuleRole ax
{-
Note [Nested InstCos]
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -21,7 +21,6 @@ mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coerci
mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkCoVarCo :: CoVar -> Coercion
-mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkUnivCo :: UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
mkSymCo :: Coercion -> Coercion
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -31,7 +31,8 @@ module GHC.Core.Coercion.Axiom (
Role(..), fsFromRole,
CoAxiomRule(..), BuiltInFamRewrite(..), BuiltInFamInteract(..), TypeEqn,
- coaxrName, coaxrAsmpRoles, coaxrRole, coaxrProves,
+ coAxiomRuleArgRoles, coAxiomRuleRole,
+ coAxiomRuleBranch_maybe, isNewtypeAxiomRule_maybe,
BuiltInSynFamily(..), trivialBuiltInFamily
) where
@@ -41,7 +42,7 @@ import Language.Haskell.Syntax.Basic (Role(..))
import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprTyVar )
-import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
+import {-# SOURCE #-} GHC.Core.TyCon ( TyCon, isNewTyCon )
import GHC.Utils.Outputable
import GHC.Data.FastString
import GHC.Types.Name
@@ -80,12 +81,12 @@ axF :: { F [Int] ~ Bool
; forall (k :: *) (a :: k -> *) (b :: k). F (a b) ~ Char
}
-The axiom is used with the AxiomInstCo constructor of Coercion. If we wish
+The axiom is used with the AxiomRuleCo 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
-- or, written using concrete-ish syntax --
-AxiomInstCo axF 2 [Refl *, Refl Maybe, Refl Int]
+AxiomRuleCo axF 2 [Refl *, Refl Maybe, Refl Int]
Note that the index is 0-based.
@@ -128,8 +129,21 @@ type variable is accurate.
************************************************************************
-}
-type BranchIndex = Int -- The index of the branch in the list of branches
- -- Counting from zero
+{- Note [BranchIndex]
+~~~~~~~~~~~~~~~~~~~~
+A CoAxiom has 1 or more branches. Each branch has contains a list
+of the free type variables in that branch, the LHS type patterns,
+and the RHS type for that branch. When we apply an axiom to a list
+of coercions, we must choose which branch of the axiom we wish to
+use, as the different branches may have different numbers of free
+type variables. (The number of type patterns is always the same
+among branches, but that doesn't quite concern us here.)
+-}
+
+
+type BranchIndex = Int -- Counting from zero
+ -- The index of the branch in the list of branches
+ -- See Note [BranchIndex]
-- promoted data type
data BranchFlag = Branched | Unbranched
@@ -279,10 +293,6 @@ toUnbranchedAxiom (CoAxiom unique name role tc branches implicit)
coAxiomNumPats :: CoAxiom br -> Int
coAxiomNumPats = length . coAxBranchLHS . (flip coAxiomNthBranch 0)
-coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
-coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index
- = branchesNth bs index
-
coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
coAxiomArity ax index
= length tvs + length cvs
@@ -297,6 +307,14 @@ coAxiomRole = co_ax_role
coAxiomBranches :: CoAxiom br -> Branches br
coAxiomBranches = co_ax_branches
+coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
+coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index
+ = branchesNth bs index
+
+coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
+coAxiomSingleBranch (CoAxiom { co_ax_branches = MkBranches arr })
+ = arr ! 0
+
coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = MkBranches arr })
| snd (bounds arr) == 0
@@ -304,10 +322,6 @@ coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = MkBranches arr })
| otherwise
= Nothing
-coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
-coAxiomSingleBranch (CoAxiom { co_ax_branches = MkBranches arr })
- = arr ! 0
-
coAxiomTyCon :: CoAxiom br -> TyCon
coAxiomTyCon = co_ax_tc
@@ -580,29 +594,79 @@ CoAxiomRules come in two flavours:
-}
--- | A more explicit representation for `t1 ~ t2`.
-type TypeEqn = Pair Type
-
-- | CoAxiomRule is a sum type that joins BuiltInFamRewrite and BuiltInFamInteract
data CoAxiomRule
= BuiltInFamRewrite BuiltInFamRewrite
| BuiltInFamInteract BuiltInFamInteract
+ | BranchedAxiom (CoAxiom Branched) BranchIndex
+ | UnbranchedAxiom (CoAxiom Unbranched)
+
+instance Eq CoAxiomRule where
+ (BuiltInFamRewrite bif1) == (BuiltInFamRewrite bif2) = bifrw_name bif1 == bifrw_name bif2
+ (BuiltInFamInteract bif1) == (BuiltInFamInteract bif2) = bifint_name bif1 == bifint_name bif2
+ (UnbranchedAxiom ax1) == (UnbranchedAxiom ax2) = getUnique ax1 == getUnique ax2
+ (BranchedAxiom ax1 i1) == (BranchedAxiom ax2 i2) = getUnique ax1 == getUnique ax2 && i1 == i2
+ _ == _ = 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
+
+coAxiomRuleArgRoles :: CoAxiomRule -> [Role]
+coAxiomRuleArgRoles (BuiltInFamRewrite bif) = bifrw_arg_roles bif
+coAxiomRuleArgRoles (BuiltInFamInteract bif) = bifint_arg_roles bif
+coAxiomRuleArgRoles (UnbranchedAxiom ax) = coAxBranchRoles (coAxiomSingleBranch ax)
+coAxiomRuleArgRoles (BranchedAxiom ax i) = coAxBranchRoles (coAxiomNthBranch ax i)
+
+coAxiomRuleBranch_maybe :: CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)
+coAxiomRuleBranch_maybe (UnbranchedAxiom ax) = Just (co_ax_tc ax, co_ax_role ax, coAxiomSingleBranch ax)
+coAxiomRuleBranch_maybe (BranchedAxiom ax i) = Just (co_ax_tc ax, co_ax_role ax, coAxiomNthBranch ax i)
+coAxiomRuleBranch_maybe _ = Nothing
+
+isNewtypeAxiomRule_maybe :: CoAxiomRule -> Maybe (TyCon, CoAxBranch)
+isNewtypeAxiomRule_maybe (UnbranchedAxiom ax)
+ | let tc = coAxiomTyCon ax, isNewTyCon tc = Just (tc, coAxiomSingleBranch ax)
+isNewtypeAxiomRule_maybe _ = Nothing
+
+instance Data.Data CoAxiomRule where
+ -- don't traverse?
+ toConstr _ = abstractConstr "CoAxiomRule"
+ gunfold _ _ = error "gunfold"
+ dataTypeOf _ = mkNoRepType "CoAxiomRule"
-coaxrName :: CoAxiomRule -> FastString
-coaxrName (BuiltInFamRewrite bif) = bifrw_name bif
-coaxrName (BuiltInFamInteract bif) = bifint_name bif
+--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)
-coaxrAsmpRoles :: CoAxiomRule -> [Role]
-coaxrAsmpRoles (BuiltInFamRewrite bif) = bifrw_arg_roles bif
-coaxrAsmpRoles (BuiltInFamInteract bif) = bifint_arg_roles bif
+instance Outputable CoAxiomRule where
+ ppr (BuiltInFamRewrite bif) = ppr (bifrw_name bif)
+ ppr (BuiltInFamInteract bif) = ppr (bifint_name bif)
+ ppr (UnbranchedAxiom ax) = ppr (coAxiomName ax)
+ ppr (BranchedAxiom ax i) = ppr (coAxiomName ax) <> brackets (int i)
-coaxrRole :: CoAxiomRule -> Role
-coaxrRole (BuiltInFamRewrite bif) = bifrw_res_role bif
-coaxrRole (BuiltInFamInteract bif) = bifint_res_role bif
+{- *********************************************************************
+* *
+ Built-in families
+* *
+********************************************************************* -}
-coaxrProves :: CoAxiomRule -> [TypeEqn] -> Maybe TypeEqn
-coaxrProves (BuiltInFamRewrite bif) = bifrw_proves bif
-coaxrProves (BuiltInFamInteract bif) = bifint_proves bif
+
+-- | A more explicit representation for `t1 ~ t2`.
+type TypeEqn = Pair Type
+
+-- Type checking of built-in families
+data BuiltInSynFamily = BuiltInSynFamily
+ { 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
= BIF_Interact
@@ -610,7 +674,7 @@ data BuiltInFamInteract
, bifint_arg_roles :: [Role] -- roles of parameter equations
, bifint_res_role :: Role -- role of resulting equation
, bifint_proves :: [TypeEqn] -> Maybe TypeEqn
- -- ^ coaxrProves returns @Nothing@ when it doesn't like
+ -- ^ 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.
@@ -625,43 +689,11 @@ data BuiltInFamRewrite
, bifrw_match :: [Type] -> Maybe ([Type], Type) -- Instantiating types and result 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 coax (zipWith mkReflCo coaxrAsmpRoles ts)
+ -- That is: mkAxiomRuleCo ax (zipWith mkReflCo coAxiomRuleArgRoles ts)
-- :: F tys ~coaxrRole rhs,
, bifrw_proves :: [TypeEqn] -> Maybe TypeEqn }
-instance Data.Data CoAxiomRule where
- -- don't traverse?
- toConstr _ = abstractConstr "CoAxiomRule"
- gunfold _ _ = error "gunfold"
- dataTypeOf _ = mkNoRepType "CoAxiomRule"
-
-instance Uniquable CoAxiomRule where
- getUnique = getUnique . coaxrName
-
-instance Eq CoAxiomRule where
- x == y = coaxrName x == coaxrName y
-
-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 = ppr . coaxrName
-
--- Type checking of built-in families
-data BuiltInSynFamily = BuiltInSynFamily
- { 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
- }
-
-- Provides default implementations that do nothing.
trivialBuiltInFamily :: BuiltInSynFamily
trivialBuiltInFamily = BuiltInSynFamily { sfMatchFam = [], sfInteract = [] }
-
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -355,19 +355,19 @@ 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 (AxiomInstCo con ind cos)
+opt_co4 env sym rep r (AxiomRuleCo con cos)
-- Do *not* push sym inside top-level axioms
-- e.g. if g is a top-level axiom
-- g a : f a ~ a
-- then (sym (g ty)) /= g (sym ty) !!
- = assert (r == coAxiomRole con )
- wrapRole rep (coAxiomRole con) $
+ = assert (r == coAxiomRuleRole con )
+ wrapRole rep (coAxiomRuleRole con) $
wrapSym sym $
-- some sub-cos might be P: use opt_co2
-- See Note [Optimising coercion optimisation]
- AxiomInstCo con ind (zipWith (opt_co2 env False)
- (coAxBranchRoles (coAxiomNthBranch con ind))
- cos)
+ AxiomRuleCo 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
@@ -506,13 +506,6 @@ opt_co4 env sym _ r (SubCo co)
= assert (r == Representational) $
opt_co4_wrap env sym True Nominal co
--- This could perhaps be optimized more.
-opt_co4 env sym rep r (AxiomRuleCo co cs)
- = assert (r == coaxrRole co) $
- wrapRole rep r $
- wrapSym sym $
- AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
-
{- Note [Optimise CoVarCo to Refl]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we have (c :: t~t) we can optimise it to Refl. That increases the
@@ -840,15 +833,13 @@ 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, ax1, ind1, cos1) <- isAxiom_maybe co1
- , Just (sym2, ax2, ind2, cos2) <- isAxiom_maybe co2
- , ax1 == ax2
- , ind1 == ind2
+ | Just (sym1, axr1, cos1) <- isAxiomRuleCo_maybe co1
+ , Just (sym2, axr2, cos2) <- isAxiomRuleCo_maybe co2
+ , axr1 == axr2
, sym1 == not sym2
- , let branch = coAxiomNthBranch ax1 ind1
- role = coAxiomRole ax1
- qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
- lhs = coAxNthLHS ax1 ind1
+ , Just (tc, role, branch) <- coAxiomRuleBranch_maybe axr1
+ , let qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
+ lhs = mkTyConApp tc (coAxBranchLHS branch)
rhs = coAxBranchRHS branch
pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
, all (`elemVarSet` pivot_tvs) qtvs
@@ -862,35 +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, con, ind, cos1) <- isAxiom_maybe co1
- , isNewTyCon (coAxiomTyCon con)
+ | Just (sym, axr, cos1) <- isAxiomRuleCo_maybe co1
, True <- sym
- , Just cos2 <- matchAxiom sym con ind co2
- , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
+ , Just cos2 <- matchNewtypeBranch sym axr co2
+ , let newAxInst = AxiomRuleCo axr (opt_transList is (map mkSymCo cos2) cos1)
= fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
-- TrPushAxR
- | Just (sym, con, ind, cos1) <- isAxiom_maybe co1
- , isNewTyCon (coAxiomTyCon con)
+ | Just (sym, axr, cos1) <- isAxiomRuleCo_maybe co1
, False <- sym
- , Just cos2 <- matchAxiom sym con ind co2
- , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+ , Just cos2 <- matchNewtypeBranch sym axr co2
+ , let newAxInst = AxiomRuleCo axr (opt_transList is cos1 cos2)
= fireTransRule "TrPushAxR" co1 co2 newAxInst
-- TrPushSymAxL
- | Just (sym, con, ind, cos2) <- isAxiom_maybe co2
- , isNewTyCon (coAxiomTyCon con)
+ | Just (sym, axr, cos2) <- isAxiomRuleCo_maybe co2
, True <- sym
- , Just cos1 <- matchAxiom (not sym) con ind co1
- , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
+ , Just cos1 <- matchNewtypeBranch (not sym) axr co1
+ , let newAxInst = AxiomRuleCo axr (opt_transList is cos2 (map mkSymCo cos1))
= fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
-- TrPushAxL
- | Just (sym, con, ind, cos2) <- isAxiom_maybe co2
- , isNewTyCon (coAxiomTyCon con)
+ | Just (sym, axr, cos2) <- isAxiomRuleCo_maybe co2
, False <- sym
- , Just cos1 <- matchAxiom (not sym) con ind co1
- , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+ , Just cos1 <- matchNewtypeBranch (not sym) axr co1
+ , let newAxInst = AxiomRuleCo axr (opt_transList is cos1 cos2)
= fireTransRule "TrPushAxL" co1 co2 newAxInst
@@ -1145,24 +1132,24 @@ chooseRole True _ = Representational
chooseRole _ r = r
-----------
-isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
+isAxiomRuleCo_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.)
-isAxiom_maybe (SymCo (AxiomInstCo ax ind cos))
- = Just (True, ax, ind, cos)
-isAxiom_maybe (AxiomInstCo ax ind cos)
- = Just (False, ax, ind, cos)
-isAxiom_maybe _ = Nothing
-
-matchAxiom :: Bool -- True = match LHS, False = match RHS
- -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
-matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
- | CoAxBranch { cab_tvs = qtvs
+isAxiomRuleCo_maybe (SymCo (AxiomRuleCo ax cos)) = Just (True, ax, cos)
+isAxiomRuleCo_maybe (AxiomRuleCo ax cos) = Just (False, ax, cos)
+isAxiomRuleCo_maybe _ = Nothing
+
+matchNewtypeBranch :: Bool -- True = match LHS, False = match RHS
+ -> CoAxiomRule
+ -> Coercion -> Maybe [Coercion]
+matchNewtypeBranch sym axr co
+ | Just (tc,branch) <- isNewtypeAxiomRule_maybe axr
+ , CoAxBranch { cab_tvs = qtvs
, cab_cvs = [] -- can't infer these, so fail if there are any
, cab_roles = roles
, cab_lhs = lhs
- , cab_rhs = rhs } <- coAxiomNthBranch ax ind
+ , cab_rhs = rhs } <- branch
, Just subst <- liftCoMatch (mkVarSet qtvs)
(if sym then (mkTyConApp tc lhs) else rhs)
co
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -40,7 +40,7 @@ module GHC.Core.FVs (
-- * Orphan names
orphNamesOfType, orphNamesOfTypes,
- orphNamesOfCo, orphNamesOfCoCon, orphNamesOfAxiomLHS,
+ orphNamesOfCo, orphNamesOfAxiomLHS,
exprsOrphNames,
-- * Core syntax tree annotation with free variables
@@ -394,7 +394,7 @@ orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
`unionNameSet` orphNamesOfCo co1
`unionNameSet` orphNamesOfCo co2
orphNamesOfCo (CoVarCo _) = emptyNameSet
-orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
+orphNamesOfCo (AxiomRuleCo con cos) = orphNamesOfAxRule con `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (UnivCo { uco_lty = t1, uco_rty = t2 })
= orphNamesOfType t1 `unionNameSet` orphNamesOfType t2
orphNamesOfCo (SymCo co) = orphNamesOfCo co
@@ -404,14 +404,19 @@ orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
orphNamesOfCo (KindCo co) = orphNamesOfCo co
orphNamesOfCo (SubCo co) = orphNamesOfCo co
-orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs
orphNamesOfCo (HoleCo _) = emptyNameSet
orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo
-orphNamesOfCoCon :: CoAxiom br -> NameSet
-orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
+orphNamesOfAxRule :: CoAxiomRule -> NameSet
+orphNamesOfAxRule (BuiltInFamRewrite {}) = emptyNameSet
+orphNamesOfAxRule (BuiltInFamInteract {}) = emptyNameSet
+orphNamesOfAxRule (UnbranchedAxiom ax) = orphNamesOfCoAx ax
+orphNamesOfAxRule (BranchedAxiom ax _) = orphNamesOfCoAx ax
+
+orphNamesOfCoAx :: CoAxiom br -> NameSet
+orphNamesOfCoAx (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
= orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches
orphNamesOfCoAxBranches :: Branches br -> NameSet
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -1193,13 +1193,14 @@ reduceTyFamApp_maybe envs role tc tys
| Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
, Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
- = let co = mkAxInstCo role ax ind inst_tys inst_cos
+ = let co = mkAxInstCo role (BranchedAxiom ax ind) inst_tys inst_cos
in Just $ coercionRedn co
| Just builtin_fam <- isBuiltInSynFamTyCon_maybe tc
- , Just (coax,ts,ty) <- tryMatchFam builtin_fam tys
- , role == coaxrRole coax
- = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
+ , 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)
in Just $ mkReduction co ty
| otherwise
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2611,42 +2611,47 @@ lintCoercion (InstCo co arg)
; _ -> failWithL (text "Bad argument of inst") }}}
-lintCoercion co@(AxiomInstCo con ind cos)
- = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
- (bad_ax (text "index out of range"))
- ; let CoAxBranch { cab_tvs = ktvs
- , cab_cvs = cvs
- , cab_roles = roles } = coAxiomNthBranch con ind
- ; unless (cos `equalLength` (ktvs ++ cvs)) $
- bad_ax (text "lengths")
- ; cos' <- mapM lintCoercion cos
- ; subst <- getSubst
- ; let empty_subst = zapSubst subst
- ; _ <- foldlM check_ki (empty_subst, empty_subst)
- (zip3 (ktvs ++ cvs) roles cos')
- ; let fam_tc = coAxiomTyCon con
- ; case checkAxInstCo co of
- Just bad_branch -> bad_ax $ text "inconsistent with" <+>
- pprCoAxBranch fam_tc bad_branch
- Nothing -> return ()
- ; return (AxiomInstCo con ind cos') }
+lintCoercion this_co@(AxiomRuleCo 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') }
where
- bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
- 2 (ppr co))
+ 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
+ lint_ax (UnbranchedAxiom ax) prs
+ = lintBranch this_co (coAxiomTyCon ax) (coAxiomSingleBranch ax) prs
+ lint_ax (BranchedAxiom ax ind) prs
+ = do { checkL (0 <= ind && ind < numBranches (coAxiomBranches ax))
+ (bad_ax this_co (text "index out of range"))
+ ; lintBranch this_co (coAxiomTyCon ax) (coAxiomNthBranch ax ind) prs }
+
+ bad_bif = bad_ax this_co (text "Proves returns Nothing")
+
+ err :: forall a. String -> [SDoc] -> LintM a
+ err m xs = failWithL $
+ hang (text m) 2 $ vcat (text "Rule:" <+> ppr ax : xs)
+
+ lint_roles n (e : es) (co : cos)
+ | e == coercionRole co
+ = lint_roles (n+1) es cos
+ | otherwise = err "Argument roles mismatch"
+ [ text "In argument:" <+> int (n+1)
+ , text "Expected:" <+> ppr e
+ , text "Found:" <+> ppr (coercionRole co) ]
+ lint_roles _ [] [] = return ()
+ lint_roles n [] rs = err "Too many coercion arguments"
+ [ text "Expected:" <+> int n
+ , text "Provided:" <+> int (n + length rs) ]
+
+ lint_roles n es [] = err "Not enough coercion arguments"
+ [ text "Expected:" <+> int (n + length es)
+ , text "Provided:" <+> int n ]
- check_ki (subst_l, subst_r) (ktv, role, arg')
- = do { let Pair s' t' = coercionKind arg'
- sk' = typeKind s'
- tk' = typeKind t'
- ; lintRole arg' role (coercionRole arg')
- ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
- ktv_kind_r = substTy subst_r (tyVarKind ktv)
- ; unless (sk' `eqType` ktv_kind_l)
- (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr sk', ppr ktv, ppr ktv_kind_l ] ))
- ; unless (tk' `eqType` ktv_kind_r)
- (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr tk', ppr ktv, ppr ktv_kind_r ] ))
- ; return (extendTCvSubst subst_l ktv s',
- extendTCvSubst subst_r ktv t') }
lintCoercion (KindCo co)
= do { co' <- lintCoercion co
@@ -2657,40 +2662,14 @@ lintCoercion (SubCo co')
; lintRole co' Nominal (coercionRole co')
; return (SubCo co') }
-lintCoercion this@(AxiomRuleCo ax cos)
- = do { cos' <- mapM lintCoercion cos
- ; lint_roles 0 (coaxrAsmpRoles ax) cos'
- ; case coaxrProves ax (map coercionKind cos') of
- Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
- Just _ -> return (AxiomRuleCo ax cos') }
- where
- err :: forall a. String -> [SDoc] -> LintM a
- err m xs = failWithL $
- hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName ax) : xs)
-
- lint_roles n (e : es) (co : cos)
- | e == coercionRole co = lint_roles (n+1) es cos
- | otherwise = err "Argument roles mismatch"
- [ text "In argument:" <+> int (n+1)
- , text "Expected:" <+> ppr e
- , text "Found:" <+> ppr (coercionRole co) ]
- lint_roles _ [] [] = return ()
- lint_roles n [] rs = err "Too many coercion arguments"
- [ text "Expected:" <+> int n
- , text "Provided:" <+> int (n + length rs) ]
-
- lint_roles n es [] = err "Not enough coercion arguments"
- [ text "Expected:" <+> int (n + length es)
- , text "Provided:" <+> int n ]
-
lintCoercion (HoleCo h)
= do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
; lintCoercion (CoVarCo (coHoleCoVar h)) }
{-
-Note [Conflict checking with AxiomInstCo]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Conflict checking for axiom applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following type family and axiom:
type family Equal (a :: k) (b :: k) :: Bool
@@ -2718,28 +2697,53 @@ docs/core-spec, which defines the corresponding no_conflict function used by the
Co_AxiomInstCo rule in the section "Coercion typing".
-}
--- | Check to make sure that an AxInstCo is internally consistent.
+-- | Check to make sure that an axiom application is internally consistent.
-- Returns the conflicting branch, if it exists
--- See Note [Conflict checking with AxiomInstCo]
-checkAxInstCo :: Coercion -> Maybe CoAxBranch
+-- Note [Conflict checking for axiom applications]
+lintBranch :: Coercion -> TyCon-> CoAxBranch -> [Pair Type] -> LintM ()
-- defined here to avoid dependencies in GHC.Core.Coercion
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism] in GHC.Core.Lint
-checkAxInstCo (AxiomInstCo ax ind cos)
- = let branch = coAxiomNthBranch ax ind
- tvs = coAxBranchTyVars branch
- cvs = coAxBranchCoVars branch
- incomps = coAxBranchIncomps branch
- (tys, cotys) = splitAtList tvs (map coercionLKind cos)
- co_args = map stripCoercionTy cotys
- subst = zipTvSubst tvs tys `composeTCvSubst`
- zipCvSubst cvs co_args
- target = Type.substTys subst (coAxBranchLHS branch)
- in_scope = mkInScopeSet $
- unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
- flattened_target = flattenTys in_scope target in
- check_no_conflict flattened_target incomps
+lintBranch this_co fam_tc branch arg_kinds
+ | CoAxBranch { cab_tvs = ktvs, cab_cvs = cvs } <- branch
+ = do { checkL (arg_kinds `equalLength` (ktvs ++ cvs)) $
+ (bad_ax this_co (text "lengths"))
+
+ ; subst <- getSubst
+ ; let empty_subst = zapSubst subst
+ ; _ <- foldlM check_ki (empty_subst, empty_subst)
+ (zip (ktvs ++ cvs) arg_kinds)
+
+ ; case check_no_conflict flattened_target incomps of
+ Nothing -> return ()
+ Just bad_branch -> failWithL $ bad_ax this_co $
+ text "inconsistent with" <+>
+ pprCoAxBranch fam_tc bad_branch }
where
+ check_ki (subst_l, subst_r) (ktv, Pair s' t')
+ = do { let sk' = typeKind s'
+ tk' = typeKind t'
+ ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
+ ktv_kind_r = substTy subst_r (tyVarKind ktv)
+ ; checkL (sk' `eqType` ktv_kind_l)
+ (bad_ax this_co (text "check_ki1" <+> vcat [ ppr this_co, ppr sk', ppr ktv, ppr ktv_kind_l ] ))
+ ; checkL (tk' `eqType` ktv_kind_r)
+ (bad_ax this_co (text "check_ki2" <+> vcat [ ppr this_co, ppr tk', ppr ktv, ppr ktv_kind_r ] ))
+ ; return (extendTCvSubst subst_l ktv s',
+ extendTCvSubst subst_r ktv t') }
+
+ tvs = coAxBranchTyVars branch
+ cvs = coAxBranchCoVars branch
+ incomps = coAxBranchIncomps branch
+ (tys, cotys) = splitAtList tvs (map pFst arg_kinds)
+ co_args = map stripCoercionTy cotys
+ subst = zipTvSubst tvs tys `composeTCvSubst`
+ zipCvSubst cvs co_args
+ target = Type.substTys subst (coAxBranchLHS branch)
+ in_scope = mkInScopeSet $
+ unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
+ flattened_target = flattenTys in_scope target
+
check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict _ [] = Nothing
check_no_conflict flat (b at CoAxBranch { cab_lhs = lhs_incomp } : rest)
@@ -2748,7 +2752,10 @@ checkAxInstCo (AxiomInstCo ax ind cos)
= check_no_conflict flat rest
| otherwise
= Just b
-checkAxInstCo _ = Nothing
+
+bad_ax :: Coercion -> SDoc -> SDoc
+bad_ax this_co what
+ = hang (text "Bad axiom application" <+> parens what) 2 (ppr this_co)
{-
=====================================
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( coAxiomTyCon )
+import GHC.Core.Coercion.Axiom( CoAxiomRule(..), 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 (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
+tyCoFVsOfCo (AxiomRuleCo _ 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
@@ -679,7 +679,6 @@ tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in
tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar v fv_cand in_scope acc
@@ -717,8 +716,8 @@ 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 (AxiomInstCo _ _ cos) cv
- = almost_devoid_co_var_of_cos cos cv
+almost_devoid_co_var_of_co (AxiomRuleCo _ 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
&& almost_devoid_co_var_of_type t1 cv
@@ -739,8 +738,6 @@ almost_devoid_co_var_of_co (KindCo co) cv
= almost_devoid_co_var_of_co co cv
almost_devoid_co_var_of_co (SubCo co) cv
= almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
- = almost_devoid_co_var_of_cos cs cv
almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos [] _ = True
@@ -1129,7 +1126,7 @@ 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 (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
+ 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 (CoVarCo {}) = emptyUniqSet
go_co (HoleCo {}) = emptyUniqSet
@@ -1140,7 +1137,6 @@ tyConsOfType ty
go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
go_co (KindCo co) = go_co co
go_co (SubCo co) = go_co co
- go_co (AxiomRuleCo _ cs) = go_cos cs
go_mco MRefl = emptyUniqSet
go_mco (MCo co) = go_co co
@@ -1148,7 +1144,11 @@ tyConsOfType ty
go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
go_tc tc = unitUniqSet tc
- go_ax ax = go_tc $ coAxiomTyCon ax
+
+ go_ax (UnbranchedAxiom ax) = go_tc $ coAxiomTyCon ax
+ go_ax (BranchedAxiom ax _) = go_tc $ coAxiomTyCon ax
+ go_ax (BuiltInFamRewrite {}) = emptyUniqSet
+ go_ax (BuiltInFamInteract {}) = emptyUniqSet
tyConsOfTypes :: [Type] -> UniqSet TyCon
tyConsOfTypes tys = foldr (unionUniqSets . tyConsOfType) emptyUniqSet tys
@@ -1326,8 +1326,8 @@ occCheckExpand vs_to_avoid ty
| bad_var_occ as (ch_co_var h) = Nothing
| otherwise = return co
- go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
- ; return (AxiomInstCo ax ind args') }
+ 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
@@ -1348,6 +1348,4 @@ occCheckExpand vs_to_avoid ty
; return (KindCo co') }
go_co cxt (SubCo co) = do { co' <- go_co cxt co
; return (SubCo co') }
- go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
- ; return (AxiomRuleCo ax cs') }
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -907,9 +907,7 @@ data Coercion
| CoVarCo CoVar -- :: _ -> (N or R)
-- result role depends on the tycon of the variable's type
- -- AxiomInstCo :: e -> _ -> ?? -> e
- | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
- -- See also [CoAxiom index]
+ | AxiomRuleCo CoAxiomRule [Coercion]
-- The coercion arguments always *precisely* saturate
-- arity of (that branch of) the CoAxiom. If there are
-- any left over, we use AppCo.
@@ -917,11 +915,6 @@ data Coercion
-- The roles of the argument coercions are determined
-- by the cab_roles field of the relevant branch of the CoAxiom
- | AxiomRuleCo CoAxiomRule [Coercion]
- -- AxiomRuleCo is very like AxiomInstCo, but for a CoAxiomRule
- -- The number of coercions should match exactly the expectations
- -- of the CoAxiomRule (i.e., the rule is fully saturated).
-
| UnivCo -- See Note [UnivCo]
-- Of kind (lty ~role rty)
{ uco_prov :: UnivCoProvenance
@@ -1198,19 +1191,6 @@ Now we have
which can be optimized to F g.
-Note [CoAxiom index]
-~~~~~~~~~~~~~~~~~~~~
-A CoAxiom has 1 or more branches. Each branch has contains a list
-of the free type variables in that branch, the LHS type patterns,
-and the RHS type for that branch. When we apply an axiom to a list
-of coercions, we must choose which branch of the axiom we wish to
-use, as the different branches may have different numbers of free
-type variables. (The number of type patterns is always the same
-among branches, but that doesn't quite concern us here.)
-
-The Int in the AxiomInstCo constructor is the 0-indexed number
-of the chosen branch.
-
Note [Required foralls in Core]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the CoreExpr (Lam a e) where `a` is a TyVar, and (e::e_ty).
@@ -1981,14 +1961,13 @@ 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 (AxiomInstCo _ _ args) = go_cos env args
+ go_co env (AxiomRuleCo _ 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
`mappend` go_cos env deps
go_co env (SymCo co) = go_co env co
go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2
- go_co env (AxiomRuleCo _ cos) = go_cos env cos
go_co env (SelCo _ co) = go_co env co
go_co env (LRCo _ co) = go_co env co
go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg
@@ -2054,7 +2033,7 @@ coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2
+ coercionSize w
coercionSize (CoVarCo _) = 1
coercionSize (HoleCo _) = 1
-coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
+coercionSize (AxiomRuleCo _ 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
@@ -2063,7 +2042,6 @@ coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg
coercionSize (KindCo co) = 1 + coercionSize co
coercionSize (SubCo co) = 1 + coercionSize co
-coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs)
{-
************************************************************************
=====================================
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
- , mkAxiomInstCo, mkAppCo, mkGReflCo
+ , mkAxiomRuleCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
, coercionKind, coercionLKind, coVarKindsTypesRole )
@@ -879,6 +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 (AppCo co arg) = (mkAppCo $! go co) $! go arg
go (ForAllCo tv visL visR kind_co co)
= case substForAllCoBndrUnchecked subst tv kind_co of
@@ -886,7 +887,6 @@ subst_co subst co
((mkForAllCo $! tv') visL visR $! kind_co') $! subst_co subst' co
go (FunCo r afl afr w co1 co2) = ((mkFunCo2 r afl afr $! go w) $! go co1) $! go co2
go (CoVarCo cv) = substCoVar subst cv
- go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
go (UnivCo { uco_prov = p, uco_role = r
, uco_lty = t1, uco_rty = t2, uco_deps = deps })
= ((((mkUnivCo $! p) $! go_cos deps) $! r) $!
@@ -898,8 +898,6 @@ subst_co subst co
go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
go (KindCo co) = mkKindCo $! (go co)
go (SubCo co) = mkSubCo $! (go co)
- go (AxiomRuleCo c cs) = let cs1 = map go cs
- in cs1 `seqList` AxiomRuleCo c cs1
go (HoleCo h) = HoleCo $! go_hole h
go_cos cos = let cos' = map go cos
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -342,8 +342,8 @@ 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 (AxiomInstCo con ind cos) = AxiomInstCo con ind $! strictMap go cos
- go co@(UnivCo { uco_lty = t1, uco_rty = t2 })
+ go (AxiomRuleCo ax cos) = AxiomRuleCo 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
go (SymCo co) = SymCo $! go co
@@ -353,7 +353,6 @@ tidyCo env co
go (InstCo co ty) = (InstCo $! go co) $! go ty
go (KindCo co) = KindCo $! go co
go (SubCo co) = SubCo $! go co
- go (AxiomRuleCo ax cos) = AxiomRuleCo ax $ strictMap go cos
go_cv cv = tidyTyCoVarOcc env cv
=====================================
compiler/GHC/Core/TyCon.hs-boot
=====================================
@@ -12,6 +12,7 @@ instance Outputable TyCon
type TyConRepName = Name
+isNewTyCon :: TyCon -> Bool
isTupleTyCon :: TyCon -> Bool
isUnboxedTupleTyCon :: TyCon -> Bool
=====================================
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, mkAxiomInstCo, mkUnivCo
+ , mkForAllCo, mkFunCo2, mkAxiomRuleCo, 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 (AxiomInstCo ax ind args)
- = mkAxiomInstCo ax ind (map (go_co subst) args)
+ go_co subst (AxiomRuleCo ax cs)
+ = mkAxiomRuleCo 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)
@@ -574,8 +574,6 @@ expandTypeSynonyms ty
= mkKindCo (go_co subst co)
go_co subst (SubCo co)
= mkSubCo (go_co subst co)
- go_co subst (AxiomRuleCo ax cs)
- = AxiomRuleCo ax (map (go_co subst) cs)
go_co _ (HoleCo h)
= pprPanic "expandTypeSynonyms hit a hole" (ppr h)
@@ -976,13 +974,12 @@ 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) = AxiomRuleCo r <$> go_cos env cos
+ go_co !env (AxiomRuleCo r cos) = mkAxiomRuleCo 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
go_co !env (KindCo co) = mkKindCo <$> go_co env co
go_co !env (SubCo co) = mkSubCo <$> go_co env co
- go_co !env (AxiomInstCo ax i cos) = mkAxiomInstCo ax i <$> go_cos env cos
go_co !env co@(TyConAppCo r tc cos)
| isTcTyCon tc
= do { tc' <- tycon tc
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -296,8 +296,7 @@ toIfaceCoercionX fr 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 (mkIfLclName (coaxrName co)) (map go cs)
- go (AxiomInstCo c i cs) = IfaceAxiomInstCo (coAxiomName c) i (map go cs)
+ go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (toIfaceAxiomRule co) (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)
@@ -317,6 +316,12 @@ toIfaceCoercionX fr co
where
fr' = fr `delVarSet` tv
+toIfaceAxiomRule :: CoAxiomRule -> IfaceAxiomRule
+toIfaceAxiomRule (BuiltInFamRewrite bif) = IfaceAR_X (mkIfLclName (bifrw_name bif))
+toIfaceAxiomRule (BuiltInFamInteract bif) = IfaceAR_X (mkIfLclName (bifint_name bif))
+toIfaceAxiomRule (BranchedAxiom ax i) = IfaceAR_B (coAxiomName ax) i
+toIfaceAxiomRule (UnbranchedAxiom ax) = IfaceAR_U (coAxiomName ax)
+
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -661,39 +661,29 @@ rnIfaceMCo IfaceMRefl = pure IfaceMRefl
rnIfaceMCo (IfaceMCo co) = IfaceMCo <$> rnIfaceCo co
rnIfaceCo :: Rename IfaceCoercion
-rnIfaceCo (IfaceReflCo ty) = IfaceReflCo <$> rnIfaceType ty
-rnIfaceCo (IfaceGReflCo role ty mco)
- = IfaceGReflCo role <$> rnIfaceType ty <*> rnIfaceMCo mco
-rnIfaceCo (IfaceFunCo role w co1 co2)
- = IfaceFunCo role <$> rnIfaceCo w <*> rnIfaceCo co1 <*> rnIfaceCo co2
-rnIfaceCo (IfaceTyConAppCo role tc cos)
- = IfaceTyConAppCo role <$> rnIfaceTyCon tc <*> mapM rnIfaceCo cos
-rnIfaceCo (IfaceAppCo co1 co2)
- = IfaceAppCo <$> rnIfaceCo co1 <*> rnIfaceCo co2
+rnIfaceCo (IfaceReflCo ty) = IfaceReflCo <$> rnIfaceType ty
+rnIfaceCo (IfaceGReflCo role ty mco) = IfaceGReflCo role <$> rnIfaceType ty <*> rnIfaceMCo mco
+rnIfaceCo (IfaceFunCo role w co1 co2) = IfaceFunCo role <$> rnIfaceCo w <*> rnIfaceCo co1 <*> rnIfaceCo co2
+rnIfaceCo (IfaceTyConAppCo role tc cos) = IfaceTyConAppCo role <$> rnIfaceTyCon tc <*> mapM rnIfaceCo cos
+rnIfaceCo (IfaceAppCo co1 co2) = IfaceAppCo <$> rnIfaceCo co1 <*> rnIfaceCo co2
+rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c)
+rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
+rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl
+rnIfaceCo (IfaceSymCo c) = IfaceSymCo <$> rnIfaceCo c
+rnIfaceCo (IfaceTransCo c1 c2) = IfaceTransCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
+rnIfaceCo (IfaceInstCo c1 c2) = IfaceInstCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
+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 (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 (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c)
-rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
-rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl
-rnIfaceCo (IfaceAxiomInstCo n i cs)
- = IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs
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
-rnIfaceCo (IfaceSymCo c)
- = IfaceSymCo <$> rnIfaceCo c
-rnIfaceCo (IfaceTransCo c1 c2)
- = IfaceTransCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
-rnIfaceCo (IfaceInstCo c1 c2)
- = IfaceInstCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
-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 (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
rnIfaceTyCon :: Rename IfaceTyCon
rnIfaceTyCon (IfaceTyCon n info)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1781,8 +1781,6 @@ freeNamesIfCoercion (IfaceForAllCo _tcv _visL _visR kind_co co)
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
-freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
- = unitNameSet ax &&& fnList freeNamesIfCoercion cos
freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2 _)
= freeNamesIfType t1 &&& freeNamesIfType t2
-- Ignoring uco_deps field, which are all local,
@@ -1801,9 +1799,13 @@ freeNamesIfCoercion (IfaceKindCo c)
= freeNamesIfCoercion c
freeNamesIfCoercion (IfaceSubCo co)
= freeNamesIfCoercion co
-freeNamesIfCoercion (IfaceAxiomRuleCo _ax cos)
- -- the axiom is just a string, so we don't count it as a name.
- = fnList freeNamesIfCoercion cos
+freeNamesIfCoercion (IfaceAxiomRuleCo ax cos)
+ = fnAxRule ax &&& fnList freeNamesIfCoercion cos
+
+fnAxRule :: IfaceAxiomRule -> NameSet
+fnAxRule (IfaceAR_X _) = emptyNameSet -- the axiom is just a string, so we don't count it as a name.
+fnAxRule (IfaceAR_U n) = unitNameSet n
+fnAxRule (IfaceAR_B n _) = unitNameSet n
freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -14,7 +14,7 @@ module GHC.Iface.Type (
IfLclName(..), mkIfLclName, ifLclNameFS,
IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
- IfaceMCoercion(..),
+ IfaceAxiomRule(..),IfaceMCoercion(..),
IfaceMult,
IfaceTyCon(..),
IfaceTyConInfo(..), mkIfaceTyConInfo,
@@ -476,8 +476,7 @@ data IfaceCoercion
| IfaceAppCo IfaceCoercion IfaceCoercion
| IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceCoercion IfaceCoercion
| IfaceCoVarCo IfLclName
- | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
- | IfaceAxiomRuleCo IfLclName [IfaceCoercion]
+ | IfaceAxiomRuleCo 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
@@ -494,6 +493,12 @@ data IfaceCoercion
deriving (Eq, Ord)
-- Why Ord? See Note [Ord instance of IfaceType]
+data IfaceAxiomRule
+ = IfaceAR_X IfLclName -- Built-in
+ | IfaceAR_B IfExtName BranchIndex -- Branched
+ | IfaceAR_U IfExtName -- Unbranched
+ deriving (Eq, Ord)
+
{- Note [Holes in IfaceCoercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When typechecking fails the typechecker will produce a HoleCo to stand
@@ -698,7 +703,6 @@ substIfaceType env ty
go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar cv
go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv
go_co (IfaceHoleCo cv) = IfaceHoleCo cv
- go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
go_co (IfaceUnivCo p r t1 t2 ds) = IfaceUnivCo p r (go t1) (go t2) (go_cos ds)
go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
go_co (IfaceTransCo co1 co2) = IfaceTransCo (go_co co1) (go_co co2)
@@ -2009,11 +2013,8 @@ ppr_co ctxt_prec (IfaceInstCo co ty)
text "Inst" <+> sep [ pprParendIfaceCoercion co
, pprParendIfaceCoercion ty ]
-ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
- = maybeParen ctxt_prec appPrec $ ppr tc <+> parens (interpp'SP cos)
-
-ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
- = ppr_special_co ctxt_prec (ppr n <> brackets (ppr i)) cos
+ppr_co ctxt_prec (IfaceAxiomRuleCo ax cos)
+ = ppr_special_co ctxt_prec (pprIfAxRule ax) cos
ppr_co ctxt_prec (IfaceSymCo co)
= ppr_special_co ctxt_prec (text "Sym") [co]
ppr_co ctxt_prec (IfaceTransCo co1 co2)
@@ -2036,6 +2037,11 @@ ppr_special_co ctxt_prec doc cos
= maybeParen ctxt_prec appPrec
(sep [doc, nest 4 (sep (map pprParendIfaceCoercion cos))])
+pprIfAxRule :: IfaceAxiomRule -> SDoc
+pprIfAxRule (IfaceAR_X n) = ppr n
+pprIfAxRule (IfaceAR_U n) = ppr n
+pprIfAxRule (IfaceAR_B n i) = ppr n <> brackets (int i)
+
ppr_role :: Role -> SDoc
ppr_role r = underscore <> pp_role
where pp_role = case r of
@@ -2361,11 +2367,6 @@ instance Binary IfaceCoercion where
put_ bh (IfaceCoVarCo a) = do
putByte bh 7
put_ bh a
- put_ bh (IfaceAxiomInstCo a b c) = do
- putByte bh 8
- put_ bh a
- put_ bh b
- put_ bh c
put_ bh (IfaceUnivCo a b c d deps) = do
putByte bh 9
put_ bh a
@@ -2438,10 +2439,6 @@ instance Binary IfaceCoercion where
return $ IfaceForAllCo a visL visR b c
7 -> do a <- get bh
return $ IfaceCoVarCo a
- 8 -> do a <- get bh
- b <- get bh
- c <- get bh
- return $ IfaceAxiomInstCo a b c
9 -> do a <- get bh
b <- get bh
c <- get bh
@@ -2471,6 +2468,17 @@ instance Binary IfaceCoercion where
return $ IfaceAxiomRuleCo a b
_ -> panic ("get IfaceCoercion " ++ show tag)
+instance Binary IfaceAxiomRule where
+ put_ bh (IfaceAR_X n) = putByte bh 0 >> put_ bh n
+ put_ bh (IfaceAR_U n) = putByte bh 1 >> put_ bh n
+ put_ bh (IfaceAR_B n i) = putByte bh 1 >> put_ bh n >> put_ bh i
+
+ get bh = do h <- getByte bh
+ case h of
+ 0 -> do { n <- get bh; return (IfaceAR_X n) }
+ 1 -> do { n <- get bh; return (IfaceAR_U n) }
+ _ -> do { n <- get bh; i <- get bh; return (IfaceAR_B n i) }
+
instance Binary (DefMethSpec IfaceType) where
put_ bh VanillaDM = putByte bh 0
put_ bh (GenericDM t) = putByte bh 1 >> put_ bh t
@@ -2508,7 +2516,6 @@ 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
- IfaceAxiomInstCo f1 f2 f3 -> rnf f1 `seq` rnf f2 `seq` rnf f3
IfaceAxiomRuleCo 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
@@ -2521,6 +2528,12 @@ instance NFData IfaceCoercion where
IfaceFreeCoVar f1 -> f1 `seq` ()
IfaceHoleCo f1 -> f1 `seq` ()
+instance NFData IfaceAxiomRule where
+ rnf = \case
+ IfaceAR_X n -> rnf n
+ IfaceAR_U n -> rnf n
+ IfaceAR_B n i -> rnf n `seq` rnf i
+
instance NFData IfaceMCoercion where
rnf x = seq x ()
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -707,11 +707,10 @@ tc_iface_decl _ _ (IfaceData {ifName = tc_name,
= do { tc_rep_name <- newTyConRepName tc_name
; return (VanillaAlgTyCon tc_rep_name) }
tc_parent _ (IfDataInstance ax_name _ arg_tys)
- = do { ax <- tcIfaceCoAxiom ax_name
+ = do { ax <- tcIfaceUnbranchedAxiom ax_name
; let fam_tc = coAxiomTyCon ax
- ax_unbr = toUnbranchedAxiom ax
; lhs_tys <- tcIfaceAppArgs arg_tys
- ; return (DataFamInstTyCon ax_unbr fam_tc lhs_tys) }
+ ; return (DataFamInstTyCon ax fam_tc lhs_tys) }
tc_iface_decl _ _ (IfaceSynonym {ifName = tc_name,
ifRoles = roles,
@@ -748,7 +747,7 @@ tc_iface_decl parent _ (IfaceFamily {ifName = tc_name,
; return (DataFamilyTyCon tc_rep_name) }
tc_fam_flav _ IfaceOpenSynFamilyTyCon= return OpenSynFamilyTyCon
tc_fam_flav _ (IfaceClosedSynFamilyTyCon mb_ax_name_branches)
- = do { ax <- traverse (tcIfaceCoAxiom . fst) mb_ax_name_branches
+ = do { ax <- traverse (tcIfaceBranchedAxiom . fst) mb_ax_name_branches
; return (ClosedSynFamilyTyCon ax) }
tc_fam_flav _ IfaceAbstractClosedSynFamilyTyCon
= return AbstractClosedSynFamilyTyCon
@@ -1244,11 +1243,10 @@ tcIfaceFamInst (IfaceFamInst { ifFamInstFam = fam, ifFamInstTys = mb_tcs
, ifFamInstAxiom = axiom_name
, ifFamInstOrph = orphan } )
= do { axiom' <- forkM (text "Axiom" <+> ppr axiom_name) $
- tcIfaceCoAxiom axiom_name
+ tcIfaceUnbranchedAxiom axiom_name
-- will panic if branched, but that's OK
- ; let axiom'' = toUnbranchedAxiom axiom'
- mb_tcs' = map tcRoughTyCon mb_tcs
- ; return (mkImportedFamInst fam mb_tcs' axiom'' orphan) }
+ ; let mb_tcs' = map tcRoughTyCon mb_tcs
+ ; return (mkImportedFamInst fam mb_tcs' axiom' orphan) }
{-
************************************************************************
@@ -1472,7 +1470,6 @@ tcIfaceCo = go
; bindIfaceBndr tv $ \ tv' ->
ForAllCo tv' visL visR k' <$> go c }
go (IfaceCoVarCo n) = CoVarCo <$> go_var n
- go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs
go (IfaceUnivCo p r t1 t2 ds) = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2
; ds' <- mapM go ds
; return (UnivCo { uco_prov = p, uco_role = r
@@ -2023,21 +2020,28 @@ tcIfaceTyCon (IfaceTyCon name _info)
AConLike (RealDataCon dc) -> return (promoteDataCon dc)
_ -> pprPanic "tcIfaceTyCon" (ppr thing) }
-tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
-tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
- ; return (tyThingCoAxiom thing) }
-
-
-tcIfaceCoAxiomRule :: IfLclName -> IfL CoAxiomRule
+tcIfaceCoAxiomRule :: 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 n
- | Just ax <- lookupUFM typeNatCoAxiomRules (ifLclNameFS n)
- = return ax
+tcIfaceCoAxiomRule (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) }
+
+tcIfaceUnbranchedAxiom :: IfExtName -> IfL (CoAxiom Unbranched)
+tcIfaceUnbranchedAxiom name
+ = do { thing <- tcIfaceImplicit name
+ ; return (toUnbranchedAxiom (tyThingCoAxiom thing)) }
+
+tcIfaceBranchedAxiom :: IfExtName -> IfL (CoAxiom Branched)
+tcIfaceBranchedAxiom name
+ = do { thing <- tcIfaceImplicit name
+ ; return (tyThingCoAxiom thing) }
tcIfaceDataCon :: Name -> IfL DataCon
tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
=====================================
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 (AxiomInstCo _ _ cs) = go_co_s cs
+ go_co (AxiomRuleCo _ 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
@@ -152,7 +152,6 @@ synonymTyConsOfType ty
go_co (InstCo co co') = go_co co `plusNameEnv` go_co co'
go_co (KindCo co) = go_co co
go_co (SubCo co) = go_co co
- go_co (AxiomRuleCo _ cs) = go_co_s cs
go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
| otherwise = emptyNameEnv
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1563,7 +1563,6 @@ 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 (AxiomInstCo _ _ cos) = foldlM go_co dv cos
go_co dv (AxiomRuleCo _ 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
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/03beee7128a77a43f9de4ad9b2ec64bf4e5d4c39
--
This project does not include diff previews in email notifications.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/03beee7128a77a43f9de4ad9b2ec64bf4e5d4c39
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/20240705/9b09a6f1/attachment-0001.html>
More information about the ghc-commits
mailing list