never executed always true always false
    1 {-# LANGUAGE BangPatterns  #-}
    2 
    3 {-# LANGUAGE DeriveFunctor #-}
    4 
    5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    6 
    7 module GHC.Tc.Solver.Rewrite(
    8    rewrite, rewriteKind, rewriteArgsNom,
    9    rewriteType
   10  ) where
   11 
   12 import GHC.Prelude
   13 
   14 import GHC.Core.TyCo.Ppr ( pprTyVar )
   15 import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters),
   16                       TcPluginRewriter, TcPluginRewriteResult(..),
   17                       RewriteEnv(..),
   18                       runTcPluginM )
   19 import GHC.Tc.Types.Constraint
   20 import GHC.Core.Predicate
   21 import GHC.Tc.Utils.TcType
   22 import GHC.Core.Type
   23 import GHC.Tc.Types.Evidence
   24 import GHC.Core.TyCon
   25 import GHC.Core.TyCo.Rep   -- performs delicate algorithm on types
   26 import GHC.Core.Coercion
   27 import GHC.Core.Reduction
   28 import GHC.Types.Unique.FM
   29 import GHC.Types.Var
   30 import GHC.Types.Var.Set
   31 import GHC.Types.Var.Env
   32 import GHC.Driver.Session
   33 import GHC.Utils.Outputable
   34 import GHC.Utils.Panic
   35 import GHC.Utils.Panic.Plain
   36 import GHC.Tc.Solver.Monad as TcS
   37 import GHC.Tc.Solver.Types
   38 import GHC.Utils.Misc
   39 import GHC.Data.Maybe
   40 import GHC.Exts (oneShot)
   41 import Control.Monad
   42 import GHC.Utils.Monad ( zipWith3M )
   43 import Data.List.NonEmpty ( NonEmpty(..) )
   44 import Control.Applicative (liftA3)
   45 import GHC.Builtin.Types.Prim (tYPETyCon)
   46 
   47 {-
   48 ************************************************************************
   49 *                                                                      *
   50 *                RewriteEnv & RewriteM
   51 *             The rewriting environment & monad
   52 *                                                                      *
   53 ************************************************************************
   54 -}
   55 
   56 -- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
   57 newtype RewriteM a
   58   = RewriteM { runRewriteM :: RewriteEnv -> TcS a }
   59   deriving (Functor)
   60 
   61 -- | Smart constructor for 'RewriteM', as describe in Note [The one-shot state
   62 -- monad trick] in "GHC.Utils.Monad".
   63 mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
   64 mkRewriteM f = RewriteM (oneShot f)
   65 {-# INLINE mkRewriteM #-}
   66 
   67 instance Monad RewriteM where
   68   m >>= k  = mkRewriteM $ \env ->
   69              do { a  <- runRewriteM m env
   70                 ; runRewriteM (k a) env }
   71 
   72 instance Applicative RewriteM where
   73   pure x = mkRewriteM $ \_ -> pure x
   74   (<*>) = ap
   75 
   76 instance HasDynFlags RewriteM where
   77   getDynFlags = liftTcS getDynFlags
   78 
   79 liftTcS :: TcS a -> RewriteM a
   80 liftTcS thing_inside
   81   = mkRewriteM $ \_ -> thing_inside
   82 
   83 -- convenient wrapper when you have a CtEvidence describing
   84 -- the rewriting operation
   85 runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS a
   86 runRewriteCtEv ev
   87   = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
   88 
   89 -- Run thing_inside (which does the rewriting)
   90 runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
   91 runRewrite loc flav eq_rel thing_inside
   92   = runRewriteM thing_inside fmode
   93   where
   94     fmode = FE { fe_loc  = loc
   95                , fe_flavour = flav
   96                , fe_eq_rel = eq_rel }
   97 
   98 traceRewriteM :: String -> SDoc -> RewriteM ()
   99 traceRewriteM herald doc = liftTcS $ traceTcS herald doc
  100 {-# INLINE traceRewriteM #-}  -- see Note [INLINE conditional tracing utilities]
  101 
  102 getRewriteEnv :: RewriteM RewriteEnv
  103 getRewriteEnv
  104   = mkRewriteM $ \env -> return env
  105 
  106 getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
  107 getRewriteEnvField accessor
  108   = mkRewriteM $ \env -> return (accessor env)
  109 
  110 getEqRel :: RewriteM EqRel
  111 getEqRel = getRewriteEnvField fe_eq_rel
  112 
  113 getRole :: RewriteM Role
  114 getRole = eqRelRole <$> getEqRel
  115 
  116 getFlavour :: RewriteM CtFlavour
  117 getFlavour = getRewriteEnvField fe_flavour
  118 
  119 getFlavourRole :: RewriteM CtFlavourRole
  120 getFlavourRole
  121   = do { flavour <- getFlavour
  122        ; eq_rel <- getEqRel
  123        ; return (flavour, eq_rel) }
  124 
  125 getLoc :: RewriteM CtLoc
  126 getLoc = getRewriteEnvField fe_loc
  127 
  128 checkStackDepth :: Type -> RewriteM ()
  129 checkStackDepth ty
  130   = do { loc <- getLoc
  131        ; liftTcS $ checkReductionDepth loc ty }
  132 
  133 -- | Change the 'EqRel' in a 'RewriteM'.
  134 setEqRel :: EqRel -> RewriteM a -> RewriteM a
  135 setEqRel new_eq_rel thing_inside
  136   = mkRewriteM $ \env ->
  137     if new_eq_rel == fe_eq_rel env
  138     then runRewriteM thing_inside env
  139     else runRewriteM thing_inside (env { fe_eq_rel = new_eq_rel })
  140 {-# INLINE setEqRel #-}
  141 
  142 -- | Make sure that rewriting actually produces a coercion (in other
  143 -- words, make sure our flavour is not Derived)
  144 -- Note [No derived kind equalities]
  145 noBogusCoercions :: RewriteM a -> RewriteM a
  146 noBogusCoercions thing_inside
  147   = mkRewriteM $ \env ->
  148     -- No new thunk is made if the flavour hasn't changed (note the bang).
  149     let !env' = case fe_flavour env of
  150           Derived -> env { fe_flavour = Wanted WDeriv }
  151           _       -> env
  152     in
  153     runRewriteM thing_inside env'
  154 
  155 bumpDepth :: RewriteM a -> RewriteM a
  156 bumpDepth (RewriteM thing_inside)
  157   = mkRewriteM $ \env -> do
  158       -- bumpDepth can be called a lot during rewriting so we force the
  159       -- new env to avoid accumulating thunks.
  160       { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) }
  161       ; thing_inside env' }
  162 
  163 {-
  164 Note [Rewriter EqRels]
  165 ~~~~~~~~~~~~~~~~~~~~~~~
  166 When rewriting, we need to know which equality relation -- nominal
  167 or representation -- we should be respecting. The only difference is
  168 that we rewrite variables by representational equalities when fe_eq_rel
  169 is ReprEq, and that we unwrap newtypes when rewriting w.r.t.
  170 representational equality.
  171 
  172 Note [Rewriter CtLoc]
  173 ~~~~~~~~~~~~~~~~~~~~~~
  174 The rewriter does eager type-family reduction.
  175 Type families might loop, and we
  176 don't want GHC to do so. A natural solution is to have a bounded depth
  177 to these processes. A central difficulty is that such a solution isn't
  178 quite compositional. For example, say it takes F Int 10 steps to get to Bool.
  179 How many steps does it take to get from F Int -> F Int to Bool -> Bool?
  180 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
  181 know and hard to track. So, we punt, essentially. We store a CtLoc in
  182 the RewriteEnv and just update the environment when recurring. In the
  183 TyConApp case, where there may be multiple type families to rewrite,
  184 we just copy the current CtLoc into each branch. If any branch hits the
  185 stack limit, then the whole thing fails.
  186 
  187 A consequence of this is that setting the stack limits appropriately
  188 will be essentially impossible. So, the official recommendation if a
  189 stack limit is hit is to disable the check entirely. Otherwise, there
  190 will be baffling, unpredictable errors.
  191 
  192 Note [Phantoms in the rewriter]
  193 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  194 Suppose we have
  195 
  196 data Proxy p = Proxy
  197 
  198 and we're rewriting (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
  199 is really irrelevant -- it will be ignored when solving for representational
  200 equality later on. So, we omit rewriting `ty` entirely. This may
  201 violate the expectation of "xi"s for a bit, but the canonicaliser will
  202 soon throw out the phantoms when decomposing a TyConApp. (Or, the
  203 canonicaliser will emit an insoluble, in which case we get
  204 a better error message anyway.)
  205 
  206 Note [No derived kind equalities]
  207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  208 A kind-level coercion can appear in types, via mkCastTy. So, whenever
  209 we are generating a coercion in a dependent context (in other words,
  210 in a kind) we need to make sure that our flavour is never Derived
  211 (as Derived constraints have no evidence). The noBogusCoercions function
  212 changes the flavour from Derived just for this purpose.
  213 
  214 -}
  215 
  216 {- *********************************************************************
  217 *                                                                      *
  218 *      Externally callable rewriting functions                         *
  219 *                                                                      *
  220 ************************************************************************
  221 -}
  222 
  223 -- | See Note [Rewriting].
  224 -- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty
  225 -- where r is the role in @ev@.
  226 rewrite :: CtEvidence -> TcType
  227         -> TcS Reduction
  228 rewrite ev ty
  229   = do { traceTcS "rewrite {" (ppr ty)
  230        ; redn <- runRewriteCtEv ev (rewrite_one ty)
  231        ; traceTcS "rewrite }" (ppr $ reductionReducedType redn)
  232        ; return redn }
  233 
  234 -- specialized to rewriting kinds: never Derived, always Nominal
  235 -- See Note [No derived kind equalities]
  236 -- See Note [Rewriting]
  237 rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS ReductionN
  238 rewriteKind loc flav ty
  239   = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty)
  240        ; let flav' = case flav of
  241                        Derived -> Wanted WDeriv  -- the WDeriv/WOnly choice matters not
  242                        _       -> flav
  243        ; redn <- runRewrite loc flav' NomEq (rewrite_one ty)
  244        ; traceTcS "rewriteKind }" (ppr redn) -- the coercion inside the reduction is never a panic
  245        ; return redn }
  246 
  247 -- See Note [Rewriting]
  248 rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
  249                -> TcS Reductions
  250 -- Externally-callable, hence runRewrite
  251 -- Rewrite a vector of types all at once; in fact they are
  252 -- always the arguments of type family or class, so
  253 --      ctEvFlavour ev = Nominal
  254 -- and we want to rewrite all at nominal role
  255 -- The kind passed in is the kind of the type family or class, call it T
  256 -- The kind of T args must be constant (i.e. not depend on the args)
  257 --
  258 -- For Derived constraints the returned coercion may be undefined
  259 -- because rewriting may use a Derived equality ([D] a ~ ty)
  260 rewriteArgsNom ev tc tys
  261   = do { traceTcS "rewrite_args {" (vcat (map ppr tys))
  262        ; ArgsReductions redns@(Reductions _ tys') kind_co
  263            <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys)
  264        ; massert (isReflMCo kind_co)
  265        ; traceTcS "rewrite }" (vcat (map ppr tys'))
  266        ; return redns }
  267 
  268 -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite
  269 -- a type w.r.t. any givens. It does not do type-family reduction. This
  270 -- will never emit new constraints. Call this when the inert set contains
  271 -- only givens.
  272 rewriteType :: CtLoc -> TcType -> TcS TcType
  273 rewriteType loc ty
  274   = do { redn <- runRewrite loc Given NomEq $
  275                     rewrite_one ty
  276                      -- use Given flavor so that it is rewritten
  277                      -- only w.r.t. Givens, never Wanteds/Deriveds
  278                      -- (Shouldn't matter, if only Givens are present
  279                      -- anyway)
  280        ; return $ reductionReducedType redn }
  281 
  282 {- *********************************************************************
  283 *                                                                      *
  284 *           The main rewriting functions
  285 *                                                                      *
  286 ********************************************************************* -}
  287 
  288 {- Note [Rewriting]
  289 ~~~~~~~~~~~~~~~~~~~~
  290   rewrite ty  ==>  Reduction co xi
  291     where
  292       xi has no reducible type functions
  293          has no skolems that are mapped in the inert set
  294          has no filled-in metavariables
  295       co :: ty ~ xi (coercions in reductions are always left-to-right)
  296 
  297 Key invariants:
  298   (F0) co :: zonk(ty') ~ xi   where zonk(ty') ~ zonk(ty)
  299   (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
  300   (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
  301 
  302 Note that it is rewrite's job to try to reduce *every type function it sees*.
  303 
  304 Rewriting also:
  305   * zonks, removing any metavariables, and
  306   * applies the substitution embodied in the inert set
  307 
  308 Because rewriting zonks and the returned coercion ("co" above) is also
  309 zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead,
  310 we can rely on this fact:
  311 
  312   (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty)
  313 
  314 Note that the right-hand type of co is *always* precisely xi. The left-hand
  315 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
  316 then the left-hand type of co will be the zonk-equal to ty.
  317 It is for this reason that we occasionally have to explicitly zonk,
  318 when (co :: ty ~ xi) is important even before we zonk the whole program.
  319 For example, see the RTRNotFollowed case in rewriteTyVar.
  320 
  321 Why have these invariants on rewriting? Because we sometimes use tcTypeKind
  322 during canonicalisation, and we want this kind to be zonked (e.g., see
  323 GHC.Tc.Solver.Canonical.canEqCanLHS).
  324 
  325 Rewriting is always homogeneous. That is, the kind of the result of rewriting is
  326 always the same as the kind of the input, modulo zonking. More formally:
  327 
  328   (F2) zonk(tcTypeKind(ty)) `eqType` tcTypeKind(xi)
  329 
  330 This invariant means that the kind of a rewritten type might not itself be rewritten.
  331 
  332 Note that we prefer to leave type synonyms unexpanded when possible,
  333 so when the rewriter encounters one, it first asks whether its
  334 transitive expansion contains any type function applications or is
  335 forgetful -- that is, omits one or more type variables in its RHS.  If so,
  336 it expands the synonym and proceeds; if not, it simply returns the
  337 unexpanded synonym. See also Note [Rewriting synonyms].
  338 
  339 Where do we actually perform rewriting within a type? See Note [Rewritable] in
  340 GHC.Tc.Solver.InertSet.
  341 
  342 Note [rewrite_args performance]
  343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  344 In programs with lots of type-level evaluation, rewrite_args becomes
  345 part of a tight loop. For example, see test perf/compiler/T9872a, which
  346 calls rewrite_args a whopping 7,106,808 times. It is thus important
  347 that rewrite_args be efficient.
  348 
  349 Performance testing showed that the current implementation is indeed
  350 efficient. It's critically important that zipWithAndUnzipM be
  351 specialized to TcS, and it's also quite helpful to actually `inline`
  352 it. On test T9872a, here are the allocation stats (Dec 16, 2014):
  353 
  354  * Unspecialized, uninlined:     8,472,613,440 bytes allocated in the heap
  355  * Specialized, uninlined:       6,639,253,488 bytes allocated in the heap
  356  * Specialized, inlined:         6,281,539,792 bytes allocated in the heap
  357 
  358 To improve performance even further, rewrite_args_nom is split off
  359 from rewrite_args, as nominal equality is the common case. This would
  360 be natural to write using mapAndUnzipM, but even inlined, that function
  361 is not as performant as a hand-written loop.
  362 
  363  * mapAndUnzipM, inlined:        7,463,047,432 bytes allocated in the heap
  364  * hand-written recursion:       5,848,602,848 bytes allocated in the heap
  365 
  366 If you make any change here, pay close attention to the T9872{a,b,c} tests
  367 and T5321Fun.
  368 
  369 If we need to make this yet more performant, a possible way forward is to
  370 duplicate the rewriter code for the nominal case, and make that case
  371 faster. This doesn't seem quite worth it, yet.
  372 
  373 Note [rewrite_exact_fam_app performance]
  374 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  375 Once we've got a rewritten rhs, we extend the famapp-cache to record
  376 the result. Doing so can save lots of work when the same redex shows up more
  377 than once. Note that we record the link from the redex all the way to its
  378 *final* value, not just the single step reduction.
  379 
  380 If we can reduce the family application right away (the first call
  381 to try_to_reduce), we do *not* add to the cache. There are two possibilities
  382 here: 1) we just read the result from the cache, or 2) we used one type
  383 family instance. In either case, recording the result in the cache doesn't
  384 save much effort the next time around. And adding to the cache here is
  385 actually disastrous: it more than doubles the allocations for T9872a. So
  386 we skip adding to the cache here.
  387 -}
  388 
  389 {-# INLINE rewrite_args_tc #-}
  390 rewrite_args_tc
  391   :: TyCon         -- T
  392   -> Maybe [Role]  -- Nothing: ambient role is Nominal; all args are Nominal
  393                    -- Otherwise: no assumptions; use roles provided
  394   -> [Type]
  395   -> RewriteM ArgsReductions -- See the commentary on rewrite_args
  396 rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet
  397   -- NB: TyCon kinds are always closed
  398   where
  399   -- There are many bang patterns in here. It's been observed that they
  400   -- greatly improve performance of an optimized build.
  401   -- The T9872 test cases are good witnesses of this fact.
  402 
  403     (bndrs, named)
  404       = ty_con_binders_ty_binders' (tyConBinders tc)
  405     -- it's possible that the result kind has arrows (for, e.g., a type family)
  406     -- so we must split it
  407     (inner_bndrs, inner_ki, inner_named) = split_pi_tys' (tyConResKind tc)
  408     !all_bndrs                           = bndrs `chkAppend` inner_bndrs
  409     !any_named_bndrs                     = named || inner_named
  410     -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.
  411 
  412 {-# INLINE rewrite_args #-}
  413 rewrite_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
  414                                      -- named.
  415              -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
  416              -> Maybe [Role] -> [Type]    -- these are in 1-to-1 correspondence
  417                                           -- Nothing: use all Nominal
  418              -> RewriteM ArgsReductions
  419 -- This function returns ArgsReductions (Reductions cos xis) res_co
  420 --   coercions: co_i :: ty_i ~ xi_i, at roles given
  421 --   types:     xi_i
  422 --   coercion:  res_co :: tcTypeKind(fun tys) ~N tcTypeKind(fun xis)
  423 -- That is, the result coercion relates the kind of some function (whose kind is
  424 -- passed as the first parameter) instantiated at tys to the kind of that
  425 -- function instantiated at the xis. This is useful in keeping rewriting
  426 -- homogeneous. The list of roles must be at least as long as the list of
  427 -- types.
  428 rewrite_args orig_binders
  429              any_named_bndrs
  430              orig_inner_ki
  431              orig_fvs
  432              orig_m_roles
  433              orig_tys
  434   = case (orig_m_roles, any_named_bndrs) of
  435       (Nothing, False) -> rewrite_args_fast orig_tys
  436       _ -> rewrite_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
  437         where orig_roles = fromMaybe (repeat Nominal) orig_m_roles
  438 
  439 {-# INLINE rewrite_args_fast #-}
  440 -- | fast path rewrite_args, in which none of the binders are named and
  441 -- therefore we can avoid tracking a lifting context.
  442 rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
  443 rewrite_args_fast orig_tys
  444   = fmap finish (iterate orig_tys)
  445   where
  446 
  447     iterate :: [Type] -> RewriteM Reductions
  448     iterate (ty : tys) = do
  449       Reduction  co  xi  <- rewrite_one ty
  450       Reductions cos xis <- iterate tys
  451       pure $ Reductions (co : cos) (xi : xis)
  452     iterate [] = pure $ Reductions [] []
  453 
  454     {-# INLINE finish #-}
  455     finish :: Reductions -> ArgsReductions
  456     finish redns = ArgsReductions redns MRefl
  457 
  458 {-# INLINE rewrite_args_slow #-}
  459 -- | Slow path, compared to rewrite_args_fast, because this one must track
  460 -- a lifting context.
  461 rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
  462                   -> [Role] -> [Type]
  463                   -> RewriteM ArgsReductions
  464 rewrite_args_slow binders inner_ki fvs roles tys
  465 -- Arguments used dependently must be rewritten with proper coercions, but
  466 -- we're not guaranteed to get a proper coercion when rewriting with the
  467 -- "Derived" flavour. So we must call noBogusCoercions when rewriting arguments
  468 -- corresponding to binders that are dependent. However, we might legitimately
  469 -- have *more* arguments than binders, in the case that the inner_ki is a variable
  470 -- that gets instantiated with a Π-type. We conservatively choose not to produce
  471 -- bogus coercions for these, too. Note that this might miss an opportunity for
  472 -- a Derived rewriting a Derived. The solution would be to generate evidence for
  473 -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
  474 -- Note [No derived kind equalities]
  475   = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True)
  476                                         roles tys
  477        ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }
  478   where
  479     {-# INLINE rw #-}
  480     rw :: Bool   -- must we ensure to produce a real coercion here?
  481                  -- see comment at top of function
  482        -> Role -> Type -> RewriteM Reduction
  483     rw True  r ty = noBogusCoercions $ rw1 r ty
  484     rw False r ty =                    rw1 r ty
  485 
  486     {-# INLINE rw1 #-}
  487     rw1 :: Role -> Type -> RewriteM Reduction
  488     rw1 Nominal ty
  489       = setEqRel NomEq $
  490         rewrite_one ty
  491 
  492     rw1 Representational ty
  493       = setEqRel ReprEq $
  494         rewrite_one ty
  495 
  496     rw1 Phantom ty
  497     -- See Note [Phantoms in the rewriter]
  498       = do { ty <- liftTcS $ zonkTcType ty
  499            ; return $ mkReflRedn Phantom ty }
  500 
  501 ------------------
  502 rewrite_one :: TcType -> RewriteM Reduction
  503 -- Rewrite a type to get rid of type function applications, returning
  504 -- the new type-function-free type, and a collection of new equality
  505 -- constraints.  See Note [Rewriting] for more detail.
  506 --
  507 -- Postcondition:
  508 -- the role on the result coercion matches the EqRel in the RewriteEnv
  509 
  510 rewrite_one ty
  511   | Just ty' <- rewriterView ty  -- See Note [Rewriting synonyms]
  512   = rewrite_one ty'
  513 
  514 rewrite_one xi@(LitTy {})
  515   = do { role <- getRole
  516        ; return $ mkReflRedn role xi }
  517 
  518 rewrite_one (TyVarTy tv)
  519   = rewriteTyVar tv
  520 
  521 rewrite_one (AppTy ty1 ty2)
  522   = rewrite_app_tys ty1 [ty2]
  523 
  524 rewrite_one (TyConApp tc tys)
  525   -- If it's a type family application, try to reduce it
  526   | isTypeFamilyTyCon tc
  527   = rewrite_fam_app tc tys
  528 
  529   -- For * a normal data type application
  530   --     * data family application
  531   -- we just recursively rewrite the arguments.
  532   | otherwise
  533   = rewrite_ty_con_app tc tys
  534 
  535 rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
  536   = do { arg_redn <- rewrite_one ty1
  537        ; res_redn <- rewrite_one ty2
  538 
  539         -- Important: look at the *reduced* type, so that any unzonked variables
  540         -- in kinds are gone and the getRuntimeRep succeeds.
  541         -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical.
  542        ; let arg_rep = getRuntimeRep (reductionReducedType arg_redn)
  543              res_rep = getRuntimeRep (reductionReducedType res_redn)
  544 
  545        ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $
  546            liftA3 (,,) (rewrite_one mult)
  547                        (rewrite_one arg_rep)
  548                        (rewrite_one res_rep)
  549        ; role <- getRole
  550 
  551        ; let arg_rep_co = reductionCoercion arg_rep_redn
  552                 -- :: arg_rep ~ arg_rep_xi
  553              arg_ki_co  = mkTyConAppCo Nominal tYPETyCon [arg_rep_co]
  554                 -- :: TYPE arg_rep ~ TYPE arg_rep_xi
  555              casted_arg_redn = mkCoherenceRightRedn role arg_redn arg_ki_co
  556                 -- :: ty1 ~> arg_xi |> arg_ki_co
  557 
  558              res_rep_co = reductionCoercion res_rep_redn
  559              res_ki_co  = mkTyConAppCo Nominal tYPETyCon [res_rep_co]
  560              casted_res_redn = mkCoherenceRightRedn role res_redn res_ki_co
  561 
  562           -- We must rewrite the representations, because that's what would
  563           -- be done if we used TyConApp instead of FunTy. These rewritten
  564           -- representations are seen only in casts of the arg and res, below.
  565           -- Forgetting this caused #19677.
  566        ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn }
  567 
  568 rewrite_one ty@(ForAllTy {})
  569 -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
  570 -- the bound tyvar. Doing so will require carrying around a substitution
  571 -- and the usual substTyVarBndr-like silliness. Argh.
  572 
  573 -- We allow for-alls when, but only when, no type function
  574 -- applications inside the forall involve the bound type variables.
  575   = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty
  576        ; redn <- rewrite_one rho
  577        ; return $ mkHomoForAllRedn bndrs redn }
  578 
  579 rewrite_one (CastTy ty g)
  580   = do { redn <- rewrite_one ty
  581        ; g'   <- rewrite_co g
  582        ; role <- getRole
  583        ; return $ mkCastRedn1 role ty g' redn }
  584       -- This calls castCoercionKind1.
  585       -- It makes a /big/ difference to call castCoercionKind1 not
  586       -- the more general castCoercionKind2.
  587       -- See Note [castCoercionKind1] in GHC.Core.Coercion
  588 
  589 rewrite_one (CoercionTy co)
  590   = do { co' <- rewrite_co co
  591        ; role <- getRole
  592        ; return $ mkReflCoRedn role co' }
  593 
  594 -- | "Rewrite" a coercion. Really, just zonk it so we can uphold
  595 -- (F1) of Note [Rewriting]
  596 rewrite_co :: Coercion -> RewriteM Coercion
  597 rewrite_co co = liftTcS $ zonkCo co
  598 
  599 -- | Rewrite a reduction, composing the resulting coercions.
  600 rewrite_reduction :: Reduction -> RewriteM Reduction
  601 rewrite_reduction (Reduction co xi)
  602   = do { redn <- bumpDepth $ rewrite_one xi
  603        ; return $ co `mkTransRedn` redn }
  604 
  605 -- rewrite (nested) AppTys
  606 rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
  607 -- commoning up nested applications allows us to look up the function's kind
  608 -- only once. Without commoning up like this, we would spend a quadratic amount
  609 -- of time looking up functions' types
  610 rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys)
  611 rewrite_app_tys fun_ty arg_tys
  612   = do { redn <- rewrite_one fun_ty
  613        ; rewrite_app_ty_args redn arg_tys }
  614 
  615 -- Given a rewritten function (with the coercion produced by rewriting) and
  616 -- a bunch of unrewritten arguments, rewrite the arguments and apply.
  617 -- The coercion argument's role matches the role stored in the RewriteM monad.
  618 --
  619 -- The bang patterns used here were observed to improve performance. If you
  620 -- wish to remove them, be sure to check for regressions in allocations.
  621 rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
  622 rewrite_app_ty_args redn []
  623   -- this will be a common case when called from rewrite_fam_app, so shortcut
  624   = return redn
  625 rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys
  626   = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of
  627            Just (tc, xis) ->
  628              do { let tc_roles  = tyConRolesRepresentational tc
  629                       arg_roles = dropList xis tc_roles
  630                 ; ArgsReductions (Reductions arg_cos arg_xis) kind_co
  631                     <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys
  632 
  633                   -- We start with a reduction of the form
  634                   --   fun_co :: ty ~ T xi_1 ... xi_n
  635                   -- and further arguments a_1, ..., a_m.
  636                   -- We rewrite these arguments, and obtain coercions:
  637                   --   arg_co_i :: a_i ~ zeta_i
  638                   -- Now, we need to apply fun_co to the arg_cos. The problem is
  639                   -- that using mkAppCo is wrong because that function expects
  640                   -- its second coercion to be Nominal, and the arg_cos might
  641                   -- not be. The solution is to use transitivity:
  642                   -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m
  643                 ; eq_rel <- getEqRel
  644                 ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
  645                       app_co = case eq_rel of
  646                         NomEq  -> mkAppCos fun_co arg_cos
  647                         ReprEq -> mkAppCos fun_co (map mkNomReflCo arg_tys)
  648                                   `mkTcTransCo`
  649                                   mkTcTyConAppCo Representational tc
  650                                     (zipWith mkReflCo tc_roles xis ++ arg_cos)
  651 
  652                 ; return $
  653                     mkHetReduction
  654                       (mkReduction app_co app_xi )
  655                       kind_co }
  656            Nothing ->
  657              do { ArgsReductions redns kind_co
  658                     <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
  659                 ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }
  660 
  661        ; role <- getRole
  662        ; return (homogeniseHetRedn role het_redn) }
  663 
  664 rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
  665 rewrite_ty_con_app tc tys
  666   = do { role <- getRole
  667        ; let m_roles | Nominal <- role = Nothing
  668                      | otherwise       = Just $ tyConRolesX role tc
  669        ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
  670        ; let tyconapp_redn
  671                 = mkHetReduction
  672                     (mkTyConAppRedn role tc redns)
  673                     kind_co
  674        ; return $ homogeniseHetRedn role tyconapp_redn }
  675 
  676 -- Rewrite a vector (list of arguments).
  677 rewrite_vector :: Kind   -- of the function being applied to these arguments
  678                -> [Role] -- If we're rewriting w.r.t. ReprEq, what roles do the
  679                          -- args have?
  680                -> [Type] -- the args to rewrite
  681                -> RewriteM ArgsReductions
  682 rewrite_vector ki roles tys
  683   = do { eq_rel <- getEqRel
  684        ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles }
  685        ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys
  686        }
  687   where
  688     (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
  689     fvs                                = tyCoVarsOfType ki
  690 {-# INLINE rewrite_vector #-}
  691 
  692 {-
  693 Note [Rewriting synonyms]
  694 ~~~~~~~~~~~~~~~~~~~~~~~~~~
  695 Not expanding synonyms aggressively improves error messages, and
  696 keeps types smaller. But we need to take care.
  697 
  698 Suppose
  699    type Syn a = Int
  700    type instance F Bool = Syn (F Bool)
  701    [G] F Bool ~ Syn (F Bool)
  702 
  703 If we don't expand the synonym, we'll get a spurious occurs-check
  704 failure. This is normally what occCheckExpand takes care of, but
  705 the LHS is a type family application, and occCheckExpand (already
  706 complex enough as it is) does not know how to expand to avoid
  707 a type family application.
  708 
  709 In addition, expanding the forgetful synonym like this
  710 will generally yield a *smaller* type. To wit, if we spot
  711 S ( ... F tys ... ), where S is forgetful, we don't want to bother
  712 doing hard work simplifying (F tys). We thus expand forgetful
  713 synonyms, but not others.
  714 
  715 isForgetfulSynTyCon returns True more often than it needs to, so
  716 we err on the side of more expansion.
  717 
  718 We also, of course, must expand type synonyms that mention type families,
  719 so those families can get reduced.
  720 
  721 ************************************************************************
  722 *                                                                      *
  723              Rewriting a type-family application
  724 *                                                                      *
  725 ************************************************************************
  726 
  727 Note [How to normalise a family application]
  728 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  729 Given an exactly saturated family application, how should we normalise it?
  730 This Note spells out the algorithm and its reasoning.
  731 
  732 First, we attempt to directly rewrite the type family application,
  733 without simplifying any of the arguments first, in an attempt to avoid
  734 doing unnecessary work.
  735 
  736 STEP 1a. Call the rewriting plugins. If any plugin rewrites the type family
  737 application, jump to FINISH.
  738 
  739 STEP 1b. Try the famapp-cache. If we get a cache hit, jump to FINISH.
  740 
  741 STEP 1c. Try top-level instances. Remember: we haven't simplified the arguments
  742   yet. Example:
  743     type instance F (Maybe a) = Int
  744     target: F (Maybe (G Bool))
  745   Instead of first trying to simplify (G Bool), we use the instance first. This
  746   avoids the work of simplifying G Bool.
  747 
  748   If an instance is found, jump to FINISH.
  749 
  750 STEP 2: At this point we rewrite all arguments. This might expose more
  751   information, which might allow plugins to make progress, or allow us to
  752   pick up a top-level instance.
  753 
  754 STEP 3. Try the inerts. Note that we try the inerts *after* rewriting the
  755   arguments, because the inerts will have rewritten LHSs.
  756 
  757   If an inert is found, jump to FINISH.
  758 
  759 Next, we try STEP 1 again, as we might be able to make further progress after
  760 having rewritten the arguments:
  761 
  762 STEP 4a. Query the rewriting plugins again.
  763 
  764   If any plugin supplies a rewriting, jump to FINISH.
  765 
  766 STEP 4b. Try the famapp-cache again.
  767 
  768   If we get a cache hit, jump to FINISH.
  769 
  770 STEP 4c. Try top-level instances again.
  771 
  772   If an instance is found, jump to FINISH.
  773 
  774 STEP 5: GIVEUP. No progress to be made. Return what we have. (Do not FINISH.)
  775 
  776 FINISH 1. We've made a reduction, but the new type may still have more
  777   work to do. So rewrite the new type.
  778 
  779 FINISH 2. Add the result to the famapp-cache, connecting the type we started
  780   with to the one we ended with.
  781 
  782 Because STEP 1{a,b,c} and STEP 4{a,b,c} happen the same way, they are abstracted into
  783 try_to_reduce.
  784 
  785 FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance]
  786 tells us that we should not add to the famapp-cache after STEP 1. So `finish`
  787 is inlined in that case, and only FINISH 1 is performed.
  788 
  789 -}
  790 
  791 rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
  792   --   rewrite_fam_app            can be over-saturated
  793   --   rewrite_exact_fam_app      lifts out the application to top level
  794   -- Postcondition: Coercion :: Xi ~ F tys
  795 rewrite_fam_app tc tys  -- Can be over-saturated
  796     = assertPpr (tys `lengthAtLeast` tyConArity tc)
  797                 (ppr tc $$ ppr (tyConArity tc) $$ ppr tys) $
  798 
  799                  -- Type functions are saturated
  800                  -- The type function might be *over* saturated
  801                  -- in which case the remaining arguments should
  802                  -- be dealt with by AppTys
  803       do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
  804          ; redn <- rewrite_exact_fam_app tc tys1
  805          ; rewrite_app_ty_args redn tys_rest }
  806 
  807 -- the [TcType] exactly saturate the TyCon
  808 -- See Note [How to normalise a family application]
  809 rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
  810 rewrite_exact_fam_app tc tys
  811   = do { checkStackDepth (mkTyConApp tc tys)
  812 
  813        -- Query the typechecking plugins for all their rewriting functions
  814        -- which apply to a type family application headed by the TyCon 'tc'.
  815        ; tc_rewriters <- getTcPluginRewritersForTyCon tc
  816 
  817        -- STEP 1. Try to reduce without reducing arguments first.
  818        ; result1 <- try_to_reduce tc tys tc_rewriters
  819        ; case result1 of
  820              -- Don't use the cache;
  821              -- See Note [rewrite_exact_fam_app performance]
  822          { Just redn -> finish False redn
  823          ; Nothing ->
  824 
  825         -- That didn't work. So reduce the arguments, in STEP 2.
  826     do { eq_rel <- getEqRel
  827           -- checking eq_rel == NomEq saves ~0.5% in T9872a
  828        ; ArgsReductions (Reductions cos xis) kind_co <-
  829             if eq_rel == NomEq
  830             then rewrite_args_tc tc Nothing tys
  831             else setEqRel NomEq $
  832                  rewrite_args_tc tc Nothing tys
  833 
  834          -- If we manage to rewrite the type family application after
  835          -- rewriting the arguments, we will need to compose these
  836          -- reductions.
  837          --
  838          -- We have:
  839          --
  840          --   arg_co_i :: ty_i ~ xi_i
  841          --   fam_co :: F xi_1 ... xi_n ~ zeta
  842          --
  843          -- The full reduction is obtained as a composite:
  844          --
  845          --   full_co :: F ty_1 ... ty_n ~ zeta
  846          --   full_co = F co_1 ... co_n ;; fam_co
  847        ; let
  848            role    = eqRelRole eq_rel
  849            args_co = mkTyConAppCo role tc cos
  850        ;  let homogenise :: Reduction -> Reduction
  851               homogenise redn
  852                 = homogeniseHetRedn role
  853                 $ mkHetReduction
  854                     (args_co `mkTransRedn` redn)
  855                     kind_co
  856 
  857               give_up :: Reduction
  858               give_up = homogenise $ mkReflRedn role reduced
  859                 where reduced = mkTyConApp tc xis
  860 
  861          -- STEP 3: try the inerts
  862        ; result2 <- liftTcS $ lookupFamAppInert tc xis
  863        ; flavour <- getFlavour
  864        ; case result2 of
  865          { Just (redn, fr@(_, inert_eq_rel))
  866 
  867              | fr `eqCanRewriteFR` (flavour, eq_rel) ->
  868                  do { traceRewriteM "rewrite family application with inert"
  869                                 (ppr tc <+> ppr xis $$ ppr redn)
  870                     ; finish True (homogenise downgraded_redn) }
  871                -- this will sometimes duplicate an inert in the cache,
  872                -- but avoiding doing so had no impact on performance, and
  873                -- it seems easier not to weed out that special case
  874              where
  875                inert_role      = eqRelRole inert_eq_rel
  876                role            = eqRelRole eq_rel
  877                downgraded_redn = downgradeRedn role inert_role redn
  878 
  879          ; _ ->
  880 
  881          -- inerts didn't work. Try to reduce again, in STEP 4.
  882     do { result3 <- try_to_reduce tc xis tc_rewriters
  883        ; case result3 of
  884            Just redn -> finish True (homogenise redn)
  885            -- we have made no progress at all: STEP 5 (GIVEUP).
  886            _         -> return give_up }}}}}
  887   where
  888       -- call this if the above attempts made progress.
  889       -- This recursively rewrites the result and then adds to the cache
  890     finish :: Bool  -- add to the cache?
  891            -> Reduction -> RewriteM Reduction
  892     finish use_cache redn
  893       = do { -- rewrite the result: FINISH 1
  894              final_redn <- rewrite_reduction redn
  895            ; eq_rel <- getEqRel
  896            ; flavour <- getFlavour
  897 
  898              -- extend the cache: FINISH 2
  899            ; when (use_cache && eq_rel == NomEq && flavour /= Derived) $
  900              -- the cache only wants Nominal eqs
  901              -- and Wanteds can rewrite Deriveds; the cache
  902              -- has only Givens
  903              liftTcS $ extendFamAppCache tc tys final_redn
  904            ; return final_redn }
  905     {-# INLINE finish #-}
  906 
  907 -- Returned coercion is input ~r output, where r is the role in the RewriteM monad
  908 -- See Note [How to normalise a family application]
  909 try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
  910               -> RewriteM (Maybe Reduction)
  911 try_to_reduce tc tys tc_rewriters
  912   = do { rewrite_env <- getRewriteEnv
  913        ; result <-
  914             liftTcS $ firstJustsM
  915               [ runTcPluginRewriters rewrite_env tc_rewriters tys -- STEP 1a & STEP 4a
  916               , lookupFamAppCache tc tys                          -- STEP 1b & STEP 4b
  917               , matchFam tc tys ]                                 -- STEP 1c & STEP 4c
  918        ; traverse downgrade result }
  919   where
  920     -- The result above is always Nominal. We might want a Representational
  921     -- coercion; this downgrades (and prints, out of convenience).
  922     downgrade :: Reduction -> RewriteM Reduction
  923     downgrade redn
  924       = do { traceRewriteM "Eager T.F. reduction success" $
  925              vcat [ ppr tc
  926                   , ppr tys
  927                   , ppr redn
  928                   ]
  929            ; eq_rel <- getEqRel
  930               -- manually doing it this way avoids allocation in the vastly
  931               -- common NomEq case
  932            ; case eq_rel of
  933                NomEq  -> return redn
  934                ReprEq -> return $ mkSubRedn redn }
  935 
  936 -- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application
  937 -- headed by the given 'TyCon`.
  938 getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
  939 getTcPluginRewritersForTyCon tc
  940   = liftTcS $ do { rewriters <- tcg_tc_plugin_rewriters <$> getGblEnv
  941                  ; return (lookupWithDefaultUFM rewriters [] tc) }
  942 
  943 -- Run a collection of rewriting functions obtained from type-checking plugins,
  944 -- querying in sequence if any plugin wants to rewrite the type family
  945 -- applied to the given arguments.
  946 --
  947 -- Note that the 'TcPluginRewriter's provided all pertain to the same type family
  948 -- (the 'TyCon' of which has been obtained ahead of calling this function).
  949 runTcPluginRewriters :: RewriteEnv
  950                      -> [TcPluginRewriter]
  951                      -> [TcType]
  952                      -> TcS (Maybe Reduction)
  953 runTcPluginRewriters rewriteEnv rewriterFunctions tys
  954   | null rewriterFunctions
  955   = return Nothing -- short-circuit for common case
  956   | otherwise
  957   = do { givens <- getInertGivens
  958        ; runRewriters givens rewriterFunctions }
  959   where
  960   runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
  961   runRewriters _ []
  962     = return Nothing
  963   runRewriters givens (rewriter:rewriters)
  964     = do
  965         rewriteResult <- wrapTcS . runTcPluginM $ rewriter rewriteEnv givens tys
  966         case rewriteResult of
  967            TcPluginRewriteTo
  968              { tcPluginReduction    = redn
  969              , tcRewriterNewWanteds = wanteds
  970              } -> do { emitWork wanteds; return $ Just redn }
  971            TcPluginNoRewrite {} -> runRewriters givens rewriters
  972 
  973 {-
  974 ************************************************************************
  975 *                                                                      *
  976              Rewriting a type variable
  977 *                                                                      *
  978 ********************************************************************* -}
  979 
  980 -- | The result of rewriting a tyvar "one step".
  981 data RewriteTvResult
  982   = RTRNotFollowed
  983       -- ^ The inert set doesn't make the tyvar equal to anything else
  984 
  985   | RTRFollowed !Reduction
  986       -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
  987       -- The role is determined by the RewriteEnv.
  988       --
  989       -- With Quick Look, the returned TcType can be a polytype;
  990       -- that is, in the constraint solver, a unification variable
  991       -- can contain a polytype.  See GHC.Tc.Gen.App
  992       -- Note [Instantiation variables are short lived]
  993 
  994 rewriteTyVar :: TyVar -> RewriteM Reduction
  995 rewriteTyVar tv
  996   = do { mb_yes <- rewrite_tyvar1 tv
  997        ; case mb_yes of
  998            RTRFollowed redn -> rewrite_reduction redn
  999 
 1000            RTRNotFollowed   -- Done, but make sure the kind is zonked
 1001                             -- Note [Rewriting] invariant (F0) and (F1)
 1002              -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
 1003                    ; role <- getRole
 1004                    ; let ty' = mkTyVarTy tv'
 1005                    ; return $ mkReflRedn role ty' } }
 1006 
 1007 rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
 1008 -- "Rewriting" a type variable means to apply the substitution to it
 1009 -- Specifically, look up the tyvar in
 1010 --   * the internal MetaTyVar box
 1011 --   * the inerts
 1012 -- See also the documentation for RewriteTvResult
 1013 
 1014 rewrite_tyvar1 tv
 1015   = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv
 1016        ; case mb_ty of
 1017            Just ty -> do { traceRewriteM "Following filled tyvar"
 1018                              (ppr tv <+> equals <+> ppr ty)
 1019                          ; role <- getRole
 1020                          ; return $ RTRFollowed $
 1021                              mkReflRedn role ty }
 1022            Nothing -> do { traceRewriteM "Unfilled tyvar" (pprTyVar tv)
 1023                          ; fr <- getFlavourRole
 1024                          ; rewrite_tyvar2 tv fr } }
 1025 
 1026 rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
 1027 -- The tyvar is not a filled-in meta-tyvar
 1028 -- Try in the inert equalities
 1029 -- See Definition [Applying a generalised substitution] in GHC.Tc.Solver.Monad
 1030 -- See Note [Stability of rewriting] in GHC.Tc.Solver.Monad
 1031 
 1032 rewrite_tyvar2 tv fr@(_, eq_rel)
 1033   = do { ieqs <- liftTcS $ getInertEqs
 1034        ; case lookupDVarEnv ieqs tv of
 1035            Just (EqualCtList (ct :| _))   -- If the first doesn't work,
 1036                                           -- the subsequent ones won't either
 1037              | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
 1038                       , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct
 1039              , let ct_fr = (ctEvFlavour ctev, ct_eq_rel)
 1040              , ct_fr `eqCanRewriteFR` fr  -- This is THE key call of eqCanRewriteFR
 1041              -> do { traceRewriteM "Following inert tyvar"
 1042                         (ppr tv <+>
 1043                          equals <+>
 1044                          ppr rhs_ty $$ ppr ctev)
 1045                     ; let rewriting_co1 = ctEvCoercion ctev
 1046                           rewriting_co  = case (ct_eq_rel, eq_rel) of
 1047                             (ReprEq, _rel)  -> assert (_rel == ReprEq )
 1048                                     -- if this ASSERT fails, then
 1049                                     -- eqCanRewriteFR answered incorrectly
 1050                                                rewriting_co1
 1051                             (NomEq, NomEq)  -> rewriting_co1
 1052                             (NomEq, ReprEq) -> mkSubCo rewriting_co1
 1053 
 1054                     ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty }
 1055                     -- NB: ct is Derived then fmode must be also, hence
 1056                     -- we are not going to touch the returned coercion
 1057                     -- so ctEvCoercion is fine.
 1058 
 1059            _other -> return RTRNotFollowed }
 1060 
 1061 {-
 1062 Note [An alternative story for the inert substitution]
 1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1064 (This entire note is just background, left here in case we ever want
 1065  to return the previous state of affairs)
 1066 
 1067 We used (GHC 7.8) to have this story for the inert substitution inert_eqs
 1068 
 1069  * 'a' is not in fvs(ty)
 1070  * They are *inert* in the weaker sense that there is no infinite chain of
 1071    (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc
 1072 
 1073 This means that rewriting must be recursive, but it does allow
 1074   [G] a ~ [b]
 1075   [G] b ~ Maybe c
 1076 
 1077 This avoids "saturating" the Givens, which can save a modest amount of work.
 1078 It is easy to implement, in GHC.Tc.Solver.Interact.kick_out, by only kicking out an inert
 1079 only if (a) the work item can rewrite the inert AND
 1080         (b) the inert cannot rewrite the work item
 1081 
 1082 This is significantly harder to think about. It can save a LOT of work
 1083 in occurs-check cases, but we don't care about them much.  #5837
 1084 is an example, but it causes trouble only with the old (pre-Fall 2020)
 1085 rewriting story. It is unclear if there is any gain w.r.t. to
 1086 the new story.
 1087 
 1088 -}
 1089 
 1090 --------------------------------------
 1091 -- Utilities
 1092 
 1093 -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at
 1094 -- least one named binder.
 1095 split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
 1096 split_pi_tys' ty = split ty ty
 1097   where
 1098      -- put common cases first
 1099   split _       (ForAllTy b res) = let -- This bang is necessary lest we see rather
 1100                                        -- terrible reboxing, as noted in #19102.
 1101                                        !(bs, ty, _) = split res res
 1102                                    in  (Named b : bs, ty, True)
 1103   split _       (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res })
 1104                                  = let -- See #19102
 1105                                        !(bs, ty, named) = split res res
 1106                                    in  (Anon af (mkScaled w arg) : bs, ty, named)
 1107 
 1108   split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
 1109   split orig_ty _                = ([], orig_ty, False)
 1110 {-# INLINE split_pi_tys' #-}
 1111 
 1112 -- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff
 1113 -- there is at least one named binder.
 1114 ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
 1115 ty_con_binders_ty_binders' = foldr go ([], False)
 1116   where
 1117     go (Bndr tv (NamedTCB vis)) (bndrs, _)
 1118       = (Named (Bndr tv vis) : bndrs, True)
 1119     go (Bndr tv (AnonTCB af))   (bndrs, n)
 1120       = (Anon af (tymult (tyVarKind tv)) : bndrs, n)
 1121     {-# INLINE go #-}
 1122 {-# INLINE ty_con_binders_ty_binders' #-}