[Git][ghc/ghc][wip/zap-coercions] 2 commits: Rules: Match UnivCos
Ben Gamari
gitlab at gitlab.haskell.org
Fri Mar 27 20:41:16 UTC 2020
Ben Gamari pushed to branch wip/zap-coercions at Glasgow Haskell Compiler / GHC
Commits:
8711a4f8 by Ben Gamari at 2020-03-27T14:45:35-04:00
Rules: Match UnivCos
- - - - -
6a41b6b1 by Ben Gamari at 2020-03-27T16:38:25-04:00
Fix it
- - - - -
12 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Rules.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/Driver/Session.hs
- compiler/GHC/IfaceToCore.hs
- compiler/typecheck/TcFlatten.hs
- compiler/typecheck/TcMType.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -43,7 +43,10 @@ module GHC.Core.Coercion (
mkKindCo, castCoercionKind, castCoercionKindI,
--
-- ** Zapping coercions
- mkZappedCoercion, zapCoercion,
+
+ mkZappedCo, mkTcZappedCo,
+ mkZappedProv, mkTcZappedProv,
+ perhapsZapCoercion, zapCoercion,
mkHeteroCoercionType,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
@@ -62,6 +65,7 @@ module GHC.Core.Coercion (
splitFunCo_maybe,
splitForAllCo_maybe,
splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
+ splitUnivCo_maybe,
nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
@@ -478,6 +482,10 @@ splitForAllCo_co_maybe (ForAllCo cv k_co co)
| isCoVar cv = Just (cv, k_co, co)
splitForAllCo_co_maybe _ = Nothing
+splitUnivCo_maybe :: Coercion -> Maybe (UnivCoProvenance, Role, Pair Type)
+splitUnivCo_maybe (UnivCo prov r t1 t2) = Just (prov, r, Pair t1 t2)
+splitUnivCo_maybe _ = Nothing
+
-------------------------------------------------------
-- and some coercion kind stuff
@@ -980,12 +988,12 @@ mkTransCo co1 co2 | isReflCo co1 = co2
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
+ = UnivCo (mkZappedProv (fvs1 `unionDVarSet` fvs2)) r t1a t2b
mkTransCo (UnivCo (ZappedProv fvs) r t1a _t1b) co2
- = UnivCo (ZappedProv (fvs `unionDVarSet` tyCoVarsOfCoDSet co2)) r t1a t2b
+ = UnivCo (mkZappedProv (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
+ = UnivCo (mkZappedProv (fvs `unionDVarSet` tyCoVarsOfCoDSet co1)) r t1a t2b
where Pair t1a _t1b = coercionKind co1
mkTransCo co1 co2 = TransCo co1 co2
@@ -1737,23 +1745,59 @@ keyword):
-}
+mkZappedProv :: HasDebugCallStack
+ => DTyCoVarSet
+ -> UnivCoProvenance
+mkZappedProv fvs
+ -- | debugIsOn && anyDVarSet isCoercionHole fvs = pprPanic "mkZappedProv(unexpected cohole)" (ppr fvs)
+ | otherwise =
+ ZappedProv $ filterDVarSet (not . isCoercionHole) fvs
+
+mkTcZappedProv :: HasDebugCallStack
+ => DTyCoVarSet
+ -> [CoercionHole]
+ -> UnivCoProvenance
+mkTcZappedProv fvs coholes
+ | debugIsOn && anyDVarSet isCoercionHole fvs =
+ pprPanic "mkTcZappedProv(unexpected cohole)" (ppr fvs)
+ | otherwise =
+ TcZappedProv (filterDVarSet (not . isCoercionHole) fvs) coholes
+
+-- | Smart constructor for 'TcZappedProv' 'UnivCo's.
+mkTcZappedCo :: HasDebugCallStack
+ => Pair Type
+ -> Role
+ -> DTyCoVarSet
+ -> [CoercionHole]
+ -> Coercion
+mkTcZappedCo (Pair ty1 ty2) role fvs coholes
+ = mkUnivCo (mkTcZappedProv fvs coholes) role ty1 ty2
+
+-- | Smart constructor for 'ZappedProv' 'UnivCo's.
+mkZappedCo :: HasDebugCallStack
+ => Pair Type
+ -> Role
+ -> DTyCoVarSet
+ -> Coercion
+mkZappedCo (Pair ty1 ty2) role fvs =
+ mkUnivCo (mkZappedProv fvs) role ty1 ty2
+
-- | 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
+perhapsZapCoercion :: 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
+perhapsZapCoercion dflags co pair@(Pair ty1 ty2) role fvs
| debugIsOn && real_role /= role =
- pprPanic "mkZappedCoercion(roles mismatch)" panic_doc
+ pprPanic "perhapsZapCoercion(roles mismatch)" panic_doc
| debugIsOn && not co_kind_ok =
- pprPanic "mkZappedCoercion(kind mismatch)" panic_doc
+ pprPanic "perhapsZapCoercion(kind mismatch)" panic_doc
| shouldBuildCoercions dflags = co
- | otherwise =
- mkUnivCo (ZappedProv fvs) role ty1 ty2
+ | otherwise = mkZappedCo pair role fvs
where
(Pair real_ty1 real_ty2, real_role) = coercionKindRole co
real_fvs = tyCoVarsOfCoDSet co
@@ -1781,7 +1825,7 @@ 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
+ perhapsZapCoercion dflags co (Pair t1 t2) role fvs
where
(Pair t1 t2, role) = coercionKindRole co
fvs = filterDVarSet (not . isCoercionHole) $ tyCoVarsOfCoDSet co
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -9,7 +9,9 @@ import {-# SOURCE #-} GHC.Core.TyCon
import BasicTypes ( LeftOrRight )
import GHC.Core.Coercion.Axiom
+import GHC.Core.TyCo.Rep (CoercionHole)
import Var
+import VarSet
import Pair
import Util
@@ -41,6 +43,9 @@ decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coer
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
coVarRole :: CoVar -> Role
+mkZappedProv :: HasDebugCallStack => DTyCoVarSet -> UnivCoProvenance
+mkTcZappedProv :: HasDebugCallStack => DTyCoVarSet -> [CoercionHole] -> UnivCoProvenance
+
mkCoercionType :: Role -> Type -> Type -> Type
data LiftingContext
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -499,17 +499,17 @@ opt_univ env sym (PhantomProv h) _r ty1 ty2
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'
+ = mkZappedCo pair role fvs'
where
+ pair = if sym then Pair ty2' ty1' else Pair ty1' ty2'
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'
+ = mkTcZappedCo pair role fvs' coholes
where
+ pair = if sym then Pair ty2' ty1' else Pair ty1' ty2'
ty1' = substTy (lcSubstLeft env) ty1
ty2' = substTy (lcSubstRight env) ty2
fvs' = substFreeDVarSet (lcTCvSubst env) fvs
@@ -573,9 +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
+ ZappedProv fvs -> mkZappedProv $ substFreeDVarSet (lcTCvSubst env) fvs
TcZappedProv fvs coholes
- -> TcZappedProv (substFreeDVarSet (lcTCvSubst env) fvs) coholes
+ -> mkTcZappedProv (substFreeDVarSet (lcTCvSubst env) fvs) coholes
-------------
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -658,10 +658,10 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
= 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
+ = Just $ mkZappedProv $ fvs1 `unionDVarSet` fvs2
opt_trans_prov (TcZappedProv fvs1 coholes1)
(TcZappedProv fvs2 coholes2)
- = Just $ TcZappedProv (fvs1 `unionDVarSet` fvs2) (coholes1 ++ coholes2)
+ = Just $ mkTcZappedProv (fvs1 `unionDVarSet` fvs2) (coholes1 ++ coholes2)
opt_trans_prov _ _ = Nothing
-- Push transitivity down through matching top-level constructors.
=====================================
compiler/GHC/Core/Rules.hs
=====================================
@@ -63,6 +63,7 @@ import Outputable
import FastString
import Maybes
import Bag
+import Pair
import Util
import Data.List
import Data.Ord
@@ -840,6 +841,14 @@ match_co renv subst co1 co2
Just (arg2, res2)
-> match_cos renv subst [arg1, res1] [arg2, res2]
_ -> Nothing
+match_co renv subst co1 co2
+ | Just (prov1, r1, Pair ty1a ty1b) <- splitUnivCo_maybe co1
+ , Just (prov2, r2, Pair ty2a ty2b) <- splitUnivCo_maybe co2
+ = do { guard (r1 == r2)
+ -- TODO: Should we try to match provenance?
+ ; subst' <- match_ty renv subst ty1a ty2a
+ ; match_ty renv subst' ty1b ty2b
+ }
match_co _ _ _co1 _co2
-- Currently just deals with CoVarCo, TyConAppCo and Refl
#if defined(DEBUG)
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1875,7 +1875,7 @@ foldTyCo (TyCoFolder { tcf_view = view
where f v acc
| isTyVar v = tyvar env v `mappend` acc
| isCoVar v = covar env v `mappend` acc
- | otherwise = error "unknown thingy"
+ | otherwise = pprPanic "unknown thingy" (ppr v)
{- *********************************************************************
* *
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -64,7 +64,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
, mkFunCo, mkForAllCo, mkUnivCo
, mkAxiomInstCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
- , mkCoercionType
+ , mkCoercionType, mkZappedProv, mkTcZappedProv
, coercionKind, coercionLKind, coVarKindsTypesRole )
import GHC.Core.TyCo.Rep
@@ -825,9 +825,9 @@ 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 (ZappedProv fvs) = mkZappedProv (substFreeDVarSet subst fvs)
go_prov (TcZappedProv fvs coholes)
- = TcZappedProv (substFreeDVarSet subst fvs) coholes
+ = mkTcZappedProv (substFreeDVarSet subst fvs) coholes
-- See Note [Substituting in a coercion hole]
go_hole h@(CoercionHole { ch_co_var = cv })
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -21,6 +21,7 @@ module GHC.Core.TyCo.Tidy
import GhcPrelude
import GHC.Core.TyCo.Rep
+import {-# SOURCE #-} GHC.Core.Coercion ( mkZappedProv, mkTcZappedProv )
import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
import Name hiding (varName)
@@ -230,10 +231,10 @@ 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 (ZappedProv fvs) = mkZappedProv $ mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs)
go_prov (TcZappedProv fvs coholes)
- = TcZappedProv (mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs))
- coholes -- Tidying needed?
+ = mkTcZappedProv (mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs))
+ coholes -- Tidying needed?
substCoVar cv = fromMaybe cv $ lookupVarEnv subst cv
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -254,6 +254,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
, mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
, mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
, mkKindCo, mkSubCo, mkFunCo, mkAxiomInstCo
+ , mkZappedProv, mkTcZappedProv
, decomposePiCos, coercionKind, coercionLKind
, coercionRKind, coercionType
, isReflexiveCo, seqCo )
@@ -475,9 +476,9 @@ expandTypeSynonyms ty
go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
go_prov _ p@(PluginProv _) = p
go_prov subst (ZappedProv fvs)
- = ZappedProv $ substFreeDVarSet subst fvs
+ = mkZappedProv $ substFreeDVarSet subst fvs
go_prov subst (TcZappedProv fvs coholes)
- = TcZappedProv (substFreeDVarSet subst fvs) coholes
+ = mkTcZappedProv (substFreeDVarSet subst fvs) coholes
-- the "False" and "const" are to accommodate the type of
-- substForAllCoBndrUsing, which is general enough to
@@ -721,21 +722,18 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
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'
+ = do { fvs' <- unionDVarSets <$> mapM (bndr_fvs env) (dVarSetElems fvs)
+ ; return $ mkZappedProv 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''
+ = do { fvs' <- unionDVarSets <$> mapM (bndr_fvs env) (dVarSetElems fvs)
+ ; coholes' <- mapM (cohole env) coholes
+ ; let fvs'' = mapUnionDVarSet tyCoVarsOfCoDSet coholes'
+ ; return $ mkZappedProv $ fvs' `unionDVarSet` fvs'' }
+
+ bndr_fvs env v
+ | isCoVar v = tyCoVarsOfCoDSet <$> covar env v
+ | isTyVar v = tyCoVarsOfTypeDSet <$> tyvar env v
+ | otherwise = pprPanic "mapCoercion(ZappedProv): Bad free variable" (ppr v)
{-
************************************************************************
=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -1191,7 +1191,7 @@ data RtsOptsEnabled
-- See Note [Zapping coercions] for details.
shouldBuildCoercions :: DynFlags -> Bool
shouldBuildCoercions dflags =
- gopt Opt_DoCoreLinting dflags && not (gopt Opt_DropCoercions dflags)
+ not (gopt Opt_DropCoercions dflags) -- && gopt Opt_DoCoreLinting dflags
-- TODO: Add flag to explicitly enable coercion generation without linting?
-- | Are we building with @-fPIE@ or @-fPIC@ enabled?
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1260,7 +1260,7 @@ tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str
tcIfaceUnivCoProv (IfaceZappedProv tvs cvs _)
= do cvs' <- mapM tcIfaceLclId cvs
tvs' <- mapM tcIfaceTyVar tvs
- return $ ZappedProv $ mkDVarSet $ cvs' ++ tvs'
+ return $ mkZappedProv $ mkDVarSet $ cvs' ++ tvs'
{-
************************************************************************
=====================================
compiler/typecheck/TcFlatten.hs
=====================================
@@ -1511,7 +1511,7 @@ flatten_exact_fam_app_fully tc tys
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 $ perhapsZapCoercion dflags co' co'_kind role fvs
--co'' = update_co co'
; return $ Just (xi', co'') }
Nothing -> pure Nothing }
@@ -1536,7 +1536,7 @@ flatten_exact_fam_app_fully tc tys
; let role = eqRelRole eq_rel
; let co = mkSymCo (maybeTcSubCo eq_rel norm_co
`mkTransCo` mkSymCo final_co)
- co' = mkZappedCoercion dflags co (Pair xi fam_ty) role fvs
+ co' = perhapsZapCoercion dflags co (Pair xi fam_ty) role fvs
--co' = co
; return $ Just (xi, co') }
Nothing -> pure Nothing }
=====================================
compiler/typecheck/TcMType.hs
=====================================
@@ -113,6 +113,7 @@ import TcRnMonad -- TcType, amongst others
import Constraint
import TcEvidence
import Id
+import IdInfo (IdDetails(CoercionHoleId))
import Name
import VarSet
import TysWiredIn
@@ -328,7 +329,7 @@ newCoercionHole :: BlockSubstFlag -- should the presence of this hole block sub
-- Note [Equalities with incompatible kinds]
-> TcPredType -> TcM CoercionHole
newCoercionHole blocker pred_ty
- = do { co_var <- newEvVar pred_ty
+ = do { co_var <- fmap (`setIdDetails` CoercionHoleId) (newEvVar pred_ty)
; traceTc "New coercion hole:" (ppr co_var <+> ppr blocker)
; ref <- newMutVar Nothing
; return $ CoercionHole { ch_co_var = co_var, ch_blocker = blocker
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/81578d45f7bb2cc84d153c8152a1e8faa9fd53b5...6a41b6b1fc23f2d0251cf7da634e9453a20810d0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/81578d45f7bb2cc84d153c8152a1e8faa9fd53b5...6a41b6b1fc23f2d0251cf7da634e9453a20810d0
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/f7bbdb4a/attachment-0001.html>
More information about the ghc-commits
mailing list