summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTobias Dammers <tdammers@gmail.com>2018-01-25 20:33:58 +0100
committerTobias Dammers <tdammers@gmail.com>2018-04-20 10:33:00 +0200
commit03ed25a8f228c2f6d56793bc45f5709b9afb02c7 (patch)
treed8c706c85b1cc601215d11b623f35c7592ba7ef0
parent8f4ee8d5a349bc2395eafb4f45fd26e7f547f1d8 (diff)
downloadhaskell-wip/tdammers/D4394-squash.tar.gz
Cache coercion roles in NthCowip/tdammers/D4394-squash
Most callers of mkNthCo know the role of the coercion they are trying to make. So instead of calculating this role, we pass it in, forcing the caller to calculate it when needed. This introduces a performance regression in perf/compiler/T9872d.
-rw-r--r--compiler/coreSyn/CoreFVs.hs2
-rw-r--r--compiler/coreSyn/CoreLint.hs8
-rw-r--r--compiler/coreSyn/CoreOpt.hs24
-rw-r--r--compiler/coreSyn/CoreUtils.hs2
-rw-r--r--compiler/iface/TcIface.hs3
-rw-r--r--compiler/iface/ToIface.hs2
-rw-r--r--compiler/typecheck/TcCanonical.hs2
-rw-r--r--compiler/typecheck/TcEvidence.hs12
-rw-r--r--compiler/typecheck/TcTyDecls.hs2
-rw-r--r--compiler/typecheck/TcType.hs4
-rw-r--r--compiler/typecheck/TcUnify.hs4
-rw-r--r--compiler/typecheck/TcValidity.hs2
-rw-r--r--compiler/types/Coercion.hs415
-rw-r--r--compiler/types/Coercion.hs-boot2
-rw-r--r--compiler/types/FamInstEnv.hs2
-rw-r--r--compiler/types/OptCoercion.hs103
-rw-r--r--compiler/types/TyCoRep.hs39
-rw-r--r--compiler/types/Type.hs20
-rw-r--r--compiler/types/Unify.hs4
-rw-r--r--docs/core-spec/CoreLint.ott4
-rw-r--r--docs/core-spec/CoreSyn.ott6
-rw-r--r--docs/core-spec/core-spec.mng2
-rw-r--r--docs/core-spec/core-spec.pdfbin354307 -> 355707 bytes
m---------libraries/array0
-rw-r--r--testsuite/tests/perf/compiler/all.T13
-rw-r--r--testsuite/tests/perf/haddock/all.T3
-rw-r--r--testsuite/tests/pmcheck/should_compile/T11195.hs2
27 files changed, 414 insertions, 268 deletions
diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index 7fcff90c71..7e7727164c 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -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
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 78902dfea4..af888b6fb0 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1732,12 +1732,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
@@ -1751,7 +1752,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
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 04e604eb06..68b826cd7d 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -928,13 +928,13 @@ Here we implement the "push rules" from FC papers:
by pushing the coercion into the arguments
-}
-pushCoArgs :: Coercion -> [CoreArg] -> Maybe ([CoreArg], Coercion)
+pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], Coercion)
pushCoArgs co [] = return ([], co)
pushCoArgs co (arg:args) = do { (arg', co1) <- pushCoArg co arg
; (args', co2) <- pushCoArgs co1 args
; return (arg':args', co2) }
-pushCoArg :: Coercion -> CoreArg -> Maybe (CoreArg, Coercion)
+pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, 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
@@ -967,7 +967,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.
@@ -977,7 +977,7 @@ pushCoTyArg co ty
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
-- Arg of mkInstCo is always nominal, hence mkNomReflCo
-pushCoValArg :: Coercion -> Maybe (Coercion, Coercion)
+pushCoValArg :: CoercionR -> Maybe (Coercion, Coercion)
-- We have (fun |> co) arg
-- Push the coercion through to return
-- (fun (arg |> co_arg)) |> co_res
@@ -987,7 +987,7 @@ pushCoValArg co
= Just (mkRepReflCo arg, mkRepReflCo res)
| isFunTy tyL
- , (co1, co2) <- decomposeFunCo co
+ , (co1, co2) <- decomposeFunCo Representational co
-- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
-- then co1 :: tyL1 ~ tyR1
-- co2 :: tyL2 ~ tyR2
@@ -1001,7 +1001,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
-- ===>
@@ -1011,7 +1011,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
@@ -1057,7 +1057,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
@@ -1104,7 +1104,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
@@ -1112,20 +1112,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
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index 5608afc334..1e8a7304a1 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -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")
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index ca1a17dba4..1d18c125d5 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -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
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index da24d38f9e..4593c1481c 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -224,7 +224,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)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 8e6e18f917..dc85fe237c 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -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) ]
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 0930d7afd8..8c72efad05 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -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
@@ -760,11 +760,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)
-
{-
************************************************************************
@@ -792,6 +787,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
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 548f058811..2f6387ac0e 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -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'
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index f15f704f70..9758d0370d 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -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,
---------------------------------
@@ -910,7 +910,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
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b7031df093..20d281c31d 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -2175,8 +2175,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
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index d2d32c6091..7df904e7df 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1972,7 +1972,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
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 4cc8cefcea..556dd8e1c9 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -28,8 +28,8 @@ module Coercion (
mkAxInstRHS, mkUnbranchedAxInstRHS,
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
- mkSymCo, mkTransCo,
- mkNthCo, mkLRCo,
+ mkSymCo, mkTransCo, mkTransAppCo,
+ mkNthCo, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos,
mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
mkPhantomCo,
@@ -129,8 +129,7 @@ import ListSetOps
import Maybes
import UniqFM
-import Control.Monad (foldM)
-import Control.Arrow ( first )
+import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
{-
@@ -229,18 +228,23 @@ where co_rep1, co_rep2 are the coercions on the representations.
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
--
--- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
-decomposeCo :: Arity -> Coercion -> [Coercion]
-decomposeCo arity co
- = [mkNthCo n co | n <- [0..(arity-1)] ]
+-- > decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]
+decomposeCo :: Arity -> Coercion
+ -> [Role] -- the roles of the output coercions
+ -- this must have at least as many
+ -- entries as the Arity provided
+ -> [Coercion]
+decomposeCo arity co rs
+ = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
-- Remember, Nth is zero-indexed
-decomposeFunCo :: Coercion -> (Coercion, Coercion)
+decomposeFunCo :: Role -- of the input coercion
+ -> Coercion -> (Coercion, Coercion)
-- Expects co :: (s1 -> t1) ~ (s2 -> t2)
-- Returns (co1 :: s1~s2, co2 :: t1~t2)
-- See Note [Function coercions] for the "2" and "3"
-decomposeFunCo co = ASSERT2( all_ok, ppr co )
- (mkNthCo 2 co, mkNthCo 3 co)
+decomposeFunCo r co = ASSERT2( all_ok, ppr co )
+ (mkNthCo r 2 co, mkNthCo r 3 co)
where
Pair s1t1 s2t2 = coercionKind co
all_ok = isFunTy s1t1 && isFunTy s2t2
@@ -274,7 +278,7 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg
-- ty :: s2
-- need arg_co :: s2 ~ s1
-- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
- = let arg_co = mkNthCo 0 (mkSymCo co)
+ = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co)
subst' = extendTCvSubst subst kv ty
in
@@ -286,7 +290,7 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg
-- ty :: s2
-- need arg_co :: s2 ~ s1
-- res_co :: t1 ~ t2
- = let (sym_arg_co, res_co) = decomposeFunCo co
+ = let (sym_arg_co, res_co) = decomposeFunCo Nominal co
arg_co = mkSymCo sym_arg_co
in
go (arg_co : acc_arg_cos) subst res_ki tys res_co
@@ -325,10 +329,14 @@ splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- ^ Attempt to take a coercion application apart.
splitAppCo_maybe (AppCo co arg) = Just (co, arg)
splitAppCo_maybe (TyConAppCo r tc args)
- | mightBeUnsaturatedTyCon tc || args `lengthExceeds` tyConArity tc
+ | args `lengthExceeds` tyConArity tc
+ , Just (args', arg') <- snocView args
+ = Just ( mkTyConAppCo r tc args', arg' )
+
+ | mightBeUnsaturatedTyCon tc
-- Never create unsaturated type family apps!
, Just (args', arg') <- snocView args
- , Just arg'' <- setNominalRole_maybe arg'
+ , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
= Just ( mkTyConAppCo r tc args', arg'' )
-- Use mkTyConAppCo to preserve the invariant
-- that identity coercions are always represented by Refl
@@ -404,7 +412,7 @@ mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType"
-- produce a coercion @rep_co :: r1 ~ r2@.
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo co
- = mkNthCo 0 kind_co
+ = mkNthCo Nominal 0 kind_co
where
kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
-- (up to silliness with Constraint)
@@ -593,6 +601,68 @@ mkAppCos :: Coercion
-> Coercion
mkAppCos co1 cos = foldl mkAppCo co1 cos
+-- | Like `mkAppCo`, but allows the second coercion to be other than
+-- nominal. See Note [mkTransAppCo]. Role r3 cannot be more stringent
+-- than either r1 or r2.
+mkTransAppCo :: Role -- ^ r1
+ -> Coercion -- ^ co1 :: ty1a ~r1 ty1b
+ -> Type -- ^ ty1a
+ -> Type -- ^ ty1b
+ -> Role -- ^ r2
+ -> Coercion -- ^ co2 :: ty2a ~r2 ty2b
+ -> Type -- ^ ty2a
+ -> Type -- ^ ty2b
+ -> Role -- ^ r3
+ -> Coercion -- ^ :: ty1a ty2a ~r3 ty1b ty2b
+mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
+-- How incredibly fiddly! Is there a better way??
+ = case (r1, r2, r3) of
+ (_, _, Phantom)
+ -> mkPhantomCo kind_co (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
+ where -- ty1a :: k1a -> k2a
+ -- ty1b :: k1b -> k2b
+ -- ty2a :: k1a
+ -- ty2b :: k1b
+ -- ty1a ty2a :: k2a
+ -- ty1b ty2b :: k2b
+ kind_co1 = mkKindCo co1 -- :: k1a -> k2a ~N k1b -> k2b
+ kind_co = mkNthCo Nominal 1 kind_co1 -- :: k2a ~N k2b
+
+ (_, _, Nominal)
+ -> ASSERT( r1 == Nominal && r2 == Nominal )
+ mkAppCo co1 co2
+ (Nominal, Nominal, Representational)
+ -> mkSubCo (mkAppCo co1 co2)
+ (_, Nominal, Representational)
+ -> ASSERT( r1 == Representational )
+ mkAppCo co1 co2
+ (Nominal, Representational, Representational)
+ -> go (mkSubCo co1)
+ (_ , _, Representational)
+ -> ASSERT( r1 == Representational && r2 == Representational )
+ go co1
+ where
+ go co1_repr
+ | Just (tc1b, tys1b) <- splitTyConApp_maybe ty1b
+ , nextRole ty1b == r2
+ = (mkAppCo co1_repr (mkNomReflCo ty2a)) `mkTransCo`
+ (mkTyConAppCo Representational tc1b
+ (zipWith mkReflCo (tyConRolesRepresentational tc1b) tys1b
+ ++ [co2]))
+
+ | Just (tc1a, tys1a) <- splitTyConApp_maybe ty1a
+ , nextRole ty1a == r2
+ = (mkTyConAppCo Representational tc1a
+ (zipWith mkReflCo (tyConRolesRepresentational tc1a) tys1a
+ ++ [co2]))
+ `mkTransCo`
+ (mkAppCo co1_repr (mkNomReflCo ty2b))
+
+ | otherwise
+ = pprPanic "mkTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
+ , ppr r2, ppr co2, ppr ty2a, ppr ty2b
+ , ppr r3 ])
+
-- | Make a Coercion from a tyvar, a kind coercion, and a body coercion.
-- The kind of the tyvar should be the left-hand kind of the kind coercion.
mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
@@ -766,49 +836,118 @@ mkTransCo co1 (Refl {}) = co1
mkTransCo (Refl {}) co2 = co2
mkTransCo co1 co2 = TransCo co1 co2
-mkNthCo :: Int -> Coercion -> Coercion
-mkNthCo 0 (Refl _ ty)
- | Just (tv, _) <- splitForAllTy_maybe ty
- = Refl Nominal (tyVarKind tv)
-mkNthCo n (Refl r ty)
- = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
- mkReflCo r' (tyConAppArgN n ty)
- where tc = tyConAppTyCon ty
- r' = nthRole r tc n
-
- ok_tc_app :: Type -> Int -> Bool
- ok_tc_app ty n
- | Just (_, tys) <- splitTyConApp_maybe ty
- = tys `lengthExceeds` n
- | isForAllTy ty -- nth:0 pulls out a kind coercion from a hetero forall
- = n == 0
- | otherwise
- = False
-
-mkNthCo 0 (ForAllCo _ kind_co _) = kind_co
- -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
- -- then (nth 0 co :: k1 ~ k2)
-
-mkNthCo n co@(FunCo _ arg res)
- -- See Note [Function coercions]
- -- If FunCo _ arg_co res_co :: (s1:TYPE sk1 -> s2:TYPE sk2)
- -- ~ (t1:TYPE tk1 -> t2:TYPE tk2)
- -- Then we want to behave as if co was
- -- TyConAppCo argk_co resk_co arg_co res_co
- -- where
- -- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co)
- -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co)
- -- i.e. mkRuntimeRepCo
- = case n of
- 0 -> mkRuntimeRepCo arg
- 1 -> mkRuntimeRepCo res
- 2 -> arg
- 3 -> res
- _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
-
-mkNthCo n (TyConAppCo _ _ arg_cos) = arg_cos `getNth` n
-
-mkNthCo n co = NthCo n co
+mkNthCo :: HasDebugCallStack
+ => Role -- the role of the coercion you're creating
+ -> Int
+ -> Coercion
+ -> Coercion
+mkNthCo r n co
+ = ASSERT(good_call)
+ go r n co
+ where
+ Pair ty1 ty2 = coercionKind co
+
+ good_call
+ -- If the Coercion passed in is between forall-types, then the Int must
+ -- be 0 and the role must be Nominal.
+ | Just (_tv1, _) <- splitForAllTy_maybe ty1
+ , Just (_tv2, _) <- splitForAllTy_maybe ty2
+ = n == 0 && r == Nominal
+
+ -- If the Coercion passed in is between T tys and T tys', then the Int
+ -- must be less than the length of tys/tys' (which must be the same
+ -- lengths).
+ --
+ -- If the role of the Coercion is nominal, then the role passed in must
+ -- be nominal. If the role of the Coercion is representational, then the
+ -- role passed in must be tyConRolesRepresentational T !! n. If the role
+ -- of the Coercion is Phantom, then the role passed in must be Phantom.
+ --
+ -- See also Note [NthCo Cached Roles] if you're wondering why it's
+ -- blaringly obvious that we should be *computing* this role instead of
+ -- passing it in.
+ | Just (tc1, tys1) <- splitTyConApp_maybe ty1
+ , Just (tc2, tys2) <- splitTyConApp_maybe ty2
+ , tc1 == tc2
+ = let len1 = length tys1
+ len2 = length tys2
+ good_role = case coercionRole co of
+ Nominal -> r == Nominal
+ Representational -> r == (tyConRolesRepresentational tc1 !! n)
+ Phantom -> r == Phantom
+ in len1 == len2 && n < len1 && good_role
+
+ | otherwise
+ = True
+
+ go r 0 (Refl _ ty)
+ | Just (tv, _) <- splitForAllTy_maybe ty
+ = ASSERT( r == Nominal )
+ Refl r (tyVarKind tv)
+ go r n (Refl r0 ty)
+ = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
+ ASSERT( nthRole r0 tc n == r )
+ mkReflCo r (tyConAppArgN n ty)
+ where tc = tyConAppTyCon ty
+
+ ok_tc_app :: Type -> Int -> Bool
+ ok_tc_app ty n
+ | Just (_, tys) <- splitTyConApp_maybe ty
+ = tys `lengthExceeds` n
+ | isForAllTy ty -- nth:0 pulls out a kind coercion from a hetero forall
+ = n == 0
+ | otherwise
+ = False
+
+ go r 0 (ForAllCo _ kind_co _)
+ = ASSERT( r == Nominal )
+ kind_co
+ -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
+ -- then (nth 0 co :: k1 ~N k2)
+
+ go r n co@(FunCo r0 arg res)
+ -- See Note [Function coercions]
+ -- If FunCo _ arg_co res_co :: (s1:TYPE sk1 -> s2:TYPE sk2)
+ -- ~ (t1:TYPE tk1 -> t2:TYPE tk2)
+ -- Then we want to behave as if co was
+ -- TyConAppCo argk_co resk_co arg_co res_co
+ -- where
+ -- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co)
+ -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co)
+ -- i.e. mkRuntimeRepCo
+ = case n of
+ 0 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
+ 1 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
+ 2 -> ASSERT( r == r0 ) arg
+ 3 -> ASSERT( r == r0 ) res
+ _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
+
+ go r n (TyConAppCo r0 tc arg_cos) = ASSERT2( r == nthRole r0 tc n
+ , (vcat [ ppr tc
+ , ppr arg_cos
+ , ppr r0
+ , ppr n
+ , ppr r ]) )
+ arg_cos `getNth` n
+
+ go r n co =
+ NthCo r n co
+
+-- | If you're about to call @mkNthCo r n co@, then @r@ should be
+-- whatever @nthCoRole n co@ returns.
+nthCoRole :: Int -> Coercion -> Role
+nthCoRole n co
+ | Just (tc, _) <- splitTyConApp_maybe lty
+ = nthRole r tc n
+
+ | Just _ <- splitForAllTy_maybe lty
+ = Nominal
+
+ | otherwise
+ = pprPanic "nthCoRole" (ppr co)
+
+ where
+ (Pair lty _, r) = coercionKindRole co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
@@ -935,40 +1074,45 @@ mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r
-- | Converts a coercion to be nominal, if possible.
-- See Note [Role twiddling functions]
-setNominalRole_maybe :: Coercion -> Maybe Coercion
-setNominalRole_maybe co
- | Nominal <- coercionRole co = Just co
-setNominalRole_maybe (SubCo co) = Just co
-setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
-setNominalRole_maybe (TyConAppCo Representational tc cos)
- = do { cos' <- mapM setNominalRole_maybe cos
- ; return $ TyConAppCo Nominal tc cos' }
-setNominalRole_maybe (FunCo Representational co1 co2)
- = do { co1' <- setNominalRole_maybe co1
- ; co2' <- setNominalRole_maybe co2
- ; return $ FunCo Nominal co1' co2'
- }
-setNominalRole_maybe (SymCo co)
- = SymCo <$> setNominalRole_maybe co
-setNominalRole_maybe (TransCo co1 co2)
- = TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
-setNominalRole_maybe (AppCo co1 co2)
- = AppCo <$> setNominalRole_maybe co1 <*> pure co2
-setNominalRole_maybe (ForAllCo tv kind_co co)
- = ForAllCo tv kind_co <$> setNominalRole_maybe co
-setNominalRole_maybe (NthCo n co)
- = NthCo n <$> setNominalRole_maybe co
-setNominalRole_maybe (InstCo co arg)
- = InstCo <$> setNominalRole_maybe co <*> pure arg
-setNominalRole_maybe (CoherenceCo co1 co2)
- = CoherenceCo <$> setNominalRole_maybe co1 <*> pure co2
-setNominalRole_maybe (UnivCo prov _ co1 co2)
- | case prov of UnsafeCoerceProv -> True -- it's always unsafe
- PhantomProv _ -> False -- should always be phantom
- ProofIrrelProv _ -> True -- it's always safe
- PluginProv _ -> False -- who knows? This choice is conservative.
- = Just $ UnivCo prov Nominal co1 co2
-setNominalRole_maybe _ = Nothing
+setNominalRole_maybe :: Role -- of input coercion
+ -> Coercion -> Maybe Coercion
+setNominalRole_maybe r co
+ | r == Nominal = Just co
+ | otherwise = setNominalRole_maybe_helper co
+ where
+ setNominalRole_maybe_helper (SubCo co) = Just co
+ setNominalRole_maybe_helper (Refl _ ty) = Just $ Refl Nominal ty
+ setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
+ = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
+ ; return $ TyConAppCo Nominal tc cos' }
+ setNominalRole_maybe_helper (FunCo Representational co1 co2)
+ = do { co1' <- setNominalRole_maybe Representational co1
+ ; co2' <- setNominalRole_maybe Representational co2
+ ; return $ FunCo Nominal co1' co2'
+ }
+ setNominalRole_maybe_helper (SymCo co)
+ = SymCo <$> setNominalRole_maybe_helper co
+ setNominalRole_maybe_helper (TransCo co1 co2)
+ = TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
+ setNominalRole_maybe_helper (AppCo co1 co2)
+ = AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
+ setNominalRole_maybe_helper (ForAllCo tv kind_co co)
+ = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
+ setNominalRole_maybe_helper (NthCo _r n co)
+ -- NB, this case recurses via setNominalRole_maybe, not
+ -- setNominalRole_maybe_helper!
+ = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
+ setNominalRole_maybe_helper (InstCo co arg)
+ = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
+ setNominalRole_maybe_helper (CoherenceCo co1 co2)
+ = CoherenceCo <$> setNominalRole_maybe_helper co1 <*> pure co2
+ setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
+ | case prov of UnsafeCoerceProv -> True -- it's always unsafe
+ PhantomProv _ -> False -- should always be phantom
+ ProofIrrelProv _ -> True -- it's always safe
+ PluginProv _ -> False -- who knows? This choice is conservative.
+ = Just $ UnivCo prov Nominal co1 co2
+ setNominalRole_maybe_helper _ = Nothing
-- | Make a phantom coercion between two types. The coercion passed
-- in must be a nominal coercion between the kinds of the
@@ -1017,7 +1161,7 @@ ltRole Nominal _ = True
-- | like mkKindCo, but aggressively & recursively optimizes to avoid using
-- a KindCo constructor. The output role is nominal.
-promoteCoercion :: Coercion -> Coercion
+promoteCoercion :: Coercion -> CoercionN
-- First cases handles anything that should yield refl.
promoteCoercion co = case co of
@@ -1066,7 +1210,7 @@ promoteCoercion co = case co of
TransCo co1 co2
-> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
- NthCo n co1
+ NthCo _ n co1
| Just (_, args) <- splitTyConAppCo_maybe co1
, args `lengthExceeds` n
-> promoteCoercion (args !! n)
@@ -1109,22 +1253,22 @@ promoteCoercion co = case co of
-- where @g' = promoteCoercion (h w)@.
-- fails if this is not possible, if @g@ coerces between a forall and an ->
-- or if second parameter has a representational role and can't be used
--- with an InstCo. The result role matches is representational.
+-- with an InstCo.
instCoercion :: Pair Type -- type of the first coercion
- -> Coercion -- ^ must be nominal
+ -> CoercionN -- ^ must be nominal
-> Coercion
- -> Maybe Coercion
+ -> Maybe CoercionN
instCoercion (Pair lty rty) g w
| isForAllTy lty && isForAllTy rty
- , Just w' <- setNominalRole_maybe w
+ , Just w' <- setNominalRole_maybe (coercionRole w) w
= Just $ mkInstCo g w'
| isFunTy lty && isFunTy rty
- = Just $ mkNthCo 3 g -- extract result type, which is the 4th argument to (->)
+ = Just $ mkNthCo Nominal 3 g -- extract result type, which is the 4th argument to (->)
| otherwise -- one forall, one funty...
= Nothing
- where
-instCoercions :: Coercion -> [Coercion] -> Maybe Coercion
+-- | Repeated use of 'instCoercion'
+instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
instCoercions g ws
= let arg_ty_pairs = map coercionKind ws in
snd <$> foldM go (coercionKind g, g) (zip arg_ty_pairs ws)
@@ -1153,22 +1297,26 @@ mkPiCo :: Role -> Var -> Coercion -> Coercion
mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
| otherwise = mkFunCo r (mkReflCo r (varType v)) co
--- The second coercion is sometimes lifted (~) and sometimes unlifted (~#).
--- So, we have to make sure to supply the right parameter to decomposeCo.
--- mkCoCast (c :: s1 ~# t1) (g :: (s1 ~# s2) ~# (t1 ~# t2)) :: s2 ~# t2
--- Both coercions *must* have the same role.
-mkCoCast :: Coercion -> Coercion -> Coercion
+-- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
+-- The first coercion might be lifted or unlifted; thus the ~? above
+-- Lifted and unlifted equalities take different numbers of arguments,
+-- so we have to make sure to supply the right parameter to decomposeCo.
+-- Also, note that the role of the first coercion is the same as the role of
+-- the equalities related by the second coercion. The second coercion is
+-- itself always representational.
+mkCoCast :: Coercion -> CoercionR -> Coercion
mkCoCast c g
+ | (g2:g1:_) <- reverse co_list
= mkSymCo g1 `mkTransCo` c `mkTransCo` g2
+
+ | otherwise
+ = pprPanic "mkCoCast" (ppr g $$ ppr (coercionKind g))
where
- -- g :: (s1 ~# s2) ~# (t1 ~# t2)
- -- g1 :: s1 ~# t1
- -- g2 :: s2 ~# t2
- (_, args) = splitTyConApp (pFst $ coercionKind g)
- n_args = length args
- co_list = decomposeCo n_args g
- g1 = co_list `getNth` (n_args - 2)
- g2 = co_list `getNth` (n_args - 1)
+ -- g :: (s1 ~# t1) ~# (s2 ~# t2)
+ -- g1 :: s1 ~# s2
+ -- g2 :: t1 ~# t2
+ (tc, _) = splitTyConApp (pFst $ coercionKind g)
+ co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
{-
%************************************************************************
@@ -1614,7 +1762,7 @@ seqCo (UnivCo p r t1 t2)
= seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
-seqCo (NthCo n co) = n `seq` seqCo co
+seqCo (NthCo r n co) = r `seq` n `seq` seqCo co
seqCo (LRCo lr co) = lr `seq` seqCo co
seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
seqCo (CoherenceCo co1 co2) = seqCo co1 `seq` seqCo co2
@@ -1698,7 +1846,7 @@ coercionKind co =
go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
go (SymCo co) = swap $ go co
go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
- go g@(NthCo d co)
+ go g@(NthCo _ d co)
| Just argss <- traverse tyConAppArgs_maybe tys
= ASSERT( and $ (`lengthExceeds` d) <$> argss )
(`getNth` d) <$> argss
@@ -1755,8 +1903,6 @@ substitute for them all at once. Remarkably, for Trac #11735 this single
change reduces /total/ compile time by a factor of more than ten.
-}
-=======
->>>>>>> Applying patch suggested in #11735 to improve coercionKind perf
-- | Apply 'coercionKind' to multiple 'Coercion's
coercionKinds :: [Coercion] -> Pair [Type]
@@ -1776,41 +1922,20 @@ coercionRole = go
go (AppCo co1 _) = go co1
go (ForAllCo _ _ co) = go co
go (FunCo r _ _) = r
- go (CoVarCo cv) = go_var cv
- go (HoleCo h) = go_var (coHoleCoVar h)
+ go (CoVarCo cv) = coVarRole cv
+ go (HoleCo h) = coVarRole (coHoleCoVar h)
go (AxiomInstCo ax _ _) = coAxiomRole ax
go (UnivCo _ r _ _) = r
go (SymCo co) = go co
- go (TransCo co1 co2) = go co1
- go (NthCo d co)
- | Just (tv1, _) <- splitForAllTy_maybe ty1
- = ASSERT( d == 0 )
- Nominal
-
- | otherwise
- = let (tc1, args1) = splitTyConApp ty1
- (_tc2, args2) = splitTyConApp ty2
- in
- ASSERT2( tc1 == _tc2, ppr d $$ ppr tc1 $$ ppr _tc2 )
- (nthRole r tc1 d)
-
- where
- (Pair ty1 ty2, r) = coercionKindRole co
+ go (TransCo co1 _co2) = go co1
+ go (NthCo r _d _co) = r
go (LRCo {}) = Nominal
- go (InstCo co arg) = go_app co
+ go (InstCo co _) = go co
go (CoherenceCo co1 _) = go co1
go (KindCo {}) = Nominal
go (SubCo _) = Representational
go (AxiomRuleCo ax _) = coaxrRole ax
- -------------
- go_var = coVarRole
-
- -------------
- go_app :: Coercion -> Role
- go_app (InstCo co arg) = go_app co
- go_app co = go co
-
{-
Note [Nested InstCos]
~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index 1508e6fb10..e607c88a84 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -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
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 732a0957db..8f3279ed80 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -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
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 11aeb932cc..0fa15f6d3e 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -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
@@ -435,62 +466,6 @@ opt_univ env sym prov role oty1 oty2
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
@@ -985,7 +962,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) )
@@ -1028,7 +1005,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
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 95c2e0a26b..abc932ce73 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -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:
@@ -1571,7 +1592,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
@@ -1634,7 +1655,7 @@ coVarsOfCo (AxiomInstCo _ _ as) = coVarsOfCos as
coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2]
coVarsOfCo (SymCo co) = coVarsOfCo co
coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
-coVarsOfCo (NthCo _ co) = coVarsOfCo co
+coVarsOfCo (NthCo _ _ co) = coVarsOfCo co
coVarsOfCo (LRCo _ co) = coVarsOfCo co
coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg
coVarsOfCo (CoherenceCo c1 c2) = coVarsOfCos [c1, c2]
@@ -1741,7 +1762,7 @@ noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p &&
noFreeVarsOfType t2
noFreeVarsOfCo (SymCo co) = noFreeVarsOfCo co
noFreeVarsOfCo (TransCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
-noFreeVarsOfCo (NthCo _ co) = noFreeVarsOfCo co
+noFreeVarsOfCo (NthCo _ _ co) = noFreeVarsOfCo co
noFreeVarsOfCo (LRCo _ co) = noFreeVarsOfCo co
noFreeVarsOfCo (InstCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
noFreeVarsOfCo (CoherenceCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
@@ -2410,7 +2431,7 @@ subst_co subst co
(go_ty t1)) $! (go_ty t2)
go (SymCo co) = mkSymCo $! (go co)
go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
- go (NthCo d co) = mkNthCo d $! (go co)
+ go (NthCo r d co) = mkNthCo r d $! (go co)
go (LRCo lr co) = mkLRCo lr $! (go co)
go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
go (CoherenceCo co1 co2) = (mkCoherenceCo $! (go co1)) $! (go co2)
@@ -3010,7 +3031,7 @@ tidyCo env@(_, subst) co
tidyType env t1) $! tidyType env t2
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
- go (NthCo d co) = NthCo d $! go co
+ go (NthCo r d co) = NthCo r d $! go co
go (LRCo lr co) = LRCo lr $! go co
go (InstCo co ty) = (InstCo $! go co) $! go ty
go (CoherenceCo co1 co2) = (CoherenceCo $! go co1) $! go co2
@@ -3069,7 +3090,7 @@ coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
-coercionSize (NthCo _ co) = 1 + coercionSize co
+coercionSize (NthCo _ _ co) = 1 + coercionSize co
coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg
coercionSize (CoherenceCo c1 c2) = 1 + coercionSize c1 + coercionSize c2
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index c274116864..e599012925 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -30,7 +30,7 @@ module Type (
mkTyConApp, mkTyConTy,
tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
- splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
+ splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
splitListTyConApp_maybe,
repSplitTyConApp_maybe,
@@ -423,8 +423,8 @@ expandTypeSynonyms ty
= mkSymCo (go_co subst co)
go_co subst (TransCo co1 co2)
= mkTransCo (go_co subst co1) (go_co subst co2)
- go_co subst (NthCo n co)
- = mkNthCo n (go_co subst co)
+ go_co subst (NthCo r n co)
+ = mkNthCo r n (go_co subst co)
go_co subst (LRCo lr co)
= mkLRCo lr (go_co subst co)
go_co subst (InstCo co arg)
@@ -560,7 +560,7 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
go (SymCo co) = mksymco <$> go co
go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
- go (NthCo i co) = mknthco i <$> go co
+ go (NthCo r i co) = mknthco r i <$> go co
go (LRCo lr co) = mklrco lr <$> go co
go (InstCo co arg) = mkinstco <$> go co <*> go arg
go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
@@ -1140,6 +1140,16 @@ splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
Just (tc,[e]) | tc == listTyCon -> Just e
_other -> Nothing
+nextRole :: Type -> Role
+nextRole ty
+ | Just (tc, tys) <- splitTyConApp_maybe ty
+ , let num_tys = length tys
+ , num_tys < tyConArity tc
+ = tyConRoles tc `getNth` num_tys
+
+ | otherwise
+ = Nominal
+
newTyConInstRhs :: TyCon -> [Type] -> Type
-- ^ Unwrap one 'layer' of newtype on a type constructor and its
-- arguments, using an eta-reduced version of the @newtype@ if possible.
@@ -2380,7 +2390,7 @@ tyConsOfType ty
go_co (HoleCo {}) = emptyUniqSet
go_co (SymCo co) = go_co co
go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
- 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 `unionUniqSets` go_co arg
go_co (CoherenceCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 34f2fac56b..46cd84f2cd 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -862,7 +862,7 @@ type AmIUnifying = Bool -- True <=> Unifying
unify_ty :: UMEnv
-> Type -> Type -- Types to be unified and a co
- -> Coercion -- A coercion between their kinds
+ -> CoercionN -- A coercion between their kinds
-- See Note [Kind coercions in Unify]
-> UM ()
-- See Note [Specification of unification]
@@ -954,7 +954,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
, not (cv `elemVarEnv` c_subst)
, BindMe <- tvBindFlag env cv
-> do { checkRnEnv env (tyCoVarsOfCo co2)
- ; let (co_l, co_r) = decomposeFunCo kco
+ ; let (co_l, co_r) = decomposeFunCo Nominal kco
-- cv :: t1 ~ t2
-- co2 :: s1 ~ s2
-- co_l :: t1 ~ s1
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 3a3468d53b..d18525a028 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -300,11 +300,11 @@ not (si is_a_coercion)
not (ti is_a_coercion)
R' = (tyConRolesX R T)[i]
---------------------- :: NthCoTyCon
-G |-co nth i g : si k2~R' k2' ti
+G |-co nth R' i g : si k2~R' k2' ti
G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2)
--------------------------- :: NthCoForAll
-G |-co nth 0 g : k1 *~Nom * k2
+G |-co nth Nom 0 g : k1 *~Nom * k2
G |-co g : (s1 s2) k~Nom k' (t1 t2)
G |-ty s1 : k1
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 78118d532c..e12f68ba4f 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -152,8 +152,8 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| g1 ; g2 :: :: TransCo {{ com \ctor{TransCo}: Transitivity }}
| mu </ ti // i /> $ </ gj // j />
:: :: AxiomRuleCo {{ com \ctor{AxiomRuleCo}: Axiom-rule application (for type-nats) }}
- | nth I g :: :: NthCo {{ com \ctor{NthCo}: Projection (0-indexed) }}
- {{ tex \textsf{nth}^{[[I]]}\,[[g]] }}
+ | nth R I g :: :: NthCo {{ com \ctor{NthCo}: Projection (0-indexed) }}
+ {{ tex \textsf{nth}^{[[I]]}_{[[R]]}\,[[g]] }}
| LorR g :: :: LRCo {{ com \ctor{LRCo}: Left/right projection }}
| g @ h :: :: InstCo {{ com \ctor{InstCo}: Instantiation }}
| g |> h :: :: CoherenceCo {{ com \ctor{CoherenceCo}: Coherence }}
@@ -453,6 +453,8 @@ formula :: 'formula_' ::=
| role_list1 = role_list2 :: :: eq_role_list
| R1 /= R2 :: :: role_neq
| R1 = R2 :: :: eq_role
+ | R1 <= R2 :: :: lte_role
+ {{ tex [[R1]] \leq [[R2]] }}
| </ Ki // i /> = tyConDataCons T :: :: tyConDataCons
| O ( n ) = R :: :: role_lookup
| R elt role_list :: :: role_elt
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 580032129d..64e90bb7d0 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -30,7 +30,7 @@ System FC, as implemented in GHC\footnote{This
document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
but it should be maintained by anyone who edits the functions or data structures
mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large 23 October, 2015
+\Large 26 January, 2018
\end{center}
\section{Introduction}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 1e139115cd..3732818e2e 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
Binary files differ
diff --git a/libraries/array b/libraries/array
-Subproject 1d0435f4937f03901e32304e279f46ce19b0f08
+Subproject 9d63218fd067ff4885c0efa43b388238421a5c8
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 09251059dd..ba36b4197e 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -476,12 +476,13 @@ test('parsing001',
[(wordsize(32), 232777056, 10),
# Initial: 274000576
# 2017-03-24: 232777056
- (wordsize(64), 490228304, 5)]),
+ (wordsize(64), 519401296, 5)]),
# expected value: 587079016 (amd64/Linux)
# 2016-09-01: 581551384 (amd64/Linux) Restore w/w limit (#11565)
# 2016-12-19: 493730288 (amd64/Linux) Join points (#12988)
# 2017-02-14: 463931280 Early inlining patch; acutal improvement 7%
# 2017-12-11: 490228304 BlockArguments
+ # 2018-04-09: 519401296 Inexplicable, collateral of #14737
only_ways(['normal']),
],
compile_fail, [''])
@@ -549,6 +550,9 @@ test('T5321Fun',
# 2016-04-06: 279922360 x86/Linux
# 2017-03-24: 244387620 x86/Linux (64-bit machine)
+ (platform('x86_64-apple-darwin'), 446893600, 5),
+ # 2018-03-17: 423774560 # OS X-only (reason unknown, see #11753)
+
(wordsize(64), 423774560, 5)])
# prev: 585521080
# 2012-08-29: 713385808 # (increase due to new codegen)
@@ -882,7 +886,7 @@ test('T9872c',
test('T9872d',
[ only_ways(['normal']),
compiler_stats_num_field('bytes allocated',
- [(wordsize(64), 526485920, 5),
+ [(wordsize(64), 572537984, 5),
# 2014-12-18 796071864 Initally created
# 2014-12-18 739189056 Reduce type families even more eagerly
# 2015-01-07 687562440 TrieMap leaf compression
@@ -896,6 +900,7 @@ test('T9872d',
# 2017-02-25 498855104 Early inlining
# 2017-03-03 462817352 Share Typeable KindReps
# 2018-03-25 526485920 Flattener patch does more work (#12919)
+ # 2018-04-11 572537984 simplCast improvement collateral (#11735)
(wordsize(32), 232954000, 5)
# some date 328810212
@@ -1230,7 +1235,9 @@ test('T14697',
test('T14683',
[ compiler_stats_num_field('bytes allocated',
- [(wordsize(64), 25189145632, 10),
+ [(wordsize(64), 14675353056, 10),
+ # initial: 25189145632
+ # 2018-04-19: 14675353056 Cache NthCo role (#14683)
]),
],
multimod_compile,
diff --git a/testsuite/tests/perf/haddock/all.T b/testsuite/tests/perf/haddock/all.T
index db378fe178..09ed19a303 100644
--- a/testsuite/tests/perf/haddock/all.T
+++ b/testsuite/tests/perf/haddock/all.T
@@ -10,7 +10,7 @@ test('haddock.base',
# 2017-02-19 24286343184 (x64/Windows) - Generalize kind of (->)
# 2017-12-24 18733710728 (x64/Windows) - Unknown
- ,(wordsize(64), 19694554424, 5)
+ ,(wordsize(64), 20727464616, 5)
# 2012-08-14: 5920822352 (amd64/Linux)
# 2012-09-20: 5829972376 (amd64/Linux)
# 2012-10-08: 5902601224 (amd64/Linux)
@@ -44,6 +44,7 @@ test('haddock.base',
# 2017-06-06: 25173968808 (x86_64/Linux) - Don't pass on -dcore-lint in Haddock.mk
# 2017-07-12: 23677299848 (x86_64/Linux) - Use getNameToInstancesIndex
# 2017-08-22: 19694554424 (x86_64/Linux) - Various Haddock optimizations
+ # 2018-04-11: 20727464616 (x86_64/Linux) - Collateral of simplCast improvement (#14737)
,(platform('i386-unknown-mingw32'), 2885173512, 5)
# 2013-02-10: 3358693084 (x86/Windows)
diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs
index 236932e86f..0c35b4fd27 100644
--- a/testsuite/tests/pmcheck/should_compile/T11195.hs
+++ b/testsuite/tests/pmcheck/should_compile/T11195.hs
@@ -62,7 +62,7 @@ opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
-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
, co1 `compatible_co` co2 = undefined