From 1146825a3f59da1f88401d61380328806b5b2c07 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Mon, 12 Feb 2018 13:02:23 -0500 Subject: Tighten cached role in NthCo --- compiler/backpack/RnModIface.hs | 2 +- compiler/coreSyn/CoreLint.hs | 9 +-- compiler/coreSyn/CoreUtils.hs | 2 +- compiler/iface/IfaceSyn.hs | 2 +- compiler/iface/IfaceType.hs | 14 ++-- compiler/iface/TcIface.hs | 3 +- compiler/iface/ToIface.hs | 2 +- compiler/typecheck/TcEvidence.hs | 2 +- compiler/types/Coercion.hs | 158 +++++++++++++++++++++++++-------------- compiler/types/Coercion.hs-boot | 2 +- compiler/types/OptCoercion.hs | 23 ++---- compiler/types/TyCoRep.hs | 5 +- docs/core-spec/CoreLint.ott | 5 +- 13 files changed, 131 insertions(+), 98 deletions(-) diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index e26b4a5d4a..c52fce772d 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -665,7 +665,7 @@ rnIfaceCo (IfaceTransCo c1 c2) = IfaceTransCo <$> rnIfaceCo c1 <*> rnIfaceCo c2 rnIfaceCo (IfaceInstCo c1 c2) = IfaceInstCo <$> rnIfaceCo c1 <*> rnIfaceCo c2 -rnIfaceCo (IfaceNthCo r d c) = IfaceNthCo r d <$> rnIfaceCo c +rnIfaceCo (IfaceNthCo d c) = IfaceNthCo d <$> rnIfaceCo c rnIfaceCo (IfaceLRCo lr c) = IfaceLRCo lr <$> rnIfaceCo c rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c rnIfaceCo (IfaceAxiomRuleCo ax cos) diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index d1d912bea3..00f9595ff1 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1736,7 +1736,8 @@ lintCoercion the_co@(NthCo r0 n 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, r0) -- NB: any role for r is OK here. + -> do { lintRole the_co Nominal r0 + ; return (ks, kt, ts, tt, r0) } where ts = tyVarKind tv_s tt = tyVarKind tv_t @@ -1750,11 +1751,7 @@ lintCoercion the_co@(NthCo r0 n co) -- see Note [NthCo and newtypes] in TyCoRep , tys_s `equalLength` tys_t , tys_s `lengthExceeds` n - -> do { lintL (tr `lteRole` r0) - (vcat [ text "Role mismatch in NthCo" - , text "NthCo has role" <+> ppr r0 - , text "but needs to be greater than" <+> ppr tr - , text "Coercion:" <+> ppr the_co ]) + -> do { lintRole the_co tr r0 ; return (ks, kt, ts, tt, r0) } where ts = getNth tys_s n diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs index 6644c185a4..ba68c512c3 100644 --- a/compiler/coreSyn/CoreUtils.hs +++ b/compiler/coreSyn/CoreUtils.hs @@ -268,7 +268,7 @@ mkCast (Coercion e_co) co -- The guard here checks that g has a (~#) on both sides, -- otherwise decomposeCo fails. Can in principle happen -- with unsafeCoerce - = Coercion (mkCoCast Representational e_co co) + = Coercion (mkCoCast e_co co) mkCast (Cast expr co2) co = WARN(let { Pair from_ty _to_ty = coercionKind co; diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 8b82e84118..9afd2b8191 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -1446,7 +1446,7 @@ freeNamesIfCoercion (IfaceSymCo c) = freeNamesIfCoercion c freeNamesIfCoercion (IfaceTransCo c1 c2) = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2 -freeNamesIfCoercion (IfaceNthCo _ _ co) +freeNamesIfCoercion (IfaceNthCo _ co) = freeNamesIfCoercion co freeNamesIfCoercion (IfaceLRCo _ co) = freeNamesIfCoercion co diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index dbdf075c4e..62b33cd100 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -260,7 +260,7 @@ data IfaceCoercion | IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType | IfaceSymCo IfaceCoercion | IfaceTransCo IfaceCoercion IfaceCoercion - | IfaceNthCo Role Int IfaceCoercion + | IfaceNthCo Int IfaceCoercion | IfaceLRCo LeftOrRight IfaceCoercion | IfaceInstCo IfaceCoercion IfaceCoercion | IfaceCoherenceCo IfaceCoercion IfaceCoercion @@ -420,7 +420,7 @@ substIfaceType env ty go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2) go_co (IfaceSymCo co) = IfaceSymCo (go_co co) go_co (IfaceTransCo co1 co2) = IfaceTransCo (go_co co1) (go_co co2) - go_co (IfaceNthCo r n co) = IfaceNthCo r n (go_co co) + go_co (IfaceNthCo n co) = IfaceNthCo n (go_co co) go_co (IfaceLRCo lr co) = IfaceLRCo lr (go_co co) go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2) go_co (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo (go_co c1) (go_co c2) @@ -1103,8 +1103,8 @@ ppr_co ctxt_prec (IfaceSymCo co) ppr_co ctxt_prec (IfaceTransCo co1 co2) = maybeParen ctxt_prec TyOpPrec $ ppr_co TyOpPrec co1 <+> semi <+> ppr_co TyOpPrec co2 -ppr_co ctxt_prec (IfaceNthCo r d co) - = ppr_special_co ctxt_prec (text "Nth:" <> int d <> ppr_role r) [co] +ppr_co ctxt_prec (IfaceNthCo d co) + = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co] ppr_co ctxt_prec (IfaceLRCo lr co) = ppr_special_co ctxt_prec (ppr lr) [co] ppr_co ctxt_prec (IfaceSubCo co) @@ -1386,11 +1386,10 @@ instance Binary IfaceCoercion where putByte bh 10 put_ bh a put_ bh b - put_ bh (IfaceNthCo a b c) = do + put_ bh (IfaceNthCo a b) = do putByte bh 11 put_ bh a put_ bh b - put_ bh c put_ bh (IfaceLRCo a b) = do putByte bh 12 put_ bh a @@ -1458,8 +1457,7 @@ instance Binary IfaceCoercion where return $ IfaceTransCo a b 11-> do a <- get bh b <- get bh - c <- get bh - return $ IfaceNthCo a b c + return $ IfaceNthCo a b 12-> do a <- get bh b <- get bh return $ IfaceLRCo a b diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index 790ca9c65a..dfd30466b7 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 r d c) = mkNthCo r 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 bb326cb7f0..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 r d co) = IfaceNthCo r 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/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 29d884be82..e6d474db2f 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -794,7 +794,7 @@ evTermCoercion :: EvTerm -> TcCoercion -- See Note [Coercion evidence terms] evTermCoercion (EvId v) = mkCoVarCo v evTermCoercion (EvCoercion co) = co -evTermCoercion (EvCast tm co) = mkCoCast Representational (evTermCoercion tm) co +evTermCoercion (EvCast tm co) = mkCoCast (evTermCoercion tm) co evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm) evVarsOfTerm :: EvTerm -> VarSet diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 530fedef0d..4f653cce78 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -29,7 +29,7 @@ module Coercion ( mkAxInstLHS, mkUnbranchedAxInstLHS, mkPiCo, mkPiCos, mkCoCast, mkSymCo, mkTransCo, mkTransAppCo, - mkNthCo, mkLRCo, + mkNthCo, nthCoRole, mkLRCo, mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos, mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl, mkPhantomCo, @@ -128,7 +128,7 @@ import ListSetOps import Maybes import UniqFM -import Control.Monad (foldM) +import Control.Monad (foldM, zipWithM) import Data.Function ( on ) {- @@ -269,10 +269,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 @@ -807,16 +811,27 @@ mkTransCo co1 (Refl {}) = co1 mkTransCo (Refl {}) co2 = co2 mkTransCo co1 co2 = TransCo co1 co2 -mkNthCo :: Role -- the role of the coercion you're creating - -- This might be a super-role of what is required would return - -- that is, the role can be Rep even though Nom would be allowed +mkNthCo :: HasDebugCallStack + => Role -- the role of the coercion you're creating -> Int -> Coercion -> Coercion +-- If the Coercion passed in is between forall-types, then the Int must +-- be 0 and the role must be 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. mkNthCo r 0 (Refl _ ty) | Just (tv, _) <- splitForAllTy_maybe ty - = Refl r (tyVarKind tv) + = ASSERT( r == Nominal ) + Refl r (tyVarKind tv) mkNthCo r n (Refl r0 ty) = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty ) - ASSERT( nthRole r0 tc n `lteRole` r ) + ASSERT( nthRole r0 tc n == r ) mkReflCo r (tyConAppArgN n ty) where tc = tyConAppTyCon ty @@ -830,9 +845,10 @@ mkNthCo r n (Refl r0 ty) = False mkNthCo r 0 (ForAllCo _ kind_co _) - = downgradeRole r Nominal kind_co + = ASSERT( r == Nominal ) + kind_co -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2) - -- then (nth 0 co :: k1 ~ k2) + -- then (nth 0 co :: k1 ~N k2) mkNthCo r n co@(FunCo r0 arg res) -- See Note [Function coercions] @@ -845,17 +861,39 @@ mkNthCo r n co@(FunCo r0 arg res) -- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co) -- i.e. mkRuntimeRepCo = case n of - 0 -> mkRuntimeRepCo arg - 1 -> mkRuntimeRepCo res - 2 -> ASSERT( r0 `lteRole` r ) arg - 3 -> ASSERT( r0 `lteRole` r ) res + 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) -mkNthCo _r n (TyConAppCo _ _ arg_cos) = arg_cos `getNth` n +mkNthCo 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 mkNthCo 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)) mkLRCo lr co = LRCo lr co @@ -981,40 +1019,41 @@ 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 +setNominalRole_maybe :: Role -- of input coercion + -> Coercion -> Maybe Coercion +setNominalRole_maybe r co + | r == Nominal = Just co +setNominalRole_maybe _ (SubCo co) = Just co +setNominalRole_maybe _ (Refl _ ty) = Just $ Refl Nominal ty +setNominalRole_maybe _ (TyConAppCo Representational tc cos) + = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos ; return $ TyConAppCo Nominal tc cos' } -setNominalRole_maybe (FunCo Representational co1 co2) - = do { co1' <- setNominalRole_maybe co1 - ; co2' <- setNominalRole_maybe co2 +setNominalRole_maybe _ (FunCo Representational co1 co2) + = do { co1' <- setNominalRole_maybe Representational co1 + ; co2' <- setNominalRole_maybe Representational 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 r n co) - = NthCo r 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) +setNominalRole_maybe r (SymCo co) + = SymCo <$> setNominalRole_maybe r co +setNominalRole_maybe r (TransCo co1 co2) + = TransCo <$> setNominalRole_maybe r co1 <*> setNominalRole_maybe r co2 +setNominalRole_maybe r (AppCo co1 co2) + = AppCo <$> setNominalRole_maybe r co1 <*> pure co2 +setNominalRole_maybe r (ForAllCo tv kind_co co) + = ForAllCo tv kind_co <$> setNominalRole_maybe r co +setNominalRole_maybe _ (NthCo _r n co) + = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co +setNominalRole_maybe r (InstCo co arg) + = InstCo <$> setNominalRole_maybe r co <*> pure arg +setNominalRole_maybe r (CoherenceCo co1 co2) + = CoherenceCo <$> setNominalRole_maybe r 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 _ _ = Nothing -- | Make a phantom coercion between two types. The coercion passed -- in must be a nominal coercion between the kinds of the @@ -1167,7 +1206,7 @@ instCoercion :: Pair Type -- type of the first 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 Nominal 3 g -- extract result type, which is the 4th argument to (->) @@ -1204,20 +1243,29 @@ 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, passed in. -mkCoCast :: Role -> Coercion -> Coercion -> Coercion -mkCoCast r c g +-- 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 = mkSymCo g1 `mkTransCo` c `mkTransCo` g2 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 (repeat r) + -- g :: (s1 ~# t1) ~# (s2 ~# t2) + -- g1 :: s1 ~# s2 + -- g2 :: t1 ~# t2 + (tc, _) = splitTyConApp (pFst $ coercionKind g) + (n_args, role) + | tc `hasKey` eqPrimTyConKey = (4, Nominal) + | tc `hasKey` eqReprPrimTyConKey = (4, Representational) + | tc `hasKey` eqTyConKey = (3, Nominal) + | tc `hasKey` heqTyConKey = (4, Nominal) + | tc `hasKey` coercibleTyConKey = (3, Representational) + | otherwise = pprPanic "mkCoCast" (ppr g $$ ppr coercionKind g) + co_list = decomposeCo n_args g (replicate (n_args - 2) Nominal ++ repeat role) g1 = co_list `getNth` (n_args - 2) g2 = co_list `getNth` (n_args - 1) diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot index 0bc9984ea5..e9e2510147 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 :: Role -> 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/OptCoercion.hs b/compiler/types/OptCoercion.hs index 9804f7a816..a0cea12b88 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -277,12 +277,9 @@ opt_co4 env _sym rep r (NthCo _r n (Refl _r2 ty)) , Just (tv, _) <- splitForAllTy_maybe ty = liftCoSubst (chooseRole rep r) env (tyVarKind tv) -opt_co4 env sym rep r (NthCo _r n (TyConAppCo r2 tc cos)) - = ASSERT( r == _r ) - ASSERT( r3 /= Phantom ) - opt_co4_wrap env sym rep r3 (cos `getNth` n) - where - r3 = nthRole r2 tc n +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 ) @@ -290,26 +287,22 @@ opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _)) opt_co4_wrap env sym rep Nominal eta opt_co4 env sym rep r (NthCo _r n co) - | TyConAppCo r2 tc cos <- co' - , let nth_co = cos `getNth` n - nth_co_role = nthRole r2 tc n - = if rep' && (nth_co_role == Nominal) + | 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' + = if rep then opt_co4_wrap (zapLiftingContext env) False True Nominal eta else eta | otherwise - = if rep' - then NthCo Representational n co' - else NthCo Nominal n co' + = wrapRole rep r $ NthCo r n co' where co' = opt_co1 env sym co - rep' = rep || r == Representational opt_co4 env sym rep r (LRCo lr co) | Just pr_co <- splitAppCo_maybe co diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 9df407a586..29d169338f 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -825,13 +825,10 @@ data Coercion | AxiomRuleCo CoAxiomRule [Coercion] | NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn) - -- :: "e" _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles]) + -- :: "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] -- See Note [NthCo Cached Roles] - -- The Role might be more permissive than otherwise possible. That is, even - -- if the Coercion inside is Nominal, the role could be Representational - -- (it's like using a SubCo) | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right) -- :: _ -> N -> N diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 1fb9e09559..d18525a028 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -299,13 +299,12 @@ G |-ty ti : k2' not (si is_a_coercion) not (ti is_a_coercion) R' = (tyConRolesX R T)[i] -R' <= R0 ---------------------- :: NthCoTyCon -G |-co nth R0 i g : si k2~R0 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 R0 0 g : k1 *~R0 * k2 +G |-co nth Nom 0 g : k1 *~Nom * k2 G |-co g : (s1 s2) k~Nom k' (t1 t2) G |-ty s1 : k1 -- cgit v1.2.1