Coercion Quantification
[ghc.git] / compiler / types / OptCoercion.hs
index b75cd30..8a44b86 100644 (file)
@@ -2,52 +2,40 @@
 
 {-# LANGUAGE CPP #-}
 
+-- The default iteration limit is a bit too low for the definitions
+-- in this module.
+{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
+
 module OptCoercion ( optCoercion, checkAxInstCo ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
+import DynFlags
+import TyCoRep
 import Coercion
-import Type hiding( substTyVarBndr, substTy, extendTvSubst )
-import TcType       ( exactTyVarsOfType )
+import Type hiding( substTyVarBndr, substTy )
+import TcType       ( exactTyCoVarsOfType )
 import TyCon
 import CoAxiom
-import Var
 import VarSet
-import FamInstEnv   ( flattenTys )
 import VarEnv
-import StaticFlags      ( opt_NoOptCoercion )
 import Outputable
+import FamInstEnv ( flattenTys )
 import Pair
-import FastString
+import ListSetOps ( getNth )
 import Util
 import Unify
-import ListSetOps
 import InstEnv
 import Control.Monad   ( zipWithM )
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
                  Optimising coercions
-*                                                                      *
-************************************************************************
-
-Note [Subtle shadowing in coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Supose we optimising a coercion
-    optCoercion (forall (co_X5:t1~t2). ...co_B1...)
-The co_X5 is a wild-card; the bound variable of a coercion for-all
-should never appear in the body of the forall. Indeed we often
-write it like this
-    optCoercion ( (t1~t2) => ...co_B1... )
-
-Just because it's a wild-card doesn't mean we are free to choose
-whatever variable we like.  For example it'd be wrong for optCoercion
-to return
-   forall (co_B1:t1~t2). ...co_B1...
-because now the co_B1 (which is really free) has been captured, and
-subsequent substitutions will go wrong.  That's why we can't use
-mkCoPredTy in the ForAll case, where this note appears.
+%*                                                                      *
+%************************************************************************
 
 Note [Optimising coercion optimisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -64,21 +52,98 @@ checks that opt_co4 can avoid. This is a big win because Phantom coercions
 rarely appear within non-phantom coercions -- only in some TyConAppCos
 and some AxiomInstCos. We handle these cases specially by calling
 opt_co2.
+
+Note [Optimising InstCo]
+~~~~~~~~~~~~~~~~~~~~~~~~
+(1) tv is a type variable
+When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.
+
+Let's look at the typing rules.
+
+h : k1 ~ k2
+tv:k1 |- g : t1 ~ t2
+-----------------------------
+ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])
+
+g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
+g2 : s1 ~ s2
+--------------------
+InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]
+
+We thus want some coercion proving this:
+
+  (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])
+
+If we substitute the *type* tv for the *coercion*
+(g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly.
+This is bizarre,
+though, because we're substituting a type variable with a coercion. However,
+this operation already exists: it's called *lifting*, and defined in Coercion.
+We just need to enhance the lifting operation to be able to deal with
+an ambient substitution, which is why a LiftingContext stores a TCvSubst.
+
+(2) cv is a coercion variable
+Now consider we have (InstCo (ForAllCo cv h g) g2), we want to optimise.
+
+h : (t1 ~r t2) ~N (t3 ~r t4)
+cv : t1 ~r t2 |- g : t1' ~r2 t2'
+n1 = nth r 2 (downgradeRole r N h) :: t1 ~r t3
+n2 = nth r 3 (downgradeRole r N h) :: t2 ~r t4
+------------------------------------------------
+ForAllCo cv h g : (all cv:t1 ~r t2. t1') ~r2
+                  (all cv:t3 ~r t4. t2'[cv |-> n1 ; cv ; sym n2])
+
+g1 : (all cv:t1 ~r t2. t1') ~ (all cv: t3 ~r t4. t2')
+g2 : h1 ~N h2
+h1 : t1 ~r t2
+h2 : t3 ~r t4
+------------------------------------------------
+InstCo g1 g2 : t1'[cv |-> h1] ~ t2'[cv |-> h2]
+
+We thus want some coercion proving this:
+
+  t1'[cv |-> h1] ~ t2'[cv |-> n1 ; h2; sym n2]
+
+So we substitute the coercion variable c for the coercion
+(h1 ~N (n1; h2; sym n2)) in g.
 -}
 
-optCoercion :: CvSubst -> Coercion -> NormalCo
+optCoercion :: DynFlags -> TCvSubst -> Coercion -> NormalCo
 -- ^ optCoercion applies a substitution to a coercion,
 --   *and* optimises it to reduce its size
-optCoercion env co
-  | opt_NoOptCoercion = substCo env co
-  | otherwise         = opt_co1 env False co
+optCoercion dflags env co
+  | hasNoOptCoercion dflags = substCo env co
+  | otherwise               = optCoercion' env co
+
+optCoercion' :: TCvSubst -> Coercion -> NormalCo
+optCoercion' env co
+  | debugIsOn
+  = let out_co = opt_co1 lc False co
+        (Pair in_ty1  in_ty2,  in_role)  = coercionKindRole co
+        (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
+    in
+    ASSERT2( substTy env in_ty1 `eqType` out_ty1 &&
+             substTy env in_ty2 `eqType` out_ty2 &&
+             in_role == out_role
+           , text "optCoercion changed types!"
+             $$ hang (text "in_co:") 2 (ppr co)
+             $$ hang (text "in_ty1:") 2 (ppr in_ty1)
+             $$ hang (text "in_ty2:") 2 (ppr in_ty2)
+             $$ hang (text "out_co:") 2 (ppr out_co)
+             $$ hang (text "out_ty1:") 2 (ppr out_ty1)
+             $$ hang (text "out_ty2:") 2 (ppr out_ty2)
+             $$ hang (text "subst:") 2 (ppr env) )
+    out_co
+
+  | otherwise         = opt_co1 lc False co
+  where
+    lc = mkSubstLiftingContext env
 
-type NormalCo = Coercion
+type NormalCo    = Coercion
   -- Invariants:
   --  * The substitution has been fully applied
   --  * For trans coercions (co1 `trans` co2)
   --       co1 is not a trans, and neither co1 nor co2 is identity
-  --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
 
 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
 
@@ -88,39 +153,16 @@ type SymFlag = Bool
 -- | Do we force the result to be representational?
 type ReprFlag = Bool
 
--- | Optimize a coercion, making no assumptions.
-opt_co1 :: CvSubst
+-- | Optimize a coercion, making no assumptions. All coercions in
+-- the lifting context are already optimized (and sym'd if nec'y)
+opt_co1 :: LiftingContext
         -> SymFlag
         -> Coercion -> NormalCo
 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
-{-
-opt_co env sym co
- = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
-   co1 `seq`
-   pprTrace "opt_co done }" (ppr co1) $
-   (WARN( not same_co_kind, ppr co  <+> dcolon <+> ppr (coercionType co)
-                         $$ ppr co1 <+> dcolon <+> ppr (coercionType co1) )
-    WARN( not (coreEqCoercion co1 simple_result),
-           (text "env=" <+> ppr env) $$
-           (text "input=" <+> ppr co) $$
-           (text "simple=" <+> ppr simple_result) $$
-           (text "opt=" <+> ppr co1) )
-   co1)
- where
-   co1 = opt_co' env sym co
-   same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
-   Pair s t = coercionKind (substCo env co)
-   (s1,t1) | sym = (t,s)
-           | otherwise = (s,t)
-   Pair s2 t2 = coercionKind co1
-
-   simple_result | sym = mkSymCo (substCo env co)
-                 | otherwise = substCo env co
--}
 
 -- See Note [Optimising coercion optimisation]
 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
-opt_co2 :: CvSubst
+opt_co2 :: LiftingContext
         -> SymFlag
         -> Role   -- ^ The role of the input coercion
         -> Coercion -> NormalCo
@@ -129,22 +171,59 @@ opt_co2 env sym r       co = opt_co3 env sym Nothing r co
 
 -- See Note [Optimising coercion optimisation]
 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
-opt_co3 :: CvSubst -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
-opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
-opt_co3 env sym (Just Representational) r co = opt_co4 env sym True  r co
+opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
+opt_co3 env sym (Just Phantom)          _ co = opt_phantom env sym co
+opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True  r co
   -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
-opt_co3 env sym _                       r co = opt_co4 env sym False r co
-
+opt_co3 env sym _                       r co = opt_co4_wrap env sym False r co
 
 -- See Note [Optimising coercion optimisation]
 -- | Optimize a non-phantom coercion.
-opt_co4 :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
+opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
 
-opt_co4 env _   rep r (Refl _r ty)
-  = ASSERT( r == _r )
-    Refl (chooseRole rep r) (substTy env ty)
+opt_co4_wrap = opt_co4
+{-
+opt_co4_wrap env sym rep r co
+  = pprTrace "opt_co4_wrap {"
+    ( vcat [ text "Sym:" <+> ppr sym
+           , text "Rep:" <+> ppr rep
+           , text "Role:" <+> ppr r
+           , text "Co:" <+> ppr co ]) $
+    ASSERT( r == coercionRole co )
+    let result = opt_co4 env sym rep r co in
+    pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
+    result
+-}
 
-opt_co4 env sym rep r (SymCo co)  = opt_co4 env (not sym) rep r co
+opt_co4 env _   rep r (Refl ty)
+  = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r    $$
+                           text "Found role:" <+> ppr Nominal $$
+                           text "Type:" <+> ppr ty )
+    liftCoSubst (chooseRole rep r) env ty
+
+opt_co4 env _   rep r (GRefl _r ty MRefl)
+  = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
+                      text "Found role:" <+> ppr _r   $$
+                      text "Type:" <+> ppr ty )
+    liftCoSubst (chooseRole rep r) env ty
+
+opt_co4 env sym  rep r (GRefl _r ty (MCo co))
+  = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
+                      text "Found role:" <+> ppr _r   $$
+                      text "Type:" <+> ppr ty )
+    if isGReflCo co || isGReflCo co'
+    then liftCoSubst r' env ty
+    else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
+  where
+    r'  = chooseRole rep r
+    ty' = substTy (lcSubstLeft env) ty
+    co' = opt_co4 env False False Nominal co
+
+opt_co4 env sym rep r (SymCo co)  = opt_co4_wrap env (not sym) rep r co
+  -- surprisingly, we don't have to do anything to the env here. This is
+  -- because any "lifting" substitutions in the env are tied to ForAllCos,
+  -- which treat their left and right sides differently. We don't want to
+  -- exchange them.
 
 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
   = ASSERT( r == _r )
@@ -152,37 +231,62 @@ opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
       (True, Nominal) ->
         mkTyConAppCo Representational tc
                      (zipWith3 (opt_co3 env sym)
-                               (map Just (tyConRolesRepresentational tc))
+                               (map Just (tyConRolesRepresentational tc))
                                (repeat Nominal)
                                cos)
       (False, Nominal) ->
-        mkTyConAppCo Nominal tc (map (opt_co4 env sym False Nominal) cos)
+        mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
       (_, Representational) ->
                       -- must use opt_co2 here, because some roles may be P
                       -- See Note [Optimising coercion optimisation]
         mkTyConAppCo r tc (zipWith (opt_co2 env sym)
-                                   (tyConRolesX r tc)  -- the current roles
+                                   (tyConRolesRepresentational tc)  -- the current roles
                                    cos)
       (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
 
-opt_co4 env sym rep r (AppCo co1 co2) = mkAppCo (opt_co4 env sym rep r co1)
-                                                (opt_co4 env sym False Nominal co2)
-opt_co4 env sym rep r (ForAllCo tv co)
-  = case substTyVarBndr env tv of
-      (env', tv') -> mkForAllCo tv' (opt_co4 env' sym rep r co)
+opt_co4 env sym rep r (AppCo co1 co2)
+  = mkAppCo (opt_co4_wrap env sym rep r co1)
+            (opt_co4_wrap env sym False Nominal co2)
+
+opt_co4 env sym rep r (ForAllCo tv k_co co)
+  = case optForAllCoBndr env sym tv k_co of
+      (env', tv', k_co') -> mkForAllCo tv' k_co' $
+                            opt_co4_wrap env' sym rep r co
      -- Use the "mk" functions to check for nested Refls
 
+opt_co4 env sym rep r (FunCo _r co1 co2)
+  = ASSERT( r == _r )
+    if rep
+    then mkFunCo Representational co1' co2'
+    else mkFunCo r co1' co2'
+  where
+    co1' = opt_co4_wrap env sym rep r co1
+    co2' = opt_co4_wrap env sym rep r co2
+
 opt_co4 env sym rep r (CoVarCo cv)
-  | Just co <- lookupCoVar env cv
-  = opt_co4 (zapCvSubstEnv env) sym rep r co
+  | Just co <- lookupCoVar (lcTCvSubst env) cv
+  = opt_co4_wrap (zapLiftingContext env) sym rep r co
+
+  | ty1 `eqType` ty2   -- See Note [Optimise CoVarCo to Refl]
+  = mkReflCo (chooseRole rep r) ty1
+
+  | otherwise
+  = ASSERT( isCoVar cv1 )
+    wrapRole rep r $ wrapSym sym $
+    CoVarCo cv1
+
+  where
+    Pair ty1 ty2 = coVarTypes cv1
 
-  | Just cv1 <- lookupInScope (getCvInScope env) cv
-  = ASSERT( isCoVar cv1 ) wrapRole rep r $ wrapSym sym (CoVarCo cv1)
-                -- cv1 might have a substituted kind!
+    cv1 = case lookupInScope (lcInScopeSet env) cv of
+             Just cv1 -> cv1
+             Nothing  -> WARN( True, text "opt_co: not in scope:"
+                                     <+> ppr cv $$ ppr env)
+                         cv
+          -- cv1 might have a substituted kind!
 
-  | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
-                ASSERT( isCoVar cv )
-                wrapRole rep r $ wrapSym sym (CoVarCo cv)
+opt_co4 _ _ _ _ (HoleCo h)
+  = pprPanic "opt_univ fell into a hole" (ppr h)
 
 opt_co4 env sym rep r (AxiomInstCo con ind cos)
     -- Do *not* push sym inside top-level axioms
@@ -199,141 +303,253 @@ opt_co4 env sym rep r (AxiomInstCo con ind cos)
                                  cos)
       -- Note that the_co does *not* have sym pushed into it
 
-opt_co4 env sym rep r (UnivCo _r oty1 oty2)
+opt_co4 env sym rep r (UnivCo prov _r t1 t2)
   = ASSERT( r == _r )
-    opt_univ env (chooseRole rep r) a b
-  where
-    (a,b) = if sym then (oty2,oty1) else (oty1,oty2)
+    opt_univ env sym prov (chooseRole rep r) t1 t2
 
 opt_co4 env sym rep r (TransCo co1 co2)
                       -- sym (g `o` h) = sym h `o` sym g
   | sym       = opt_trans in_scope co2' co1'
   | otherwise = opt_trans in_scope co1' co2'
   where
-    co1' = opt_co4 env sym rep r co1
-    co2' = opt_co4 env sym rep r co2
-    in_scope = getCvInScope env
+    co1' = opt_co4_wrap env sym rep r co1
+    co2' = opt_co4_wrap env sym rep r co2
+    in_scope = lcInScopeSet env
+
+opt_co4 env _sym rep r (NthCo _r n co)
+  | Just (ty, _) <- isReflCo_maybe co
+  , Just (_tc, args) <- ASSERT( r == _r )
+                        splitTyConApp_maybe ty
+  = liftCoSubst (chooseRole rep r) env (args `getNth` n)
+  | Just (ty, _) <- isReflCo_maybe co
+  , n == 0
+  , Just (tv, _) <- splitForAllTy_maybe ty
+      -- works for both tyvar and covar
+  = liftCoSubst (chooseRole rep r) env (varType 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 _))
+      -- works for both tyvar and covar
+  = 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
   = ASSERT( r == Nominal )
-    opt_co4 env sym rep Nominal (pickLR lr pr_co)
+    opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
   | Just pr_co <- splitAppCo_maybe co'
   = ASSERT( r == Nominal )
     if rep
-    then opt_co4 (zapCvSubstEnv env) False True Nominal (pickLR lr pr_co)
-    else pickLR lr pr_co
+    then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
+    else pick_lr lr pr_co
   | otherwise
   = wrapRole rep Nominal $ LRCo lr co'
   where
-    co' = opt_co4 env sym False Nominal co
-
-opt_co4 env sym rep r (InstCo co ty)
-    -- See if the first arg is already a forall
-    -- ...then we can just extend the current substitution
-  | Just (tv, co_body) <- splitForAllCo_maybe co
-  = opt_co4 (extendTvSubst env tv ty') sym rep r co_body
-
-     -- See if it is a forall after optimization
-     -- If so, do an inefficient one-variable substitution
-  | Just (tv, co'_body) <- splitForAllCo_maybe co'
-  = substCoWithTy (getCvInScope env) tv ty' co'_body
-
-  | otherwise = InstCo co' ty'
+    co' = opt_co4_wrap env sym False Nominal co
+
+    pick_lr CLeft  (l, _) = l
+    pick_lr CRight (_, r) = r
+
+-- See Note [Optimising InstCo]
+opt_co4 env sym rep r (InstCo co1 arg)
+    -- forall over type...
+  | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
+  = opt_co4_wrap (extendLiftingContext env tv
+                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg'))
+                   -- kind_co :: k1 ~ k2
+                   -- arg' :: (t1 :: k1) ~ (t2 :: k2)
+                   -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
+                 sym rep r co_body
+
+    -- forall over coercion...
+  | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
+  , CoercionTy h1 <- t1
+  , CoercionTy h2 <- t2
+  = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
+    in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
+
+    -- See if it is a forall after optimization
+    -- If so, do an inefficient one-variable substitution, then re-optimize
+
+    -- forall over type...
+  | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
+  = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
+                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg'))
+            False False r' co_body'
+
+    -- forall over coercion...
+  | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
+  , CoercionTy h1 <- t1
+  , CoercionTy h2 <- t2
+  = let new_co = mk_new_co cv' kind_co' h1 h2
+    in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
+                    False False r' co_body'
+
+  | otherwise = InstCo co1' arg'
   where
-    co' = opt_co4 env sym rep r co
-    ty' = substTy env ty
+    co1' = opt_co4_wrap env sym rep r co1
+    r'   = chooseRole rep r
+    arg' = opt_co4_wrap env sym False Nominal arg
+    Pair t1 t2 = coercionKind arg'
+
+    mk_new_co cv kind_co h1 h2
+      = let -- h1 :: (t1 ~ t2)
+            -- h2 :: (t3 ~ t4)
+            -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4)
+            -- n1 :: t1 ~ t3
+            -- n2 :: t2 ~ t4
+            -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
+            r2  = coVarRole cv
+            kind_co' = downgradeRole r2 Nominal kind_co
+            n1 = mkNthCo r2 2 kind_co'
+            n2 = mkNthCo r2 3 kind_co'
+         in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
+                           (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
+
+opt_co4 env sym _rep r (KindCo co)
+  = ASSERT( r == Nominal )
+    let kco' = promoteCoercion co in
+    case kco' of
+      KindCo co' -> promoteCoercion (opt_co1 env sym co')
+      _          -> opt_co4_wrap env sym False Nominal kco'
+  -- This might be able to be optimized more to do the promotion
+  -- and substitution/optimization at the same time
 
 opt_co4 env sym _ r (SubCo co)
   = ASSERT( r == Representational )
-    opt_co4 env sym True Nominal co
+    opt_co4_wrap env sym True Nominal co
 
--- XXX: We could add another field to CoAxiomRule that
--- would allow us to do custom simplifications.
-opt_co4 env sym rep r (AxiomRuleCo co ts cs)
+-- This could perhaps be optimized more.
+opt_co4 env sym rep r (AxiomRuleCo co cs)
   = ASSERT( r == coaxrRole co )
     wrapRole rep r $
     wrapSym sym $
-    AxiomRuleCo co (map (substTy env) ts)
-                   (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
+    AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
 
+{- Note [Optimise CoVarCo to Refl]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have (c :: t~t) we can optimise it to Refl. That increases the
+chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
+
+We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
+in Coercion.
+-}
 
 -------------
 -- | Optimize a phantom coercion. The input coercion may not necessarily
 -- be a phantom, but the output sure will be.
-opt_phantom :: CvSubst -> SymFlag -> Coercion -> NormalCo
+opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
 opt_phantom env sym co
-  = if sym
-    then opt_univ env Phantom ty2 ty1
-    else opt_univ env Phantom ty1 ty2
+  = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
   where
     Pair ty1 ty2 = coercionKind co
 
-opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
-opt_univ env role oty1 oty2
+{- Note [Differing kinds]
+   ~~~~~~~~~~~~~~~~~~~~~~
+The two types may not have the same kind (although that would be very unusual).
+But even if they have the same kind, and the same type constructor, the number
+of arguments in a `CoTyConApp` can differ. Consider
+
+  Any :: forall k. k
+
+  Any * Int                      :: *
+  Any (*->*) Maybe Int  :: *
+
+Hence the need to compare argument lengths; see Trac #13658
+ -}
+
+opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
+         -> Type -> Type -> Coercion
+opt_univ env sym (PhantomProv h) _r ty1 ty2
+  | sym       = mkPhantomCo h' ty2' ty1'
+  | otherwise = mkPhantomCo h' ty1' ty2'
+  where
+    h' = opt_co4 env sym False Nominal h
+    ty1' = substTy (lcSubstLeft  env) ty1
+    ty2' = substTy (lcSubstRight env) ty2
+
+opt_univ env sym prov role oty1 oty2
   | Just (tc1, tys1) <- splitTyConApp_maybe oty1
   , Just (tc2, tys2) <- splitTyConApp_maybe oty2
   , tc1 == tc2
-  = mkTyConAppCo role tc1 (zipWith3 (opt_univ env) (tyConRolesX role tc1) tys1 tys2)
-
-  | Just (l1, r1) <- splitAppTy_maybe oty1
-  , Just (l2, r2) <- splitAppTy_maybe oty2
-  , typeKind l1 `eqType` typeKind l2   -- kind(r1) == kind(r2) by consequence
-  = let role' = if role == Phantom then Phantom else Nominal in
-       -- role' is to comform to mkAppCo's precondition
-    mkAppCo (opt_univ env role l1 l2) (opt_univ env role' r1 r2)
-
-  | Just (tv1, ty1) <- splitForAllTy_maybe oty1
-  , Just (tv2, ty2) <- splitForAllTy_maybe oty2
-  , tyVarKind tv1 `eqType` tyVarKind tv2  -- rule out a weird unsafeCo
-  = case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
-    let ty1' = substTy env1 ty1
-        ty2' = substTy env2 ty2 in
-    mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) role ty1' ty2') }
+  , equalLength tys1 tys2 -- see Note [Differing kinds]
+      -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
+      -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
+  = let roles    = tyConRolesX role tc1
+        arg_cos  = zipWith3 (mkUnivCo prov') roles tys1 tys2
+        arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
+    in
+    mkTyConAppCo role tc1 arg_cos'
+
+  -- can't optimize the AppTy case because we can't build the kind coercions.
+
+  | Just (tv1, ty1) <- splitForAllTy_ty_maybe oty1
+  , Just (tv2, ty2) <- splitForAllTy_ty_maybe oty2
+      -- NB: prov isn't interesting here either
+  = let k1   = tyVarKind tv1
+        k2   = tyVarKind tv2
+        eta  = mkUnivCo prov' Nominal k1 k2
+          -- eta gets opt'ed soon, but not yet.
+        ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
+
+        (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
+    in
+    mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
+
+  | Just (cv1, ty1) <- splitForAllTy_co_maybe oty1
+  , Just (cv2, ty2) <- splitForAllTy_co_maybe oty2
+      -- NB: prov isn't interesting here either
+  = let k1    = varType cv1
+        k2    = varType cv2
+        r'    = coVarRole cv1
+        eta   = mkUnivCo prov' Nominal k1 k2
+        eta_d = downgradeRole r' Nominal eta
+          -- eta gets opt'ed soon, but not yet.
+        n_co  = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
+                (mkCoVarCo cv1) `mkTransCo`
+                (mkNthCo r' 3 eta_d)
+        ty2'  = substTyWithCoVars [cv2] [n_co] ty2
+
+        (env', cv1', eta') = optForAllCoBndr env sym cv1 eta
+    in
+    mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2')
 
   | otherwise
-  = mkUnivCo role (substTy env oty1) (substTy env oty2)
+  = let ty1 = substTyUnchecked (lcSubstLeft  env) oty1
+        ty2 = substTyUnchecked (lcSubstRight env) oty2
+        (a, b) | sym       = (ty2, ty1)
+               | otherwise = (ty1, ty2)
+    in
+    mkUnivCo prov' role a b
 
--------------
--- 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 :: CvSubst -> 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
-
-      -- input coercion is *not* yet sym'd or opt'd
-    opt_nths [] co = opt_co4 env sym rep r co
-    opt_nths (n:ns) (TyConAppCo _ _ cos) = opt_nths ns (cos `getNth` n)
-
-      -- 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 (zapCvSubstEnv env) False True r co
-        else co
-    opt_nths' (n:ns) (TyConAppCo _ _ cos) = opt_nths' ns (cos `getNth` n)
-    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)
+    prov' = case prov of
+      UnsafeCoerceProv   -> prov
+      PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
+      ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
+      PluginProv _       -> prov
 
 -------------
 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -342,12 +558,14 @@ opt_transList is = zipWith (opt_trans is)
 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
 opt_trans is co1 co2
   | isReflCo co1 = co2
+    -- optimize when co1 is a Refl Co
   | otherwise    = opt_trans1 is co1 co2
 
 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
 -- First arg is not the identity
 opt_trans1 is co1 co2
   | isReflCo co2 = co1
+    -- optimize when co2 is a Refl Co
   | otherwise    = opt_trans2 is co1 co2
 
 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
@@ -373,12 +591,19 @@ opt_trans2 _ co1 co2
 -- Optimize coercions with a top-level use of transitivity.
 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
 
+opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
+  = ASSERT( r1 == r2 )
+    fireTransRule "GRefl" in_co1 in_co2 $
+    mkGReflRightCo r1 t1 (opt_trans is co1 co2)
+
 -- 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
@@ -388,60 +613,119 @@ opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
 
 -- Push transitivity inside instantiation
 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
-  | ty1 `eqType` ty2
+  | ty1 `eqCoercion` ty2
   , co1 `compatible_co` co2
   = fireTransRule "TrPushInst" in_co1 in_co2 $
     mkInstCo (opt_trans is co1 co2) ty1
 
+opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
+                  in_co2@(UnivCo p2 r2 _tyl2 tyr2)
+  | Just prov' <- opt_trans_prov p1 p2
+  = ASSERT( r1 == r2 )
+    fireTransRule "UnivCo" in_co1 in_co2 $
+    mkUnivCo prov' r1 tyl1 tyr2
+  where
+    -- if the provenances are different, opt'ing will be very confusing
+    opt_trans_prov UnsafeCoerceProv      UnsafeCoerceProv      = Just UnsafeCoerceProv
+    opt_trans_prov (PhantomProv kco1)    (PhantomProv kco2)
+      = Just $ PhantomProv $ opt_trans is kco1 kco2
+    opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
+      = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
+    opt_trans_prov (PluginProv str1)     (PluginProv str2)     | str1 == str2 = Just p1
+    opt_trans_prov _ _ = Nothing
+
 -- Push transitivity down through matching top-level constructors.
 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
   | tc1 == tc2
   = ASSERT( r1 == r2 )
     fireTransRule "PushTyConApp" in_co1 in_co2 $
-    TyConAppCo r1 tc1 (opt_transList is cos1 cos2)
+    mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
+
+opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b)
+  = ASSERT( r1 == r2 )   -- Just like the TyConAppCo/TyConAppCo case
+    fireTransRule "PushFun" in_co1 in_co2 $
+    mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b)
 
 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
-  = fireTransRule "TrPushApp" in_co1 in_co2 $
-    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+  -- Must call opt_trans_rule_app; see Note [EtaAppCo]
+  = opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b]
 
 -- Eta rules
 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
   | Just cos2 <- etaTyConAppCo_maybe tc co2
-  = ASSERT( length cos1 == length cos2 )
+  = ASSERT( cos1 `equalLength` cos2 )
     fireTransRule "EtaCompL" co1 co2 $
-    TyConAppCo r tc (opt_transList is cos1 cos2)
+    mkTyConAppCo r tc (opt_transList is cos1 cos2)
 
 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
   | Just cos1 <- etaTyConAppCo_maybe tc co1
-  = ASSERT( length cos1 == length cos2 )
+  = ASSERT( cos1 `equalLength` cos2 )
     fireTransRule "EtaCompR" co1 co2 $
-    TyConAppCo r tc (opt_transList is cos1 cos2)
+    mkTyConAppCo r tc (opt_transList is cos1 cos2)
 
 opt_trans_rule is co1@(AppCo co1a co1b) co2
   | Just (co2a,co2b) <- etaAppCo_maybe co2
-  = fireTransRule "EtaAppL" co1 co2 $
-    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+  = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
 
 opt_trans_rule is co1 co2@(AppCo co2a co2b)
   | Just (co1a,co1b) <- etaAppCo_maybe co1
-  = fireTransRule "EtaAppR" co1 co2 $
-    mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+  = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
+
+-- Push transitivity inside forall
+-- forall over types.
+opt_trans_rule is co1 co2
+  | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1
+  , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2
+  = push_trans tv1 eta1 r1 tv2 eta2 r2
+
+  | Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2
+  , Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1
+  = push_trans tv1 eta1 r1 tv2 eta2 r2
+
+  where
+  push_trans tv1 eta1 r1 tv2 eta2 r2
+    -- Given:
+    --   co1 = /\ tv1 : eta1. r1
+    --   co2 = /\ tv2 : eta2. r2
+    -- Wanted:
+    --   /\tv1 : (eta1;eta2).  (r1; r2[tv2 |-> tv1 |> eta1])
+    = fireTransRule "EtaAllTy_ty" co1 co2 $
+      mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
+    where
+      is' = is `extendInScopeSet` tv1
+      r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
 
 -- Push transitivity inside forall
+-- forall over coercions.
 opt_trans_rule is co1 co2
-  | Just (tv1,r1) <- splitForAllCo_maybe co1
-  , Just (tv2,r2) <- etaForAllCo_maybe co2
-  , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
-        is' = is `extendInScopeSet` tv1
-  = fireTransRule "EtaAllL" co1 co2 $
-    mkForAllCo tv1 (opt_trans2 is' r1 r2')
-
-  | Just (tv2,r2) <- splitForAllCo_maybe co2
-  , Just (tv1,r1) <- etaForAllCo_maybe co1
-  , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
-        is' = is `extendInScopeSet` tv2
-  = fireTransRule "EtaAllR" co1 co2 $
-    mkForAllCo tv1 (opt_trans2 is' r1' r2)
+  | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1
+  , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2
+  = push_trans cv1 eta1 r1 cv2 eta2 r2
+
+  | Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2
+  , Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1
+  = push_trans cv1 eta1 r1 cv2 eta2 r2
+
+  where
+  push_trans cv1 eta1 r1 cv2 eta2 r2
+    -- Given:
+    --   co1 = /\ cv1 : eta1. r1
+    --   co2 = /\ cv2 : eta2. r2
+    -- Wanted:
+    --   n1 = nth 2 eta1
+    --   n2 = nth 3 eta1
+    --   nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
+    = fireTransRule "EtaAllTy_co" co1 co2 $
+      mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
+    where
+      is'  = is `extendInScopeSet` cv1
+      role = coVarRole cv1
+      eta1' = downgradeRole role Nominal eta1
+      n1   = mkNthCo role 2 eta1'
+      n2   = mkNthCo role 3 eta1'
+      r2'  = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
+                                        (mkCoVarCo cv1) `mkTransCo` n2])
+                    r2
 
 -- Push transitivity inside axioms
 opt_trans_rule is co1 co2
@@ -449,32 +733,32 @@ opt_trans_rule is co1 co2
   -- See Note [Why call checkAxInstCo during optimisation]
   -- TrPushSymAxR
   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
-  , Just cos2 <- matchAxiom sym con ind co2
   , True <- sym
+  , Just cos2 <- matchAxiom sym con ind co2
   , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
   , Nothing <- checkAxInstCo newAxInst
   = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
 
   -- TrPushAxR
   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
-  , Just cos2 <- matchAxiom sym con ind co2
   , False <- sym
+  , Just cos2 <- matchAxiom sym con ind co2
   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
   , Nothing <- checkAxInstCo newAxInst
   = fireTransRule "TrPushAxR" co1 co2 newAxInst
 
   -- TrPushSymAxL
   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
-  , Just cos1 <- matchAxiom (not sym) con ind co1
   , True <- sym
+  , Just cos1 <- matchAxiom (not sym) con ind co1
   , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
   , Nothing <- checkAxInstCo newAxInst
   = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
 
   -- TrPushAxL
   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
-  , Just cos1 <- matchAxiom (not sym) con ind co1
   , False <- sym
+  , Just cos1 <- matchAxiom (not sym) con ind co1
   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
   , Nothing <- checkAxInstCo newAxInst
   = fireTransRule "TrPushAxL" co1 co2 newAxInst
@@ -486,15 +770,17 @@ opt_trans_rule is co1 co2
   , ind1 == ind2
   , sym1 == not sym2
   , let branch = coAxiomNthBranch con1 ind1
-        qtvs = coAxBranchTyVars branch
+        qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
         lhs  = coAxNthLHS con1 ind1
         rhs  = coAxBranchRHS branch
-        pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
+        pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
   , all (`elemVarSet` pivot_tvs) qtvs
   = fireTransRule "TrPushAxSym" co1 co2 $
     if sym2
-    then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
-    else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
+       -- TrPushAxSym
+    then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
+       -- TrPushSymAx
+    else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
   where
     co1_is_axiom_maybe = isAxiom_maybe co1
     co2_is_axiom_maybe = isAxiom_maybe co2
@@ -505,14 +791,51 @@ opt_trans_rule _ co1 co2        -- Identity rule
   , Pair _ ty2 <- coercionKind co2
   , ty1 `eqType` ty2
   = fireTransRule "RedTypeDirRefl" co1 co2 $
-    Refl r ty2
+    mkReflCo r ty2
 
 opt_trans_rule _ _ _ = Nothing
 
+-- See Note [EtaAppCo]
+opt_trans_rule_app :: InScopeSet
+                   -> Coercion   -- original left-hand coercion (printing only)
+                   -> Coercion   -- original right-hand coercion (printing only)
+                   -> Coercion   -- left-hand coercion "function"
+                   -> [Coercion] -- left-hand coercion "args"
+                   -> Coercion   -- right-hand coercion "function"
+                   -> [Coercion] -- right-hand coercion "args"
+                   -> Maybe Coercion
+opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
+  | AppCo co1aa co1ab <- co1a
+  , Just (co2aa, co2ab) <- etaAppCo_maybe co2a
+  = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
+
+  | AppCo co2aa co2ab <- co2a
+  , Just (co1aa, co1ab) <- etaAppCo_maybe co1a
+  = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
+
+  | otherwise
+  = ASSERT( co1bs `equalLength` co2bs )
+    fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
+    let Pair _ rt1a = coercionKind co1a
+        (Pair lt2a _, rt2a) = coercionKindRole co2a
+
+        Pair _ rt1bs = traverse coercionKind co1bs
+        Pair lt2bs _ = traverse coercionKind co2bs
+        rt2bs = map coercionRole co2bs
+
+        kcoa = mkKindCo $ buildCoercion lt2a rt1a
+        kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
+
+        co2a'   = mkCoherenceLeftCo rt2a lt2a kcoa co2a
+        co2bs'  = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
+        co2bs'' = zipWith mkTransCo co2bs' co2bs
+    in
+    mkAppCos (opt_trans is co1a co2a')
+             (zipWith (opt_trans is) co1bs co2bs'')
+
 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
 fireTransRule _rule _co1 _co2 res
-  = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
-    Just res
+  = Just res
 
 {-
 Note [Conflict checking with AxiomInstCo]
@@ -524,9 +847,9 @@ type instance where
   Equal a a = True
   Equal a b = False
 --
-Equal :: forall k::BOX. k -> k -> Bool
-axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
-           ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
+Equal :: forall k::*. k -> k -> Bool
+axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
+           ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
 
 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
 0-based, so this is the second branch of the axiom.) The problem is that, on
@@ -534,8 +857,8 @@ the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
 False) and that all is OK. But, all is not OK: we want to use the first branch
 of the axiom in this case, not the second. The problem is that the parameters
 of the first branch can unify with the supplied coercions, thus meaning that
-the first branch should be taken. See also Note [Branched instance checking]
-in types/FamInstEnv.lhs.
+the first branch should be taken. See also Note [Apartness] in
+types/FamInstEnv.hs.
 
 Note [Why call checkAxInstCo during optimisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -569,6 +892,64 @@ that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
 families. At the time of writing, I (Richard Eisenberg) couldn't think of
 a way of detecting this any more efficient than just building the optimised
 coercion and checking.
+
+Note [EtaAppCo]
+~~~~~~~~~~~~~~~
+Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
+like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
+the resultant coercions might not be well kinded. Here is an example (things
+labeled with x don't matter in this example):
+
+  k1 :: Type
+  k2 :: Type
+
+  a :: k1 -> Type
+  b :: k1
+
+  h :: k1 ~ k2
+
+  co1a :: x1 ~ (a |> (h -> <Type>)
+  co1b :: x2 ~ (b |> h)
+
+  co2a :: a ~ x3
+  co2b :: b ~ x4
+
+First, convince yourself of the following:
+
+  co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
+  co2a co2b :: a b   ~ x3 x4
+
+  (a |> (h -> <Type>)) (b |> h) `eqType` a b
+
+That last fact is due to Note [Non-trivial definitional equality] in TyCoRep,
+where we ignore coercions in types as long as two types' kinds are the same.
+In our case, we meet this last condition, because
+
+  (a |> (h -> <Type>)) (b |> h) :: Type
+    and
+  a b :: Type
+
+So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
+suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
+kinds don't match up.
+
+The solution here is to twiddle the kinds in the output coercions. First, we
+need to find coercions
+
+  ak :: kind(a |> (h -> <Type>)) ~ kind(a)
+  bk :: kind(b |> h)             ~ kind(b)
+
+This can be done with mkKindCo and buildCoercion. The latter assumes two
+types are identical modulo casts and builds a coercion between them.
+
+Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
+output coercions. These are well-kinded.
+
+Also, note that all of this is done after accumulated any nested AppCo
+parameters. This step is to avoid quadratic behavior in calling coercionKind.
+
+The problem described here was first found in dependent/should_compile/dynamic-paper.
+
 -}
 
 -- | Check to make sure that an AxInstCo is internally consistent.
@@ -579,14 +960,17 @@ checkAxInstCo :: Coercion -> Maybe CoAxBranch
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism] in CoreLint
 checkAxInstCo (AxiomInstCo ax ind cos)
-  = let branch   = coAxiomNthBranch ax ind
-        tvs      = coAxBranchTyVars branch
-        incomps  = coAxBranchIncomps branch
-        tys      = map (pFst . coercionKind) cos
-        subst    = zipOpenTvSubst tvs tys
+  = let branch       = coAxiomNthBranch ax ind
+        tvs          = coAxBranchTyVars branch
+        cvs          = coAxBranchCoVars branch
+        incomps      = coAxBranchIncomps branch
+        (tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
+        co_args      = map stripCoercionTy cotys
+        subst        = zipTvSubst tvs tys `composeTCvSubst`
+                       zipCvSubst cvs co_args
         target   = Type.substTys subst (coAxBranchLHS branch)
         in_scope = mkInScopeSet $
-                   unionVarSets (map (tyVarsOfTypes . coAxBranchLHS) incomps)
+                   unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
         flattened_target = flattenTys in_scope target in
     check_no_conflict flattened_target incomps
   where
@@ -600,9 +984,10 @@ checkAxInstCo (AxiomInstCo ax ind cos)
       = Just b
 checkAxInstCo _ = Nothing
 
+
 -----------
 wrapSym :: SymFlag -> Coercion -> Coercion
-wrapSym sym co | sym       = SymCo co
+wrapSym sym co | sym       = mkSymCo co
                | otherwise = co
 
 -- | Conditionally set a role to be representational
@@ -619,18 +1004,7 @@ chooseRole :: ReprFlag
            -> Role
 chooseRole True _ = Representational
 chooseRole _    r = r
------------
--- takes two tyvars and builds env'ts to map them to the same tyvar
-substTyVarBndr2 :: CvSubst -> TyVar -> TyVar
-                -> (CvSubst, CvSubst, TyVar)
-substTyVarBndr2 env tv1 tv2
-  = case substTyVarBndr env tv1 of
-      (env1, tv1') -> (env1, extendTvSubstAndInScope env tv2 (mkTyVarTy tv1'), tv1')
-
-zapCvSubstEnv2 :: CvSubst -> CvSubst -> CvSubst
-zapCvSubstEnv2 env1 env2 = mkCvSubst (is1 `unionInScope` is2) []
-  where is1 = getCvInScope env1
-        is2 = getCvInScope env2
+
 -----------
 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
 isAxiom_maybe (SymCo co)
@@ -642,16 +1016,20 @@ isAxiom_maybe _ = Nothing
 
 matchAxiom :: Bool -- True = match LHS, False = match RHS
            -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
--- If we succeed in matching, then *all the quantified type variables are bound*
--- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
-  = let (CoAxBranch { cab_tvs   = qtvs
-                    , cab_roles = roles
-                    , cab_lhs   = lhs
-                    , cab_rhs   = rhs }) = coAxiomNthBranch ax ind in
-    case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
-      Nothing    -> Nothing
-      Just subst -> zipWithM (liftCoSubstTyVar subst) roles qtvs
+  | CoAxBranch { cab_tvs = qtvs
+               , cab_cvs = []   -- can't infer these, so fail if there are any
+               , cab_roles = roles
+               , cab_lhs = lhs
+               , cab_rhs = rhs } <- coAxiomNthBranch ax ind
+  , Just subst <- liftCoMatch (mkVarSet qtvs)
+                              (if sym then (mkTyConApp tc lhs) else rhs)
+                              co
+  , all (`isMappedByLC` subst) qtvs
+  = zipWithM (liftCoSubstTyVar subst) roles qtvs
+
+  | otherwise
+  = Nothing
 
 -------------
 compatible_co :: Coercion -> Coercion -> Bool
@@ -663,17 +1041,84 @@ compatible_co co1 co2
     Pair x2 _ = coercionKind co2
 
 -------------
-etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
--- Try to make the coercion be of form (forall tv. co)
-etaForAllCo_maybe co
-  | Just (tv, r) <- splitForAllCo_maybe co
-  = Just (tv, r)
+{-
+etaForAllCo
+~~~~~~~~~~~~~~~~~
+(1) etaForAllCo_ty_maybe
+Suppose we have
+
+  g : all a1:k1.t1  ~  all a2:k2.t2
+
+but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
+
+  g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))
+
+Call the kind coercion h1 and the body coercion h2. We can see that
+
+  h2 : t1 ~ t2[a2 |-> (a1 |> h1)]
+
+According to the typing rule for ForAllCo, we get that
+
+  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])
+
+or
+
+  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> a1])
+
+as desired.
+
+(2) etaForAllCo_co_maybe
+Suppose we have
+
+  g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2
+
+Similarly, we do this
+
+  g' = all c1:h1. h2
+     : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)]
+                                              [c1 |-> eta1;c1;sym eta2]
+
+Here,
+
+  h1   = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
+  eta1 = mkNthCo r 2 h1      :: (s1 ~ s3)
+  eta2 = mkNthCo r 3 h1      :: (s2 ~ s4)
+  h2   = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
+-}
+etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
+-- Try to make the coercion be of form (forall tv:kind_co. co)
+etaForAllCo_ty_maybe co
+  | Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co
+  = Just (tv, kind_co, r)
 
   | Pair ty1 ty2  <- coercionKind co
-  , Just (tv1, _) <- splitForAllTy_maybe ty1
-  , Just (tv2, _) <- splitForAllTy_maybe ty2
-  , tyVarKind tv1 `eqKind` tyVarKind tv2
-  = Just (tv1, mkInstCo co (mkTyVarTy tv1))
+  , Just (tv1, _) <- splitForAllTy_ty_maybe ty1
+  , isForAllTy_ty ty2
+  , let kind_co = mkNthCo Nominal 0 co
+  = Just ( tv1, kind_co
+         , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
+
+  | otherwise
+  = Nothing
+
+etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
+-- Try to make the coercion be of form (forall cv:kind_co. co)
+etaForAllCo_co_maybe co
+  | Just (cv, kind_co, r) <- splitForAllCo_co_maybe co
+  = Just (cv, kind_co, r)
+
+  | Pair ty1 ty2  <- coercionKind co
+  , Just (cv1, _) <- splitForAllTy_co_maybe ty1
+  , isForAllTy_co ty2
+  = let kind_co  = mkNthCo Nominal 0 co
+        r        = coVarRole cv1
+        l_co     = mkCoVarCo cv1
+        kind_co' = downgradeRole r Nominal kind_co
+        r_co     = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
+                   l_co `mkTransCo`
+                   (mkNthCo r 3 kind_co')
+    in Just ( cv1, kind_co
+            , mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
 
   | otherwise
   = Nothing
@@ -688,7 +1133,9 @@ etaAppCo_maybe co
   | (Pair ty1 ty2, Nominal) <- coercionKindRole co
   , Just (_,t1) <- splitAppTy_maybe ty1
   , Just (_,t2) <- splitAppTy_maybe ty2
-  , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
+  , let isco1 = isCoercionTy t1
+  , let isco2 = isCoercionTy t2
+  , isco1 == isco2
   = Just (LRCo CLeft co, LRCo CRight co)
   | otherwise
   = Nothing
@@ -701,15 +1148,18 @@ etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
   = ASSERT( tc == tc2 ) Just cos2
 
 etaTyConAppCo_maybe tc co
-  | isDecomposableTyCon tc
-  , Pair ty1 ty2     <- coercionKind co
-  , Just (tc1, tys1) <- splitTyConApp_maybe ty1
-  , Just (tc2, tys2) <- splitTyConApp_maybe ty2
+  | mightBeUnsaturatedTyCon tc
+  , (Pair ty1 ty2, r) <- coercionKindRole co
+  , Just (tc1, tys1)  <- splitTyConApp_maybe ty1
+  , Just (tc2, tys2)  <- splitTyConApp_maybe ty2
   , tc1 == tc2
+  , isInjectiveTyCon tc r  -- See Note [NthCo and newtypes] in TyCoRep
   , let n = length tys1
+  , tys2 `lengthIs` n      -- This can fail in an erroneous progam
+                           -- E.g. T a ~# T a b
+                           -- Trac #14607
   = ASSERT( tc == tc1 )
-    ASSERT( n == length tys2 )
-    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
@@ -738,4 +1188,10 @@ because if g is well-kinded then
   kind (s1 t2) = kind (s2 t2)
 and these two imply
   kind s1 = kind s2
+
 -}
+
+optForAllCoBndr :: LiftingContext -> Bool
+                -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
+optForAllCoBndr env sym
+  = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env