Commit 2fbe0b51 authored by Tobias Dammers's avatar Tobias Dammers 🦈 Committed by Ben Gamari

Caching coercion roles in NthCo and coercionKindsRole refactoring

While addressing nonlinear behavior related to coercion roles,
particularly `NthCo`, we noticed that coercion roles are recalculated
often even though they should be readily at hand already in most cases.
This patch adds a `Role` to the `NthCo` constructor so that we can cache
them rather than having to recalculate them on the fly.
https://ghc.haskell.org/trac/ghc/ticket/11735#comment:23 explains the
approach.

Performance improvement over GHC HEAD, when compiling Grammar.hs (see below):

GHC 8.2.1:
```
ghc Grammar.hs  176.27s user 0.23s system 99% cpu 2:56.81 total
```

before patch (but with other optimizations applied):
```
ghc Grammar.hs -fforce-recomp  175.77s user 0.19s system 100% cpu 2:55.78 total
```

after:
```
../../ghc/inplace/bin/ghc-stage2 Grammar.hs  10.32s user 0.17s system 98% cpu 10.678 total
```

Introduces the following regressions:

- perf/compiler/parsing001 (possibly false positive)
- perf/compiler/T9872
- perf/compiler/haddock.base

Reviewers: goldfire, bgamari, simonpj

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #11735

Differential Revision: https://phabricator.haskell.org/D4394
parent b41a42e3
......@@ -379,7 +379,7 @@ orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orph
orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1 `unionNameSet` orphNamesOfType t2
orphNamesOfCo (SymCo co) = orphNamesOfCo co
orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (NthCo _ co) = orphNamesOfCo co
orphNamesOfCo (NthCo _ _ co) = orphNamesOfCo co
orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
......
......@@ -1759,12 +1759,13 @@ lintCoercion co@(TransCo co1 co2)
; lintRole co r1 r2
; return (k1a, k2b, ty1a, ty2b, r1) }
lintCoercion the_co@(NthCo n co)
lintCoercion the_co@(NthCo r0 n co)
= do { (_, _, s, t, r) <- lintCoercion co
; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
{ (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
| n == 0
-> return (ks, kt, ts, tt, Nominal)
-> do { lintRole the_co Nominal r0
; return (ks, kt, ts, tt, r0) }
where
ts = tyVarKind tv_s
tt = tyVarKind tv_t
......@@ -1778,7 +1779,8 @@ lintCoercion the_co@(NthCo n co)
-- see Note [NthCo and newtypes] in TyCoRep
, tys_s `equalLength` tys_t
, tys_s `lengthExceeds` n
-> return (ks, kt, ts, tt, tr)
-> do { lintRole the_co tr r0
; return (ks, kt, ts, tt, r0) }
where
ts = getNth tys_s n
tt = getNth tys_t n
......
......@@ -930,7 +930,7 @@ Here we implement the "push rules" from FC papers:
by pushing the coercion into the arguments
-}
pushCoArgs :: Coercion -> [CoreArg] -> Maybe ([CoreArg], Maybe Coercion)
pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], Maybe Coercion)
pushCoArgs co [] = return ([], Just co)
pushCoArgs co (arg:args) = do { (arg', m_co1) <- pushCoArg co arg
; case m_co1 of
......@@ -938,7 +938,7 @@ pushCoArgs co (arg:args) = do { (arg', m_co1) <- pushCoArg co arg
; return (arg':args', m_co2) }
Nothing -> return (arg':args, Nothing) }
pushCoArg :: Coercion -> CoreArg -> Maybe (CoreArg, Maybe Coercion)
pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, Maybe Coercion)
-- We have (fun |> co) arg, and we want to transform it to
-- (fun arg) |> co
-- This may fail, e.g. if (fun :: N) where N is a newtype
......@@ -973,7 +973,7 @@ pushCoTyArg co ty
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
co1 = mkNthCo 0 co
co1 = mkNthCo Nominal 0 co
-- co1 :: k1 ~N k2
-- Note that NthCo can extract a Nominal equality between the
-- kinds of the types related by a coercion between forall-types.
......@@ -983,7 +983,7 @@ pushCoTyArg co ty
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
-- Arg of mkInstCo is always nominal, hence mkNomReflCo
pushCoValArg :: Coercion -> Maybe (Coercion, Maybe Coercion)
pushCoValArg :: CoercionR -> Maybe (Coercion, Maybe Coercion)
-- We have (fun |> co) arg
-- Push the coercion through to return
-- (fun (arg |> co_arg)) |> co_res
......@@ -995,7 +995,7 @@ pushCoValArg co
= Just (mkRepReflCo arg, Nothing)
| isFunTy tyL
, (co1, co2) <- decomposeFunCo co
, (co1, co2) <- decomposeFunCo Representational co
-- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
-- then co1 :: tyL1 ~ tyR1
-- co2 :: tyL2 ~ tyR2
......@@ -1009,7 +1009,7 @@ pushCoValArg co
Pair tyL tyR = coercionKind co
pushCoercionIntoLambda
:: InScopeSet -> Var -> CoreExpr -> Coercion -> Maybe (Var, CoreExpr)
:: InScopeSet -> Var -> CoreExpr -> CoercionR -> Maybe (Var, CoreExpr)
-- This implements the Push rule from the paper on coercions
-- (\x. e) |> co
-- ===>
......@@ -1019,7 +1019,7 @@ pushCoercionIntoLambda in_scope x e co
, Pair s1s2 t1t2 <- coercionKind co
, Just (_s1,_s2) <- splitFunTy_maybe s1s2
, Just (t1,_t2) <- splitFunTy_maybe t1t2
= let (co1, co2) = decomposeFunCo co
= let (co1, co2) = decomposeFunCo Representational co
-- Should we optimize the coercions here?
-- Otherwise they might not match too well
x' = x `setIdType` t1
......@@ -1065,7 +1065,7 @@ pushCoDataCon dc dc_args co
(ex_args, val_args) = splitAtList dc_ex_tyvars non_univ_args
-- Make the "Psi" from the paper
omegas = decomposeCo tc_arity co
omegas = decomposeCo tc_arity co (tyConRolesRepresentational to_tc)
(psi_subst, to_ex_arg_tys)
= liftCoSubstWithEx Representational
dc_univ_tyvars
......@@ -1112,7 +1112,7 @@ collectBindersPushingCo e
go bs e = (reverse bs, e)
-- We are in a cast; peel off casts until we hit a lambda.
go_c :: [Var] -> CoreExpr -> Coercion -> ([Var], CoreExpr)
go_c :: [Var] -> CoreExpr -> CoercionR -> ([Var], CoreExpr)
-- (go_c bs e c) is same as (go bs e (e |> c))
go_c bs (Cast e co1) co2 = go_c bs e (co1 `mkTransCo` co2)
go_c bs (Lam b e) co = go_lam bs b e co
......@@ -1120,20 +1120,20 @@ collectBindersPushingCo e
-- We are in a lambda under a cast; peel off lambdas and build a
-- new coercion for the body.
go_lam :: [Var] -> Var -> CoreExpr -> Coercion -> ([Var], CoreExpr)
go_lam :: [Var] -> Var -> CoreExpr -> CoercionR -> ([Var], CoreExpr)
-- (go_lam bs b e c) is same as (go_c bs (\b.e) c)
go_lam bs b e co
| isTyVar b
, let Pair tyL tyR = coercionKind co
, ASSERT( isForAllTy tyL )
isForAllTy tyR
, isReflCo (mkNthCo 0 co) -- See Note [collectBindersPushingCo]
, isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo]
= go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b)))
| isId b
, let Pair tyL tyR = coercionKind co
, ASSERT( isFunTy tyL) isFunTy tyR
, (co_arg, co_res) <- decomposeFunCo co
, (co_arg, co_res) <- decomposeFunCo Representational co
, isReflCo co_arg -- See Note [collectBindersPushingCo]
= go_c (b:bs) e co_res
......
......@@ -257,7 +257,7 @@ applyTypeToArgs e op_ty args
-- | Wrap the given expression in the coercion safely, dropping
-- identity coercions and coalescing nested coercions
mkCast :: CoreExpr -> Coercion -> CoreExpr
mkCast :: CoreExpr -> CoercionR -> CoreExpr
mkCast e co
| ASSERT2( coercionRole co == Representational
, text "coercion" <+> ppr co <+> ptext (sLit "passed to mkCast")
......
......@@ -1353,7 +1353,8 @@ tcIfaceCo = go
<*> go c2
go (IfaceInstCo c1 t2) = InstCo <$> go c1
<*> go t2
go (IfaceNthCo d c) = NthCo d <$> go c
go (IfaceNthCo d c) = do { c' <- go c
; return $ mkNthCo (nthCoRole d c') d c' }
go (IfaceLRCo lr c) = LRCo lr <$> go c
go (IfaceCoherenceCo c1 c2) = CoherenceCo <$> go c1
<*> go c2
......
......@@ -231,7 +231,7 @@ toIfaceCoercionX fr co
go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2)
go (SymCo co) = IfaceSymCo (go co)
go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
go (NthCo d co) = IfaceNthCo d (go co)
go (NthCo _r d co) = IfaceNthCo d (go co)
go (LRCo lr co) = IfaceLRCo lr (go co)
go (InstCo co arg) = IfaceInstCo (go co) (go arg)
go (CoherenceCo c1 c2) = IfaceCoherenceCo (go c1) (go c2)
......
......@@ -128,8 +128,8 @@ simplTopBinds env0 binds0
-- anything into scope, then we don't get a complaint about that.
-- It's rather as if the top-level binders were imported.
-- See note [Glomming] in OccurAnal.
; env1 <- simplRecBndrs env0 (bindersOfBinds binds0)
; (floats, env2) <- simpl_binds env1 binds0
; env1 <- {-#SCC "simplTopBinds-simplRecBndrs" #-} simplRecBndrs env0 (bindersOfBinds binds0)
; (floats, env2) <- {-#SCC "simplTopBinds-simpl_binds" #-} simpl_binds env1 binds0
; freeTick SimplifierDone
; return (floats, env2) }
where
......@@ -197,17 +197,20 @@ simplRecOrTopPair :: SimplEnv
simplRecOrTopPair env top_lvl is_rec mb_cont old_bndr new_bndr rhs
| Just env' <- preInlineUnconditionally env top_lvl old_bndr rhs env
= trace_bind "pre-inline-uncond" $
= {-#SCC "simplRecOrTopPair-pre-inline-uncond" #-}
trace_bind "pre-inline-uncond" $
do { tick (PreInlineUnconditionally old_bndr)
; return ( emptyFloats env, env' ) }
| Just cont <- mb_cont
= ASSERT( isNotTopLevel top_lvl && isJoinId new_bndr )
= {-#SCC "simplRecOrTopPair-join" #-}
ASSERT( isNotTopLevel top_lvl && isJoinId new_bndr )
trace_bind "join" $
simplJoinBind env cont old_bndr new_bndr rhs env
| otherwise
= trace_bind "normal" $
= {-#SCC "simplRecOrTopPair-normal" #-}
trace_bind "normal" $
simplLazyBind env top_lvl is_rec old_bndr new_bndr rhs env
where
......@@ -254,12 +257,12 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
-- should eta-reduce.
; (body_env, tvs') <- simplBinders rhs_env tvs
; (body_env, tvs') <- {-#SCC "simplBinders" #-} simplBinders rhs_env tvs
-- See Note [Floating and type abstraction] in SimplUtils
-- Simplify the RHS
; let rhs_cont = mkRhsStop (substTy body_env (exprType body))
; (body_floats0, body0) <- simplExprF body_env body rhs_cont
; (body_floats0, body0) <- {-#SCC "simplExprF" #-} simplExprF body_env body rhs_cont
-- Never float join-floats out of a non-join let-binding
-- So wrap the body in the join-floats right now
......@@ -268,21 +271,24 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
-- ANF-ise a constructor or PAP rhs
-- We get at most one float per argument here
; (let_floats, body2) <- prepareRhs (getMode env) top_lvl
; (let_floats, body2) <- {-#SCC "prepareRhs" #-} prepareRhs (getMode env) top_lvl
(getOccFS bndr1) (idInfo bndr1) body1
; let body_floats2 = body_floats1 `addLetFloats` let_floats
; (rhs_floats, rhs')
<- if not (doFloatFromRhs top_lvl is_rec False body_floats2 body2)
then -- No floating, revert to body1
{-#SCC "simplLazyBind-no-floating" #-}
do { rhs' <- mkLam env tvs' (wrapFloats body_floats2 body1) rhs_cont
; return (emptyFloats env, rhs') }
else if null tvs then -- Simple floating
{-#SCC "simplLazyBind-simple-floating" #-}
do { tick LetFloatFromLet
; return (body_floats2, body2) }
else -- Do type-abstraction first
{-#SCC "simplLazyBind-type-abstraction-first" #-}
do { tick LetFloatFromLet
; (poly_binds, body3) <- abstractFloats (seDynFlags env) top_lvl
tvs' body_floats2 body2
......@@ -850,14 +856,14 @@ simplExprF1 _ (Type ty) _
-- The (Type ty) case is handled separately by simplExpr
-- and by the other callers of simplExprF
simplExprF1 env (Var v) cont = simplIdF env v cont
simplExprF1 env (Lit lit) cont = rebuild env (Lit lit) cont
simplExprF1 env (Tick t expr) cont = simplTick env t expr cont
simplExprF1 env (Cast body co) cont = simplCast env body co cont
simplExprF1 env (Coercion co) cont = simplCoercionF env co cont
simplExprF1 env (Var v) cont = {-#SCC "simplIdF" #-} simplIdF env v cont
simplExprF1 env (Lit lit) cont = {-#SCC "rebuild" #-} rebuild env (Lit lit) cont
simplExprF1 env (Tick t expr) cont = {-#SCC "simplTick" #-} simplTick env t expr cont
simplExprF1 env (Cast body co) cont = {-#SCC "simplCast" #-} simplCast env body co cont
simplExprF1 env (Coercion co) cont = {-#SCC "simplCoercionF" #-} simplCoercionF env co cont
simplExprF1 env (App fun arg) cont
= case arg of
= {-#SCC "simplExprF1-App" #-} case arg of
Type ty -> do { -- The argument type will (almost) certainly be used
-- in the output program, so just force it now.
-- See Note [Avoiding space leaks in OutType]
......@@ -877,7 +883,8 @@ simplExprF1 env (App fun arg) cont
, sc_dup = NoDup, sc_cont = cont }
simplExprF1 env expr@(Lam {}) cont
= simplLam env zapped_bndrs body cont
= {-#SCC "simplExprF1-Lam" #-}
simplLam env zapped_bndrs body cont
-- The main issue here is under-saturated lambdas
-- (\x1. \x2. e) arg1
-- Here x1 might have "occurs-once" occ-info, because occ-info
......@@ -899,28 +906,30 @@ simplExprF1 env expr@(Lam {}) cont
| otherwise = zapLamIdInfo b
simplExprF1 env (Case scrut bndr _ alts) cont
= simplExprF env scrut (Select { sc_dup = NoDup, sc_bndr = bndr
= {-#SCC "simplExprF1-Case" #-}
simplExprF env scrut (Select { sc_dup = NoDup, sc_bndr = bndr
, sc_alts = alts
, sc_env = env, sc_cont = cont })
simplExprF1 env (Let (Rec pairs) body) cont
| Just pairs' <- joinPointBindings_maybe pairs
= simplRecJoinPoint env pairs' body cont
= {-#SCC "simplRecJoinPoin" #-} simplRecJoinPoint env pairs' body cont
| otherwise
= simplRecE env pairs body cont
= {-#SCC "simplRecE" #-} simplRecE env pairs body cont
simplExprF1 env (Let (NonRec bndr rhs) body) cont
| Type ty <- rhs -- First deal with type lets (let a = Type ty in e)
= ASSERT( isTyVar bndr )
= {-#SCC "simplExprF1-NonRecLet-Type" #-}
ASSERT( isTyVar bndr )
do { ty' <- simplType env ty
; simplExprF (extendTvSubst env bndr ty') body cont }
| Just (bndr', rhs') <- joinPointBinding_maybe bndr rhs
= simplNonRecJoinPoint env bndr' rhs' body cont
= {-#SCC "simplNonRecJoinPoint" #-} simplNonRecJoinPoint env bndr' rhs' body cont
| otherwise
= simplNonRecE env bndr (rhs, env) ([], body) cont
= {-#SCC "simplNonRecE" #-} simplNonRecE env bndr (rhs, env) ([], body) cont
{- Note [Avoiding space leaks in OutType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1203,9 +1212,9 @@ rebuild env expr cont
simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
-> SimplM (SimplFloats, OutExpr)
simplCast env body co0 cont0
= do { co1 <- simplCoercion env co0
; cont1 <- addCoerce co1 cont0
; simplExprF env body cont1 }
= do { co1 <- {-#SCC "simplCast-simplCoercion" #-} simplCoercion env co0
; cont1 <- {-#SCC "simplCast-addCoerce" #-} addCoerce co1 cont0
; {-#SCC "simplCast-simplExprF" #-} simplExprF env body cont1 }
where
-- If the first parameter is Nothing, then simplifying revealed a
-- reflexive coercion. Omit.
......@@ -1216,11 +1225,13 @@ simplCast env body co0 cont0
addCoerce :: OutCoercion -> SimplCont -> SimplM SimplCont
addCoerce co1 (CastIt co2 cont)
= addCoerce (mkTransCo co1 co2) cont
= {-#SCC "addCoerce-simple-recursion" #-}
addCoerce (mkTransCo co1 co2) cont
addCoerce co cont@(ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail })
| Just (arg_ty', m_co') <- pushCoTyArg co arg_ty
= do { tail' <- addCoerce0 m_co' tail
= {-#SCC "addCoerce-pushCoTyArg" #-}
do { tail' <- addCoerce0 m_co' tail
; return (cont { sc_arg_ty = arg_ty', sc_cont = tail' }) }
addCoerce co cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se
......@@ -1230,7 +1241,8 @@ simplCast env body co0 cont0
, not (isTypeLevPoly new_ty) -- without this check, we get a lev-poly arg
-- See Note [Levity polymorphism invariants] in CoreSyn
-- test: typecheck/should_run/EtaExpandLevPoly
= do { tail' <- addCoerce0 m_co2 tail
= {-#SCC "addCoerce-pushCoValArg" #-}
do { tail' <- addCoerce0 m_co2 tail
; if isReflCo co1
then return (cont { sc_cont = tail' })
-- Avoid simplifying if possible;
......@@ -1248,8 +1260,10 @@ simplCast env body co0 cont0
, sc_cont = tail' }) } }
addCoerce co cont
| isReflexiveCo co = return cont
| otherwise = return (CastIt co cont)
| isReflexiveCo co = {-#SCC "addCoerce-reflexive" #-}
return cont
| otherwise = {-#SCC "addCoerce-other" #-}
return (CastIt co cont)
-- It's worth checking isReflexiveCo.
-- For example, in the initial form of a worker
-- we may find (coerce T (coerce S (\x.e))) y
......@@ -3278,7 +3292,7 @@ simplLetUnfolding env top_lvl cont_mb id new_rhs rhs_ty unf
| isStableUnfolding unf
= simplStableUnfolding env top_lvl cont_mb id unf rhs_ty
| isExitJoinId id
= return noUnfolding -- see Note [Do not inline exit join points] in Exitify
= return noUnfolding -- see Note [Do not inline exit join points]
| otherwise
= mkLetUnfolding (seDynFlags env) top_lvl InlineRhs id new_rhs
......
......@@ -1294,7 +1294,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-> do { let ev_co = mkCoVarCo evar
; given_evs <- newGivenEvVars loc $
[ ( mkPrimEqPredRole r ty1 ty2
, evCoercion $ mkNthCo i ev_co )
, evCoercion $ mkNthCo r i ev_co )
| (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
, r /= Phantom
, not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
......
......@@ -110,7 +110,7 @@ mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
-> [TcCoercion] -> TcCoercionR
mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
mkTcNthCo :: Int -> TcCoercion -> TcCoercion
mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcSubCo :: TcCoercionN -> TcCoercionR
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
......@@ -768,11 +768,6 @@ isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
evTermCoercion :: EvTerm -> TcCoercion
-- Applied only to EvTerms of type (s~t)
-- See Note [Coercion evidence terms]
evTermCoercion (EvExpr (Var v)) = mkCoVarCo v
evTermCoercion (EvExpr (Coercion co)) = co
evTermCoercion (EvExpr (Cast tm co)) = mkCoCast (evTermCoercion (EvExpr tm)) co
evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
{-
************************************************************************
......@@ -800,6 +795,11 @@ findNeededEvVars ev_binds seeds
| otherwise
= needs
evTermCoercion (EvExpr (Var v)) = mkCoVarCo v
evTermCoercion (EvExpr (Coercion co)) = co
evTermCoercion (EvExpr (Cast tm co)) = mkCoCast (evTermCoercion (EvExpr tm)) co
evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
......
......@@ -122,7 +122,7 @@ synonymTyConsOfType ty
go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
go_co (SymCo co) = go_co co
go_co (TransCo co co') = go_co co `plusNameEnv` go_co co'
go_co (NthCo _ co) = go_co co
go_co (NthCo _ _ co) = go_co co
go_co (LRCo _ co) = go_co co
go_co (InstCo co co') = go_co co `plusNameEnv` go_co co'
go_co (CoherenceCo co co') = go_co co `plusNameEnv` go_co co'
......
......@@ -68,7 +68,7 @@ module TcType (
tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
tcRepGetNumAppTys,
tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar,
tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
---------------------------------
......@@ -941,7 +941,7 @@ exactTyCoVarsOfType ty
goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2
goCo (SymCo co) = goCo co
goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2
goCo (NthCo _ co) = goCo co
goCo (NthCo _ _ co) = goCo co
goCo (LRCo _ co) = goCo co
goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg
goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
......
......@@ -2182,8 +2182,8 @@ occCheckExpand tv ty
go_co env (TransCo co1 co2) = do { co1' <- go_co env co1
; co2' <- go_co env co2
; return (mkTransCo co1' co2') }
go_co env (NthCo n co) = do { co' <- go_co env co
; return (mkNthCo n co') }
go_co env (NthCo r n co) = do { co' <- go_co env co
; return (mkNthCo r n co') }
go_co env (LRCo lr co) = do { co' <- go_co env co
; return (mkLRCo lr co') }
go_co env (InstCo co arg) = do { co' <- go_co env co
......
......@@ -1937,7 +1937,7 @@ fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
fvCo (SymCo co) = fvCo co
fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
fvCo (NthCo _ co) = fvCo co
fvCo (NthCo _ _ co) = fvCo co
fvCo (LRCo _ co) = fvCo co
fvCo (InstCo co arg) = fvCo co ++ fvCo arg
fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2
......
This diff is collapsed.
......@@ -25,7 +25,7 @@ mkUnsafeCo :: Role -> Type -> Type -> Coercion
mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkSymCo :: Coercion -> Coercion
mkTransCo :: Coercion -> Coercion -> Coercion
mkNthCo :: Int -> Coercion -> Coercion
mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkInstCo :: Coercion -> Coercion -> Coercion
mkCoherenceCo :: Coercion -> Coercion -> Coercion
......
......@@ -1635,7 +1635,7 @@ allTyVarsInTy = go
go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
go_co (SymCo co) = go_co co
go_co (TransCo c1 c2) = go_co c1 `unionVarSet` go_co c2
go_co (NthCo _ co) = go_co co
go_co (NthCo _ _ co) = go_co co
go_co (LRCo _ co) = go_co co
go_co (InstCo co arg) = go_co co `unionVarSet` go_co arg
go_co (CoherenceCo c1 c2) = go_co c1 `unionVarSet` go_co c2
......
......@@ -269,9 +269,40 @@ opt_co4 env sym rep r (TransCo co1 co2)
co2' = opt_co4_wrap env sym rep r co2
in_scope = lcInScopeSet env
opt_co4 env _sym rep r (NthCo _r n (Refl _r2 ty))
| Just (_tc, args) <- ASSERT( r == _r )
splitTyConApp_maybe ty
= liftCoSubst (chooseRole rep r) env (args `getNth` n)
| n == 0
, Just (tv, _) <- splitForAllTy_maybe ty
= liftCoSubst (chooseRole rep r) env (tyVarKind tv)
opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
= ASSERT( r == r1 )
opt_co4_wrap env sym rep r (cos `getNth` n)
opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
= ASSERT( r == _r )
ASSERT( n == 0 )
opt_co4_wrap env sym rep Nominal eta
opt_co4 env sym rep r (NthCo _r n co)
| TyConAppCo _ _ cos <- co'
, let nth_co = cos `getNth` n
= if rep && (r == Nominal)
-- keep propagating the SubCo
then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
else nth_co
| ForAllCo _ eta _ <- co'
= if rep
then opt_co4_wrap (zapLiftingContext env) False True Nominal eta
else eta
opt_co4 env sym rep r co@(NthCo {})
= opt_nth_co env sym rep r co
| otherwise
= wrapRole rep r $ NthCo r n co'
where
co' = opt_co1 env sym co
opt_co4 env sym rep r (LRCo lr co)
| Just pr_co <- splitAppCo_maybe co
......@@ -434,62 +465,6 @@ opt_univ env sym prov role oty1 oty2
ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
PluginProv _ -> prov
-------------
-- NthCo must be handled separately, because it's the one case where we can't
-- tell quickly what the component coercion's role is from the containing
-- coercion. To avoid repeated coercionRole calls as opt_co1 calls opt_co2,
-- we just look for nested NthCo's, which can happen in practice.
opt_nth_co :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
opt_nth_co env sym rep r = go []
where
go ns (NthCo n co) = go (n:ns) co
-- previous versions checked if the tycon is decomposable. This
-- is redundant, because a non-decomposable tycon under an NthCo
-- is entirely bogus. See docs/core-spec/core-spec.pdf.
go ns co
= opt_nths ns co
-- try to resolve 1 Nth
push_nth n (Refl r1 ty)
| Just (tc, args) <- splitTyConApp_maybe ty
= Just (Refl (nthRole r1 tc n) (args `getNth` n))
| n == 0
, Just (tv, _) <- splitForAllTy_maybe ty
= Just (Refl Nominal (tyVarKind tv))
push_nth n (TyConAppCo _ _ cos)
= Just (cos `getNth` n)
push_nth 0 (ForAllCo _ eta _)
= Just eta
push_nth _ _ = Nothing
-- input coercion is *not* yet sym'd or opt'd
opt_nths [] co = opt_co4_wrap env sym rep r co
opt_nths (n:ns) co
| Just co' <- push_nth n co
= opt_nths ns co'
-- here, the co isn't a TyConAppCo, so we opt it, hoping to get
-- a TyConAppCo as output. We don't know the role, so we use
-- opt_co1. This is slightly annoying, because opt_co1 will call
-- coercionRole, but as long as we don't have a long chain of
-- NthCo's interspersed with some other coercion former, we should
-- be OK.
opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
-- input coercion *is* sym'd and opt'd
opt_nths' [] co
= if rep && (r == Nominal)
-- propagate the SubCo:
then opt_co4_wrap (zapLiftingContext env) False True r co
else co
opt_nths' (n:ns) co
| Just co' <- push_nth n co
= opt_nths' ns co'
opt_nths' ns co = wrapRole rep r (mk_nths ns co)
mk_nths [] co = co
mk_nths (n:ns) co = mk_nths ns (mkNthCo n co)
-------------
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
......@@ -529,11 +504,13 @@ opt_trans2 _ co1 co2
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
-- Push transitivity through matching destructors
opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
| d1 == d2
, coercionRole co1 == coercionRole co2
, co1 `compatible_co` co2
= fireTransRule "PushNth" in_co1 in_co2 $
mkNthCo d1 (opt_trans is co1 co2)
= ASSERT( r1 == r2 )
fireTransRule "PushNth" in_co1 in_co2 $
mkNthCo r1 d1 (opt_trans is co1 co2)
opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
| d1 == d2
......@@ -984,7 +961,7 @@ etaForAllCo_maybe co
| Pair ty1 ty2 <- coercionKind co
, Just (tv1, _) <- splitForAllTy_maybe ty1
, isForAllTy ty2
, let kind_co = mkNthCo 0 co
, let kind_co = mkNthCo Nominal 0 co
= Just ( tv1, kind_co
, mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_co) )
......@@ -1027,7 +1004,7 @@ etaTyConAppCo_maybe tc co
-- E.g. T a ~# T a b
-- Trac #14607
= ASSERT( tc == tc1 )
Just (decomposeCo n co)
Just (decomposeCo n co (tyConRolesX r tc1))
-- NB: n might be <> tyConArity tc
-- e.g. data family T a :: * -> *
-- g :: T a b ~ T c d
......
......@@ -904,10 +904,14 @@ data Coercion
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
| NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
-- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
| NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
-- :: "e" -> _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles])
-- Using NthCo on a ForAllCo gives an N coercion always
-- See Note [NthCo and newtypes]
--
-- Invariant: (NthCo r i co), it is always the case that r = role of (Nth i co)
-- That is: the role of the entire coercion is redundantly cached here.
-- See Note [NthCo Cached Roles]
| LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
-- :: _ -> N -> N
......@@ -1217,7 +1221,7 @@ We can then build
for any `a` and `b`. Because of the role annotation on N, if we use
NthCo, we'll get out a representational coercion. That is:
NthCo 0 co :: forall a b. a ~R b
NthCo r 0 co :: forall a b. a ~R b
Yikes! Clearly, this is terrible. The solution is simple: forbid
NthCo to be used on newtypes if the internal coercion is representational.
......@@ -1226,6 +1230,23 @@ This is not just some corner case discovered by a segfault somewhere;
it was discovered in the proof of soundness of roles and described
in the "Safe Coercions" paper (ICFP '14).
Note [NthCo Cached Roles]
~~~~~~~~~~~~~~~~~~~~~~~~~
Why do we cache the role of NthCo in the NthCo constructor?
Because computing role(Nth i co) involves figuring out that
co :: T tys1 ~ T tys2
using coercionKind, and finding (coercionRole co), and then looking
at the tyConRoles of T. Avoiding bad asymptotic behaviour here means
we have to compute the kind and role of a coercion simultaneously,
which makes the code complicated and inefficient.
This only happens for NthCo. Caching the role solves the problem, and
allows coercionKind and coercionRole to be simple.
See Trac #11735
Note [InstCo roles]
~~~~~~~~~~~~~~~~~~~
Here is (essentially) the typing rule for InstCo:
......@@ -1574,7 +1595,7 @@ tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
`unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
tyCoFVsOfCo (NthCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (NthCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
tyCoFVsOfCo (CoherenceCo c1 c2) fv_cand in_scope acc = (tyCoFVsOfCo c1 `unionFV` tyCoFVsOfCo c2) fv_cand in_scope acc
......@@ -1637,7 +1658,7 @@ coVarsOfCo (AxiomInstCo _ _ as) = coVarsOfCos as
coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2]