diff options
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 Binary files differindex 1e139115cd..3732818e2e 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf 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 |