[Git][ghc/ghc][wip/zap-coercions] Coercion zapping
Ben Gamari
gitlab at gitlab.haskell.org
Fri Mar 27 15:21:40 UTC 2020
Ben Gamari pushed to branch wip/zap-coercions at Glasgow Haskell Compiler / GHC
Commits:
81578d45 by Ben Gamari at 2020-03-27T11:21:28-04:00
Coercion zapping
- - - - -
27 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/SimpleOpt.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/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Iface/Env.hs
- compiler/GHC/Iface/Load.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/basicTypes/IdInfo.hs
- compiler/basicTypes/IdInfo.hs-boot
- compiler/basicTypes/Var.hs
- compiler/basicTypes/VarSet.hs
- compiler/typecheck/TcFlatten.hs
- compiler/typecheck/TcMType.hs
- compiler/typecheck/TcTyDecls.hs
- testsuite/tests/profiling/should_run/T2552.prof.sample
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -41,6 +41,9 @@ module GHC.Core.Coercion (
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo, castCoercionKind, castCoercionKindI,
+ --
+ -- ** Zapping coercions
+ mkZappedCoercion, zapCoercion,
mkHeteroCoercionType,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
@@ -136,9 +139,10 @@ import Var
import VarEnv
import VarSet
import Name hiding ( varName )
-import Util
+import Util hiding ( seqList )
import BasicTypes
import Outputable
+import GHC.Driver.Session ( DynFlags, shouldBuildCoercions )
import Unique
import Pair
import SrcLoc
@@ -963,6 +967,9 @@ mkSymCo :: Coercion -> Coercion
mkSymCo co | isReflCo co = co
mkSymCo (SymCo co) = co
mkSymCo (SubCo (SymCo co)) = SubCo co
+mkSymCo (UnivCo (ZappedProv fvs) r t1 t2) = UnivCo (ZappedProv fvs) r t2 t1
+mkSymCo (UnivCo (TcZappedProv fvs coholes) r t1 t2) = UnivCo (TcZappedProv fvs coholes) r t2 t1
+-- TODO: Handle other provenances
mkSymCo co = SymCo co
-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
@@ -972,6 +979,14 @@ mkTransCo co1 co2 | isReflCo co1 = co2
| isReflCo co2 = co1
mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
= GRefl r t1 (MCo $ mkTransCo co1 co2)
+mkTransCo (UnivCo (ZappedProv fvs1) r t1a _t1b) (UnivCo (ZappedProv fvs2) _ _t2a t2b)
+ = UnivCo (ZappedProv (fvs1 `unionDVarSet` fvs2)) r t1a t2b
+mkTransCo (UnivCo (ZappedProv fvs) r t1a _t1b) co2
+ = UnivCo (ZappedProv (fvs `unionDVarSet` tyCoVarsOfCoDSet co2)) r t1a t2b
+ where Pair _t2a t2b = coercionKind co2
+mkTransCo co1 (UnivCo (ZappedProv fvs) r _t2a t2b)
+ = UnivCo (ZappedProv (fvs `unionDVarSet` tyCoVarsOfCoDSet co1)) r t1a t2b
+ where Pair t1a _t1b = coercionKind co1
mkTransCo co1 co2 = TransCo co1 co2
-- | Compose two MCoercions via transitivity
@@ -1108,6 +1123,14 @@ nthCoRole n co
r = coercionRole co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
+mkLRCo lr (UnivCo (ZappedProv fvs) r t1 t2)
+ = UnivCo (ZappedProv fvs) r
+ (pickLR lr (splitAppTy t1))
+ (pickLR lr (splitAppTy t2))
+mkLRCo lr (UnivCo (TcZappedProv fvs coholes) r t1 t2)
+ = UnivCo (TcZappedProv fvs coholes) r
+ (pickLR lr (splitAppTy t1))
+ (pickLR lr (splitAppTy t2))
mkLRCo lr co
| Just (ty, eq) <- isReflCo_maybe co
= mkReflCo eq (pickLR lr (splitAppTy ty))
@@ -1146,9 +1169,6 @@ mkGReflLeftCo r ty co
-- is a GRefl coercion.
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceLeftCo r ty co co2
- | debugIsOn
- , Pair ty' _ <- coercionKind co2
- , not $ ty `eqType` ty' = pprPanic "mkCoherenceLeftCo" (ppr ty $$ ppr co $$ ppr co2)
| isGReflCo co = co2
| otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
@@ -1158,9 +1178,6 @@ mkCoherenceLeftCo r ty co co2
-- is a GRefl coercion.
mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceRightCo r ty co co2
- | debugIsOn
- , Pair _ ty' <- coercionKind co2
- , not $ ty `eqType` ty' = pprPanic "mkCoherenceLeftCo" (ppr ty $$ ppr co $$ ppr co2)
| isGReflCo co = co2
| otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
@@ -1170,6 +1187,8 @@ mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
mkKindCo (GRefl _ _ (MCo co)) = co
mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
+mkKindCo (UnivCo (ZappedProv fvs) _ ty1 ty2) = mkUnivCo (ZappedProv fvs) Nominal (typeKind ty1) (typeKind ty2)
+mkKindCo (UnivCo (TcZappedProv fvs coholes) _ ty1 ty2) = mkUnivCo (TcZappedProv fvs coholes) Nominal (typeKind ty1) (typeKind ty2)
mkKindCo co
| Pair ty1 ty2 <- coercionKind co
-- generally, calling coercionKind during coercion creation is a bad idea,
@@ -1193,6 +1212,9 @@ mkSubCo (FunCo Nominal arg res)
= FunCo Representational
(downgradeRole Representational Nominal arg)
(downgradeRole Representational Nominal res)
+mkSubCo (UnivCo (ZappedProv fvs) Nominal t1 t2) = UnivCo (ZappedProv fvs) Representational t1 t2
+mkSubCo (UnivCo (TcZappedProv fvs coholes) Nominal t1 t2) = UnivCo (TcZappedProv fvs coholes) Representational t1 t2
+mkSubCo co@(SubCo _) = co
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
SubCo co
@@ -1285,6 +1307,8 @@ setNominalRole_maybe r co
| case prov of PhantomProv _ -> False -- should always be phantom
ProofIrrelProv _ -> True -- it's always safe
PluginProv _ -> False -- who knows? This choice is conservative.
+ ZappedProv _ -> False -- conservatively say no
+ TcZappedProv _ _ -> False -- conservatively say no
= Just $ UnivCo prov Nominal co1 co2
setNominalRole_maybe_helper _ = Nothing
@@ -1391,6 +1415,8 @@ promoteCoercion co = case co of
UnivCo (PhantomProv kco) _ _ _ -> kco
UnivCo (ProofIrrelProv kco) _ _ _ -> kco
UnivCo (PluginProv _) _ _ _ -> mkKindCo co
+ UnivCo (ZappedProv _) _ _ _ -> mkKindCo co
+ UnivCo (TcZappedProv _ _) _ _ _ -> mkKindCo co
SymCo g
-> mkSymCo (promoteCoercion g)
@@ -1535,6 +1561,232 @@ mkCoCast c g
(tc, _) = splitTyConApp (coercionLKind g)
co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
+{-
+%************************************************************************
+%* *
+ Zapping coercions into oblivion
+%* *
+%************************************************************************
+-}
+
+{- Note [Zapping coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Coercions for even small programs can grow to be quite large (e.g. #8095),
+especially when type families are involved. For instance, the case of addition
+of inductive natural numbers can build coercions quadratic in size of the
+summands. For instance, consider the type-level addition operation defined on
+Peano naturals,
+
+ data Nat = Z | Succ Nat
+
+ type family (+) (a :: Nat) (b :: Nat)
+ type instance (+) Z a = a -- CoAx1
+ type instance (+) (Succ a) b = Succ (a + b) -- CoAx2
+
+Now consider what is necessary to reduce (S (S (S Z)) + S Z). This
+reduction will produce two results: the reduced (i.e. flattened) type, and a
+coercion witnessing the reduction. The reduction will proceed as follows:
+
+ S (S (S Z)) + S Z |> Refl
+ ~> S (S (S Z) + S Z) |> CoAx2 Refl
+ ~> S (S (S Z + S Z)) |> CoAx2 (CoAx2 Refl)
+ ~> S (S (S (Z + S Z))) |> CoAx2 (CoAx2 (CoAx2 Refl))
+ ~> S (S (S (S (S Z)))) |> CoAx1 (CoAx2 (CoAx2 (CoAx2 Refl)))
+
+Note that when we are building coercions [TODO]
+
+Moreover, coercions are really only useful when validating core transformations
+(i.e. by the Core Linter). To avoid burdening users who aren't linting with the
+cost of maintaining these structures, we replace coercions with placeholders
+("zap" them) them unless -dcore-lint is enabled. These placeholders are
+represented by UnivCo with ZappedProv provenance. Concretely, a coercion
+
+ co :: t1 ~r t2
+
+is replaced by
+
+ UnivCo (ZappedProv fvs) r t1 t2
+
+To ensure that such coercions aren't floated out of the scope of proofs they
+require, the ZappedProv constructor includes the coercion's set of free type
+and coercion variables (as a DVarSet, since these sets are included in
+interface files).
+
+
+Zapping during type family reduction
+------------------------------------
+
+To avoid the quadratic blow-up in coercion size during type family reduction
+described above, we zap on every type family reduction step taken by
+TcFlatten.flatten_exact_fam_app_fully. When zapping we take care to avoid
+looking at the constructed coercion and instead build up a zapped coercion
+directly from type being reduced, its free variables, and the result of the
+reduction. This allows us to reduce recursive type families in time linear to
+the size of the type at the expense of Core Lint's ability to validate the
+reduction.
+
+Note that the free variable set of the zapped coercion is taken to be the free
+variable set of the unreduced family application, which is computed once at the
+beginning of reduction. This is an important optimisation as it allows us to
+avoid recomputing the free variable set (which requires linear work in the size
+of the coercion) with every reduction step. Moreover, this gives us the same
+result as naively computing the free variables of every reduction:
+
+ * The FV set of the unreduced type cannot be smaller than that of the reduced type
+ because there is nowhere for extra FVs to come from. Type family equations
+ are essentially function reduction, which can never introduce new fvs.
+
+ * The FV set of the unreducecd type cannot be larger than that of the reduced
+ type because the zapped coercion's kind must mention the types these fvs come
+ from, so the FVs of the zapped coercion must be at least those in the
+ starting types.
+
+Thus, the two sets are subsets of each other and are equal.
+
+
+Other places where we zap
+-------------------------
+
+Besides during type family reduction, we also zap coercions in a number of other
+places (again, only when DynFlags.shouldBuildCoercions is False). This zapping
+occurs in zapCoercion, which maps a coercion to its zapped form. However, there
+are a few optimisations which we implement:
+
+ * We don't zap coercions which are already zapping; this avoids an unnecessary
+ free variable computation.
+
+ * We don't zap Refl coercions. This is because Refls are actually far more
+ compact than zapped coercions: the coercion (Refl T) holds only one
+ reference to T, whereas its zapped equivalent would hold two. While this
+ makes little difference directly after construction due to sharing, this
+ sharing will be lost when we substitute or otherwise manipulate the zapped
+ coercion, resulting in a doubling of the coercions representation size.
+
+zapCoercion is called in a few places:
+
+ * CoreOpt.pushCoTyArg zaps the coercions it produces to avoid pile-up during
+ simplification [TODO]
+
+ * TcIface.tcIfaceCo
+
+ * Type.mapCoercion (which is used by zonking) can optionally zap coercions,
+ although this is currently disabled since it causes compiler allocations to
+ regress in a few cases.
+
+ * We considered zapping as well in optCoercion, although this too caused
+ significant allocation regressions.
+
+The importance of tracking free coercion variables
+--------------------------------------------------
+
+It is quite important that zapped coercions track their free coercion variables.
+To see why, consider this program:
+
+ data T a where
+ T1 :: Bool -> T Bool
+ T2 :: T Int
+
+ f :: T a -> a -> Bool
+ f = /\a (x:T a) (y:a).
+ case x of
+ T1 (c : a~Bool) (z : Bool) -> not (y |> c)
+ T2 -> True
+
+Now imagine that we zap the coercion `c`, replacing it with a generic UnivCo
+between `a` and Bool. If we didn't record the fact that this coercion was
+previously free in `c`, we may incorrectly float the expression `not (y |> c)`
+out of the case alternative which brings proof of `c` into scope. If this
+happened then `f T2 (I# 5)` would try to interpret `y` as a Bool, at
+which point we aren't far from a segmentation fault or much worse.
+
+Note that we don't need to track the coercion's free *type* variables. This
+means that we may float past type variables which the original proof had as free
+variables. While surprising, this doesn't jeopardise the validity of the
+coercion, which only depends upon the scoping relative to the free coercion
+variables.
+
+
+Differences between zapped and unzapped coercions
+-------------------------------------------------
+
+Alas, sometimes zapped coercions will behave slightly differently from their
+unzapped counterparts. Specifically, we are a bit lax in tracking external names
+that are present in the unzapped coercion but not its kind. This manifests in a
+few places (these are labelled in the source with the [ZappedCoDifference]
+keyword):
+
+ * IfaceSyn.freeNamesIfCoercion will fail to report top-level names present in
+ the unzapped proof but not its kind.
+
+ * TcTyDecls.synonymTyConsOfType will fail to report type synonyms present in
+ in the unzapped proof but not its kind.
+
+ * The result of TcValidity.fvCo will contain each free variable of a ZappedCo
+ only once, even if it would have reported multiple occurrences in the
+ unzapped coercion.
+
+ * Type.tyConsOfType does not report TyCons which appear only in the unzapped
+ proof and not its kind.
+
+ * Zapped coercions are represented in interface files as IfaceZappedProv. This
+ representation only includes local free variables, since these are sufficient
+ to avoid unsound floating. This means that the free variable lists of zapped
+ coercions loaded from interface files will lack top-level things (e.g. type
+ constructors) that appear only in the unzapped proof.
+
+-}
+
+-- | Make a zapped coercion if building of coercions is disabled, otherwise
+-- return the given un-zapped coercion.
+mkZappedCoercion :: HasDebugCallStack
+ => DynFlags
+ -> Coercion -- ^ the un-zapped coercion
+ -> Pair Type -- ^ the kind of the coercion
+ -> Role -- ^ the role of the coercion
+ -> DTyCoVarSet -- ^ the free variables of the coercion
+ -> Coercion
+mkZappedCoercion dflags co (Pair ty1 ty2) role fvs
+ | debugIsOn && real_role /= role =
+ pprPanic "mkZappedCoercion(roles mismatch)" panic_doc
+ | debugIsOn && not co_kind_ok =
+ pprPanic "mkZappedCoercion(kind mismatch)" panic_doc
+ | shouldBuildCoercions dflags = co
+ | otherwise =
+ mkUnivCo (ZappedProv fvs) role ty1 ty2
+ where
+ (Pair real_ty1 real_ty2, real_role) = coercionKindRole co
+ real_fvs = tyCoVarsOfCoDSet co
+ -- We must unify here (at the loss of some precision in the assertion)
+ -- since we may encounter flattening skolems.
+ --co_kind_ok = isJust $ tcUnifyTys (const BindMe) [real_ty1, real_ty2] [ty1, ty2]
+ co_kind_ok = True
+ -- N.B. It's not generally possible to check fCvs against the actual
+ -- free variable set since we may encounter flattening skolems during
+ -- reduction.
+ panic_doc = vcat
+ [ text "real role:" <+> ppr real_role
+ , text "given role:" <+> ppr role
+ , text "real ty1:" <+> ppr real_ty1
+ , text "given ty1:" <+> ppr ty1
+ , text "real ty2:" <+> ppr real_ty2
+ , text "given ty2:" <+> ppr ty2
+ , text "real free co vars:" <+> ppr real_fvs
+ , text "given free co vars:" <+> ppr fvs
+ , text "coercion:" <+> ppr co
+ ]
+
+-- | Replace a coercion with a zapped coercion unless coercions are needed.
+zapCoercion :: DynFlags -> Coercion -> Coercion
+zapCoercion _ co@(UnivCo (ZappedProv _) _ _ _) = co -- already zapped
+zapCoercion _ co@(Refl _) = co -- Refl is smaller than zapped coercions
+zapCoercion dflags co =
+ mkZappedCoercion dflags co (Pair t1 t2) role fvs
+ where
+ (Pair t1 t2, role) = coercionKindRole co
+ fvs = filterDVarSet (not . isCoercionHole) $ tyCoVarsOfCoDSet co
+
+
{-
%************************************************************************
%* *
@@ -2147,10 +2399,15 @@ seqProv :: UnivCoProvenance -> ()
seqProv (PhantomProv co) = seqCo co
seqProv (ProofIrrelProv co) = seqCo co
seqProv (PluginProv _) = ()
+seqProv (ZappedProv fvs) = seqDVarSet fvs
+seqProv (TcZappedProv fvs coholes) = seqDVarSet fvs `seq` seqList (\h -> coHoleCoVar h `seq` ()) coholes
+
+seqList :: (a -> ()) -> [a] -> ()
+seqList _ [] = ()
+seqList f (x:xs) = f x `seq` seqList f xs
seqCos :: [Coercion] -> ()
-seqCos [] = ()
-seqCos (co:cos) = seqCo co `seq` seqCos cos
+seqCos = seqList seqCo
{-
%************************************************************************
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -48,6 +48,7 @@ liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
seqCo :: Coercion -> ()
coercionKind :: Coercion -> Pair Type
+coercionKindRole :: Coercion -> (Pair Type, Role)
coercionLKind :: Coercion -> Type
coercionRKind :: Coercion -> Type
coercionType :: Coercion -> Type
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -498,6 +498,22 @@ opt_univ env sym (PhantomProv h) _r ty1 ty2
ty1' = substTy (lcSubstLeft env) ty1
ty2' = substTy (lcSubstRight env) ty2
+opt_univ env sym (ZappedProv fvs) role ty1 ty2
+ | sym = mkUnivCo (ZappedProv fvs') role ty2' ty1'
+ | otherwise = mkUnivCo (ZappedProv fvs') role ty1' ty2'
+ where
+ ty1' = substTy (lcSubstLeft env) ty1
+ ty2' = substTy (lcSubstRight env) ty2
+ fvs' = substFreeDVarSet (lcTCvSubst env) fvs
+
+opt_univ env sym (TcZappedProv fvs coholes) role ty1 ty2
+ | sym = mkUnivCo (TcZappedProv fvs' coholes) role ty2' ty1'
+ | otherwise = mkUnivCo (TcZappedProv fvs' coholes) role ty1' ty2'
+ where
+ ty1' = substTy (lcSubstLeft env) ty1
+ ty2' = substTy (lcSubstRight env) ty2
+ fvs' = substFreeDVarSet (lcTCvSubst env) fvs
+
opt_univ env sym prov role oty1 oty2
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
, Just (tc2, tys2) <- splitTyConApp_maybe oty2
@@ -557,6 +573,9 @@ opt_univ env sym prov role oty1 oty2
PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
PluginProv _ -> prov
+ ZappedProv fvs -> ZappedProv $ substFreeDVarSet (lcTCvSubst env) fvs
+ TcZappedProv fvs coholes
+ -> TcZappedProv (substFreeDVarSet (lcTCvSubst env) fvs) coholes
-------------
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -638,6 +657,11 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
= Just $ ProofIrrelProv $ opt_trans is kco1 kco2
opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
+ opt_trans_prov (ZappedProv fvs1) (ZappedProv fvs2)
+ = Just $ ZappedProv $ fvs1 `unionDVarSet` fvs2
+ opt_trans_prov (TcZappedProv fvs1 coholes1)
+ (TcZappedProv fvs2 coholes2)
+ = Just $ TcZappedProv (fvs1 `unionDVarSet` fvs2) (coholes1 ++ coholes2)
opt_trans_prov _ _ = Nothing
-- Push transitivity down through matching top-level constructors.
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -396,6 +396,10 @@ orphNamesOfProv :: UnivCoProvenance -> NameSet
orphNamesOfProv (PhantomProv co) = orphNamesOfCo co
orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
orphNamesOfProv (PluginProv _) = emptyNameSet
+orphNamesOfProv (ZappedProv _) = emptyNameSet
+orphNamesOfProv (TcZappedProv _ _) = emptyNameSet
+ -- [ZappedCoDifference] Zapped coercions refer to no orphan names, even if the
+ -- original contained such names.
orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1879,6 +1879,11 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
; check_kinds kco k1 k2 }
PluginProv _ -> return () -- no extra checks
+ ZappedProv fvs -> mapM_ lintTyCoVarInScope (dVarSetElems fvs)
+ TcZappedProv fvs coholes
+ -> do { addErrL $ text "Unfilled coercion hole:" <+> ppr coholes
+ ; mapM_ lintTyCoVarInScope (dVarSetElems fvs)
+ }
; when (r /= Phantom && classifiesTypeWithValues k1
&& classifiesTypeWithValues k2)
@@ -2105,7 +2110,6 @@ lintCoercion (HoleCo h)
= do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
; lintCoercion (CoVarCo (coHoleCoVar h)) }
-
----------
lintUnliftedCoVar :: CoVar -> LintM ()
lintUnliftedCoVar cv
=====================================
compiler/GHC/Core/SimpleOpt.hs
=====================================
@@ -1284,13 +1284,15 @@ pushCoTyArg co ty
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
- co1 = mkSymCo (mkNthCo Nominal 0 co)
+ zap = id -- zapCoercion dflags
+
+ co1 = zap $ mkSymCo (mkNthCo Nominal 0 co)
-- co1 :: k2 ~N k1
-- Note that NthCo can extract a Nominal equality between the
-- kinds of the types related by a coercion between forall-types.
-- See the NthCo case in GHC.Core.Lint.
- co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1)
+ co2 = zap $ mkInstCo co (mkGReflLeftCo Nominal ty co1)
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
-- Arg of mkInstCo is always nominal, hence mkNomReflCo
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -645,6 +645,9 @@ tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+tyCoFVsOfProv (ZappedProv fvs) fv_cand in_scope acc = (mkFVs $ dVarSetElems fvs) fv_cand in_scope acc
+tyCoFVsOfProv (TcZappedProv fvs coholes)
+ fv_cand in_scope acc = (mkFVs $ dVarSetElems fvs ++ map coHoleCoVar coholes) fv_cand in_scope acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -714,6 +717,8 @@ almost_devoid_co_var_of_prov (PhantomProv co) cv
almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
= almost_devoid_co_var_of_co co cv
almost_devoid_co_var_of_prov (PluginProv _) _ = True
+almost_devoid_co_var_of_prov (ZappedProv fvs) cv = cv `elemDVarSet` fvs
+almost_devoid_co_var_of_prov (TcZappedProv fvs coholes) cv = cv `elemDVarSet` fvs || cv `elem` map coHoleCoVar coholes
almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type (TyVarTy _) _ = True
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1531,12 +1531,24 @@ data UnivCoProvenance
| PluginProv String -- ^ From a plugin, which asserts that this coercion
-- is sound. The string is for the use of the plugin.
+ | ZappedProv { zappedFreeVars :: DTyCoVarSet }
+ -- ^ See Note [Zapping coercions].
+ -- Free variables must be tracked in 'DVarSet' since they appear in
+ -- interface files. See Note [Deterministic UniqFM] for details.
+
+ | TcZappedProv { zappedFreeVars :: DTyCoVarSet
+ , zappedCoHoles :: [CoercionHole]
+ }
+
deriving Data.Data
instance Outputable UnivCoProvenance where
ppr (PhantomProv _) = text "(phantom)"
ppr (ProofIrrelProv _) = text "(proof irrel.)"
ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
+ ppr (ZappedProv fvs) = parens (text "zapped" <+> brackets (ppr fvs))
+ ppr (TcZappedProv fvs coholes)
+ = parens (text "zapped" <+> brackets (ppr fvs) <+> brackets (ppr coholes))
-- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
data CoercionHole
@@ -1602,12 +1614,15 @@ equality types story] in TysPrim for background on equality constraints.
For unboxed equalities:
- Generate a CoercionHole, a mutable variable just like a unification
- variable
+ variable.
- Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest
- Use the CoercionHole in a Coercion, via HoleCo
- Solve the constraint later
- When solved, fill in the CoercionHole by side effect, instead of
doing the let-binding thing
+ - To ensure that Core Lint can catch when a CoercionHole variable
+ inappropriately persists beyond typechecking we distinguish such
+ variables by giving them the CoercionHoleId IdDetails.
The main reason for all this is that there may be no good place to let-bind
the evidence for unboxed equalities:
@@ -1853,6 +1868,14 @@ foldTyCo (TyCoFolder { tcf_view = view
go_prov env (PhantomProv co) = go_co env co
go_prov env (ProofIrrelProv co) = go_co env co
go_prov _ (PluginProv _) = mempty
+ go_prov env (ZappedProv fvs) = tycovars env fvs
+ go_prov env (TcZappedProv fvs hole) = tycovars env fvs `mappend` foldMap (cohole env) hole
+
+ tycovars env = foldDVarSet f mempty
+ where f v acc
+ | isTyVar v = tyvar env v `mappend` acc
+ | isCoVar v = covar env v `mappend` acc
+ | otherwise = error "unknown thingy"
{- *********************************************************************
* *
@@ -1908,3 +1931,5 @@ provSize :: UnivCoProvenance -> Int
provSize (PhantomProv co) = 1 + coercionSize co
provSize (ProofIrrelProv co) = 1 + coercionSize co
provSize (PluginProv _) = 1
+provSize (ZappedProv _) = 1
+provSize (TcZappedProv _ _) = 1
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -46,6 +46,7 @@ module GHC.Core.TyCo.Subst
substTyVarBndr, substTyVarBndrs,
substCoVarBndr,
substTyVar, substTyVars, substTyCoVars,
+ substFreeDVarSet,
substForAllCoBndr,
substVarBndrUsing, substForAllCoBndrUsing,
checkValidSubst, isValidTCvSubst,
@@ -824,11 +825,22 @@ subst_co subst co
go_prov (PhantomProv kco) = PhantomProv (go kco)
go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
go_prov p@(PluginProv _) = p
+ go_prov (ZappedProv fvs) = ZappedProv (substFreeDVarSet subst fvs)
+ go_prov (TcZappedProv fvs coholes)
+ = TcZappedProv (substFreeDVarSet subst fvs) coholes
-- See Note [Substituting in a coercion hole]
go_hole h@(CoercionHole { ch_co_var = cv })
= h { ch_co_var = updateVarType go_ty cv }
+-- | Perform a substitution within a 'DVarSet' of free variables.
+substFreeDVarSet :: TCvSubst -> DVarSet -> DVarSet
+substFreeDVarSet subst =
+ let f v
+ | isTyVar v = tyCoVarsOfTypeDSet $ substTyVar subst v
+ | otherwise = tyCoVarsOfCoDSet $ substCoVar subst v
+ in mapUnionDVarSet f . dVarSetElems
+
substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
-> (TCvSubst, TyCoVar, Coercion)
substForAllCoBndr subst
@@ -908,14 +920,15 @@ substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv)
substCoVar :: TCvSubst -> CoVar -> Coercion
substCoVar (TCvSubst _ _ cenv) cv
- = case lookupVarEnv cenv cv of
+ = ASSERT( isCoVar cv )
+ case lookupVarEnv cenv cv of
Just co -> co
Nothing -> CoVarCo cv
substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
substCoVars subst cvs = map (substCoVar subst) cvs
-lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
+lookupCoVar :: TCvSubst -> CoVar -> Maybe Coercion
lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -26,9 +26,11 @@ import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
import Name hiding (varName)
import Var
import VarEnv
+import VarSet
import Util (seqList)
import Data.List (mapAccumL)
+import Data.Maybe (fromMaybe)
{-
%************************************************************************
@@ -209,9 +211,7 @@ tidyCo env@(_, subst) co
-- the case above duplicates a bit of work in tidying h and the kind
-- of tv. But the alternative is to use coercionKind, which seems worse.
go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2
- go (CoVarCo cv) = case lookupVarEnv subst cv of
- Nothing -> CoVarCo cv
- Just cv' -> CoVarCo cv'
+ go (CoVarCo cv) = CoVarCo $ substCoVar cv
go (HoleCo h) = HoleCo h
go (AxiomInstCo con ind cos) = let args = map go cos
in args `seqList` AxiomInstCo con ind args
@@ -230,6 +230,12 @@ tidyCo env@(_, subst) co
go_prov (PhantomProv co) = PhantomProv (go co)
go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
go_prov p@(PluginProv _) = p
+ go_prov (ZappedProv fvs) = ZappedProv $ mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs)
+ go_prov (TcZappedProv fvs coholes)
+ = TcZappedProv (mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs))
+ coholes -- Tidying needed?
+
+ substCoVar cv = fromMaybe cv $ lookupVarEnv subst cv
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -474,6 +474,10 @@ expandTypeSynonyms ty
go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
go_prov _ p@(PluginProv _) = p
+ go_prov subst (ZappedProv fvs)
+ = ZappedProv $ substFreeDVarSet subst fvs
+ go_prov subst (TcZappedProv fvs coholes)
+ = TcZappedProv (substFreeDVarSet subst fvs) coholes
-- the "False" and "const" are to accommodate the type of
-- substForAllCoBndrUsing, which is general enough to
@@ -716,7 +720,22 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
go_prov env (PhantomProv co) = PhantomProv <$> go_co env co
go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
go_prov _ p@(PluginProv _) = return p
-
+ go_prov env (ZappedProv fvs)
+ = let bndrFVs v
+ | isCoVar v = tyCoVarsOfCoDSet <$> covar env v
+ | isTyVar v = tyCoVarsOfTypeDSet <$> tyvar env v
+ | otherwise = pprPanic "mapCoercion(ZappedProv): Bad free variable" (ppr v)
+ in do fvs' <- unionDVarSets <$> mapM bndrFVs (dVarSetElems fvs)
+ return $ ZappedProv fvs'
+ go_prov env (TcZappedProv fvs coholes)
+ = let bndrFVs v
+ | isCoVar v = tyCoVarsOfCoDSet <$> covar env v
+ | isTyVar v = tyCoVarsOfTypeDSet <$> tyvar env v
+ | otherwise = pprPanic "mapCoercion(TcZappedProv): Bad free variable" (ppr v)
+ in do fvs' <- unionDVarSets <$> mapM bndrFVs (dVarSetElems fvs)
+ coholes' <- mapM (cohole env) coholes
+ let fvs'' = mapUnionDVarSet tyCoVarsOfCoDSet coholes'
+ return $ ZappedProv $ fvs' `unionDVarSet` fvs''
{-
************************************************************************
@@ -2772,7 +2791,8 @@ occCheckExpand vs_to_avoid ty
go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
go_prov _ p@(PluginProv _) = return p
-
+ go_prov _ p@(ZappedProv _) = return p
+ go_prov _ p@(TcZappedProv{}) = return p
{-
%************************************************************************
@@ -2827,6 +2847,11 @@ tyConsOfType ty
go_prov (PluginProv _) = emptyUniqSet
-- this last case can happen from the tyConsOfType used from
-- checkTauTvUpdate
+ go_prov (ZappedProv _) = emptyUniqSet
+ go_prov (TcZappedProv _ _) = emptyUniqSet
+ -- [ZappedCoDifference] that this will not report TyCons present in the
+ -- unzapped proof but not its kind. See Note [Zapping coercions] in
+ -- TyCoRep.
go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys
go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -304,6 +304,16 @@ toIfaceCoercionX fr co
go_prov (PhantomProv co) = IfacePhantomProv (go co)
go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
go_prov (PluginProv str) = IfacePluginProv str
+ go_prov (ZappedProv fvs) = IfaceZappedProv tvs cvs openVars
+ where
+ (tvs, cvs, openVars) = foldl' f ([], [], []) (dVarSetElems fvs)
+ isOpen = (`elemVarSet` fr)
+ f (a,b,c) v
+ | isOpen v = (a, b, v:c)
+ | isCoVar v = (a, toIfaceCoVar v:b, c)
+ | isTyVar v = (toIfaceTyVar v:a, b, c)
+ | otherwise = panic "ToIface.toIfaceCoercionX(go_prov): Bad free variable in ZappedProv"
+ go_prov (TcZappedProv _ _) = panic "ToIface.toIfaceCoercionX(go_prov): TcZappedProv"
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
=====================================
compiler/GHC/Driver/Flags.hs
=====================================
@@ -120,6 +120,7 @@ data GeneralFlag
| Opt_D_faststring_stats
| Opt_D_dump_minimal_imports
| Opt_DoCoreLinting
+ | Opt_DropCoercions
| Opt_DoStgLinting
| Opt_DoCmmLinting
| Opt_DoAsmLinting
=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -40,6 +40,7 @@ module GHC.Driver.Session (
lang_set,
whenGeneratingDynamicToo, ifGeneratingDynamicToo,
whenCannotGenerateDynamicToo,
+ shouldBuildCoercions,
dynamicTooMkDynamicDynFlags,
dynamicOutputFile,
DynFlags(..),
@@ -1185,6 +1186,14 @@ data RtsOptsEnabled
| RtsOptsAll
deriving (Show)
+-- | Should we generate coercions?
+--
+-- See Note [Zapping coercions] for details.
+shouldBuildCoercions :: DynFlags -> Bool
+shouldBuildCoercions dflags =
+ gopt Opt_DoCoreLinting dflags && not (gopt Opt_DropCoercions dflags)
+ -- TODO: Add flag to explicitly enable coercion generation without linting?
+
-- | Are we building with @-fPIE@ or @-fPIC@ enabled?
positionIndependent :: DynFlags -> Bool
positionIndependent dflags = gopt Opt_PIC dflags || gopt Opt_PIE dflags
@@ -2808,6 +2817,8 @@ dynamic_flags_deps = [
(setDumpFlag Opt_D_dump_rtti)
, make_ord_flag defGhcFlag "dcore-lint"
(NoArg (setGeneralFlag Opt_DoCoreLinting))
+ , make_ord_flag defGhcFlag "ddrop-coercions"
+ (NoArg (setGeneralFlag Opt_DropCoercions))
, make_ord_flag defGhcFlag "dstg-lint"
(NoArg (setGeneralFlag Opt_DoStgLinting))
, make_ord_flag defGhcFlag "dcmm-lint"
=====================================
compiler/GHC/Iface/Env.hs
=====================================
@@ -226,7 +226,7 @@ tcIfaceLclId occ
= do { lcl <- getLclEnv
; case (lookupFsEnv (if_id_env lcl) occ) of
Just ty_var -> return ty_var
- Nothing -> failIfM (text "Iface id out of scope: " <+> ppr occ)
+ Nothing -> failIfM (text "Iface id out of scope: " <+> ppr occ $$ ppr (if_id_env lcl))
}
extendIfaceIdEnv :: [Id] -> IfL a -> IfL a
=====================================
compiler/GHC/Iface/Load.hs
=====================================
@@ -843,7 +843,7 @@ loadDecl ignore_prags (_version, decl)
[(n, lookup n) | n <- implicit_names]
}
where
- doc = text "Declaration for" <+> ppr (ifName decl)
+ doc = text "Declaration for" <+> ppr (ifName decl) $$ ppr decl
bumpDeclStats :: Name -> IfL () -- Record that one more declaration has actually been used
bumpDeclStats name
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1614,6 +1614,9 @@ freeNamesIfProv :: IfaceUnivCoProv -> NameSet
freeNamesIfProv (IfacePhantomProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfacePluginProv _) = emptyNameSet
+freeNamesIfProv (IfaceZappedProv _ _ _) = emptyNameSet
+ -- [ZappedCoDifference]: This won't report top-level names present in the
+ -- unzapped proof but not its kind.
freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -359,6 +359,13 @@ data IfaceUnivCoProv
= IfacePhantomProv IfaceCoercion
| IfaceProofIrrelProv IfaceCoercion
| IfacePluginProv String
+ | IfaceZappedProv [IfLclName] [IfLclName] [Var]
+ -- ^ @local tyvars, local covars, open free variables@
+ --
+ -- Local variables are those bound in the current IfaceType; free variables
+ -- are used only when printing open types and are not serialised; see Note
+ -- [Free tyvars in IfaceType].
+ -- See Note [Zapping coercions] in TyCoRep.
{- Note [Holes in IfaceCoercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -532,6 +539,8 @@ substIfaceType env ty
go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co)
go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
go_prov (IfacePluginProv str) = IfacePluginProv str
+ go_prov (IfaceZappedProv tvs cvs fCvs)
+ = IfaceZappedProv tvs cvs fCvs
substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
substIfaceAppArgs env args
@@ -1606,6 +1615,12 @@ pprIfaceUnivCoProv (IfaceProofIrrelProv co)
= text "irrel" <+> pprParendIfaceCoercion co
pprIfaceUnivCoProv (IfacePluginProv s)
= text "plugin" <+> doubleQuotes (text s)
+pprIfaceUnivCoProv (IfaceZappedProv tvs cvs fCvs)
+ = text "Zapped" <> brackets (whenPprDebug fvsDoc)
+ where
+ fvsDoc = text "free tyvars:" <+> ppr tvs
+ $$ text "free covars:" <+> ppr cvs
+ $$ text "open free covars:" <+> ppr fCvs
-------------------
instance Outputable IfaceTyCon where
@@ -1956,6 +1971,12 @@ instance Binary IfaceUnivCoProv where
put_ bh (IfacePluginProv a) = do
putByte bh 3
put_ bh a
+ put_ bh (IfaceZappedProv tyFvs coFvs _) = do
+ putByte bh 5
+ put_ bh tyFvs
+ put_ bh coFvs
+ -- N.B. Free variables aren't serialised; see Note [Free tyvars in
+ -- IfaceType].
get bh = do
tag <- getByte bh
@@ -1966,6 +1987,11 @@ instance Binary IfaceUnivCoProv where
return $ IfaceProofIrrelProv a
3 -> do a <- get bh
return $ IfacePluginProv a
+ 5 -> do a <- get bh
+ b <- get bh
+ -- N.B. Open free variables aren't serialised; see Note
+ -- [Free tyvars in IfaceType].
+ return $ IfaceZappedProv a b []
_ -> panic ("get IfaceUnivCoProv " ++ show tag)
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1212,7 +1212,12 @@ tcIfaceTyLit (IfaceStrTyLit n) = return (StrTyLit n)
-}
tcIfaceCo :: IfaceCoercion -> IfL Coercion
-tcIfaceCo = go
+tcIfaceCo = \co0 -> do
+ dflags <- getDynFlags
+ co <- go co0
+ if shouldBuildCoercions dflags
+ then return co
+ else return $ zapCoercion dflags co
where
go_mco IfaceMRefl = pure MRefl
go_mco (IfaceMCo co) = MCo <$> (go co)
@@ -1252,6 +1257,10 @@ tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco
tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str
+tcIfaceUnivCoProv (IfaceZappedProv tvs cvs _)
+ = do cvs' <- mapM tcIfaceLclId cvs
+ tvs' <- mapM tcIfaceTyVar tvs
+ return $ ZappedProv $ mkDVarSet $ cvs' ++ tvs'
{-
************************************************************************
=====================================
compiler/basicTypes/IdInfo.hs
=====================================
@@ -15,7 +15,8 @@ Haskell. [WDP 94/11])
module IdInfo (
-- * The IdDetails type
- IdDetails(..), pprIdDetails, coVarDetails, isCoVarDetails,
+ IdDetails(..), pprIdDetails, coVarDetails,
+ isCoVarDetails, isCoercionHoleDetails,
JoinArity, isJoinIdDetails_maybe,
RecSelParent(..),
@@ -164,6 +165,9 @@ data IdDetails
| CoVarId -- ^ A coercion variable
-- This only covers /un-lifted/ coercions, of type
-- (t1 ~# t2) or (t1 ~R# t2), not their lifted variants
+ | CoercionHoleId -- ^ A variable introduced for tracking the scoping of
+ -- a coercion hole during typechecking. See
+ -- Note [Coercion holes] in TyCoRep.
| JoinId JoinArity -- ^ An 'Id' for a join point taking n arguments
-- Note [Join points] in GHC.Core
@@ -189,6 +193,11 @@ isCoVarDetails :: IdDetails -> Bool
isCoVarDetails CoVarId = True
isCoVarDetails _ = False
+-- | Check if an 'IdDetails' says 'CoercionHoleId'.
+isCoercionHoleDetails :: IdDetails -> Bool
+isCoercionHoleDetails CoercionHoleId = True
+isCoercionHoleDetails _ = False
+
isJoinIdDetails_maybe :: IdDetails -> Maybe JoinArity
isJoinIdDetails_maybe (JoinId join_arity) = Just join_arity
isJoinIdDetails_maybe _ = Nothing
@@ -212,6 +221,7 @@ pprIdDetails other = brackets (pp other)
= brackets $ text "RecSel" <>
ppWhen is_naughty (text "(naughty)")
pp CoVarId = text "CoVarId"
+ pp CoercionHoleId = text "CoercionHoleId"
pp (JoinId arity) = text "JoinId" <> parens (int arity)
{-
=====================================
compiler/basicTypes/IdInfo.hs-boot
=====================================
@@ -7,5 +7,6 @@ data IdDetails
vanillaIdInfo :: IdInfo
coVarDetails :: IdDetails
isCoVarDetails :: IdDetails -> Bool
+isCoercionHoleDetails :: IdDetails -> Bool
pprIdDetails :: IdDetails -> SDoc
=====================================
compiler/basicTypes/Var.hs
=====================================
@@ -58,7 +58,7 @@ module Var (
-- ** Predicates
isId, isTyVar, isTcTyVar,
- isLocalVar, isLocalId, isCoVar, isNonCoVarId, isTyCoVar,
+ isLocalVar, isLocalId, isCoVar, isCoercionHole, isNonCoVarId, isTyCoVar,
isGlobalId, isExportedId,
mustHaveLocalBinding,
@@ -94,7 +94,8 @@ import GhcPrelude
import {-# SOURCE #-} GHC.Core.TyCo.Rep( Type, Kind )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr( pprKind )
import {-# SOURCE #-} TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTv )
-import {-# SOURCE #-} IdInfo( IdDetails, IdInfo, coVarDetails, isCoVarDetails,
+import {-# SOURCE #-} IdInfo( IdDetails, IdInfo, coVarDetails,
+ isCoVarDetails, isCoercionHoleDetails,
vanillaIdInfo, pprIdDetails )
import Name hiding (varName)
@@ -728,6 +729,11 @@ isCoVar :: Var -> Bool
isCoVar (Id { id_details = details }) = isCoVarDetails details
isCoVar _ = False
+-- | Is this a CoercionHoleId? See Note [Coercion holes] in TyCoRep.
+isCoercionHole :: Var -> Bool
+isCoercionHole (Id { id_details = details }) = isCoercionHoleDetails details
+isCoercionHole _ = False
+
-- | Is this a term variable ('Id') that is /not/ a coercion variable?
-- Satisfies @'isId' v ==> 'isCoVar' v == not ('isNonCoVarId' v)@.
isNonCoVarId :: Var -> Bool
=====================================
compiler/basicTypes/VarSet.hs
=====================================
@@ -26,7 +26,7 @@ module VarSet (
nonDetFoldVarSet,
-- * Deterministic Var set types
- DVarSet, DIdSet, DTyVarSet, DTyCoVarSet,
+ DVarSet, DIdSet, DTyVarSet, DCoVarSet, DTyCoVarSet,
-- ** Manipulating these sets
emptyDVarSet, unitDVarSet, mkDVarSet,
@@ -229,6 +229,9 @@ type DIdSet = UniqDSet Id
-- | Deterministic Type Variable Set
type DTyVarSet = UniqDSet TyVar
+-- | Deterministic Coercion Variable Set
+type DCoVarSet = UniqDSet CoVar
+
-- | Deterministic Type or Coercion Variable Set
type DTyCoVarSet = UniqDSet TyCoVar
=====================================
compiler/typecheck/TcFlatten.hs
=====================================
@@ -28,10 +28,12 @@ import Var
import VarSet
import VarEnv
import Outputable
+import GHC.Driver.Session ( HasDynFlags(..) )
import TcSMonad as TcS
import BasicTypes( SwapFlag(..) )
import Util
+import Pair
import Bag
import Control.Monad
import MonadUtils ( zipWith3M )
@@ -501,6 +503,9 @@ instance Applicative FlatM where
pure x = FlatM $ const (pure x)
(<*>) = ap
+instance HasDynFlags FlatM where
+ getDynFlags = liftTcS getDynFlags
+
liftTcS :: TcS a -> FlatM a
liftTcS thing_inside
= FlatM $ const thing_inside
@@ -1376,7 +1381,7 @@ flatten_exact_fam_app_fully tc tys
-- See Note [Reduce type family applications eagerly]
-- the following tcTypeKind should never be evaluated, as it's just used in
-- casting, and casts by refl are dropped
- = do { mOut <- try_to_reduce_nocache tc tys
+ = do { mOut <- try_to_reduce_nocache tc tys emptyDVarSet
; case mOut of
Just out -> pure out
Nothing -> do
@@ -1386,6 +1391,7 @@ flatten_exact_fam_app_fully tc tys
-- each arg
flatten_args_tc tc (repeat Nominal) tys
-- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
+ -- cos !! n :: (xis !! n) ~N (tys !! n)
; eq_rel <- getEqRel
; cur_flav <- getFlavour
; let role = eqRelRole eq_rel
@@ -1420,6 +1426,7 @@ flatten_exact_fam_app_fully tc tys
_ -> do { mOut <- try_to_reduce tc
xis
kind_co
+ (tyCoVarsOfCoDSet ret_co)
(`mkTransCo` ret_co)
; case mOut of
Just out -> pure out
@@ -1465,25 +1472,34 @@ flatten_exact_fam_app_fully tc tys
-- where
-- orig_args is what was passed to the outer
-- function
+ -> DTyCoVarSet -- free variables of ret_co
-> ( Coercion -- :: (xi |> kind_co) ~ F args
-> Coercion ) -- what to return from outer function
-> FlatM (Maybe (Xi, Coercion))
- try_to_reduce tc tys kind_co update_co
- = do { checkStackDepth (mkTyConApp tc tys)
+ try_to_reduce tc tys kind_co ret_co_fvs update_co
+ = do { let fvs = tyCoVarsOfTypesDSet tys
+ `unionDVarSet` tyCoVarsOfCoDSet kind_co
+ `unionDVarSet` ret_co_fvs
+ -- See Note [Zapping coercions] in TyCoRep
+ fam_ty = mkTyConApp tc tys
+ ; checkStackDepth (mkTyConApp tc tys)
+ ; dflags <- getDynFlags
; mb_match <- liftTcS $ matchFam tc tys
; case mb_match of
-- NB: norm_co will always be homogeneous. All type families
-- are homogeneous.
- Just (norm_co, norm_ty)
+ Just (norm_co, norm_ty) -- norm_co :: fam_ty ~R norm_ty
-> do { traceFlat "Eager T.F. reduction success" $
vcat [ ppr tc, ppr tys, ppr norm_ty
, ppr norm_co <+> dcolon
<+> ppr (coercionKind norm_co)
]
; (xi, final_co) <- bumpDepth $ flatten_one norm_ty
+ -- final_co :: xi ~ norm_ty
; eq_rel <- getEqRel
; let co = maybeTcSubCo eq_rel norm_co
`mkTransCo` mkSymCo final_co
+ -- co :: fam_ty ~eq_rel xi
; flavour <- getFlavour
-- NB: only extend cache with nominal equalities
; when (eq_rel == NomEq) $
@@ -1491,16 +1507,25 @@ flatten_exact_fam_app_fully tc tys
extendFlatCache tc tys ( co, xi, flavour )
; let role = eqRelRole eq_rel
xi' = xi `mkCastTy` kind_co
- co' = update_co $
- mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
- ; return $ Just (xi', co') }
+ -- See Note [Zapping coercions]
+ co' = mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
+ co'_kind = Pair xi' fam_ty
+ -- co' :: (xi |> kind_co) ~role fam_ty
+ co'' = update_co $ mkZappedCoercion dflags co' co'_kind role fvs
+ --co'' = update_co co'
+ ; return $ Just (xi', co'') }
Nothing -> pure Nothing }
try_to_reduce_nocache :: TyCon -- F, family tycon
-> [Type] -- args, not necessarily flattened
+ -> DTyCoVarSet -- free variables of ret_co
-> FlatM (Maybe (Xi, Coercion))
- try_to_reduce_nocache tc tys
- = do { checkStackDepth (mkTyConApp tc tys)
+ try_to_reduce_nocache tc tys fvs_ret_co
+ = do { let fvs = tyCoVarsOfTypesDSet tys `unionDVarSet` fvs_ret_co
+ -- See Note [Zapping coercions] in TyCoRep
+ fam_ty = mkTyConApp tc tys
+ ; checkStackDepth fam_ty
+ ; dflags <- getDynFlags
; mb_match <- liftTcS $ matchFam tc tys
; case mb_match of
-- NB: norm_co will always be homogeneous. All type families
@@ -1508,9 +1533,12 @@ flatten_exact_fam_app_fully tc tys
Just (norm_co, norm_ty)
-> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty
; eq_rel <- getEqRel
+ ; let role = eqRelRole eq_rel
; let co = mkSymCo (maybeTcSubCo eq_rel norm_co
`mkTransCo` mkSymCo final_co)
- ; return $ Just (xi, co) }
+ co' = mkZappedCoercion dflags co (Pair xi fam_ty) role fvs
+ --co' = co
+ ; return $ Just (xi, co') }
Nothing -> pure Nothing }
{- Note [Reduce type family applications eagerly]
=====================================
compiler/typecheck/TcMType.hs
=====================================
@@ -1383,11 +1383,7 @@ collect_cand_qtvs_co orig_ty bound = go_co
go_co dv (KindCo co) = go_co dv co
go_co dv (SubCo co) = go_co dv co
- go_co dv (HoleCo hole)
- = do m_co <- unpackCoercionHole_maybe hole
- case m_co of
- Just co -> go_co dv co
- Nothing -> go_cv dv (coHoleCoVar hole)
+ go_co dv (HoleCo hole) = go_cohole dv hole
go_co dv (CoVarCo cv) = go_cv dv cv
@@ -1401,6 +1397,10 @@ collect_cand_qtvs_co orig_ty bound = go_co
go_prov dv (PhantomProv co) = go_co dv co
go_prov dv (ProofIrrelProv co) = go_co dv co
go_prov dv (PluginProv _) = return dv
+ go_prov dv (ZappedProv fvs) = foldlM go_cv dv (dVarSetElems fvs)
+ go_prov dv (TcZappedProv fvs coholes)
+ = do dv1 <- foldlM go_cv dv (dVarSetElems fvs)
+ foldlM go_cohole dv1 coholes
go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
go_cv dv@(DV { dv_cvs = cvs }) cv
@@ -1412,6 +1412,14 @@ collect_cand_qtvs_co orig_ty bound = go_co
(dv { dv_cvs = cvs `extendVarSet` cv })
(idType cv)
+ go_cohole :: CandidatesQTvs -> CoercionHole -> TcM CandidatesQTvs
+ go_cohole dv cohole
+ = do { m_co <- unpackCoercionHole_maybe cohole
+ ; case m_co of
+ Just co -> go_co dv co
+ Nothing -> go_cv dv (coHoleCoVar cohole)
+ }
+
is_bound tv = tv `elemVarSet` bound
{- Note [Order of accumulation]
=====================================
compiler/typecheck/TcTyDecls.hs
=====================================
@@ -141,6 +141,10 @@ synonymTyConsOfType ty
go_prov (PhantomProv co) = go_co co
go_prov (ProofIrrelProv co) = go_co co
go_prov (PluginProv _) = emptyNameEnv
+ go_prov (ZappedProv _) = emptyNameEnv
+ go_prov (TcZappedProv _ _) = emptyNameEnv
+ -- [ZappedCoDifference]: This won't report type synonyms present in the
+ -- unzapped proof but not its kind.
go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
| otherwise = emptyNameEnv
=====================================
testsuite/tests/profiling/should_run/T2552.prof.sample
=====================================
@@ -17,7 +17,8 @@ COST CENTRE MODULE SRC no. entr
MAIN MAIN <built-in> 45 0 0.0 0.0 100.0 100.0
CAF Main <entire-module> 89 0 0.0 0.0 100.0 100.0
- main Main T2552.hs:(17,1)-(20,17) 90 1 0.0 0.0 100.0 100.0
+ main Main T2552.hs:12:1-12 90 1 0.0 0.0 100.0 100.0
+ fib3 Main T2552.hs:(1,1)-(5,61) 92 1 0.0 0.0 37.8 33.3
fib1 Main T2552.hs:(1,1)-(5,61) 92 1 0.0 0.0 37.8 33.3
fib1.fib1' Main T2552.hs:(3,5)-(5,61) 93 1 0.0 0.0 37.8 33.3
nfib' Main T2552.hs:3:35-40 94 1 0.0 0.0 37.8 33.3
@@ -25,7 +26,7 @@ MAIN MAIN <built-in> 45
fib2 Main T2552.hs:7:1-16 96 1 0.0 0.0 31.1 33.3
fib2' Main T2552.hs:(8,1)-(10,57) 97 1 0.0 0.0 31.1 33.3
fib2'.nfib Main T2552.hs:10:5-57 98 1028457 31.1 33.3 31.1 33.3
- fib3 Main T2552.hs:12:1-12 99 1 0.0 0.0 0.0 0.0
+ fib3 Main T2552.hs:12:1-12 99 0 0.0 0.0 0.0 0.0
fib3' Main T2552.hs:(13,1)-(15,57) 100 1 0.0 0.0 31.1 33.3
fib3'.nfib Main T2552.hs:15:5-57 101 1028457 31.1 33.3 31.1 33.3
CAF GHC.IO.Handle.FD <entire-module> 84 0 0.0 0.0 0.0 0.0
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/81578d45f7bb2cc84d153c8152a1e8faa9fd53b5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/81578d45f7bb2cc84d153c8152a1e8faa9fd53b5
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/20200327/cb89484c/attachment-0001.html>
More information about the ghc-commits
mailing list