Cache coercion roles in NthCo wip/tdammers/D4394-squash
authorTobias Dammers <tdammers@gmail.com>
Thu, 25 Jan 2018 19:33:58 +0000 (20:33 +0100)
committerTobias Dammers <tdammers@gmail.com>
Fri, 20 Apr 2018 08:33:00 +0000 (10:33 +0200)
Most callers of mkNthCo know the role of the coercion they
are trying to make. So instead of calculating this role, we
pass it in, forcing the caller to calculate it when needed.

This introduces a performance regression in perf/compiler/T9872d.

27 files changed:
compiler/coreSyn/CoreFVs.hs
compiler/coreSyn/CoreLint.hs
compiler/coreSyn/CoreOpt.hs
compiler/coreSyn/CoreUtils.hs
compiler/iface/TcIface.hs
compiler/iface/ToIface.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcTyDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Coercion.hs
compiler/types/Coercion.hs-boot
compiler/types/FamInstEnv.hs
compiler/types/OptCoercion.hs
compiler/types/TyCoRep.hs
compiler/types/Type.hs
compiler/types/Unify.hs
docs/core-spec/CoreLint.ott
docs/core-spec/CoreSyn.ott
docs/core-spec/core-spec.mng
docs/core-spec/core-spec.pdf
libraries/array
testsuite/tests/perf/compiler/all.T
testsuite/tests/perf/haddock/all.T
testsuite/tests/pmcheck/should_compile/T11195.hs

index 7fcff90..7e77271 100644 (file)
@@ -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
index 78902df..af888b6 100644 (file)
@@ -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
index 04e604e..68b826c 100644 (file)
@@ -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
 
index 5608afc..1e8a730 100644 (file)
@@ -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")
index ca1a17d..1d18c12 100644 (file)
@@ -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
index da24d38..4593c14 100644 (file)
@@ -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)
index 8e6e18f..dc85fe2 100644 (file)
@@ -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 i ev_co )
                              | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
                              , r /= Phantom
                              , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
index 0930d7a..8c72efa 100644 (file)
@@ -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
index 548f058..2f6387a 100644 (file)
@@ -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'
index f15f704..9758d03 100644 (file)
@@ -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
index b7031df..20d281c 100644 (file)
@@ -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 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
index d2d32c6..7df904e 100644 (file)
@@ -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
index 4cc8cef..556dd8e 100644 (file)
@@ -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 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]
 ~~~~~~~~~~~~~~~~~~~~~
index 1508e6f..e607c88 100644 (file)
@@ -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
index 732a095..8f3279e 100644 (file)
@@ -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
index 11aeb93..0fa15f6 100644 (file)
@@ -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
index 95c2e0a..abc932c 100644 (file)
@@ -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 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
index c274116..e599012 100644 (file)
@@ -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 n co)
+      = mkNthCo 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
index 34f2fac..46cd84f 100644 (file)
@@ -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
index 3a3468d..d18525a 100644 (file)
@@ -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
index 78118d5..e12f68b 100644 (file)
@@ -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
index 5800321..64e90bb 100644 (file)
@@ -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}
index 1e13911..3732818 100644 (file)
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ
index 1d0435f..9d63218 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 1d0435f4937f03901e32304e279f46ce19b0f089
+Subproject commit 9d63218fd067ff4885c0efa43b388238421a5c89
index 0925105..ba36b41 100644 (file)
@@ -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,
index db378fe..09ed19a 100644 (file)
@@ -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)
index 236932e..0c35b4f 100644 (file)
@@ -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