never executed always true always false
    1 {-# LANGUAGE BangPatterns #-}
    2 {-# LANGUAGE ScopedTypeVariables #-}
    3 {-# LANGUAGE FlexibleContexts #-}
    4 
    5 module GHC.Core.Reduction
    6   (
    7      -- * Reductions
    8      Reduction(..), ReductionN, ReductionR, HetReduction(..),
    9      Reductions(..),
   10      mkReduction, mkReductions, mkHetReduction, coercionRedn,
   11      reductionOriginalType,
   12      downgradeRedn, mkSubRedn,
   13      mkTransRedn, mkCoherenceRightRedn, mkCoherenceRightMRedn,
   14      mkCastRedn1, mkCastRedn2,
   15      mkReflRedn, mkGReflRightRedn, mkGReflRightMRedn,
   16      mkGReflLeftRedn, mkGReflLeftMRedn,
   17      mkAppRedn, mkAppRedns, mkFunRedn,
   18      mkForAllRedn, mkHomoForAllRedn, mkTyConAppRedn, mkClassPredRedn,
   19      mkProofIrrelRedn, mkReflCoRedn,
   20      homogeniseHetRedn,
   21      unzipRedns,
   22 
   23      -- * Rewriting type arguments
   24      ArgsReductions(..),
   25      simplifyArgsWorker
   26 
   27   ) where
   28 
   29 import GHC.Prelude
   30 
   31 import GHC.Core.Class      ( Class(classTyCon) )
   32 import GHC.Core.Coercion
   33 import GHC.Core.Predicate  ( mkClassPred )
   34 import GHC.Core.TyCon      ( TyCon )
   35 import GHC.Core.Type
   36 
   37 import GHC.Data.Pair       ( Pair(Pair) )
   38 
   39 import GHC.Types.Var       ( setTyVarKind )
   40 import GHC.Types.Var.Env   ( mkInScopeSet )
   41 import GHC.Types.Var.Set   ( TyCoVarSet )
   42 
   43 import GHC.Utils.Misc      ( HasDebugCallStack, equalLength )
   44 import GHC.Utils.Outputable
   45 import GHC.Utils.Panic     ( assertPpr, panic )
   46 
   47 {-
   48 %************************************************************************
   49 %*                                                                      *
   50       Reductions
   51 %*                                                                      *
   52 %************************************************************************
   53 
   54 Note [The Reduction type]
   55 ~~~~~~~~~~~~~~~~~~~~~~~~~
   56 Many functions in the type-checker rewrite a type, using Given type equalitie
   57 or type-family reductions, and return a Reduction, which is just a pair of the
   58 coercion and the RHS type of the coercion:
   59   data Reduction = Reduction Coercion !Type
   60 
   61 The order of the arguments to the constructor serves as a reminder
   62 of what the Type is.  In
   63     Reduction co ty
   64 `ty` appears to the right of `co`, reminding us that we must have:
   65     co :: unrewritten_ty ~ ty
   66 
   67 Example functions that use this datatype:
   68    GHC.Core.FamInstEnv.topNormaliseType_maybe
   69      :: FamInstEnvs -> Type -> Maybe Reduction
   70    GHC.Tc.Solver.Rewrite.rewrite
   71      :: CtEvidence -> TcType -> TcS Reduction
   72 
   73 Having Reduction as a data type, with a strict Type field, rather than using
   74 a pair (Coercion,Type) gives several advantages (see #20161)
   75 * The strictness in Type improved performance in rewriting of type families
   76   (around 2.5% improvement in T9872),
   77 * Compared to the situation before, it gives improved consistency around
   78   orientation of rewritings, as a Reduction is always left-to-right
   79   (the coercion's RHS type is always the type stored in the 'Reduction').
   80   No more 'mkSymCo's needed to convert between left-to-right and right-to-left.
   81 
   82 One could imagine storing the LHS type of the coercion in the Reduction as well,
   83 but in fact `reductionOriginalType` is very seldom used, so it's not worth it.
   84 -}
   85 
   86 -- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.
   87 -- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@
   88 -- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined
   89 -- by the context. That is, the LHS type of the coercion is the original type
   90 -- @ty_in@, while its RHS type is the rewritten type @ty_out@.
   91 --
   92 -- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',
   93 -- which separately stores the kind coercion.
   94 --
   95 -- See Note [The Reduction type].
   96 data Reduction =
   97   Reduction
   98     { reductionCoercion    :: Coercion
   99     , reductionReducedType :: !Type
  100     }
  101 -- N.B. the 'Coercion' field must be lazy: see for instance GHC.Tc.Solver.Rewrite.rewrite_tyvar2
  102 -- which returns an error in the 'Coercion' field when dealing with a Derived constraint
  103 -- (which is OK as this Coercion gets ignored later).
  104 -- We might want to revisit the strictness once Deriveds are removed.
  105 
  106 -- | Stores a heterogeneous reduction.
  107 --
  108 -- The stored kind coercion must relate the kinds of the
  109 -- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,
  110 -- we must have:
  111 --
  112 -- >  co :: ty ~ xi
  113 -- > kco :: typeKind ty ~ typeKind xi
  114 data HetReduction =
  115   HetReduction
  116     Reduction
  117     MCoercionN
  118   -- N.B. strictness annotations don't seem to make a difference here
  119 
  120 -- | Create a heterogeneous reduction.
  121 --
  122 -- Pre-condition: the provided kind coercion (second argument)
  123 -- relates the kinds of the stored reduction.
  124 -- That is, if the coercion stored in the 'Reduction' is of the form
  125 --
  126 -- > co :: ty ~ xi
  127 --
  128 -- Then the kind coercion supplied must be of the form:
  129 --
  130 -- > kco :: typeKind ty ~ typeKind xi
  131 mkHetReduction :: Reduction  -- ^ heterogeneous reduction
  132                -> MCoercionN -- ^ kind coercion
  133                -> HetReduction
  134 mkHetReduction redn mco = HetReduction redn mco
  135 {-# INLINE mkHetReduction #-}
  136 
  137 -- | Homogenise a heterogeneous reduction.
  138 --
  139 -- Given @HetReduction (Reduction co xi) kco@, with
  140 --
  141 -- >  co :: ty ~ xi
  142 -- > kco :: typeKind(ty) ~ typeKind(xi)
  143 --
  144 -- this returns the homogeneous reduction:
  145 --
  146 -- > hco :: ty ~ ( xi |> sym kco )
  147 homogeniseHetRedn :: Role -> HetReduction -> Reduction
  148 homogeniseHetRedn role (HetReduction redn kco)
  149   = mkCoherenceRightMRedn role redn (mkSymMCo kco)
  150 {-# INLINE homogeniseHetRedn #-}
  151 
  152 -- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
  153 --
  154 -- Pre-condition: the RHS type of the coercion matches the provided type
  155 -- (perhaps up to zonking).
  156 --
  157 -- Use 'coercionRedn' when you only have the coercion.
  158 mkReduction :: Coercion -> Type -> Reduction
  159 mkReduction co ty = Reduction co ty
  160 {-# INLINE mkReduction #-}
  161 
  162 instance Outputable Reduction where
  163   ppr redn =
  164     braces $ vcat
  165       [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn)
  166       , text " reductionReducedType:" <+> ppr (reductionReducedType redn)
  167       , text "    reductionCoercion:" <+> ppr (reductionCoercion redn)
  168       ]
  169 
  170 -- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.
  171 type ReductionN = Reduction
  172 
  173 -- | A 'Reduction' in which the 'Coercion' has 'Representational' role.
  174 type ReductionR = Reduction
  175 
  176 -- | Get the original, unreduced type corresponding to a 'Reduction'.
  177 --
  178 -- This is obtained by computing the LHS kind of the stored coercion,
  179 -- which may be slow.
  180 reductionOriginalType :: Reduction -> Type
  181 reductionOriginalType = coercionLKind . reductionCoercion
  182 {-# INLINE reductionOriginalType #-}
  183 
  184 -- | Turn a 'Coercion' into a 'Reduction'
  185 -- by inspecting the RHS type of the coercion.
  186 --
  187 -- Prefer using 'mkReduction' when you already know
  188 -- the RHS type of the coercion, to avoid computing it anew.
  189 coercionRedn :: Coercion -> Reduction
  190 coercionRedn co = Reduction co (coercionRKind co)
  191 {-# INLINE coercionRedn #-}
  192 
  193 -- | Downgrade the role of the coercion stored in the 'Reduction'.
  194 downgradeRedn :: Role -- ^ desired role
  195               -> Role -- ^ current role
  196               -> Reduction
  197               -> Reduction
  198 downgradeRedn new_role old_role redn@(Reduction co _)
  199   = redn { reductionCoercion = downgradeRole new_role old_role co }
  200 {-# INLINE downgradeRedn #-}
  201 
  202 -- | Downgrade the role of the coercion stored in the 'Reduction',
  203 -- from 'Nominal' to 'Representational'.
  204 mkSubRedn :: Reduction -> Reduction
  205 mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co }
  206 {-# INLINE mkSubRedn #-}
  207 
  208 -- | Compose a reduction with a coercion on the left.
  209 --
  210 -- Pre-condition: the provided coercion's RHS type must match the LHS type
  211 -- of the coercion that is stored in the reduction.
  212 mkTransRedn :: Coercion -> Reduction -> Reduction
  213 mkTransRedn co1 redn@(Reduction co2 _)
  214   = redn { reductionCoercion = co1 `mkTransCo` co2 }
  215 {-# INLINE mkTransRedn #-}
  216 
  217 -- | The reflexive reduction.
  218 mkReflRedn :: Role -> Type -> Reduction
  219 mkReflRedn r ty = mkReduction (mkReflCo r ty) ty
  220 
  221 -- | Create a 'Reduction' from a kind cast, in which
  222 -- the casted type is the rewritten type.
  223 --
  224 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
  225 -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
  226 -- at the given 'Role'.
  227 mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
  228 mkGReflRightRedn role ty co
  229   = mkReduction
  230       (mkGReflRightCo role ty co)
  231       (mkCastTy ty co)
  232 {-# INLINE mkGReflRightRedn #-}
  233 
  234 -- | Create a 'Reduction' from a kind cast, in which
  235 -- the casted type is the rewritten type.
  236 --
  237 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
  238 -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
  239 -- at the given 'Role'.
  240 mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction
  241 mkGReflRightMRedn role ty mco
  242   = mkReduction
  243       (mkGReflRightMCo role ty mco)
  244       (mkCastTyMCo ty mco)
  245 {-# INLINE mkGReflRightMRedn #-}
  246 
  247 -- | Create a 'Reduction' from a kind cast, in which
  248 -- the casted type is the original (non-rewritten) type.
  249 --
  250 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
  251 -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
  252 -- at the given 'Role'.
  253 mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
  254 mkGReflLeftRedn role ty co
  255   = mkReduction
  256       (mkGReflLeftCo role ty co)
  257       ty
  258 {-# INLINE mkGReflLeftRedn #-}
  259 
  260 -- | Create a 'Reduction' from a kind cast, in which
  261 -- the casted type is the original (non-rewritten) type.
  262 --
  263 -- Given @ty :: k1@, @mco :: k1 ~ k2@,
  264 -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
  265 -- at the given 'Role'.
  266 mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction
  267 mkGReflLeftMRedn role ty mco
  268   = mkReduction
  269       (mkGReflLeftMCo role ty mco)
  270       ty
  271 {-# INLINE mkGReflLeftMRedn #-}
  272 
  273 -- | Apply a cast to the result of a 'Reduction'.
  274 --
  275 -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@
  276 -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@
  277 -- of the given 'Role' (which must match the role of the coercion stored
  278 -- in the 'Reduction' argument).
  279 mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
  280 mkCoherenceRightRedn r (Reduction co1 ty2) kco
  281   = mkReduction
  282       (mkCoherenceRightCo r ty2 kco co1)
  283       (mkCastTy ty2 kco)
  284 {-# INLINE mkCoherenceRightRedn #-}
  285 
  286 -- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.
  287 --
  288 -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@
  289 -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@
  290 -- of the given 'Role' (which must match the role of the coercion stored
  291 -- in the 'Reduction' argument).
  292 mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction
  293 mkCoherenceRightMRedn r (Reduction co1 ty2) kco
  294   = mkReduction
  295       (mkCoherenceRightMCo r ty2 kco co1)
  296       (mkCastTyMCo ty2 kco)
  297 {-# INLINE mkCoherenceRightMRedn #-}
  298 
  299 -- | Apply a cast to a 'Reduction', casting both the original and the reduced type.
  300 --
  301 -- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns
  302 -- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@
  303 -- of the given 'Role' (which must match the role of the coercion stored
  304 -- in the 'Reduction' argument).
  305 --
  306 -- Pre-condition: the 'Type' passed in is the same as the LHS type
  307 -- of the coercion stored in the 'Reduction'.
  308 mkCastRedn1 :: Role
  309             -> Type      -- ^ original type
  310             -> CoercionN -- ^ coercion to cast with
  311             -> Reduction -- ^ rewritten type, with rewriting coercion
  312             -> Reduction
  313 mkCastRedn1 r ty cast_co (Reduction co xi)
  314   -- co :: ty ~r ty'
  315   -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
  316   = mkReduction
  317       (castCoercionKind1 co r ty xi cast_co)
  318       (mkCastTy xi cast_co)
  319 {-# INLINE mkCastRedn1 #-}
  320 
  321 -- | Apply casts on both sides of a 'Reduction' (of the given 'Role').
  322 --
  323 -- Use 'mkCastRedn1' when you want to cast both the original and reduced types
  324 -- in a 'Reduction' using the same coercion.
  325 --
  326 -- Pre-condition: the 'Type' passed in is the same as the LHS type
  327 -- of the coercion stored in the 'Reduction'.
  328 mkCastRedn2 :: Role
  329             -> Type      -- ^ original type
  330             -> CoercionN -- ^ coercion to cast with on the left
  331             -> Reduction -- ^ rewritten type, with rewriting coercion
  332             -> CoercionN -- ^ coercion to cast with on the right
  333             -> Reduction
  334 mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co'
  335   = mkReduction
  336       (castCoercionKind2 nco r ty nty cast_co cast_co')
  337       (mkCastTy nty cast_co')
  338 {-# INLINE mkCastRedn2 #-}
  339 
  340 -- | Apply one 'Reduction' to another.
  341 --
  342 -- Combines 'mkAppCo' and 'mkAppTy`.
  343 mkAppRedn :: Reduction -> Reduction -> Reduction
  344 mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2)
  345   = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2)
  346 {-# INLINE mkAppRedn #-}
  347 
  348 -- | Create a function 'Reduction'.
  349 --
  350 -- Combines 'mkFunCo' and 'mkFunTy'.
  351 mkFunRedn :: Role
  352           -> AnonArgFlag
  353           -> ReductionN -- ^ multiplicity reduction
  354           -> Reduction  -- ^ argument reduction
  355           -> Reduction  -- ^ result reduction
  356           -> Reduction
  357 mkFunRedn r vis
  358   (Reduction w_co w_ty)
  359   (Reduction arg_co arg_ty)
  360   (Reduction res_co res_ty)
  361     = mkReduction
  362         (mkFunCo r w_co arg_co res_co)
  363         (mkFunTy vis w_ty arg_ty res_ty)
  364 {-# INLINE mkFunRedn #-}
  365 
  366 -- | Create a 'Reduction' associated to a Π type,
  367 -- from a kind 'Reduction' and a body 'Reduction'.
  368 --
  369 -- Combines 'mkForAllCo' and 'mkForAllTy'.
  370 mkForAllRedn :: ArgFlag
  371              -> TyVar
  372              -> ReductionN -- ^ kind reduction
  373              -> Reduction  -- ^ body reduction
  374              -> Reduction
  375 mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
  376   = mkReduction
  377       (mkForAllCo tv1 h co)
  378       (mkForAllTy tv2 vis ty)
  379   where
  380     tv2 = setTyVarKind tv1 ki'
  381 {-# INLINE mkForAllRedn #-}
  382 
  383 -- | Create a 'Reduction' of a quantified type from a
  384 -- 'Reduction' of the body.
  385 --
  386 -- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
  387 mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
  388 mkHomoForAllRedn bndrs (Reduction co ty)
  389   = mkReduction
  390       (mkHomoForAllCos (binderVars bndrs) co)
  391       (mkForAllTys bndrs ty)
  392 {-# INLINE mkHomoForAllRedn #-}
  393 
  394 -- | Create a 'Reduction' from a coercion between coercions.
  395 --
  396 -- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.
  397 mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"
  398                  -> CoercionN -- ^ co :: phi1 ~N phi2
  399                  -> Coercion  -- ^ g1 :: phi1
  400                  -> Coercion  -- ^ g2 :: phi2
  401                  -> Reduction -- ^ res_co :: g1 ~r g2
  402 mkProofIrrelRedn role co g1 g2
  403   = mkReduction
  404       (mkProofIrrelCo role co g1 g2)
  405       (mkCoercionTy g2)
  406 {-# INLINE mkProofIrrelRedn #-}
  407 
  408 -- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',
  409 -- with the specified 'Role'.
  410 mkReflCoRedn :: Role -> Coercion -> Reduction
  411 mkReflCoRedn role co
  412   = mkReduction
  413       (mkReflCo role co_ty)
  414       co_ty
  415   where
  416     co_ty = mkCoercionTy co
  417 {-# INLINE mkReflCoRedn #-}
  418 
  419 -- | A collection of 'Reduction's where the coercions and the types are stored separately.
  420 --
  421 -- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.
  422 --
  423 -- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',
  424 -- which expect separate types and coercions.
  425 --
  426 -- Invariant: the two stored lists are of the same length,
  427 -- and the RHS type of each coercion is the corresponding type.
  428 data Reductions = Reductions [Coercion] [Type]
  429 
  430 -- | Create 'Reductions' from individual lists of coercions and types.
  431 --
  432 -- The lists should be of the same length, and the RHS type of each coercion
  433 -- should match the specified type in the other list.
  434 mkReductions :: [Coercion] -> [Type] -> Reductions
  435 mkReductions cos tys = Reductions cos tys
  436 {-# INLINE mkReductions #-}
  437 
  438 -- | Combines 'mkAppCos' and 'mkAppTys'.
  439 mkAppRedns :: Reduction -> Reductions -> Reduction
  440 mkAppRedns (Reduction co ty) (Reductions cos tys)
  441   = mkReduction (mkAppCos co cos) (mkAppTys ty tys)
  442 {-# INLINE mkAppRedns #-}
  443 
  444 -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
  445 mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
  446 mkTyConAppRedn role tc (Reductions cos tys)
  447   = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys)
  448 {-# INLINE mkTyConAppRedn #-}
  449 
  450 -- | Reduce the arguments of a 'Class' 'TyCon'.
  451 mkClassPredRedn :: Class -> Reductions -> Reduction
  452 mkClassPredRedn cls (Reductions cos tys)
  453   = mkReduction
  454       (mkTyConAppCo Nominal (classTyCon cls) cos)
  455       (mkClassPred cls tys)
  456 {-# INLINE mkClassPredRedn #-}
  457 
  458 -- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
  459 unzipRedns :: [Reduction] -> Reductions
  460 unzipRedns = foldr accRedn (Reductions [] [])
  461   where
  462     accRedn :: Reduction -> Reductions -> Reductions
  463     accRedn (Reduction co xi) (Reductions cos xis)
  464       = Reductions (co:cos) (xi:xis)
  465 {-# INLINE unzipRedns #-}
  466 -- NB: this function is currently used in two locations:
  467 --
  468 -- - GHC.Tc.Gen.Foreign.normaliseFfiType', with one call of the form:
  469 --
  470 --   unzipRedns <$> zipWithM f tys roles
  471 --
  472 -- - GHC.Tc.Solver.Monad.breakTyVarCycle_maybe, with two calls of the form:
  473 --
  474 --   unzipRedns <$> mapM f tys
  475 --
  476 -- It is possible to write 'mapAndUnzipM' functions to handle these cases,
  477 -- but the above locations aren't performance critical, so it was deemed
  478 -- to not be worth it.
  479 
  480 {-
  481 %************************************************************************
  482 %*                                                                      *
  483        Simplifying types
  484 %*                                                                      *
  485 %************************************************************************
  486 
  487 The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in
  488 FamInstEnv, and so lives here.
  489 
  490 Note [simplifyArgsWorker]
  491 ~~~~~~~~~~~~~~~~~~~~~~~~~
  492 Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
  493 rewriting is homogeneous.
  494 This causes some trouble when rewriting a function applied to a telescope
  495 of arguments, perhaps with dependency. For example, suppose
  496 
  497   type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
  498 
  499 and we wish to rewrite the args of (with kind applications explicit)
  500 
  501   F @a @b (Just @a c) (Right @a @b d) False
  502 
  503 where all variables are skolems and
  504 
  505   a :: Type
  506   b :: Type
  507   c :: a
  508   d :: b
  509 
  510   [G] aco :: a ~ fa
  511   [G] bco :: b ~ fb
  512   [G] cco :: c ~ fc
  513   [G] dco :: d ~ fd
  514 
  515 The first step is to rewrite all the arguments. This is done before calling
  516 simplifyArgsWorker. We start from
  517 
  518   a
  519   b
  520   Just @a c
  521   Right @a @b d
  522   False
  523 
  524 and get left-to-right reductions whose coercions are as follows:
  525 
  526   co1 :: a ~ fa
  527   co2 :: b ~ fb
  528   co3 :: (Just @a c) ~ (Just @fa (fc |> aco) |> co6)
  529   co4 :: (Right @a @b d) ~ (Right @fa @fb (fd |> bco) |> co7)
  530   co5 :: False ~ False
  531 
  532 where
  533   co6 = Maybe (sym aco) :: Maybe fa ~ Maybe a
  534   co7 = Either (sym aco) (sym bco) :: Either fa fb ~ Either a b
  535 
  536 We now process the rewritten args in left-to-right order. The first two args
  537 need no further processing. But now consider the third argument. Let f3 = the rewritten
  538 result, Just fa (fc |> aco) |> co6.
  539 This f3 rewritten argument has kind (Maybe a), due to homogeneity of rewriting (F2).
  540 And yet, when we build the application (F @fa @fb ...), we need this
  541 argument to have kind (Maybe fa), not (Maybe a). We must cast this argument.
  542 The coercion to use is determined by the kind of F:
  543 we see in F's kind that the third argument has kind Maybe j.
  544 Critically, we also know that the argument corresponding to j
  545 (in our example, a) rewrote with a coercion co1. We can thus know the
  546 coercion needed for the 3rd argument is (Maybe co1), thus building
  547 (f3 |> Maybe co1)
  548 
  549 More generally, we must use the Lifting Lemma, as implemented in
  550 Coercion.liftCoSubst. As we work left-to-right, any variable that is a
  551 dependent parameter (j and k, in our example) gets mapped in a lifting context
  552 to the coercion that is output from rewriting the corresponding argument (co1
  553 and co2, in our example). Then, after rewriting later arguments, we lift the
  554 kind of these arguments in the lifting context that we've be building up.
  555 This coercion is then used to keep the result of rewriting well-kinded.
  556 
  557 Working through our example, this is what happens:
  558 
  559   1. Extend the (empty) LC with [j |-> co1]. No new casting must be done,
  560      because the binder associated with the first argument has a closed type (no
  561      variables).
  562 
  563   2. Extend the LC with [k |-> co2]. No casting to do.
  564 
  565   3. Lifting the kind (Maybe j) with our LC
  566      yields co8 :: Maybe a ~ Maybe fa. Use (f3 |> co8) as the argument to F.
  567 
  568   4. Lifting the kind (Either j k) with our LC
  569      yields co9 :: Either a b ~ Either fa fb. Use (f4 |> co9) as the 4th
  570      argument to F, where f4 is the rewritten form of argument 4, written above.
  571 
  572   5. We lift Bool with our LC, getting <Bool>; casting has no effect.
  573 
  574 We're now almost done, but the new application
  575 
  576   F @fa @fb (f3 |> co8) (f4 |> co9) False
  577 
  578 has the wrong kind. Its kind is [fb], instead of the original [b].
  579 So we must use our LC one last time to lift the result kind [k],
  580 getting res_co :: [fb] ~ [b], and we cast our result.
  581 
  582 Accordingly, the final result is
  583 
  584   F
  585     @fa
  586     @fb
  587     (Just @fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
  588     (Right @fa @fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
  589     False
  590   |> [sym bco]
  591 
  592 The res_co (in this case, [sym bco]) is the third component of the
  593 tuple returned by simplifyArgsWorker.
  594 
  595 Note [Last case in simplifyArgsWorker]
  596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  597 In writing simplifyArgsWorker's `go`, we know here that args cannot be empty,
  598 because that case is first. We've run out of
  599 binders. But perhaps inner_ki is a tyvar that has been instantiated with a
  600 Π-type.
  601 
  602 Here is an example.
  603 
  604   a :: forall (k :: Type). k -> k
  605   Proxy :: forall j. j -> Type
  606   type family Star
  607   axStar :: Star ~ Type
  608   type family NoWay :: Bool
  609   axNoWay :: NoWay ~ False
  610   bo :: Type
  611   [G] bc :: bo ~ Bool   (in inert set)
  612 
  613   co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
  614   co = forall (j :: sym axStar). (<j> -> sym axStar)
  615 
  616   We are rewriting:
  617   a (forall (j :: Star). (j |> axStar) -> Star)   -- 1
  618     (Proxy |> co)                                 -- 2
  619     (bo |> sym axStar)                            -- 3
  620     (NoWay |> sym bc)                             -- 4
  621       :: Star
  622 
  623 First, we rewrite all the arguments (before simplifyArgsWorker), like so:
  624 
  625     co1 :: (forall (j :: Star). (j |> axStar) -> Star) ~ (forall j. j -> Type) -- 1
  626     co2 :: (Proxy |> co) ~ (Proxy |> co)                                       -- 2
  627     co3 :: (bo |> sym axStar) ~ (Bool |> sym axStar)                           -- 3
  628     co4 :: (NoWay |> sym bc) ~ (False |> sym bc)                               -- 4
  629 
  630 Then we do the process described in Note [simplifyArgsWorker].
  631 
  632 1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
  633    don't use it. But we do build a lifting context [k -> co1] (where co1 is a
  634    result of rewriting an argument, written above).
  635 
  636 2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> co1).
  637    This is not a dependent argument, so we don't extend the lifting context.
  638 
  639 Now we need to deal with argument (3).
  640 The way we normally proceed is to lift the kind of the binder, to see whether
  641 it's dependent.
  642 But here, the remainder of the kind of `a` that we're left with
  643 after processing two arguments is just `k`.
  644 
  645 The way forward is look up k in the lifting context, getting co1. If we're at
  646 all well-typed, co1 will be a coercion between Π-types, with at least one binder.
  647 So, let's decompose co1 with decomposePiCos. This decomposition needs arguments to use
  648 to instantiate any kind parameters. Look at the type of co1. If we just
  649 decomposed it, we would end up with coercions whose types include j, which is
  650 out of scope here. Accordingly, decomposePiCos takes a list of types whose
  651 kinds are the *unrewritten* types in the decomposed coercion. (See comments on
  652 decomposePiCos.) Because the rewritten types have unrewritten kinds (because
  653 rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
  654 just won't do: later arguments' kinds won't be as expected. So we need to get
  655 the *unrewritten* types to pass to decomposePiCos. We can do this easily enough
  656 by taking the kind of the argument coercions, passed in originally.
  657 
  658 (Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
  659 But that function is already gnarly, and other call sites of decomposePiCos
  660 would suffer from the change, even though they are much more common than this one.)
  661 
  662 (Alternative 2: We could avoid calling decomposePiCos entirely, integrating its
  663 behavior into simplifyArgsWorker. This would work, I think, but then all of the
  664 complication of decomposePiCos would end up layered on top of all the complication
  665 here. Please, no.)
  666 
  667 (Alternative 3: We could pass the unrewritten arguments into simplifyArgsWorker
  668 so that we don't have to recreate them. But that would complicate the interface
  669 of this function to handle a very dark, dark corner case. Better to keep our
  670 demons to ourselves here instead of exposing them to callers. This decision is
  671 easily reversed if there is ever any performance trouble due to the call of
  672 coercionKind.)
  673 
  674 So we now call
  675 
  676   decomposePiCos co1
  677                  (Pair (forall (j :: Star). (j |> axStar) -> Star) (forall j. j -> Type))
  678                  [bo |> sym axStar, NoWay |> sym bc]
  679 
  680 to get
  681 
  682   co5 :: Star ~ Type
  683   co6 :: (j |> axStar) ~ (j |> co5), substituted to
  684                               (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5)
  685                            == bo ~ bo
  686   res_co :: Type ~ Star
  687 
  688 We then use these casts on (the rewritten) (3) and (4) to get
  689 
  690   (Bool |> sym axStar |> co5 :: Type)   -- (C3)
  691   (False |> sym bc |> co6    :: bo)     -- (C4)
  692 
  693 We can simplify to
  694 
  695   Bool                        -- (C3)
  696   (False |> sym bc :: bo)     -- (C4)
  697 
  698 Of course, we still must do the processing in Note [simplifyArgsWorker] to finish
  699 the job. We thus want to recur. Our new function kind is the left-hand type of
  700 co1 (gotten, recall, by lifting the variable k that was the return kind of the
  701 original function). Why the left-hand type (as opposed to the right-hand type)?
  702 Because we have casted all the arguments according to decomposePiCos, which gets
  703 us from the right-hand type to the left-hand one. We thus recur with that new
  704 function kind, zapping our lifting context, because we have essentially applied
  705 it.
  706 
  707 This recursive call returns ([Bool, False], [...], Refl). The Bool and False
  708 are the correct arguments we wish to return. But we must be careful about the
  709 result coercion: our new, rewritten application will have kind Type, but we
  710 want to make sure that the result coercion casts this back to Star. (Why?
  711 Because we started with an application of kind Star, and rewriting is homogeneous.)
  712 
  713 So, we have to twiddle the result coercion appropriately.
  714 
  715 Let's check whether this is well-typed. We know
  716 
  717   a :: forall (k :: Type). k -> k
  718 
  719   a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
  720 
  721   a (forall j. j -> Type)
  722     Proxy
  723       :: forall j. j -> Type
  724 
  725   a (forall j. j -> Type)
  726     Proxy
  727     Bool
  728       :: Bool -> Type
  729 
  730   a (forall j. j -> Type)
  731     Proxy
  732     Bool
  733     False
  734       :: Type
  735 
  736   a (forall j. j -> Type)
  737     Proxy
  738     Bool
  739     False
  740      |> res_co
  741      :: Star
  742 
  743 as desired.
  744 
  745 Whew.
  746 
  747 Historical note: I (Richard E) once thought that the final part of the kind
  748 had to be a variable k (as in the example above). But it might not be: it could
  749 be an application of a variable. Here is the example:
  750 
  751   let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
  752       k :: Type
  753       x :: k
  754 
  755   rewrite (f @Type @((->) k) x)
  756 
  757 After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
  758 is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
  759 
  760 -}
  761 
  762 -- | Stores 'Reductions' as well as a kind coercion.
  763 --
  764 -- Used when rewriting arguments to a type function @f@.
  765 --
  766 -- Invariant:
  767 --   when the stored reductions are of the form
  768 --     co_i :: ty_i ~ xi_i,
  769 --   the kind coercion is of the form
  770 --      kco :: typeKind (f ty_1 ... ty_n) ~ typeKind (f xi_1 ... xi_n)
  771 --
  772 -- The type function @f@ depends on context.
  773 data ArgsReductions =
  774   ArgsReductions
  775     {-# UNPACK #-} !Reductions
  776     !MCoercionN
  777   -- The strictness annotations and UNPACK pragma here are crucial
  778   -- to getting good performance in simplifyArgsWorker's tight loop.
  779 
  780 -- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv.
  781 -- See Note [simplifyArgsWorker]
  782 {-# INLINE simplifyArgsWorker #-}
  783 -- NB. INLINE yields a ~1% decrease in allocations in T9872d compared to INLINEABLE
  784 -- This function is only called in two locations, so the amount of code duplication
  785 -- should be rather reasonable despite the size of the function.
  786 simplifyArgsWorker :: HasDebugCallStack
  787                    => [TyCoBinder] -> Kind
  788                        -- the binders & result kind (not a Π-type) of the function applied to the args
  789                        -- list of binders can be shorter or longer than the list of args
  790                    -> TyCoVarSet   -- free vars of the args
  791                    -> [Role]       -- list of roles, r
  792                    -> [Reduction]  -- rewritten type arguments, arg_i
  793                                    -- each comes with the coercion used to rewrite it,
  794                                    -- arg_co_i :: ty_i ~ arg_i
  795                    -> ArgsReductions
  796 -- Returns ArgsReductions (Reductions cos xis) res_co, where co_i :: ty_i ~ xi_i,
  797 -- and res_co :: kind (f ty_1 ... ty_n) ~ kind (f xi_1 ... xi_n), where f is the function
  798 -- that we are applying.
  799 -- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
  800 -- then (f ty_1 ... ty_n) is well kinded. Note that (f arg_1 ... arg_n) might *not* be well-kinded.
  801 -- Massaging the arg_i in order to make the function application well-kinded is what this
  802 -- function is all about. That is, (f xi_1 ... xi_n), where xi_i are the returned arguments,
  803 -- *is* well kinded.
  804 simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
  805                    orig_roles orig_simplified_args
  806   = go orig_lc
  807        orig_ki_binders orig_inner_ki
  808        orig_roles orig_simplified_args
  809   where
  810     orig_lc = emptyLiftingContext $ mkInScopeSet orig_fvs
  811 
  812     go :: LiftingContext  -- mapping from tyvars to rewriting coercions
  813        -> [TyCoBinder]    -- Unsubsted binders of function's kind
  814        -> Kind        -- Unsubsted result kind of function (not a Pi-type)
  815        -> [Role]      -- Roles at which to rewrite these ...
  816        -> [Reduction] -- rewritten arguments, with their rewriting coercions
  817        -> ArgsReductions
  818     go !lc binders inner_ki _ []
  819         -- The !lc makes the function strict in the lifting context
  820         -- which means GHC can unbox that pair.  A modest win.
  821       = ArgsReductions
  822           (mkReductions [] [])
  823           kind_co
  824       where
  825         final_kind = mkPiTys binders inner_ki
  826         kind_co | noFreeVarsOfType final_kind = MRefl
  827                 | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind
  828 
  829     go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns)
  830       =  -- We rewrite an argument ty with arg_redn = Reduction arg_co arg
  831          -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2),
  832          -- tcTypeKind(ty) = tcTypeKind(arg).
  833          -- However, it is possible that arg will be used as an argument to a function
  834          -- whose kind is different, if earlier arguments have been rewritten.
  835          -- We thus need to compose the reduction with a kind coercion to ensure
  836          -- well-kindedness (see the call to mkCoherenceRightRedn below).
  837          --
  838          -- The bangs here have been observed to improve performance
  839          -- significantly in optimized builds; see #18502
  840          let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder)
  841              !(Reduction casted_co casted_xi)
  842                       = mkCoherenceRightRedn role arg_redn kind_co
  843          -- now, extend the lifting context with the new binding
  844              !new_lc | Just tv <- tyCoBinderVar_maybe binder
  845                      = extendLiftingContextAndInScope lc tv casted_co
  846                      | otherwise
  847                      = lc
  848              !(ArgsReductions (Reductions cos xis) final_kind_co)
  849                = go new_lc binders inner_ki roles arg_redns
  850          in ArgsReductions
  851               (Reductions (casted_co:cos) (casted_xi:xis))
  852               final_kind_co
  853 
  854     -- See Note [Last case in simplifyArgsWorker]
  855     go lc [] inner_ki roles arg_redns
  856       = let co1 = liftCoSubst Nominal lc inner_ki
  857             co1_kind              = coercionKind co1
  858             unrewritten_tys       = map reductionOriginalType arg_redns
  859             (arg_cos, res_co)     = decomposePiCos co1 co1_kind unrewritten_tys
  860             casted_args           = assertPpr (equalLength arg_redns arg_cos)
  861                                               (ppr arg_redns $$ ppr arg_cos)
  862                                   $ zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos
  863                -- In general decomposePiCos can return fewer cos than tys,
  864                -- but not here; because we're well typed, there will be enough
  865                -- binders. Note that decomposePiCos does substitutions, so even
  866                -- if the original substitution results in something ending with
  867                -- ... -> k, that k will be substituted to perhaps reveal more
  868                -- binders.
  869             zapped_lc             = zapLiftingContext lc
  870             Pair rewritten_kind _ = co1_kind
  871             (bndrs, new_inner)    = splitPiTys rewritten_kind
  872 
  873             ArgsReductions redns_out res_co_out
  874               = go zapped_lc bndrs new_inner roles casted_args
  875         in
  876           ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out)
  877 
  878     go _ _ _ _ _ = panic
  879         "simplifyArgsWorker wandered into deeper water than usual"
  880            -- This debug information is commented out because leaving it in
  881            -- causes a ~2% increase in allocations in T9872d.
  882            -- That's independent of the analogous case in rewrite_args_fast
  883            -- in GHC.Tc.Solver.Rewrite:
  884            -- each of these causes a 2% increase on its own, so commenting them
  885            -- both out gives a 4% decrease in T9872d.
  886            {-
  887 
  888              (vcat [ppr orig_binders,
  889                     ppr orig_inner_ki,
  890                     ppr (take 10 orig_roles), -- often infinite!
  891                     ppr orig_tys])
  892            -}