never executed always true always false
    1 -- (c) The University of Glasgow 2006
    2 
    3 {-# LANGUAGE CPP #-}
    4 
    5 module GHC.Core.Coercion.Opt
    6    ( optCoercion
    7    , checkAxInstCo
    8    , OptCoercionOpts (..)
    9    )
   10 where
   11 
   12 import GHC.Prelude
   13 
   14 import GHC.Tc.Utils.TcType   ( exactTyCoVarsOfType )
   15 
   16 import GHC.Core.TyCo.Rep
   17 import GHC.Core.TyCo.Subst
   18 import GHC.Core.Coercion
   19 import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
   20 import GHC.Core.TyCon
   21 import GHC.Core.Coercion.Axiom
   22 import GHC.Core.Unify
   23 
   24 import GHC.Types.Var.Set
   25 import GHC.Types.Var.Env
   26 
   27 import GHC.Data.Pair
   28 import GHC.Data.List.SetOps ( getNth )
   29 
   30 import GHC.Utils.Outputable
   31 import GHC.Utils.Constants (debugIsOn)
   32 import GHC.Utils.Misc
   33 import GHC.Utils.Panic
   34 import GHC.Utils.Panic.Plain
   35 import GHC.Utils.Trace
   36 
   37 import Control.Monad   ( zipWithM )
   38 
   39 {-
   40 %************************************************************************
   41 %*                                                                      *
   42                  Optimising coercions
   43 %*                                                                      *
   44 %************************************************************************
   45 
   46 Note [Optimising coercion optimisation]
   47 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   48 Looking up a coercion's role or kind is linear in the size of the
   49 coercion. Thus, doing this repeatedly during the recursive descent
   50 of coercion optimisation is disastrous. We must be careful to avoid
   51 doing this if at all possible.
   52 
   53 Because it is generally easy to know a coercion's components' roles
   54 from the role of the outer coercion, we pass down the known role of
   55 the input in the algorithm below. We also keep functions opt_co2
   56 and opt_co3 separate from opt_co4, so that the former two do Phantom
   57 checks that opt_co4 can avoid. This is a big win because Phantom coercions
   58 rarely appear within non-phantom coercions -- only in some TyConAppCos
   59 and some AxiomInstCos. We handle these cases specially by calling
   60 opt_co2.
   61 
   62 Note [Optimising InstCo]
   63 ~~~~~~~~~~~~~~~~~~~~~~~~
   64 (1) tv is a type variable
   65 When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.
   66 
   67 Let's look at the typing rules.
   68 
   69 h : k1 ~ k2
   70 tv:k1 |- g : t1 ~ t2
   71 -----------------------------
   72 ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])
   73 
   74 g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
   75 g2 : s1 ~ s2
   76 --------------------
   77 InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]
   78 
   79 We thus want some coercion proving this:
   80 
   81   (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])
   82 
   83 If we substitute the *type* tv for the *coercion*
   84 (g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly.
   85 This is bizarre,
   86 though, because we're substituting a type variable with a coercion. However,
   87 this operation already exists: it's called *lifting*, and defined in GHC.Core.Coercion.
   88 We just need to enhance the lifting operation to be able to deal with
   89 an ambient substitution, which is why a LiftingContext stores a TCvSubst.
   90 
   91 (2) cv is a coercion variable
   92 Now consider we have (InstCo (ForAllCo cv h g) g2), we want to optimise.
   93 
   94 h : (t1 ~r t2) ~N (t3 ~r t4)
   95 cv : t1 ~r t2 |- g : t1' ~r2 t2'
   96 n1 = nth r 2 (downgradeRole r N h) :: t1 ~r t3
   97 n2 = nth r 3 (downgradeRole r N h) :: t2 ~r t4
   98 ------------------------------------------------
   99 ForAllCo cv h g : (all cv:t1 ~r t2. t1') ~r2
  100                   (all cv:t3 ~r t4. t2'[cv |-> n1 ; cv ; sym n2])
  101 
  102 g1 : (all cv:t1 ~r t2. t1') ~ (all cv: t3 ~r t4. t2')
  103 g2 : h1 ~N h2
  104 h1 : t1 ~r t2
  105 h2 : t3 ~r t4
  106 ------------------------------------------------
  107 InstCo g1 g2 : t1'[cv |-> h1] ~ t2'[cv |-> h2]
  108 
  109 We thus want some coercion proving this:
  110 
  111   t1'[cv |-> h1] ~ t2'[cv |-> n1 ; h2; sym n2]
  112 
  113 So we substitute the coercion variable c for the coercion
  114 (h1 ~N (n1; h2; sym n2)) in g.
  115 -}
  116 
  117 -- | Coercion optimisation options
  118 newtype OptCoercionOpts = OptCoercionOpts
  119    { optCoercionEnabled :: Bool  -- ^ Enable coercion optimisation (reduce its size)
  120    }
  121 
  122 optCoercion :: OptCoercionOpts -> TCvSubst -> Coercion -> NormalCo
  123 -- ^ optCoercion applies a substitution to a coercion,
  124 --   *and* optimises it to reduce its size
  125 optCoercion opts env co
  126   | optCoercionEnabled opts = optCoercion' env co
  127   | otherwise               = substCo env co
  128 
  129 optCoercion' :: TCvSubst -> Coercion -> NormalCo
  130 optCoercion' env co
  131   | debugIsOn
  132   = let out_co = opt_co1 lc False co
  133         (Pair in_ty1  in_ty2,  in_role)  = coercionKindRole co
  134         (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
  135     in
  136     assertPpr (substTyUnchecked env in_ty1 `eqType` out_ty1 &&
  137                substTyUnchecked env in_ty2 `eqType` out_ty2 &&
  138                in_role == out_role)
  139               ( text "optCoercion changed types!"
  140                  $$ hang (text "in_co:") 2 (ppr co)
  141                  $$ hang (text "in_ty1:") 2 (ppr in_ty1)
  142                  $$ hang (text "in_ty2:") 2 (ppr in_ty2)
  143                  $$ hang (text "out_co:") 2 (ppr out_co)
  144                  $$ hang (text "out_ty1:") 2 (ppr out_ty1)
  145                  $$ hang (text "out_ty2:") 2 (ppr out_ty2)
  146                  $$ hang (text "subst:") 2 (ppr env))
  147               out_co
  148 
  149   | otherwise         = opt_co1 lc False co
  150   where
  151     lc = mkSubstLiftingContext env
  152 
  153 type NormalCo    = Coercion
  154   -- Invariants:
  155   --  * The substitution has been fully applied
  156   --  * For trans coercions (co1 `trans` co2)
  157   --       co1 is not a trans, and neither co1 nor co2 is identity
  158 
  159 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
  160 
  161 -- | Do we apply a @sym@ to the result?
  162 type SymFlag = Bool
  163 
  164 -- | Do we force the result to be representational?
  165 type ReprFlag = Bool
  166 
  167 -- | Optimize a coercion, making no assumptions. All coercions in
  168 -- the lifting context are already optimized (and sym'd if nec'y)
  169 opt_co1 :: LiftingContext
  170         -> SymFlag
  171         -> Coercion -> NormalCo
  172 opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
  173 
  174 -- See Note [Optimising coercion optimisation]
  175 -- | Optimize a coercion, knowing the coercion's role. No other assumptions.
  176 opt_co2 :: LiftingContext
  177         -> SymFlag
  178         -> Role   -- ^ The role of the input coercion
  179         -> Coercion -> NormalCo
  180 opt_co2 env sym Phantom co = opt_phantom env sym co
  181 opt_co2 env sym r       co = opt_co3 env sym Nothing r co
  182 
  183 -- See Note [Optimising coercion optimisation]
  184 -- | Optimize a coercion, knowing the coercion's non-Phantom role.
  185 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
  186 opt_co3 env sym (Just Phantom)          _ co = opt_phantom env sym co
  187 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True  r co
  188   -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
  189 opt_co3 env sym _                       r co = opt_co4_wrap env sym False r co
  190 
  191 -- See Note [Optimising coercion optimisation]
  192 -- | Optimize a non-phantom coercion.
  193 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
  194 
  195 opt_co4_wrap = opt_co4
  196 {-
  197 opt_co4_wrap env sym rep r co
  198   = pprTrace "opt_co4_wrap {"
  199     ( vcat [ text "Sym:" <+> ppr sym
  200            , text "Rep:" <+> ppr rep
  201            , text "Role:" <+> ppr r
  202            , text "Co:" <+> ppr co ]) $
  203     assert (r == coercionRole co )
  204     let result = opt_co4 env sym rep r co in
  205     pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
  206     result
  207 -}
  208 
  209 opt_co4 env _   rep r (Refl ty)
  210   = assertPpr (r == Nominal)
  211               (text "Expected role:" <+> ppr r    $$
  212                text "Found role:" <+> ppr Nominal $$
  213                text "Type:" <+> ppr ty) $
  214     liftCoSubst (chooseRole rep r) env ty
  215 
  216 opt_co4 env _   rep r (GRefl _r ty MRefl)
  217   = assertPpr (r == _r)
  218               (text "Expected role:" <+> ppr r $$
  219                text "Found role:" <+> ppr _r   $$
  220                text "Type:" <+> ppr ty) $
  221     liftCoSubst (chooseRole rep r) env ty
  222 
  223 opt_co4 env sym  rep r (GRefl _r ty (MCo co))
  224   = assertPpr (r == _r)
  225               (text "Expected role:" <+> ppr r $$
  226                text "Found role:" <+> ppr _r   $$
  227                text "Type:" <+> ppr ty) $
  228     if isGReflCo co || isGReflCo co'
  229     then liftCoSubst r' env ty
  230     else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
  231   where
  232     r'  = chooseRole rep r
  233     ty' = substTy (lcSubstLeft env) ty
  234     co' = opt_co4 env False False Nominal co
  235 
  236 opt_co4 env sym rep r (SymCo co)  = opt_co4_wrap env (not sym) rep r co
  237   -- surprisingly, we don't have to do anything to the env here. This is
  238   -- because any "lifting" substitutions in the env are tied to ForAllCos,
  239   -- which treat their left and right sides differently. We don't want to
  240   -- exchange them.
  241 
  242 opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
  243   = assert (r == _r) $
  244     case (rep, r) of
  245       (True, Nominal) ->
  246         mkTyConAppCo Representational tc
  247                      (zipWith3 (opt_co3 env sym)
  248                                (map Just (tyConRolesRepresentational tc))
  249                                (repeat Nominal)
  250                                cos)
  251       (False, Nominal) ->
  252         mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
  253       (_, Representational) ->
  254                       -- must use opt_co2 here, because some roles may be P
  255                       -- See Note [Optimising coercion optimisation]
  256         mkTyConAppCo r tc (zipWith (opt_co2 env sym)
  257                                    (tyConRolesRepresentational tc)  -- the current roles
  258                                    cos)
  259       (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
  260 
  261 opt_co4 env sym rep r (AppCo co1 co2)
  262   = mkAppCo (opt_co4_wrap env sym rep r co1)
  263             (opt_co4_wrap env sym False Nominal co2)
  264 
  265 opt_co4 env sym rep r (ForAllCo tv k_co co)
  266   = case optForAllCoBndr env sym tv k_co of
  267       (env', tv', k_co') -> mkForAllCo tv' k_co' $
  268                             opt_co4_wrap env' sym rep r co
  269      -- Use the "mk" functions to check for nested Refls
  270 
  271 opt_co4 env sym rep r (FunCo _r cow co1 co2)
  272   = assert (r == _r) $
  273     if rep
  274     then mkFunCo Representational cow' co1' co2'
  275     else mkFunCo r cow' co1' co2'
  276   where
  277     co1' = opt_co4_wrap env sym rep r co1
  278     co2' = opt_co4_wrap env sym rep r co2
  279     cow' = opt_co1 env sym cow
  280 
  281 opt_co4 env sym rep r (CoVarCo cv)
  282   | Just co <- lookupCoVar (lcTCvSubst env) cv
  283   = opt_co4_wrap (zapLiftingContext env) sym rep r co
  284 
  285   | ty1 `eqType` ty2   -- See Note [Optimise CoVarCo to Refl]
  286   = mkReflCo (chooseRole rep r) ty1
  287 
  288   | otherwise
  289   = assert (isCoVar cv1 )
  290     wrapRole rep r $ wrapSym sym $
  291     CoVarCo cv1
  292 
  293   where
  294     Pair ty1 ty2 = coVarTypes cv1
  295 
  296     cv1 = case lookupInScope (lcInScopeSet env) cv of
  297              Just cv1 -> cv1
  298              Nothing  -> warnPprTrace True
  299                           (text "opt_co: not in scope:" <+> ppr cv $$ ppr env)
  300                           cv
  301           -- cv1 might have a substituted kind!
  302 
  303 opt_co4 _ _ _ _ (HoleCo h)
  304   = pprPanic "opt_univ fell into a hole" (ppr h)
  305 
  306 opt_co4 env sym rep r (AxiomInstCo con ind cos)
  307     -- Do *not* push sym inside top-level axioms
  308     -- e.g. if g is a top-level axiom
  309     --   g a : f a ~ a
  310     -- then (sym (g ty)) /= g (sym ty) !!
  311   = assert (r == coAxiomRole con )
  312     wrapRole rep (coAxiomRole con) $
  313     wrapSym sym $
  314                        -- some sub-cos might be P: use opt_co2
  315                        -- See Note [Optimising coercion optimisation]
  316     AxiomInstCo con ind (zipWith (opt_co2 env False)
  317                                  (coAxBranchRoles (coAxiomNthBranch con ind))
  318                                  cos)
  319       -- Note that the_co does *not* have sym pushed into it
  320 
  321 opt_co4 env sym rep r (UnivCo prov _r t1 t2)
  322   = assert (r == _r )
  323     opt_univ env sym prov (chooseRole rep r) t1 t2
  324 
  325 opt_co4 env sym rep r (TransCo co1 co2)
  326                       -- sym (g `o` h) = sym h `o` sym g
  327   | sym       = opt_trans in_scope co2' co1'
  328   | otherwise = opt_trans in_scope co1' co2'
  329   where
  330     co1' = opt_co4_wrap env sym rep r co1
  331     co2' = opt_co4_wrap env sym rep r co2
  332     in_scope = lcInScopeSet env
  333 
  334 opt_co4 env _sym rep r (NthCo _r n co)
  335   | Just (ty, _) <- isReflCo_maybe co
  336   , Just (_tc, args) <- assert (r == _r )
  337                         splitTyConApp_maybe ty
  338   = liftCoSubst (chooseRole rep r) env (args `getNth` n)
  339 
  340   | Just (ty, _) <- isReflCo_maybe co
  341   , n == 0
  342   , Just (tv, _) <- splitForAllTyCoVar_maybe ty
  343       -- works for both tyvar and covar
  344   = liftCoSubst (chooseRole rep r) env (varType tv)
  345 
  346 opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
  347   = assert (r == r1 )
  348     opt_co4_wrap env sym rep r (cos `getNth` n)
  349 
  350 -- see the definition of GHC.Builtin.Types.Prim.funTyCon
  351 opt_co4 env sym rep r (NthCo r1 n (FunCo _r2 w co1 co2))
  352   = assert (r == r1 )
  353     opt_co4_wrap env sym rep r (mkNthCoFunCo n w co1 co2)
  354 
  355 opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
  356       -- works for both tyvar and covar
  357   = assert (r == _r )
  358     assert (n == 0 )
  359     opt_co4_wrap env sym rep Nominal eta
  360 
  361 opt_co4 env sym rep r (NthCo _r n co)
  362   | Just nth_co <- case co' of
  363       TyConAppCo _ _ cos -> Just (cos `getNth` n)
  364       FunCo _ w co1 co2  -> Just (mkNthCoFunCo n w co1 co2)
  365       ForAllCo _ eta _   -> Just eta
  366       _                  -> Nothing
  367   = if rep && (r == Nominal)
  368       -- keep propagating the SubCo
  369     then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
  370     else nth_co
  371 
  372   | otherwise
  373   = wrapRole rep r $ NthCo r n co'
  374   where
  375     co' = opt_co1 env sym co
  376 
  377 opt_co4 env sym rep r (LRCo lr co)
  378   | Just pr_co <- splitAppCo_maybe co
  379   = assert (r == Nominal )
  380     opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
  381   | Just pr_co <- splitAppCo_maybe co'
  382   = assert (r == Nominal) $
  383     if rep
  384     then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
  385     else pick_lr lr pr_co
  386   | otherwise
  387   = wrapRole rep Nominal $ LRCo lr co'
  388   where
  389     co' = opt_co4_wrap env sym False Nominal co
  390 
  391     pick_lr CLeft  (l, _) = l
  392     pick_lr CRight (_, r) = r
  393 
  394 -- See Note [Optimising InstCo]
  395 opt_co4 env sym rep r (InstCo co1 arg)
  396     -- forall over type...
  397   | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
  398   = opt_co4_wrap (extendLiftingContext env tv
  399                     (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg))
  400                    -- mkSymCo kind_co :: k1 ~ k2
  401                    -- sym_arg :: (t1 :: k1) ~ (t2 :: k2)
  402                    -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
  403                  sym rep r co_body
  404 
  405     -- forall over coercion...
  406   | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
  407   , CoercionTy h1 <- t1
  408   , CoercionTy h2 <- t2
  409   = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
  410     in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
  411 
  412     -- See if it is a forall after optimization
  413     -- If so, do an inefficient one-variable substitution, then re-optimize
  414 
  415     -- forall over type...
  416   | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
  417   = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
  418                     (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
  419             False False r' co_body'
  420 
  421     -- forall over coercion...
  422   | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
  423   , CoercionTy h1' <- t1'
  424   , CoercionTy h2' <- t2'
  425   = let new_co = mk_new_co cv' kind_co' h1' h2'
  426     in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
  427                     False False r' co_body'
  428 
  429   | otherwise = InstCo co1' arg'
  430   where
  431     co1'    = opt_co4_wrap env sym rep r co1
  432     r'      = chooseRole rep r
  433     arg'    = opt_co4_wrap env sym False Nominal arg
  434     sym_arg = wrapSym sym arg'
  435 
  436     -- Performance note: don't be alarmed by the two calls to coercionKind
  437     -- here, as only one call to coercionKind is actually demanded per guard.
  438     -- t1/t2 are used when checking if co1 is a forall, and t1'/t2' are used
  439     -- when checking if co1' (i.e., co1 post-optimization) is a forall.
  440     --
  441     -- t1/t2 must come from sym_arg, not arg', since it's possible that arg'
  442     -- might have an extra Sym at the front (after being optimized) that co1
  443     -- lacks, so we need to use sym_arg to balance the number of Syms. (#15725)
  444     Pair t1  t2  = coercionKind sym_arg
  445     Pair t1' t2' = coercionKind arg'
  446 
  447     mk_new_co cv kind_co h1 h2
  448       = let -- h1 :: (t1 ~ t2)
  449             -- h2 :: (t3 ~ t4)
  450             -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4)
  451             -- n1 :: t1 ~ t3
  452             -- n2 :: t2 ~ t4
  453             -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
  454             r2  = coVarRole cv
  455             kind_co' = downgradeRole r2 Nominal kind_co
  456             n1 = mkNthCo r2 2 kind_co'
  457             n2 = mkNthCo r2 3 kind_co'
  458          in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
  459                            (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
  460 
  461 opt_co4 env sym _rep r (KindCo co)
  462   = assert (r == Nominal) $
  463     let kco' = promoteCoercion co in
  464     case kco' of
  465       KindCo co' -> promoteCoercion (opt_co1 env sym co')
  466       _          -> opt_co4_wrap env sym False Nominal kco'
  467   -- This might be able to be optimized more to do the promotion
  468   -- and substitution/optimization at the same time
  469 
  470 opt_co4 env sym _ r (SubCo co)
  471   = assert (r == Representational) $
  472     opt_co4_wrap env sym True Nominal co
  473 
  474 -- This could perhaps be optimized more.
  475 opt_co4 env sym rep r (AxiomRuleCo co cs)
  476   = assert (r == coaxrRole co) $
  477     wrapRole rep r $
  478     wrapSym sym $
  479     AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
  480 
  481 {- Note [Optimise CoVarCo to Refl]
  482 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  483 If we have (c :: t~t) we can optimise it to Refl. That increases the
  484 chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)
  485 
  486 We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
  487 in GHC.Core.Coercion.
  488 -}
  489 
  490 -------------
  491 -- | Optimize a phantom coercion. The input coercion may not necessarily
  492 -- be a phantom, but the output sure will be.
  493 opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
  494 opt_phantom env sym co
  495   = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
  496   where
  497     Pair ty1 ty2 = coercionKind co
  498 
  499 {- Note [Differing kinds]
  500    ~~~~~~~~~~~~~~~~~~~~~~
  501 The two types may not have the same kind (although that would be very unusual).
  502 But even if they have the same kind, and the same type constructor, the number
  503 of arguments in a `CoTyConApp` can differ. Consider
  504 
  505   Any :: forall k. k
  506 
  507   Any * Int                      :: *
  508   Any (*->*) Maybe Int  :: *
  509 
  510 Hence the need to compare argument lengths; see #13658
  511 
  512 Note [opt_univ needs injectivity]
  513 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  514 If opt_univ sees a coercion between `T a1 a2` and `T b1 b2` it will optimize it
  515 by producing a TyConAppCo for T, and pushing the UnivCo into the arguments.  But
  516 this works only if T is injective. Otherwise we can have something like
  517 
  518   type family F x where
  519     F Int  = Int
  520     F Bool = Int
  521 
  522 where `UnivCo :: F Int ~ F Bool` is reasonable (it is effectively just an
  523 alternative representation for a couple of uses of AxiomInstCos) but we do not
  524 want to produce `F (UnivCo :: Int ~ Bool)` where the inner coercion is clearly
  525 inconsistent.  Hence the opt_univ case for TyConApps checks isInjectiveTyCon.
  526 See #19509.
  527 
  528  -}
  529 
  530 opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
  531          -> Type -> Type -> Coercion
  532 opt_univ env sym (PhantomProv h) _r ty1 ty2
  533   | sym       = mkPhantomCo h' ty2' ty1'
  534   | otherwise = mkPhantomCo h' ty1' ty2'
  535   where
  536     h' = opt_co4 env sym False Nominal h
  537     ty1' = substTy (lcSubstLeft  env) ty1
  538     ty2' = substTy (lcSubstRight env) ty2
  539 
  540 opt_univ env sym prov role oty1 oty2
  541   | Just (tc1, tys1) <- splitTyConApp_maybe oty1
  542   , Just (tc2, tys2) <- splitTyConApp_maybe oty2
  543   , tc1 == tc2
  544   , isInjectiveTyCon tc1 role  -- see Note [opt_univ needs injectivity]
  545   , equalLength tys1 tys2 -- see Note [Differing kinds]
  546       -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
  547       -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
  548   = let roles    = tyConRolesX role tc1
  549         arg_cos  = zipWith3 (mkUnivCo prov') roles tys1 tys2
  550         arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
  551     in
  552     mkTyConAppCo role tc1 arg_cos'
  553 
  554   -- can't optimize the AppTy case because we can't build the kind coercions.
  555 
  556   | Just (tv1, ty1) <- splitForAllTyVar_maybe oty1
  557   , Just (tv2, ty2) <- splitForAllTyVar_maybe oty2
  558       -- NB: prov isn't interesting here either
  559   = let k1   = tyVarKind tv1
  560         k2   = tyVarKind tv2
  561         eta  = mkUnivCo prov' Nominal k1 k2
  562           -- eta gets opt'ed soon, but not yet.
  563         ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
  564 
  565         (env', tv1', eta') = optForAllCoBndr env sym tv1 eta
  566     in
  567     mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
  568 
  569   | Just (cv1, ty1) <- splitForAllCoVar_maybe oty1
  570   , Just (cv2, ty2) <- splitForAllCoVar_maybe oty2
  571       -- NB: prov isn't interesting here either
  572   = let k1    = varType cv1
  573         k2    = varType cv2
  574         r'    = coVarRole cv1
  575         eta   = mkUnivCo prov' Nominal k1 k2
  576         eta_d = downgradeRole r' Nominal eta
  577           -- eta gets opt'ed soon, but not yet.
  578         n_co  = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
  579                 (mkCoVarCo cv1) `mkTransCo`
  580                 (mkNthCo r' 3 eta_d)
  581         ty2'  = substTyWithCoVars [cv2] [n_co] ty2
  582 
  583         (env', cv1', eta') = optForAllCoBndr env sym cv1 eta
  584     in
  585     mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2')
  586 
  587   | otherwise
  588   = let ty1 = substTyUnchecked (lcSubstLeft  env) oty1
  589         ty2 = substTyUnchecked (lcSubstRight env) oty2
  590         (a, b) | sym       = (ty2, ty1)
  591                | otherwise = (ty1, ty2)
  592     in
  593     mkUnivCo prov' role a b
  594 
  595   where
  596     prov' = case prov of
  597 #if __GLASGOW_HASKELL__ < 901
  598 -- This alt is redundant with the first match of the FunDef
  599       PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
  600 #endif
  601       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
  602       PluginProv _       -> prov
  603       CorePrepProv _     -> prov
  604 
  605 -------------
  606 opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
  607 opt_transList is = zipWithEqual "opt_transList" (opt_trans is)
  608   -- The input lists must have identical length.
  609 
  610 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
  611 opt_trans is co1 co2
  612   | isReflCo co1 = co2
  613     -- optimize when co1 is a Refl Co
  614   | otherwise    = opt_trans1 is co1 co2
  615 
  616 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
  617 -- First arg is not the identity
  618 opt_trans1 is co1 co2
  619   | isReflCo co2 = co1
  620     -- optimize when co2 is a Refl Co
  621   | otherwise    = opt_trans2 is co1 co2
  622 
  623 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
  624 -- Neither arg is the identity
  625 opt_trans2 is (TransCo co1a co1b) co2
  626     -- Don't know whether the sub-coercions are the identity
  627   = opt_trans is co1a (opt_trans is co1b co2)
  628 
  629 opt_trans2 is co1 co2
  630   | Just co <- opt_trans_rule is co1 co2
  631   = co
  632 
  633 opt_trans2 is co1 (TransCo co2a co2b)
  634   | Just co1_2a <- opt_trans_rule is co1 co2a
  635   = if isReflCo co1_2a
  636     then co2b
  637     else opt_trans1 is co1_2a co2b
  638 
  639 opt_trans2 _ co1 co2
  640   = mkTransCo co1 co2
  641 
  642 ------
  643 -- Optimize coercions with a top-level use of transitivity.
  644 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
  645 
  646 opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
  647   = assert (r1 == r2) $
  648     fireTransRule "GRefl" in_co1 in_co2 $
  649     mkGReflRightCo r1 t1 (opt_trans is co1 co2)
  650 
  651 -- Push transitivity through matching destructors
  652 opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
  653   | d1 == d2
  654   , coercionRole co1 == coercionRole co2
  655   , co1 `compatible_co` co2
  656   = assert (r1 == r2) $
  657     fireTransRule "PushNth" in_co1 in_co2 $
  658     mkNthCo r1 d1 (opt_trans is co1 co2)
  659 
  660 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
  661   | d1 == d2
  662   , co1 `compatible_co` co2
  663   = fireTransRule "PushLR" in_co1 in_co2 $
  664     mkLRCo d1 (opt_trans is co1 co2)
  665 
  666 -- Push transitivity inside instantiation
  667 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
  668   | ty1 `eqCoercion` ty2
  669   , co1 `compatible_co` co2
  670   = fireTransRule "TrPushInst" in_co1 in_co2 $
  671     mkInstCo (opt_trans is co1 co2) ty1
  672 
  673 opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
  674                   in_co2@(UnivCo p2 r2 _tyl2 tyr2)
  675   | Just prov' <- opt_trans_prov p1 p2
  676   = assert (r1 == r2) $
  677     fireTransRule "UnivCo" in_co1 in_co2 $
  678     mkUnivCo prov' r1 tyl1 tyr2
  679   where
  680     -- if the provenances are different, opt'ing will be very confusing
  681     opt_trans_prov (PhantomProv kco1)    (PhantomProv kco2)
  682       = Just $ PhantomProv $ opt_trans is kco1 kco2
  683     opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
  684       = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
  685     opt_trans_prov (PluginProv str1)     (PluginProv str2)     | str1 == str2 = Just p1
  686     opt_trans_prov _ _ = Nothing
  687 
  688 -- Push transitivity down through matching top-level constructors.
  689 opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
  690   | tc1 == tc2
  691   = assert (r1 == r2) $
  692     fireTransRule "PushTyConApp" in_co1 in_co2 $
  693     mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
  694 
  695 opt_trans_rule is in_co1@(FunCo r1 w1 co1a co1b) in_co2@(FunCo r2 w2 co2a co2b)
  696   = assert (r1 == r2) $   -- Just like the TyConAppCo/TyConAppCo case
  697     fireTransRule "PushFun" in_co1 in_co2 $
  698     mkFunCo r1 (opt_trans is w1 w2) (opt_trans is co1a co2a) (opt_trans is co1b co2b)
  699 
  700 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
  701   -- Must call opt_trans_rule_app; see Note [EtaAppCo]
  702   = opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b]
  703 
  704 -- Eta rules
  705 opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
  706   | Just cos2 <- etaTyConAppCo_maybe tc co2
  707   = fireTransRule "EtaCompL" co1 co2 $
  708     mkTyConAppCo r tc (opt_transList is cos1 cos2)
  709 
  710 opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
  711   | Just cos1 <- etaTyConAppCo_maybe tc co1
  712   = fireTransRule "EtaCompR" co1 co2 $
  713     mkTyConAppCo r tc (opt_transList is cos1 cos2)
  714 
  715 opt_trans_rule is co1@(AppCo co1a co1b) co2
  716   | Just (co2a,co2b) <- etaAppCo_maybe co2
  717   = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
  718 
  719 opt_trans_rule is co1 co2@(AppCo co2a co2b)
  720   | Just (co1a,co1b) <- etaAppCo_maybe co1
  721   = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
  722 
  723 -- Push transitivity inside forall
  724 -- forall over types.
  725 opt_trans_rule is co1 co2
  726   | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1
  727   , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2
  728   = push_trans tv1 eta1 r1 tv2 eta2 r2
  729 
  730   | Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2
  731   , Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1
  732   = push_trans tv1 eta1 r1 tv2 eta2 r2
  733 
  734   where
  735   push_trans tv1 eta1 r1 tv2 eta2 r2
  736     -- Given:
  737     --   co1 = /\ tv1 : eta1. r1
  738     --   co2 = /\ tv2 : eta2. r2
  739     -- Wanted:
  740     --   /\tv1 : (eta1;eta2).  (r1; r2[tv2 |-> tv1 |> eta1])
  741     = fireTransRule "EtaAllTy_ty" co1 co2 $
  742       mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
  743     where
  744       is' = is `extendInScopeSet` tv1
  745       r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
  746 
  747 -- Push transitivity inside forall
  748 -- forall over coercions.
  749 opt_trans_rule is co1 co2
  750   | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1
  751   , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2
  752   = push_trans cv1 eta1 r1 cv2 eta2 r2
  753 
  754   | Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2
  755   , Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1
  756   = push_trans cv1 eta1 r1 cv2 eta2 r2
  757 
  758   where
  759   push_trans cv1 eta1 r1 cv2 eta2 r2
  760     -- Given:
  761     --   co1 = /\ cv1 : eta1. r1
  762     --   co2 = /\ cv2 : eta2. r2
  763     -- Wanted:
  764     --   n1 = nth 2 eta1
  765     --   n2 = nth 3 eta1
  766     --   nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
  767     = fireTransRule "EtaAllTy_co" co1 co2 $
  768       mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
  769     where
  770       is'  = is `extendInScopeSet` cv1
  771       role = coVarRole cv1
  772       eta1' = downgradeRole role Nominal eta1
  773       n1   = mkNthCo role 2 eta1'
  774       n2   = mkNthCo role 3 eta1'
  775       r2'  = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
  776                                         (mkCoVarCo cv1) `mkTransCo` n2])
  777                     r2
  778 
  779 -- Push transitivity inside axioms
  780 opt_trans_rule is co1 co2
  781 
  782   -- See Note [Why call checkAxInstCo during optimisation]
  783   -- TrPushSymAxR
  784   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
  785   , True <- sym
  786   , Just cos2 <- matchAxiom sym con ind co2
  787   , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
  788   , Nothing <- checkAxInstCo newAxInst
  789   = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
  790 
  791   -- TrPushAxR
  792   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
  793   , False <- sym
  794   , Just cos2 <- matchAxiom sym con ind co2
  795   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
  796   , Nothing <- checkAxInstCo newAxInst
  797   = fireTransRule "TrPushAxR" co1 co2 newAxInst
  798 
  799   -- TrPushSymAxL
  800   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
  801   , True <- sym
  802   , Just cos1 <- matchAxiom (not sym) con ind co1
  803   , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
  804   , Nothing <- checkAxInstCo newAxInst
  805   = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
  806 
  807   -- TrPushAxL
  808   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
  809   , False <- sym
  810   , Just cos1 <- matchAxiom (not sym) con ind co1
  811   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
  812   , Nothing <- checkAxInstCo newAxInst
  813   = fireTransRule "TrPushAxL" co1 co2 newAxInst
  814 
  815   -- TrPushAxSym/TrPushSymAx
  816   | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
  817   , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
  818   , con1 == con2
  819   , ind1 == ind2
  820   , sym1 == not sym2
  821   , let branch = coAxiomNthBranch con1 ind1
  822         qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
  823         lhs  = coAxNthLHS con1 ind1
  824         rhs  = coAxBranchRHS branch
  825         pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
  826   , all (`elemVarSet` pivot_tvs) qtvs
  827   = fireTransRule "TrPushAxSym" co1 co2 $
  828     if sym2
  829        -- TrPushAxSym
  830     then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
  831        -- TrPushSymAx
  832     else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
  833   where
  834     co1_is_axiom_maybe = isAxiom_maybe co1
  835     co2_is_axiom_maybe = isAxiom_maybe co2
  836     role = coercionRole co1 -- should be the same as coercionRole co2!
  837 
  838 opt_trans_rule _ co1 co2        -- Identity rule
  839   | let ty1 = coercionLKind co1
  840         r   = coercionRole co1
  841         ty2 = coercionRKind co2
  842   , ty1 `eqType` ty2
  843   = fireTransRule "RedTypeDirRefl" co1 co2 $
  844     mkReflCo r ty2
  845 
  846 opt_trans_rule _ _ _ = Nothing
  847 
  848 -- See Note [EtaAppCo]
  849 opt_trans_rule_app :: InScopeSet
  850                    -> Coercion   -- original left-hand coercion (printing only)
  851                    -> Coercion   -- original right-hand coercion (printing only)
  852                    -> Coercion   -- left-hand coercion "function"
  853                    -> [Coercion] -- left-hand coercion "args"
  854                    -> Coercion   -- right-hand coercion "function"
  855                    -> [Coercion] -- right-hand coercion "args"
  856                    -> Maybe Coercion
  857 opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
  858   | AppCo co1aa co1ab <- co1a
  859   , Just (co2aa, co2ab) <- etaAppCo_maybe co2a
  860   = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
  861 
  862   | AppCo co2aa co2ab <- co2a
  863   , Just (co1aa, co1ab) <- etaAppCo_maybe co1a
  864   = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
  865 
  866   | otherwise
  867   = assert (co1bs `equalLength` co2bs) $
  868     fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
  869     let rt1a = coercionRKind co1a
  870 
  871         lt2a = coercionLKind co2a
  872         rt2a = coercionRole  co2a
  873 
  874         rt1bs = map coercionRKind co1bs
  875         lt2bs = map coercionLKind co2bs
  876         rt2bs = map coercionRole co2bs
  877 
  878         kcoa = mkKindCo $ buildCoercion lt2a rt1a
  879         kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
  880 
  881         co2a'   = mkCoherenceLeftCo rt2a lt2a kcoa co2a
  882         co2bs'  = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
  883         co2bs'' = zipWith mkTransCo co2bs' co2bs
  884     in
  885     mkAppCos (opt_trans is co1a co2a')
  886              (zipWith (opt_trans is) co1bs co2bs'')
  887 
  888 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
  889 fireTransRule _rule _co1 _co2 res
  890   = Just res
  891 
  892 {-
  893 Note [Conflict checking with AxiomInstCo]
  894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  895 Consider the following type family and axiom:
  896 
  897 type family Equal (a :: k) (b :: k) :: Bool
  898 type instance where
  899   Equal a a = True
  900   Equal a b = False
  901 --
  902 Equal :: forall k::*. k -> k -> Bool
  903 axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
  904            ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }
  905 
  906 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
  907 0-based, so this is the second branch of the axiom.) The problem is that, on
  908 the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
  909 False) and that all is OK. But, all is not OK: we want to use the first branch
  910 of the axiom in this case, not the second. The problem is that the parameters
  911 of the first branch can unify with the supplied coercions, thus meaning that
  912 the first branch should be taken. See also Note [Apartness] in
  913 "GHC.Core.FamInstEnv".
  914 
  915 Note [Why call checkAxInstCo during optimisation]
  916 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  917 It is possible that otherwise-good-looking optimisations meet with disaster
  918 in the presence of axioms with multiple equations. Consider
  919 
  920 type family Equal (a :: *) (b :: *) :: Bool where
  921   Equal a a = True
  922   Equal a b = False
  923 type family Id (a :: *) :: * where
  924   Id a = a
  925 
  926 axEq :: { [a::*].       Equal a a ~ True
  927         ; [a::*, b::*]. Equal a b ~ False }
  928 axId :: [a::*]. Id a ~ a
  929 
  930 co1 = Equal (axId[0] Int) (axId[0] Bool)
  931   :: Equal (Id Int) (Id Bool) ~  Equal Int Bool
  932 co2 = axEq[1] <Int> <Bool>
  933   :: Equal Int Bool ~ False
  934 
  935 We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
  936 co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
  937 happens when we push the coercions inside? We get
  938 
  939 co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
  940   :: Equal (Id Int) (Id Bool) ~ False
  941 
  942 which is bogus! This is because the type system isn't smart enough to know
  943 that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
  944 families. At the time of writing, I (Richard Eisenberg) couldn't think of
  945 a way of detecting this any more efficient than just building the optimised
  946 coercion and checking.
  947 
  948 Note [EtaAppCo]
  949 ~~~~~~~~~~~~~~~
  950 Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
  951 like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
  952 the resultant coercions might not be well kinded. Here is an example (things
  953 labeled with x don't matter in this example):
  954 
  955   k1 :: Type
  956   k2 :: Type
  957 
  958   a :: k1 -> Type
  959   b :: k1
  960 
  961   h :: k1 ~ k2
  962 
  963   co1a :: x1 ~ (a |> (h -> <Type>)
  964   co1b :: x2 ~ (b |> h)
  965 
  966   co2a :: a ~ x3
  967   co2b :: b ~ x4
  968 
  969 First, convince yourself of the following:
  970 
  971   co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
  972   co2a co2b :: a b   ~ x3 x4
  973 
  974   (a |> (h -> <Type>)) (b |> h) `eqType` a b
  975 
  976 That last fact is due to Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep,
  977 where we ignore coercions in types as long as two types' kinds are the same.
  978 In our case, we meet this last condition, because
  979 
  980   (a |> (h -> <Type>)) (b |> h) :: Type
  981     and
  982   a b :: Type
  983 
  984 So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
  985 suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
  986 kinds don't match up.
  987 
  988 The solution here is to twiddle the kinds in the output coercions. First, we
  989 need to find coercions
  990 
  991   ak :: kind(a |> (h -> <Type>)) ~ kind(a)
  992   bk :: kind(b |> h)             ~ kind(b)
  993 
  994 This can be done with mkKindCo and buildCoercion. The latter assumes two
  995 types are identical modulo casts and builds a coercion between them.
  996 
  997 Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
  998 output coercions. These are well-kinded.
  999 
 1000 Also, note that all of this is done after accumulated any nested AppCo
 1001 parameters. This step is to avoid quadratic behavior in calling coercionKind.
 1002 
 1003 The problem described here was first found in dependent/should_compile/dynamic-paper.
 1004 
 1005 -}
 1006 
 1007 -- | Check to make sure that an AxInstCo is internally consistent.
 1008 -- Returns the conflicting branch, if it exists
 1009 -- See Note [Conflict checking with AxiomInstCo]
 1010 checkAxInstCo :: Coercion -> Maybe CoAxBranch
 1011 -- defined here to avoid dependencies in GHC.Core.Coercion
 1012 -- If you edit this function, you may need to update the GHC formalism
 1013 -- See Note [GHC Formalism] in GHC.Core.Lint
 1014 checkAxInstCo (AxiomInstCo ax ind cos)
 1015   = let branch       = coAxiomNthBranch ax ind
 1016         tvs          = coAxBranchTyVars branch
 1017         cvs          = coAxBranchCoVars branch
 1018         incomps      = coAxBranchIncomps branch
 1019         (tys, cotys) = splitAtList tvs (map coercionLKind cos)
 1020         co_args      = map stripCoercionTy cotys
 1021         subst        = zipTvSubst tvs tys `composeTCvSubst`
 1022                        zipCvSubst cvs co_args
 1023         target   = Type.substTys subst (coAxBranchLHS branch)
 1024         in_scope = mkInScopeSet $
 1025                    unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
 1026         flattened_target = flattenTys in_scope target in
 1027     check_no_conflict flattened_target incomps
 1028   where
 1029     check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
 1030     check_no_conflict _    [] = Nothing
 1031     check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
 1032          -- See Note [Apartness] in GHC.Core.FamInstEnv
 1033       | SurelyApart <- tcUnifyTysFG alwaysBindFun flat lhs_incomp
 1034       = check_no_conflict flat rest
 1035       | otherwise
 1036       = Just b
 1037 checkAxInstCo _ = Nothing
 1038 
 1039 
 1040 -----------
 1041 wrapSym :: SymFlag -> Coercion -> Coercion
 1042 wrapSym sym co | sym       = mkSymCo co
 1043                | otherwise = co
 1044 
 1045 -- | Conditionally set a role to be representational
 1046 wrapRole :: ReprFlag
 1047          -> Role         -- ^ current role
 1048          -> Coercion -> Coercion
 1049 wrapRole False _       = id
 1050 wrapRole True  current = downgradeRole Representational current
 1051 
 1052 -- | If we require a representational role, return that. Otherwise,
 1053 -- return the "default" role provided.
 1054 chooseRole :: ReprFlag
 1055            -> Role    -- ^ "default" role
 1056            -> Role
 1057 chooseRole True _ = Representational
 1058 chooseRole _    r = r
 1059 
 1060 -----------
 1061 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
 1062 isAxiom_maybe (SymCo co)
 1063   | Just (sym, con, ind, cos) <- isAxiom_maybe co
 1064   = Just (not sym, con, ind, cos)
 1065 isAxiom_maybe (AxiomInstCo con ind cos)
 1066   = Just (False, con, ind, cos)
 1067 isAxiom_maybe _ = Nothing
 1068 
 1069 matchAxiom :: Bool -- True = match LHS, False = match RHS
 1070            -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
 1071 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
 1072   | CoAxBranch { cab_tvs = qtvs
 1073                , cab_cvs = []   -- can't infer these, so fail if there are any
 1074                , cab_roles = roles
 1075                , cab_lhs = lhs
 1076                , cab_rhs = rhs } <- coAxiomNthBranch ax ind
 1077   , Just subst <- liftCoMatch (mkVarSet qtvs)
 1078                               (if sym then (mkTyConApp tc lhs) else rhs)
 1079                               co
 1080   , all (`isMappedByLC` subst) qtvs
 1081   = zipWithM (liftCoSubstTyVar subst) roles qtvs
 1082 
 1083   | otherwise
 1084   = Nothing
 1085 
 1086 -------------
 1087 compatible_co :: Coercion -> Coercion -> Bool
 1088 -- Check whether (co1 . co2) will be well-kinded
 1089 compatible_co co1 co2
 1090   = x1 `eqType` x2
 1091   where
 1092     x1 = coercionRKind co1
 1093     x2 = coercionLKind co2
 1094 
 1095 -------------
 1096 {-
 1097 etaForAllCo
 1098 ~~~~~~~~~~~~~~~~~
 1099 (1) etaForAllCo_ty_maybe
 1100 Suppose we have
 1101 
 1102   g : all a1:k1.t1  ~  all a2:k2.t2
 1103 
 1104 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
 1105 
 1106   g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))
 1107 
 1108 Call the kind coercion h1 and the body coercion h2. We can see that
 1109 
 1110   h2 : t1 ~ t2[a2 |-> (a1 |> h1)]
 1111 
 1112 According to the typing rule for ForAllCo, we get that
 1113 
 1114   g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])
 1115 
 1116 or
 1117 
 1118   g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> a1])
 1119 
 1120 as desired.
 1121 
 1122 (2) etaForAllCo_co_maybe
 1123 Suppose we have
 1124 
 1125   g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2
 1126 
 1127 Similarly, we do this
 1128 
 1129   g' = all c1:h1. h2
 1130      : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)]
 1131                                               [c1 |-> eta1;c1;sym eta2]
 1132 
 1133 Here,
 1134 
 1135   h1   = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
 1136   eta1 = mkNthCo r 2 h1      :: (s1 ~ s3)
 1137   eta2 = mkNthCo r 3 h1      :: (s2 ~ s4)
 1138   h2   = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
 1139 -}
 1140 etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
 1141 -- Try to make the coercion be of form (forall tv:kind_co. co)
 1142 etaForAllCo_ty_maybe co
 1143   | Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co
 1144   = Just (tv, kind_co, r)
 1145 
 1146   | Pair ty1 ty2  <- coercionKind co
 1147   , Just (tv1, _) <- splitForAllTyVar_maybe ty1
 1148   , isForAllTy_ty ty2
 1149   , let kind_co = mkNthCo Nominal 0 co
 1150   = Just ( tv1, kind_co
 1151          , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
 1152 
 1153   | otherwise
 1154   = Nothing
 1155 
 1156 etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
 1157 -- Try to make the coercion be of form (forall cv:kind_co. co)
 1158 etaForAllCo_co_maybe co
 1159   | Just (cv, kind_co, r) <- splitForAllCo_co_maybe co
 1160   = Just (cv, kind_co, r)
 1161 
 1162   | Pair ty1 ty2  <- coercionKind co
 1163   , Just (cv1, _) <- splitForAllCoVar_maybe ty1
 1164   , isForAllTy_co ty2
 1165   = let kind_co  = mkNthCo Nominal 0 co
 1166         r        = coVarRole cv1
 1167         l_co     = mkCoVarCo cv1
 1168         kind_co' = downgradeRole r Nominal kind_co
 1169         r_co     = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
 1170                    l_co `mkTransCo`
 1171                    (mkNthCo r 3 kind_co')
 1172     in Just ( cv1, kind_co
 1173             , mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
 1174 
 1175   | otherwise
 1176   = Nothing
 1177 
 1178 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
 1179 -- If possible, split a coercion
 1180 --   g :: t1a t1b ~ t2a t2b
 1181 -- into a pair of coercions (left g, right g)
 1182 etaAppCo_maybe co
 1183   | Just (co1,co2) <- splitAppCo_maybe co
 1184   = Just (co1,co2)
 1185   | (Pair ty1 ty2, Nominal) <- coercionKindRole co
 1186   , Just (_,t1) <- splitAppTy_maybe ty1
 1187   , Just (_,t2) <- splitAppTy_maybe ty2
 1188   , let isco1 = isCoercionTy t1
 1189   , let isco2 = isCoercionTy t2
 1190   , isco1 == isco2
 1191   = Just (LRCo CLeft co, LRCo CRight co)
 1192   | otherwise
 1193   = Nothing
 1194 
 1195 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
 1196 -- If possible, split a coercion
 1197 --       g :: T s1 .. sn ~ T t1 .. tn
 1198 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
 1199 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
 1200   = assert (tc == tc2) $ Just cos2
 1201 
 1202 etaTyConAppCo_maybe tc co
 1203   | not (mustBeSaturated tc)
 1204   , (Pair ty1 ty2, r) <- coercionKindRole co
 1205   , Just (tc1, tys1)  <- splitTyConApp_maybe ty1
 1206   , Just (tc2, tys2)  <- splitTyConApp_maybe ty2
 1207   , tc1 == tc2
 1208   , isInjectiveTyCon tc r  -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
 1209   , let n = length tys1
 1210   , tys2 `lengthIs` n      -- This can fail in an erroneous program
 1211                            -- E.g. T a ~# T a b
 1212                            -- #14607
 1213   = assert (tc == tc1) $
 1214     Just (decomposeCo n co (tyConRolesX r tc1))
 1215     -- NB: n might be <> tyConArity tc
 1216     -- e.g.   data family T a :: * -> *
 1217     --        g :: T a b ~ T c d
 1218 
 1219   | otherwise
 1220   = Nothing
 1221 
 1222 {-
 1223 Note [Eta for AppCo]
 1224 ~~~~~~~~~~~~~~~~~~~~
 1225 Suppose we have
 1226    g :: s1 t1 ~ s2 t2
 1227 
 1228 Then we can't necessarily make
 1229    left  g :: s1 ~ s2
 1230    right g :: t1 ~ t2
 1231 because it's possible that
 1232    s1 :: * -> *         t1 :: *
 1233    s2 :: (*->*) -> *    t2 :: * -> *
 1234 and in that case (left g) does not have the same
 1235 kind on either side.
 1236 
 1237 It's enough to check that
 1238   kind t1 = kind t2
 1239 because if g is well-kinded then
 1240   kind (s1 t2) = kind (s2 t2)
 1241 and these two imply
 1242   kind s1 = kind s2
 1243 
 1244 -}
 1245 
 1246 optForAllCoBndr :: LiftingContext -> Bool
 1247                 -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
 1248 optForAllCoBndr env sym
 1249   = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env