Tighten cached role in NthCowip/tdammers/T11735

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