module GHC.Tc.Solver.Rewrite( rewrite, rewriteForErrors, rewriteArgsNom, rewriteType ) where import GHC.Prelude import GHC.Core.TyCo.Ppr ( pprTyVar ) import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters), TcPluginRewriter, TcPluginRewriteResult(..), RewriteEnv(..), runTcPluginM ) import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Utils.TcType import GHC.Core.Type import GHC.Tc.Types.Evidence import GHC.Core.TyCon import GHC.Core.TyCo.Rep -- performs delicate algorithm on types import GHC.Core.Coercion import GHC.Core.Reduction import GHC.Types.Unique.FM import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Driver.DynFlags import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Tc.Solver.Monad as TcS import GHC.Utils.Misc import GHC.Data.Maybe import GHC.Exts (oneShot) import Control.Monad import Control.Applicative (liftA3) import GHC.Builtin.Types (tYPETyCon) import Data.List ( find ) import GHC.Data.List.Infinite (Infinite) import GHC.Data.Bag( listToBag ) import qualified GHC.Data.List.Infinite as Inf {- ************************************************************************ * * * RewriteEnv & RewriteM * The rewriting environment & monad * * ************************************************************************ -} -- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv' newtype RewriteM a = RewriteM { forall a. RewriteM a -> RewriteEnv -> TcS a runRewriteM :: RewriteEnv -> TcS a } -- | Smart constructor for 'RewriteM', as describe in Note [The one-shot state -- monad trick] in "GHC.Utils.Monad". mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM :: forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM RewriteEnv -> TcS a f = (RewriteEnv -> TcS a) -> RewriteM a forall a. (RewriteEnv -> TcS a) -> RewriteM a RewriteM ((RewriteEnv -> TcS a) -> RewriteEnv -> TcS a forall a b. (a -> b) -> a -> b oneShot RewriteEnv -> TcS a f) {-# INLINE mkRewriteM #-} instance Monad RewriteM where RewriteM a m >>= :: forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b >>= a -> RewriteM b k = (RewriteEnv -> TcS b) -> RewriteM b forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b) -> (RewriteEnv -> TcS b) -> RewriteM b forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> do { a <- RewriteM a -> RewriteEnv -> TcS a forall a. RewriteM a -> RewriteEnv -> TcS a runRewriteM RewriteM a m RewriteEnv env ; runRewriteM (k a) env } instance Applicative RewriteM where pure :: forall a. a -> RewriteM a pure a x = (RewriteEnv -> TcS a) -> RewriteM a forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a) -> (RewriteEnv -> TcS a) -> RewriteM a forall a b. (a -> b) -> a -> b $ \RewriteEnv _ -> a -> TcS a forall a. a -> TcS a forall (f :: * -> *) a. Applicative f => a -> f a pure a x <*> :: forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b (<*>) = RewriteM (a -> b) -> RewriteM a -> RewriteM b forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b ap instance Functor RewriteM where fmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b fmap a -> b f (RewriteM RewriteEnv -> TcS a x) = (RewriteEnv -> TcS b) -> RewriteM b forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b) -> (RewriteEnv -> TcS b) -> RewriteM b forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> (a -> b) -> TcS a -> TcS b forall a b. (a -> b) -> TcS a -> TcS b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b f (RewriteEnv -> TcS a x RewriteEnv env) instance HasDynFlags RewriteM where getDynFlags :: RewriteM DynFlags getDynFlags = TcS DynFlags -> RewriteM DynFlags forall a. TcS a -> RewriteM a liftTcS TcS DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags liftTcS :: TcS a -> RewriteM a liftTcS :: forall a. TcS a -> RewriteM a liftTcS TcS a thing_inside = (RewriteEnv -> TcS a) -> RewriteM a forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a) -> (RewriteEnv -> TcS a) -> RewriteM a forall a b. (a -> b) -> a -> b $ \RewriteEnv _ -> TcS a thing_inside -- convenient wrapper when you have a CtEvidence describing -- the rewriting operation runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet) runRewriteCtEv :: forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet) runRewriteCtEv CtEvidence ev = CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) runRewrite (CtEvidence -> CtLoc ctEvLoc CtEvidence ev) (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ev) (CtEvidence -> EqRel ctEvRewriteEqRel CtEvidence ev) -- Run thing_inside (which does the rewriting) -- Also returns the set of Wanteds which rewrote a Wanted; -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) runRewrite :: forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) runRewrite CtLoc loc CtFlavour flav EqRel eq_rel RewriteM a thing_inside = do { rewriters_ref <- RewriterSet -> TcS (TcRef RewriterSet) forall a. a -> TcS (TcRef a) newTcRef RewriterSet emptyRewriterSet ; let fmode = RE { re_loc :: CtLoc re_loc = CtLoc loc , re_flavour :: CtFlavour re_flavour = CtFlavour flav , re_eq_rel :: EqRel re_eq_rel = EqRel eq_rel , re_rewriters :: TcRef RewriterSet re_rewriters = TcRef RewriterSet rewriters_ref } ; res <- runRewriteM thing_inside fmode ; rewriters <- readTcRef rewriters_ref ; return (res, rewriters) } traceRewriteM :: String -> SDoc -> RewriteM () traceRewriteM :: String -> SDoc -> RewriteM () traceRewriteM String herald SDoc doc = TcS () -> RewriteM () forall a. TcS a -> RewriteM a liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM () forall a b. (a -> b) -> a -> b $ String -> SDoc -> TcS () traceTcS String herald SDoc doc {-# INLINE traceRewriteM #-} -- see Note [INLINE conditional tracing utilities] getRewriteEnv :: RewriteM RewriteEnv getRewriteEnv :: RewriteM RewriteEnv getRewriteEnv = (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv) -> (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> RewriteEnv -> TcS RewriteEnv forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return RewriteEnv env getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a getRewriteEnvField :: forall a. (RewriteEnv -> a) -> RewriteM a getRewriteEnvField RewriteEnv -> a accessor = (RewriteEnv -> TcS a) -> RewriteM a forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a) -> (RewriteEnv -> TcS a) -> RewriteM a forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> a -> TcS a forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (RewriteEnv -> a accessor RewriteEnv env) getEqRel :: RewriteM EqRel getEqRel :: RewriteM EqRel getEqRel = (RewriteEnv -> EqRel) -> RewriteM EqRel forall a. (RewriteEnv -> a) -> RewriteM a getRewriteEnvField RewriteEnv -> EqRel re_eq_rel getRole :: RewriteM Role getRole :: RewriteM Role getRole = EqRel -> Role eqRelRole (EqRel -> Role) -> RewriteM EqRel -> RewriteM Role forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> RewriteM EqRel getEqRel getFlavour :: RewriteM CtFlavour getFlavour :: RewriteM CtFlavour getFlavour = (RewriteEnv -> CtFlavour) -> RewriteM CtFlavour forall a. (RewriteEnv -> a) -> RewriteM a getRewriteEnvField RewriteEnv -> CtFlavour re_flavour getFlavourRole :: RewriteM CtFlavourRole getFlavourRole :: RewriteM CtFlavourRole getFlavourRole = do { flavour <- RewriteM CtFlavour getFlavour ; eq_rel <- getEqRel ; return (flavour, eq_rel) } getLoc :: RewriteM CtLoc getLoc :: RewriteM CtLoc getLoc = (RewriteEnv -> CtLoc) -> RewriteM CtLoc forall a. (RewriteEnv -> a) -> RewriteM a getRewriteEnvField RewriteEnv -> CtLoc re_loc checkStackDepth :: Type -> RewriteM () checkStackDepth :: Xi -> RewriteM () checkStackDepth Xi ty = do { loc <- RewriteM CtLoc getLoc ; liftTcS $ checkReductionDepth loc ty } -- | Change the 'EqRel' in a 'RewriteM'. setEqRel :: EqRel -> RewriteM a -> RewriteM a setEqRel :: forall a. EqRel -> RewriteM a -> RewriteM a setEqRel EqRel new_eq_rel RewriteM a thing_inside = (RewriteEnv -> TcS a) -> RewriteM a forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a) -> (RewriteEnv -> TcS a) -> RewriteM a forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> if EqRel new_eq_rel EqRel -> EqRel -> Bool forall a. Eq a => a -> a -> Bool == RewriteEnv -> EqRel re_eq_rel RewriteEnv env then RewriteM a -> RewriteEnv -> TcS a forall a. RewriteM a -> RewriteEnv -> TcS a runRewriteM RewriteM a thing_inside RewriteEnv env else RewriteM a -> RewriteEnv -> TcS a forall a. RewriteM a -> RewriteEnv -> TcS a runRewriteM RewriteM a thing_inside (RewriteEnv env { re_eq_rel = new_eq_rel }) {-# INLINE setEqRel #-} bumpDepth :: RewriteM a -> RewriteM a bumpDepth :: forall a. RewriteM a -> RewriteM a bumpDepth (RewriteM RewriteEnv -> TcS a thing_inside) = (RewriteEnv -> TcS a) -> RewriteM a forall a. (RewriteEnv -> TcS a) -> RewriteM a mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a) -> (RewriteEnv -> TcS a) -> RewriteM a forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> do -- bumpDepth can be called a lot during rewriting so we force the -- new env to avoid accumulating thunks. { let !env' :: RewriteEnv env' = RewriteEnv env { re_loc = bumpCtLocDepth (re_loc env) } ; RewriteEnv -> TcS a thing_inside RewriteEnv env' } -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint -- Precondition: the CtEvidence is a CtWanted of an equality recordRewriter :: CtEvidence -> RewriteM () recordRewriter :: CtEvidence -> RewriteM () recordRewriter (CtWanted { ctev_dest :: CtEvidence -> TcEvDest ctev_dest = HoleDest CoercionHole hole }) = (RewriteEnv -> TcS ()) -> RewriteM () forall a. (RewriteEnv -> TcS a) -> RewriteM a RewriteM ((RewriteEnv -> TcS ()) -> RewriteM ()) -> (RewriteEnv -> TcS ()) -> RewriteM () forall a b. (a -> b) -> a -> b $ \RewriteEnv env -> TcRef RewriterSet -> (RewriterSet -> RewriterSet) -> TcS () forall a. TcRef a -> (a -> a) -> TcS () updTcRef (RewriteEnv -> TcRef RewriterSet re_rewriters RewriteEnv env) (RewriterSet -> CoercionHole -> RewriterSet `addRewriter` CoercionHole hole) recordRewriter CtEvidence other = String -> SDoc -> RewriteM () forall a. HasCallStack => String -> SDoc -> a pprPanic String "recordRewriter" (CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence other) {- Note [Rewriter EqRels] ~~~~~~~~~~~~~~~~~~~~~~~ When rewriting, we need to know which equality relation -- nominal or representational -- we should be respecting. This is controlled by the `re_eq_rel` field of RewriteEnv. * When rewriting primitive /representational/ equalities, (t1 ~# t2), we set re_eq_rel=ReprEq. * For all other constraints, we set re_eq_rel=NomEq See Note [The rewrite-role of a constraint] in GHC.Tc.Types.Constraint. The only difference is that when re_eq_rel=ReprEq * we rewrite variables by representational equalities * we unwrap newtypes Note [Rewriter CtLoc] ~~~~~~~~~~~~~~~~~~~~~~ The rewriter does eager type-family reduction. Type families might loop, and we don't want GHC to do so. A natural solution is to have a bounded depth to these processes. A central difficulty is that such a solution isn't quite compositional. For example, say it takes F Int 10 steps to get to Bool. How many steps does it take to get from F Int -> F Int to Bool -> Bool? 10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to know and hard to track. So, we punt, essentially. We store a CtLoc in the RewriteEnv and just update the environment when recurring. In the TyConApp case, where there may be multiple type families to rewrite, we just copy the current CtLoc into each branch. If any branch hits the stack limit, then the whole thing fails. A consequence of this is that setting the stack limits appropriately will be essentially impossible. So, the official recommendation if a stack limit is hit is to disable the check entirely. Otherwise, there will be baffling, unpredictable errors. Note [Phantoms in the rewriter] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have data Proxy p = Proxy and we're rewriting (Proxy ty) w.r.t. ReprEq. Then, we know that `ty` is really irrelevant -- it will be ignored when solving for representational equality later on. So, we omit rewriting `ty` entirely. This may violate the expectation of "xi"s for a bit, but the canonicaliser will soon throw out the phantoms when decomposing a TyConApp. (Or, the canonicaliser will emit an insoluble, in which case we get a better error message anyway.) -} {- ********************************************************************* * * * Externally callable rewriting functions * * * ************************************************************************ -} -- | See Note [Rewriting]. -- If (xi, co, rewriters) <- rewrite mode ev ty, then co :: xi ~r ty -- where r is the role in @ev@. -- rewriters is the set of coercion holes that have been used to rewrite -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint rewrite :: CtEvidence -> TcType -> TcS (Reduction, RewriterSet) rewrite :: CtEvidence -> Xi -> TcS (Reduction, RewriterSet) rewrite CtEvidence ev Xi ty = do { String -> SDoc -> TcS () traceTcS String "rewrite {" (Xi -> SDoc forall a. Outputable a => a -> SDoc ppr Xi ty) ; result@(redn, _) <- CtEvidence -> RewriteM Reduction -> TcS (Reduction, RewriterSet) forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet) runRewriteCtEv CtEvidence ev (Xi -> RewriteM Reduction rewrite_one Xi ty) ; traceTcS "rewrite }" (ppr $ reductionReducedType redn) ; return result } -- | See Note [Rewriting] -- `rewriteForErrors` is a variant of 'rewrite' that rewrites -- w.r.t. nominal equality only, as this is better than full rewriting -- for error messages. (This was important when we flirted with rewriting -- newtypes but perhaps less so now.) rewriteForErrors :: CtEvidence -> TcType -> TcS (Reduction, RewriterSet) rewriteForErrors :: CtEvidence -> Xi -> TcS (Reduction, RewriterSet) rewriteForErrors CtEvidence ev Xi ty = do { String -> SDoc -> TcS () traceTcS String "rewriteForErrors {" (Xi -> SDoc forall a. Outputable a => a -> SDoc ppr Xi ty) ; result@(redn, rewriters) <- CtLoc -> CtFlavour -> EqRel -> RewriteM Reduction -> TcS (Reduction, RewriterSet) forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) runRewrite (CtEvidence -> CtLoc ctEvLoc CtEvidence ev) (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ev) EqRel NomEq (Xi -> RewriteM Reduction rewrite_one Xi ty) ; traceTcS "rewriteForErrors }" (ppr $ reductionReducedType redn) ; return $ case ctEvRewriteEqRel ev of EqRel NomEq -> (Reduction, RewriterSet) result EqRel ReprEq -> (Reduction -> Reduction mkSubRedn Reduction redn, RewriterSet rewriters) } -- See Note [Rewriting] rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS (Reductions, RewriterSet) -- Externally-callable, hence runRewrite -- Rewrite a vector of types all at once; in fact they are -- always the arguments of type family or class, so -- ctEvFlavour ev = Nominal -- and we want to rewrite all at nominal role -- The kind passed in is the kind of the type family or class, call it T -- The kind of T args must be constant (i.e. not depend on the args) -- -- Final return value returned which Wanteds rewrote another Wanted -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint rewriteArgsNom :: CtEvidence -> TyCon -> [Xi] -> TcS (Reductions, RewriterSet) rewriteArgsNom CtEvidence ev TyCon tc [Xi] tys = do { String -> SDoc -> TcS () traceTcS String "rewrite_args {" ([SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((Xi -> SDoc) -> [Xi] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Xi -> SDoc forall a. Outputable a => a -> SDoc ppr [Xi] tys)) ; (ArgsReductions redns@(Reductions _ tys') kind_co, rewriters) <- CtEvidence -> RewriteM ArgsReductions -> TcS (ArgsReductions, RewriterSet) forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet) runRewriteCtEv CtEvidence ev (TyCon -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions rewrite_args_tc TyCon tc Maybe (Infinite Role) forall a. Maybe a Nothing [Xi] tys) ; massert (isReflMCo kind_co) ; traceTcS "rewrite }" (vcat (map ppr tys')) ; return (redns, rewriters) } -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite -- a type w.r.t. any givens. It does not do type-family reduction. This -- will never emit new constraints. Call this when the inert set contains -- only givens. rewriteType :: CtLoc -> TcType -> TcS TcType rewriteType :: CtLoc -> Xi -> TcS Xi rewriteType CtLoc loc Xi ty = do { (redn, _) <- CtLoc -> CtFlavour -> EqRel -> RewriteM Reduction -> TcS (Reduction, RewriterSet) forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet) runRewrite CtLoc loc CtFlavour Given EqRel NomEq (RewriteM Reduction -> TcS (Reduction, RewriterSet)) -> RewriteM Reduction -> TcS (Reduction, RewriterSet) forall a b. (a -> b) -> a -> b $ Xi -> RewriteM Reduction rewrite_one Xi ty -- use Given flavor so that it is rewritten -- only w.r.t. Givens, never Wanteds -- (Shouldn't matter, if only Givens are present -- anyway) ; return $ reductionReducedType redn } {- ********************************************************************* * * * The main rewriting functions * * ********************************************************************* -} {- Note [Rewriting] ~~~~~~~~~~~~~~~~~~~~ rewrite ty ==> Reduction co xi where xi has no reducible type functions has no skolems that are mapped in the inert set has no filled-in metavariables co :: ty ~ xi (coercions in reductions are always left-to-right) Key invariants: (F0) co :: zonk(ty') ~ xi where zonk(ty') ~ zonk(ty) (F1) typeKind(xi) succeeds and returns a fully zonked kind (F2) typeKind(xi) `eqType` zonk(typeKind(ty)) Note that it is rewrite's job to try to reduce *every type function it sees*. Rewriting also: * zonks, removing any metavariables, and * applies the substitution embodied in the inert set Because rewriting zonks and the returned coercion ("co" above) is also zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead, we can rely on this fact: (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty) Note that the right-hand type of co is *always* precisely xi. The left-hand type may or may not be ty, however: if ty has unzonked filled-in metavariables, then the left-hand type of co will be the zonk-equal to ty. It is for this reason that we occasionally have to explicitly zonk, when (co :: ty ~ xi) is important even before we zonk the whole program. For example, see the RTRNotFollowed case in rewriteTyVar. Why have these invariants on rewriting? Because we sometimes use typeKind during canonicalisation, and we want this kind to be zonked (e.g., see GHC.Tc.Solver.Equality.canEqCanLHS). Rewriting is always homogeneous. That is, the kind of the result of rewriting is always the same as the kind of the input, modulo zonking. More formally: (F2) zonk(typeKind(ty)) `eqType` typeKind(xi) This invariant means that the kind of a rewritten type might not itself be rewritten. Note that we prefer to leave type synonyms unexpanded when possible, so when the rewriter encounters one, it first asks whether its transitive expansion contains any type function applications or is forgetful -- that is, omits one or more type variables in its RHS. If so, it expands the synonym and proceeds; if not, it simply returns the unexpanded synonym. See also Note [Rewriting synonyms]. Where do we actually perform rewriting within a type? See Note [Rewritable] in GHC.Tc.Solver.InertSet. Note [rewrite_args performance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In programs with lots of type-level evaluation, rewrite_args becomes part of a tight loop. For example, see test perf/compiler/T9872a, which calls rewrite_args a whopping 7,106,808 times. It is thus important that rewrite_args be efficient. Performance testing showed that the current implementation is indeed efficient. It's critically important that zipWithAndUnzipM be specialized to TcS, and it's also quite helpful to actually `inline` it. On test T9872a, here are the allocation stats (Dec 16, 2014): * Unspecialized, uninlined: 8,472,613,440 bytes allocated in the heap * Specialized, uninlined: 6,639,253,488 bytes allocated in the heap * Specialized, inlined: 6,281,539,792 bytes allocated in the heap To improve performance even further, rewrite_args_nom is split off from rewrite_args, as nominal equality is the common case. This would be natural to write using mapAndUnzipM, but even inlined, that function is not as performant as a hand-written loop. * mapAndUnzipM, inlined: 7,463,047,432 bytes allocated in the heap * hand-written recursion: 5,848,602,848 bytes allocated in the heap If you make any change here, pay close attention to the T9872{a,b,c} tests and T5321Fun. If we need to make this yet more performant, a possible way forward is to duplicate the rewriter code for the nominal case, and make that case faster. This doesn't seem quite worth it, yet. Note [rewrite_exact_fam_app performance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Once we've got a rewritten rhs, we extend the famapp-cache to record the result. Doing so can save lots of work when the same redex shows up more than once. Note that we record the link from the redex all the way to its *final* value, not just the single step reduction. If we can reduce the family application right away (the first call to try_to_reduce), we do *not* add to the cache. There are two possibilities here: 1) we just read the result from the cache, or 2) we used one type family instance. In either case, recording the result in the cache doesn't save much effort the next time around. And adding to the cache here is actually disastrous: it more than doubles the allocations for T9872a. So we skip adding to the cache here. -} {-# INLINE rewrite_args_tc #-} rewrite_args_tc :: TyCon -- T -> Maybe (Infinite Role) -- Nothing: ambient role is Nominal; all args are Nominal -- Otherwise: no assumptions; use roles provided -> [Type] -> RewriteM ArgsReductions -- See the commentary on rewrite_args rewrite_args_tc :: TyCon -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions rewrite_args_tc TyCon tc = [PiTyBinder] -> Bool -> Xi -> TcTyCoVarSet -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions rewrite_args [PiTyBinder] all_bndrs Bool any_named_bndrs Xi inner_ki TcTyCoVarSet emptyVarSet -- NB: TyCon kinds are always closed where -- There are many bang patterns in here. It's been observed that they -- greatly improve performance of an optimized build. -- The T9872 test cases are good witnesses of this fact. ([PiTyBinder] bndrs, Bool named) = [TyConBinder] -> ([PiTyBinder], Bool) ty_con_binders_ty_binders' (TyCon -> [TyConBinder] tyConBinders TyCon tc) -- it's possible that the result kind has arrows (for, e.g., a type family) -- so we must split it ([PiTyBinder] inner_bndrs, Xi inner_ki, Bool inner_named) = Xi -> ([PiTyBinder], Xi, Bool) split_pi_tys' (TyCon -> Xi tyConResKind TyCon tc) !all_bndrs :: [PiTyBinder] all_bndrs = [PiTyBinder] bndrs [PiTyBinder] -> [PiTyBinder] -> [PiTyBinder] forall a. [a] -> [a] -> [a] `chkAppend` [PiTyBinder] inner_bndrs !any_named_bndrs :: Bool any_named_bndrs = Bool named Bool -> Bool -> Bool || Bool inner_named -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%. {-# INLINE rewrite_args #-} rewrite_args :: [PiTyBinder] -> Bool -- Binders, and True iff any of them are -- named. -> Kind -> TcTyCoVarSet -- function kind; kind's free vars -> Maybe (Infinite Role) -> [Type] -- these are in 1-to-1 correspondence -- Nothing: use all Nominal -> RewriteM ArgsReductions -- This function returns ArgsReductions (Reductions cos xis) res_co -- coercions: co_i :: ty_i ~ xi_i, at roles given -- types: xi_i -- coercion: res_co :: typeKind(fun tys) ~N typeKind(fun xis) -- That is, the result coercion relates the kind of some function (whose kind is -- passed as the first parameter) instantiated at tys to the kind of that -- function instantiated at the xis. This is useful in keeping rewriting -- homogeneous. The list of roles must be at least as long as the list of -- types. rewrite_args :: [PiTyBinder] -> Bool -> Xi -> TcTyCoVarSet -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions rewrite_args [PiTyBinder] orig_binders Bool any_named_bndrs Xi orig_inner_ki TcTyCoVarSet orig_fvs Maybe (Infinite Role) orig_m_roles [Xi] orig_tys = case (Maybe (Infinite Role) orig_m_roles, Bool any_named_bndrs) of (Maybe (Infinite Role) Nothing, Bool False) -> [Xi] -> RewriteM ArgsReductions rewrite_args_fast [Xi] orig_tys (Maybe (Infinite Role), Bool) _ -> [PiTyBinder] -> Xi -> TcTyCoVarSet -> Infinite Role -> [Xi] -> RewriteM ArgsReductions rewrite_args_slow [PiTyBinder] orig_binders Xi orig_inner_ki TcTyCoVarSet orig_fvs Infinite Role orig_roles [Xi] orig_tys where orig_roles :: Infinite Role orig_roles = Infinite Role -> Maybe (Infinite Role) -> Infinite Role forall a. a -> Maybe a -> a fromMaybe (Role -> Infinite Role forall a. a -> Infinite a Inf.repeat Role Nominal) Maybe (Infinite Role) orig_m_roles {-# INLINE rewrite_args_fast #-} -- | fast path rewrite_args, in which none of the binders are named and -- therefore we can avoid tracking a lifting context. rewrite_args_fast :: [Type] -> RewriteM ArgsReductions rewrite_args_fast :: [Xi] -> RewriteM ArgsReductions rewrite_args_fast [Xi] orig_tys = (Reductions -> ArgsReductions) -> RewriteM Reductions -> RewriteM ArgsReductions forall a b. (a -> b) -> RewriteM a -> RewriteM b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Reductions -> ArgsReductions finish ([Xi] -> RewriteM Reductions iterate [Xi] orig_tys) where iterate :: [Type] -> RewriteM Reductions iterate :: [Xi] -> RewriteM Reductions iterate (Xi ty : [Xi] tys) = do Reduction co xi <- Xi -> RewriteM Reduction rewrite_one Xi ty Reductions cos xis <- iterate tys pure $ Reductions (co : cos) (xi : xis) iterate [] = Reductions -> RewriteM Reductions forall a. a -> RewriteM a forall (f :: * -> *) a. Applicative f => a -> f a pure (Reductions -> RewriteM Reductions) -> Reductions -> RewriteM Reductions forall a b. (a -> b) -> a -> b $ [Coercion] -> [Xi] -> Reductions Reductions [] [] {-# INLINE finish #-} finish :: Reductions -> ArgsReductions finish :: Reductions -> ArgsReductions finish Reductions redns = Reductions -> MCoercionN -> ArgsReductions ArgsReductions Reductions redns MCoercionN MRefl {-# INLINE rewrite_args_slow #-} -- | Slow path, compared to rewrite_args_fast, because this one must track -- a lifting context. rewrite_args_slow :: [PiTyBinder] -> Kind -> TcTyCoVarSet -> Infinite Role -> [Type] -> RewriteM ArgsReductions rewrite_args_slow :: [PiTyBinder] -> Xi -> TcTyCoVarSet -> Infinite Role -> [Xi] -> RewriteM ArgsReductions rewrite_args_slow [PiTyBinder] binders Xi inner_ki TcTyCoVarSet fvs Infinite Role roles [Xi] tys = do { rewritten_args <- (Role -> Xi -> RewriteM Reduction) -> [Role] -> [Xi] -> RewriteM [Reduction] forall (m :: * -> *) a b c. Applicative m => (a -> b -> m c) -> [a] -> [b] -> m [c] zipWithM Role -> Xi -> RewriteM Reduction rw (Infinite Role -> [Role] forall a. Infinite a -> [a] Inf.toList Infinite Role roles) [Xi] tys ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) } where {-# INLINE rw #-} rw :: Role -> Type -> RewriteM Reduction rw :: Role -> Xi -> RewriteM Reduction rw Role Nominal Xi ty = EqRel -> RewriteM Reduction -> RewriteM Reduction forall a. EqRel -> RewriteM a -> RewriteM a setEqRel EqRel NomEq (RewriteM Reduction -> RewriteM Reduction) -> RewriteM Reduction -> RewriteM Reduction forall a b. (a -> b) -> a -> b $ Xi -> RewriteM Reduction rewrite_one Xi ty rw Role Representational Xi ty = EqRel -> RewriteM Reduction -> RewriteM Reduction forall a. EqRel -> RewriteM a -> RewriteM a setEqRel EqRel ReprEq (RewriteM Reduction -> RewriteM Reduction) -> RewriteM Reduction -> RewriteM Reduction forall a b. (a -> b) -> a -> b $ Xi -> RewriteM Reduction rewrite_one Xi ty rw Role Phantom Xi ty -- See Note [Phantoms in the rewriter] = do { ty <- TcS Xi -> RewriteM Xi forall a. TcS a -> RewriteM a liftTcS (TcS Xi -> RewriteM Xi) -> TcS Xi -> RewriteM Xi forall a b. (a -> b) -> a -> b $ Xi -> TcS Xi zonkTcType Xi ty ; return $ mkReflRedn Phantom ty } ------------------ rewrite_one :: TcType -> RewriteM Reduction -- Rewrite a type to get rid of type function applications, returning -- the new type-function-free type, and a collection of new equality -- constraints. See Note [Rewriting] for more detail. -- -- Postcondition: -- the role on the result coercion matches the EqRel in the RewriteEnv rewrite_one :: Xi -> RewriteM Reduction rewrite_one Xi ty | Just Xi ty' <- Xi -> Maybe Xi rewriterView Xi ty -- See Note [Rewriting synonyms] = Xi -> RewriteM Reduction rewrite_one Xi ty' rewrite_one xi :: Xi xi@(LitTy {}) = do { role <- RewriteM Role getRole ; return $ mkReflRedn role xi } rewrite_one (TyVarTy TcTyVar tv) = TcTyVar -> RewriteM Reduction rewriteTyVar TcTyVar tv rewrite_one (AppTy Xi ty1 Xi ty2) = Xi -> [Xi] -> RewriteM Reduction rewrite_app_tys Xi ty1 [Xi ty2] rewrite_one (TyConApp TyCon tc [Xi] tys) -- If it's a type family application, try to reduce it | TyCon -> Bool isTypeFamilyTyCon TyCon tc = TyCon -> [Xi] -> RewriteM Reduction rewrite_fam_app TyCon tc [Xi] tys | Bool otherwise -- We just recursively rewrite the arguments. -- See Note [Do not rewrite newtypes] = TyCon -> [Xi] -> RewriteM Reduction rewrite_ty_con_app TyCon tc [Xi] tys rewrite_one (FunTy { ft_af :: Xi -> FunTyFlag ft_af = FunTyFlag vis, ft_mult :: Xi -> Xi ft_mult = Xi mult, ft_arg :: Xi -> Xi ft_arg = Xi ty1, ft_res :: Xi -> Xi ft_res = Xi ty2 }) = do { arg_redn <- Xi -> RewriteM Reduction rewrite_one Xi ty1 ; res_redn <- rewrite_one ty2 -- Important: look at the *reduced* type, so that any unzonked variables -- in kinds are gone and the getRuntimeRep succeeds. -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Equality. ; let arg_rep = HasDebugCallStack => Xi -> Xi Xi -> Xi getRuntimeRep (Reduction -> Xi reductionReducedType Reduction arg_redn) res_rep = HasDebugCallStack => Xi -> Xi Xi -> Xi getRuntimeRep (Reduction -> Xi reductionReducedType Reduction res_redn) ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $ liftA3 (,,) (rewrite_one mult) (rewrite_one arg_rep) (rewrite_one res_rep) ; role <- getRole ; let arg_rep_co = Reduction -> Coercion reductionCoercion Reduction arg_rep_redn -- :: arg_rep ~ arg_rep_xi arg_ki_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role Nominal TyCon tYPETyCon [Coercion arg_rep_co] -- :: TYPE arg_rep ~ TYPE arg_rep_xi casted_arg_redn = Role -> Reduction -> Coercion -> Reduction mkCoherenceRightRedn Role role Reduction arg_redn Coercion arg_ki_co -- :: ty1 ~> arg_xi |> arg_ki_co res_rep_co = Reduction -> Coercion reductionCoercion Reduction res_rep_redn res_ki_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role Nominal TyCon tYPETyCon [Coercion res_rep_co] casted_res_redn = Role -> Reduction -> Coercion -> Reduction mkCoherenceRightRedn Role role Reduction res_redn Coercion res_ki_co -- We must rewrite the representations, because that's what would -- be done if we used TyConApp instead of FunTy. These rewritten -- representations are seen only in casts of the arg and res, below. -- Forgetting this caused #19677. ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn } rewrite_one ty :: Xi ty@(ForAllTy {}) -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of -- the bound tyvar. Doing so will require carrying around a substitution -- and the usual substTyVarBndr-like silliness. Argh. -- We allow for-alls when, but only when, no type function -- applications inside the forall involve the bound type variables. = do { let ([TyVarBinder] bndrs, Xi rho) = Xi -> ([TyVarBinder], Xi) tcSplitForAllTyVarBinders Xi ty ; redn <- Xi -> RewriteM Reduction rewrite_one Xi rho ; return $ mkHomoForAllRedn bndrs redn } rewrite_one (CastTy Xi ty Coercion g) = do { redn <- Xi -> RewriteM Reduction rewrite_one Xi ty ; g' <- rewrite_co g ; role <- getRole ; return $ mkCastRedn1 role ty g' redn } -- This calls castCoercionKind1. -- It makes a /big/ difference to call castCoercionKind1 not -- the more general castCoercionKind2. -- See Note [castCoercionKind1] in GHC.Core.Coercion rewrite_one (CoercionTy Coercion co) = do { co' <- Coercion -> RewriteM Coercion rewrite_co Coercion co ; role <- getRole ; return $ mkReflCoRedn role co' } -- | "Rewrite" a coercion. Really, just zonk it so we can uphold -- (F1) of Note [Rewriting] rewrite_co :: Coercion -> RewriteM Coercion rewrite_co :: Coercion -> RewriteM Coercion rewrite_co Coercion co = TcS Coercion -> RewriteM Coercion forall a. TcS a -> RewriteM a liftTcS (TcS Coercion -> RewriteM Coercion) -> TcS Coercion -> RewriteM Coercion forall a b. (a -> b) -> a -> b $ Coercion -> TcS Coercion zonkCo Coercion co -- | Rewrite a reduction, composing the resulting coercions. rewrite_reduction :: Reduction -> RewriteM Reduction rewrite_reduction :: Reduction -> RewriteM Reduction rewrite_reduction (Reduction Coercion co Xi xi) = do { redn <- RewriteM Reduction -> RewriteM Reduction forall a. RewriteM a -> RewriteM a bumpDepth (RewriteM Reduction -> RewriteM Reduction) -> RewriteM Reduction -> RewriteM Reduction forall a b. (a -> b) -> a -> b $ Xi -> RewriteM Reduction rewrite_one Xi xi ; return $ co `mkTransRedn` redn } -- rewrite (nested) AppTys rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction -- commoning up nested applications allows us to look up the function's kind -- only once. Without commoning up like this, we would spend a quadratic amount -- of time looking up functions' types rewrite_app_tys :: Xi -> [Xi] -> RewriteM Reduction rewrite_app_tys (AppTy Xi ty1 Xi ty2) [Xi] tys = Xi -> [Xi] -> RewriteM Reduction rewrite_app_tys Xi ty1 (Xi ty2Xi -> [Xi] -> [Xi] forall a. a -> [a] -> [a] :[Xi] tys) rewrite_app_tys Xi fun_ty [Xi] arg_tys = do { redn <- Xi -> RewriteM Reduction rewrite_one Xi fun_ty ; rewrite_app_ty_args redn arg_tys } -- Given a rewritten function (with the coercion produced by rewriting) and -- a bunch of unrewritten arguments, rewrite the arguments and apply. -- The coercion argument's role matches the role stored in the RewriteM monad. -- -- The bang patterns used here were observed to improve performance. If you -- wish to remove them, be sure to check for regressions in allocations. rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction rewrite_app_ty_args :: Reduction -> [Xi] -> RewriteM Reduction rewrite_app_ty_args Reduction redn [] -- this will be a common case when called from rewrite_fam_app, so shortcut = Reduction -> RewriteM Reduction forall a. a -> RewriteM a forall (m :: * -> *) a. Monad m => a -> m a return Reduction redn rewrite_app_ty_args fun_redn :: Reduction fun_redn@(Reduction Coercion fun_co Xi fun_xi) [Xi] arg_tys = do { het_redn <- case HasDebugCallStack => Xi -> Maybe (TyCon, [Xi]) Xi -> Maybe (TyCon, [Xi]) tcSplitTyConApp_maybe Xi fun_xi of Just (TyCon tc, [Xi] xis) -> do { let tc_roles :: Infinite Role tc_roles = TyCon -> Infinite Role tyConRolesRepresentational TyCon tc arg_roles :: Infinite Role arg_roles = [Xi] -> Infinite Role -> Infinite Role forall a b. [a] -> Infinite b -> Infinite b Inf.dropList [Xi] xis Infinite Role tc_roles ; ArgsReductions (Reductions arg_cos arg_xis) kind_co <- Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions rewrite_vector (HasDebugCallStack => Xi -> Xi Xi -> Xi typeKind Xi fun_xi) Infinite Role arg_roles [Xi] arg_tys -- We start with a reduction of the form -- fun_co :: ty ~ T xi_1 ... xi_n -- and further arguments a_1, ..., a_m. -- We rewrite these arguments, and obtain coercions: -- arg_co_i :: a_i ~ zeta_i -- Now, we need to apply fun_co to the arg_cos. The problem is -- that using mkAppCo is wrong because that function expects -- its second coercion to be Nominal, and the arg_cos might -- not be. The solution is to use transitivity: -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m ; eq_rel <- getEqRel ; let app_xi = TyCon -> [Xi] -> Xi mkTyConApp TyCon tc ([Xi] xis [Xi] -> [Xi] -> [Xi] forall a. [a] -> [a] -> [a] ++ [Xi] arg_xis) app_co = case EqRel eq_rel of EqRel NomEq -> Coercion -> [Coercion] -> Coercion mkAppCos Coercion fun_co [Coercion] arg_cos EqRel ReprEq -> Coercion -> [Coercion] -> Coercion mkAppCos Coercion fun_co ((Xi -> Coercion) -> [Xi] -> [Coercion] forall a b. (a -> b) -> [a] -> [b] map Xi -> Coercion mkNomReflCo [Xi] arg_tys) Coercion -> Coercion -> Coercion `mkTransCo` HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role Representational TyCon tc ((Role -> Xi -> Coercion) -> [Role] -> [Xi] -> [Coercion] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Role -> Xi -> Coercion mkReflCo (Infinite Role -> [Role] forall a. Infinite a -> [a] Inf.toList Infinite Role tc_roles) [Xi] xis [Coercion] -> [Coercion] -> [Coercion] forall a. [a] -> [a] -> [a] ++ [Coercion] arg_cos) ; return $ mkHetReduction (mkReduction app_co app_xi ) kind_co } Maybe (TyCon, [Xi]) Nothing -> do { ArgsReductions redns kind_co <- Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions rewrite_vector (HasDebugCallStack => Xi -> Xi Xi -> Xi typeKind Xi fun_xi) (Role -> Infinite Role forall a. a -> Infinite a Inf.repeat Role Nominal) [Xi] arg_tys ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co } ; role <- getRole ; return (homogeniseHetRedn role het_redn) } rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction rewrite_ty_con_app :: TyCon -> [Xi] -> RewriteM Reduction rewrite_ty_con_app TyCon tc [Xi] tys = do { role <- RewriteM Role getRole ; let m_roles | Role Nominal <- Role role = Maybe (Infinite Role) forall a. Maybe a Nothing | Bool otherwise = Infinite Role -> Maybe (Infinite Role) forall a. a -> Maybe a Just (Infinite Role -> Maybe (Infinite Role)) -> Infinite Role -> Maybe (Infinite Role) forall a b. (a -> b) -> a -> b $ Role -> TyCon -> Infinite Role tyConRolesX Role role TyCon tc ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys ; let tyconapp_redn = Reduction -> MCoercionN -> HetReduction mkHetReduction (Role -> TyCon -> Reductions -> Reduction mkTyConAppRedn Role role TyCon tc Reductions redns) MCoercionN kind_co ; return $ homogeniseHetRedn role tyconapp_redn } -- Rewrite a vector (list of arguments). rewrite_vector :: Kind -- of the function being applied to these arguments -> Infinite Role -- If we're rewriting w.r.t. ReprEq, what roles do the -- args have? -> [Type] -- the args to rewrite -> RewriteM ArgsReductions rewrite_vector :: Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions rewrite_vector Xi ki Infinite Role roles [Xi] tys = do { eq_rel <- RewriteM EqRel getEqRel ; let mb_roles = case EqRel eq_rel of { EqRel NomEq -> Maybe (Infinite Role) forall a. Maybe a Nothing; EqRel ReprEq -> Infinite Role -> Maybe (Infinite Role) forall a. a -> Maybe a Just Infinite Role roles } ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys } where ([PiTyBinder] bndrs, Xi inner_ki, Bool any_named_bndrs) = Xi -> ([PiTyBinder], Xi, Bool) split_pi_tys' Xi ki fvs :: TcTyCoVarSet fvs = Xi -> TcTyCoVarSet tyCoVarsOfType Xi ki {-# INLINE rewrite_vector #-} {- Note [Do not rewrite newtypes] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We flirted with unwrapping newtypes in the rewriter -- see GHC.Tc.Solver.Equality Note [Unwrap newtypes first]. But that turned out to be a bad idea because of recursive newtypes, as that Note says. So be careful if you re-add it! Note [Rewriting synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Not expanding synonyms aggressively improves error messages, and keeps types smaller. But we need to take care. Suppose type Syn a = Int type instance F Bool = Syn (F Bool) [G] F Bool ~ Syn (F Bool) If we don't expand the synonym, we'll get a spurious occurs-check failure. This is normally what occCheckExpand takes care of, but the LHS is a type family application, and occCheckExpand (already complex enough as it is) does not know how to expand to avoid a type family application. In addition, expanding the forgetful synonym like this will generally yield a *smaller* type. To wit, if we spot S ( ... F tys ... ), where S is forgetful, we don't want to bother doing hard work simplifying (F tys). We thus expand forgetful synonyms, but not others. isForgetfulSynTyCon returns True more often than it needs to, so we err on the side of more expansion. We also, of course, must expand type synonyms that mention type families, so those families can get reduced. ************************************************************************ * * Rewriting a type-family application * * ************************************************************************ Note [How to normalise a family application] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given an exactly saturated family application, how should we normalise it? This Note spells out the algorithm and its reasoning. First, we attempt to directly rewrite the type family application, without simplifying any of the arguments first, in an attempt to avoid doing unnecessary work. STEP 1a. Call the rewriting plugins. If any plugin rewrites the type family application, jump to FINISH. STEP 1b. Try the famapp-cache. If we get a cache hit, jump to FINISH. STEP 1c. Try top-level instances. Remember: we haven't simplified the arguments yet. Example: type instance F (Maybe a) = Int target: F (Maybe (G Bool)) Instead of first trying to simplify (G Bool), we use the instance first. This avoids the work of simplifying G Bool. If an instance is found, jump to FINISH. STEP 2: At this point we rewrite all arguments. This might expose more information, which might allow plugins to make progress, or allow us to pick up a top-level instance. STEP 3. Try the inerts. Note that we try the inerts *after* rewriting the arguments, because the inerts will have rewritten LHSs. If an inert is found, jump to FINISH. Next, we try STEP 1 again, as we might be able to make further progress after having rewritten the arguments: STEP 4a. Query the rewriting plugins again. If any plugin supplies a rewriting, jump to FINISH. STEP 4b. Try the famapp-cache again. If we get a cache hit, jump to FINISH. STEP 4c. Try top-level instances again. If an instance is found, jump to FINISH. STEP 5: GIVEUP. No progress to be made. Return what we have. (Do not FINISH.) FINISH 1. We've made a reduction, but the new type may still have more work to do. So rewrite the new type. FINISH 2. Add the result to the famapp-cache, connecting the type we started with to the one we ended with. Because STEP 1{a,b,c} and STEP 4{a,b,c} happen the same way, they are abstracted into try_to_reduce. FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance] tells us that we should not add to the famapp-cache after STEP 1. So `finish` is inlined in that case, and only FINISH 1 is performed. -} rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction -- rewrite_fam_app can be over-saturated -- rewrite_exact_fam_app lifts out the application to top level -- Postcondition: Coercion :: Xi ~ F tys rewrite_fam_app :: TyCon -> [Xi] -> RewriteM Reduction rewrite_fam_app TyCon tc [Xi] tys -- Can be over-saturated = Bool -> SDoc -> RewriteM Reduction -> RewriteM Reduction forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr ([Xi] tys [Xi] -> Arity -> Bool forall a. [a] -> Arity -> Bool `lengthAtLeast` TyCon -> Arity tyConArity TyCon tc) (TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tc SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Arity -> SDoc forall a. Outputable a => a -> SDoc ppr (TyCon -> Arity tyConArity TyCon tc) SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ [Xi] -> SDoc forall a. Outputable a => a -> SDoc ppr [Xi] tys) (RewriteM Reduction -> RewriteM Reduction) -> RewriteM Reduction -> RewriteM Reduction forall a b. (a -> b) -> a -> b $ -- Type functions are saturated -- The type function might be *over* saturated -- in which case the remaining arguments should -- be dealt with by AppTys do { let ([Xi] tys1, [Xi] tys_rest) = Arity -> [Xi] -> ([Xi], [Xi]) forall a. Arity -> [a] -> ([a], [a]) splitAt (TyCon -> Arity tyConArity TyCon tc) [Xi] tys ; redn <- TyCon -> [Xi] -> RewriteM Reduction rewrite_exact_fam_app TyCon tc [Xi] tys1 ; rewrite_app_ty_args redn tys_rest } -- the [TcType] exactly saturate the TyCon -- See Note [How to normalise a family application] rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction rewrite_exact_fam_app :: TyCon -> [Xi] -> RewriteM Reduction rewrite_exact_fam_app TyCon tc [Xi] tys = do { Xi -> RewriteM () checkStackDepth (TyCon -> [Xi] -> Xi mkTyConApp TyCon tc [Xi] tys) -- Query the typechecking plugins for all their rewriting functions -- which apply to a type family application headed by the TyCon 'tc'. ; tc_rewriters <- TyCon -> RewriteM [TcPluginRewriter] getTcPluginRewritersForTyCon TyCon tc -- STEP 1. Try to reduce without reducing arguments first. ; result1 <- try_to_reduce tc tys tc_rewriters ; case result1 of -- Don't use the cache; -- See Note [rewrite_exact_fam_app performance] { Just Reduction redn -> Bool -> Reduction -> RewriteM Reduction finish Bool False Reduction redn ; Maybe Reduction Nothing -> -- That didn't work. So reduce the arguments, in STEP 2. do { eq_rel <- RewriteM EqRel getEqRel -- checking eq_rel == NomEq saves ~0.5% in T9872a ; ArgsReductions (Reductions cos xis) kind_co <- if eq_rel == NomEq then rewrite_args_tc tc Nothing tys else setEqRel NomEq $ rewrite_args_tc tc Nothing tys -- If we manage to rewrite the type family application after -- rewriting the arguments, we will need to compose these -- reductions. -- -- We have: -- -- arg_co_i :: ty_i ~ xi_i -- fam_co :: F xi_1 ... xi_n ~ zeta -- -- The full reduction is obtained as a composite: -- -- full_co :: F ty_1 ... ty_n ~ zeta -- full_co = F co_1 ... co_n ;; fam_co ; let role = EqRel -> Role eqRelRole EqRel eq_rel args_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role role TyCon tc [Coercion] cos ; let homogenise :: Reduction -> Reduction homogenise Reduction redn = Role -> HetReduction -> Reduction homogeniseHetRedn Role role (HetReduction -> Reduction) -> HetReduction -> Reduction forall a b. (a -> b) -> a -> b $ Reduction -> MCoercionN -> HetReduction mkHetReduction (Coercion args_co Coercion -> Reduction -> Reduction `mkTransRedn` Reduction redn) MCoercionN kind_co give_up :: Reduction give_up = Reduction -> Reduction homogenise (Reduction -> Reduction) -> Reduction -> Reduction forall a b. (a -> b) -> a -> b $ Role -> Xi -> Reduction mkReflRedn Role role Xi reduced where reduced :: Xi reduced = TyCon -> [Xi] -> Xi mkTyConApp TyCon tc [Xi] xis -- STEP 3: try the inerts ; flavour <- getFlavour ; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis ; case result2 of { Just (Reduction redn, (CtFlavour inert_flavour, EqRel inert_eq_rel)) -> do { String -> SDoc -> RewriteM () traceRewriteM String "rewrite family application with inert" (TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tc SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [Xi] -> SDoc forall a. Outputable a => a -> SDoc ppr [Xi] xis SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Reduction -> SDoc forall a. Outputable a => a -> SDoc ppr Reduction redn) ; Bool -> Reduction -> RewriteM Reduction finish (CtFlavour inert_flavour CtFlavour -> CtFlavour -> Bool forall a. Eq a => a -> a -> Bool == CtFlavour Given) (Reduction -> Reduction homogenise Reduction downgraded_redn) } -- this will sometimes duplicate an inert in the cache, -- but avoiding doing so had no impact on performance, and -- it seems easier not to weed out that special case where inert_role :: Role inert_role = EqRel -> Role eqRelRole EqRel inert_eq_rel role :: Role role = EqRel -> Role eqRelRole EqRel eq_rel downgraded_redn :: Reduction downgraded_redn = Role -> Role -> Reduction -> Reduction downgradeRedn Role role Role inert_role Reduction redn ; Maybe (Reduction, CtFlavourRole) _ -> -- inerts didn't work. Try to reduce again, in STEP 4. do { result3 <- TyCon -> [Xi] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction) try_to_reduce TyCon tc [Xi] xis [TcPluginRewriter] tc_rewriters ; case result3 of Just Reduction redn -> Bool -> Reduction -> RewriteM Reduction finish Bool True (Reduction -> Reduction homogenise Reduction redn) -- we have made no progress at all: STEP 5 (GIVEUP). Maybe Reduction _ -> Reduction -> RewriteM Reduction forall a. a -> RewriteM a forall (m :: * -> *) a. Monad m => a -> m a return Reduction give_up }}}}} where -- call this if the above attempts made progress. -- This recursively rewrites the result and then adds to the cache finish :: Bool -- add to the cache? -- Precondition: True ==> input coercion has -- no coercion holes -> Reduction -> RewriteM Reduction finish :: Bool -> Reduction -> RewriteM Reduction finish Bool use_cache Reduction redn = do { -- rewrite the result: FINISH 1 final_redn <- Reduction -> RewriteM Reduction rewrite_reduction Reduction redn ; eq_rel <- getEqRel -- extend the cache: FINISH 2 ; when (use_cache && eq_rel == NomEq) $ -- the cache only wants Nominal eqs liftTcS $ extendFamAppCache tc tys final_redn ; return final_redn } {-# INLINE finish #-} -- Returned coercion is input ~r output, where r is the role in the RewriteM monad -- See Note [How to normalise a family application] try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction) try_to_reduce :: TyCon -> [Xi] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction) try_to_reduce TyCon tc [Xi] tys [TcPluginRewriter] tc_rewriters = do { rewrite_env <- RewriteM RewriteEnv getRewriteEnv ; result <- liftTcS $ firstJustsM [ runTcPluginRewriters rewrite_env tc_rewriters tys -- STEP 1a & STEP 4a , lookupFamAppCache tc tys -- STEP 1b & STEP 4b , matchFam tc tys ] -- STEP 1c & STEP 4c ; traverse downgrade result } where -- The result above is always Nominal. We might want a Representational -- coercion; this downgrades (and prints, out of convenience). downgrade :: Reduction -> RewriteM Reduction downgrade :: Reduction -> RewriteM Reduction downgrade Reduction redn = do { String -> SDoc -> RewriteM () traceRewriteM String "Eager T.F. reduction success" (SDoc -> RewriteM ()) -> SDoc -> RewriteM () forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tc , [Xi] -> SDoc forall a. Outputable a => a -> SDoc ppr [Xi] tys , Reduction -> SDoc forall a. Outputable a => a -> SDoc ppr Reduction redn ] ; eq_rel <- RewriteM EqRel getEqRel -- manually doing it this way avoids allocation in the vastly -- common NomEq case ; case eq_rel of EqRel NomEq -> Reduction -> RewriteM Reduction forall a. a -> RewriteM a forall (m :: * -> *) a. Monad m => a -> m a return Reduction redn EqRel ReprEq -> Reduction -> RewriteM Reduction forall a. a -> RewriteM a forall (m :: * -> *) a. Monad m => a -> m a return (Reduction -> RewriteM Reduction) -> Reduction -> RewriteM Reduction forall a b. (a -> b) -> a -> b $ Reduction -> Reduction mkSubRedn Reduction redn } -- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application -- headed by the given 'TyCon`. getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter] getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter] getTcPluginRewritersForTyCon TyCon tc = TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter] forall a. TcS a -> RewriteM a liftTcS (TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]) -> TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter] forall a b. (a -> b) -> a -> b $ do { rewriters <- TcGblEnv -> UniqFM TyCon [TcPluginRewriter] tcg_tc_plugin_rewriters (TcGblEnv -> UniqFM TyCon [TcPluginRewriter]) -> TcS TcGblEnv -> TcS (UniqFM TyCon [TcPluginRewriter]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> TcS TcGblEnv getGblEnv ; return (lookupWithDefaultUFM rewriters [] tc) } -- Run a collection of rewriting functions obtained from type-checking plugins, -- querying in sequence if any plugin wants to rewrite the type family -- applied to the given arguments. -- -- Note that the 'TcPluginRewriter's provided all pertain to the same type family -- (the 'TyCon' of which has been obtained ahead of calling this function). runTcPluginRewriters :: RewriteEnv -> [TcPluginRewriter] -> [TcType] -> TcS (Maybe Reduction) runTcPluginRewriters :: RewriteEnv -> [TcPluginRewriter] -> [Xi] -> TcS (Maybe Reduction) runTcPluginRewriters RewriteEnv rewriteEnv [TcPluginRewriter] rewriterFunctions [Xi] tys | [TcPluginRewriter] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [TcPluginRewriter] rewriterFunctions = Maybe Reduction -> TcS (Maybe Reduction) forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return Maybe Reduction forall a. Maybe a Nothing -- short-circuit for common case | Bool otherwise = do { givens <- TcS [Ct] getInertGivens ; runRewriters givens rewriterFunctions } where runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction) runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction) runRewriters [Ct] _ [] = Maybe Reduction -> TcS (Maybe Reduction) forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return Maybe Reduction forall a. Maybe a Nothing runRewriters [Ct] givens (TcPluginRewriter rewriter:[TcPluginRewriter] rewriters) = do rewriteResult <- TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult forall a. TcM a -> TcS a wrapTcS (TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult) -> (TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult) -> TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult forall b c a. (b -> c) -> (a -> b) -> a -> c . TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult forall a. TcPluginM a -> TcM a runTcPluginM (TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult) -> TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult forall a b. (a -> b) -> a -> b $ TcPluginRewriter rewriter RewriteEnv rewriteEnv [Ct] givens [Xi] tys case rewriteResult of TcPluginRewriteTo { tcPluginReduction :: TcPluginRewriteResult -> Reduction tcPluginReduction = Reduction redn , tcRewriterNewWanteds :: TcPluginRewriteResult -> [Ct] tcRewriterNewWanteds = [Ct] wanteds } -> do { Cts -> TcS () emitWork ([Ct] -> Cts forall a. [a] -> Bag a listToBag [Ct] wanteds); Maybe Reduction -> TcS (Maybe Reduction) forall a. a -> TcS a forall (m :: * -> *) a. Monad m => a -> m a return (Maybe Reduction -> TcS (Maybe Reduction)) -> Maybe Reduction -> TcS (Maybe Reduction) forall a b. (a -> b) -> a -> b $ Reduction -> Maybe Reduction forall a. a -> Maybe a Just Reduction redn } TcPluginNoRewrite {} -> [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction) runRewriters [Ct] givens [TcPluginRewriter] rewriters {- ************************************************************************ * * Rewriting a type variable * * ********************************************************************* -} -- | The result of rewriting a tyvar "one step". data RewriteTvResult = RTRNotFollowed -- ^ The inert set doesn't make the tyvar equal to anything else | RTRFollowed !Reduction -- ^ The tyvar rewrites to a not-necessarily rewritten other type. -- The role is determined by the RewriteEnv. -- -- With Quick Look, the returned TcType can be a polytype; -- that is, in the constraint solver, a unification variable -- can contain a polytype. See GHC.Tc.Gen.App -- Note [Instantiation variables are short lived] rewriteTyVar :: TyVar -> RewriteM Reduction rewriteTyVar :: TcTyVar -> RewriteM Reduction rewriteTyVar TcTyVar tv = do { mb_yes <- TcTyVar -> RewriteM RewriteTvResult rewrite_tyvar1 TcTyVar tv ; case mb_yes of RTRFollowed Reduction redn -> Reduction -> RewriteM Reduction rewrite_reduction Reduction redn RewriteTvResult RTRNotFollowed -- Done, but make sure the kind is zonked -- Note [Rewriting] invariant (F0) and (F1) -> do { tv' <- TcS TcTyVar -> RewriteM TcTyVar forall a. TcS a -> RewriteM a liftTcS (TcS TcTyVar -> RewriteM TcTyVar) -> TcS TcTyVar -> RewriteM TcTyVar forall a b. (a -> b) -> a -> b $ (Xi -> TcS Xi) -> TcTyVar -> TcS TcTyVar forall (m :: * -> *). Monad m => (Xi -> m Xi) -> TcTyVar -> m TcTyVar updateTyVarKindM Xi -> TcS Xi zonkTcType TcTyVar tv ; role <- getRole ; let ty' = TcTyVar -> Xi mkTyVarTy TcTyVar tv' ; return $ mkReflRedn role ty' } } rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult -- "Rewriting" a type variable means to apply the substitution to it -- Specifically, look up the tyvar in -- * the internal MetaTyVar box -- * the inerts -- See also the documentation for RewriteTvResult rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult rewrite_tyvar1 TcTyVar tv = do { mb_ty <- TcS (Maybe Xi) -> RewriteM (Maybe Xi) forall a. TcS a -> RewriteM a liftTcS (TcS (Maybe Xi) -> RewriteM (Maybe Xi)) -> TcS (Maybe Xi) -> RewriteM (Maybe Xi) forall a b. (a -> b) -> a -> b $ TcTyVar -> TcS (Maybe Xi) isFilledMetaTyVar_maybe TcTyVar tv ; case mb_ty of Just Xi ty -> do { String -> SDoc -> RewriteM () traceRewriteM String "Following filled tyvar" (TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> SDoc forall doc. IsLine doc => doc equals SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Xi -> SDoc forall a. Outputable a => a -> SDoc ppr Xi ty) ; role <- RewriteM Role getRole ; return $ RTRFollowed $ mkReflRedn role ty } Maybe Xi Nothing -> do { String -> SDoc -> RewriteM () traceRewriteM String "Unfilled tyvar" (TcTyVar -> SDoc pprTyVar TcTyVar tv) ; fr <- RewriteM CtFlavourRole getFlavourRole ; rewrite_tyvar2 tv fr } } rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult -- The tyvar is not a filled-in meta-tyvar -- Try in the inert equalities -- See Definition [Applying a generalised substitution] in GHC.Tc.Solver.Monad -- See Note [Stability of rewriting] in GHC.Tc.Solver.Monad rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult rewrite_tyvar2 TcTyVar tv fr :: CtFlavourRole fr@(CtFlavour _, EqRel eq_rel) = do { ieqs <- TcS InertEqs -> RewriteM InertEqs forall a. TcS a -> RewriteM a liftTcS (TcS InertEqs -> RewriteM InertEqs) -> TcS InertEqs -> RewriteM InertEqs forall a b. (a -> b) -> a -> b $ TcS InertEqs getInertEqs ; case lookupDVarEnv ieqs tv of Just EqualCtList equal_ct_list | Just EqCt ct <- (EqCt -> Bool) -> EqualCtList -> Maybe EqCt forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find EqCt -> Bool can_rewrite EqualCtList equal_ct_list , EqCt { eq_ev :: EqCt -> CtEvidence eq_ev = CtEvidence ctev, eq_lhs :: EqCt -> CanEqLHS eq_lhs = TyVarLHS TcTyVar tv , eq_rhs :: EqCt -> Xi eq_rhs = Xi rhs_ty, eq_eq_rel :: EqCt -> EqRel eq_eq_rel = EqRel ct_eq_rel } <- EqCt ct -> do { let wrw :: Bool wrw = CtEvidence -> Bool isWanted CtEvidence ctev ; String -> SDoc -> RewriteM () traceRewriteM String "Following inert tyvar" (SDoc -> RewriteM ()) -> SDoc -> RewriteM () forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> SDoc forall doc. IsLine doc => doc equals SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Xi -> SDoc forall a. Outputable a => a -> SDoc ppr Xi rhs_ty , CtEvidence -> SDoc forall a. Outputable a => a -> SDoc ppr CtEvidence ctev , String -> SDoc forall doc. IsLine doc => String -> doc text String "wanted_rewrite_wanted:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Bool -> SDoc forall a. Outputable a => a -> SDoc ppr Bool wrw ] ; Bool -> RewriteM () -> RewriteM () forall (f :: * -> *). Applicative f => Bool -> f () -> f () when Bool wrw (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM () forall a b. (a -> b) -> a -> b $ CtEvidence -> RewriteM () recordRewriter CtEvidence ctev ; let rewriting_co1 :: Coercion rewriting_co1 = HasDebugCallStack => CtEvidence -> Coercion CtEvidence -> Coercion ctEvCoercion CtEvidence ctev rewriting_co :: Coercion rewriting_co = case (EqRel ct_eq_rel, EqRel eq_rel) of (EqRel ReprEq, EqRel _rel) -> Bool -> Coercion -> Coercion forall a. HasCallStack => Bool -> a -> a assert (EqRel _rel EqRel -> EqRel -> Bool forall a. Eq a => a -> a -> Bool == EqRel ReprEq) -- if this assert fails, then -- eqCanRewriteFR answered incorrectly Coercion rewriting_co1 (EqRel NomEq, EqRel NomEq) -> Coercion rewriting_co1 (EqRel NomEq, EqRel ReprEq) -> HasDebugCallStack => Coercion -> Coercion Coercion -> Coercion mkSubCo Coercion rewriting_co1 ; RewriteTvResult -> RewriteM RewriteTvResult forall a. a -> RewriteM a forall (m :: * -> *) a. Monad m => a -> m a return (RewriteTvResult -> RewriteM RewriteTvResult) -> RewriteTvResult -> RewriteM RewriteTvResult forall a b. (a -> b) -> a -> b $ Reduction -> RewriteTvResult RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult forall a b. (a -> b) -> a -> b $ Coercion -> Xi -> Reduction mkReduction Coercion rewriting_co Xi rhs_ty } Maybe EqualCtList _other -> RewriteTvResult -> RewriteM RewriteTvResult forall a. a -> RewriteM a forall (m :: * -> *) a. Monad m => a -> m a return RewriteTvResult RTRNotFollowed } where can_rewrite :: EqCt -> Bool can_rewrite :: EqCt -> Bool can_rewrite EqCt ct = EqCt -> CtFlavourRole eqCtFlavourRole EqCt ct CtFlavourRole -> CtFlavourRole -> Bool `eqCanRewriteFR` CtFlavourRole fr -- This is THE key call of eqCanRewriteFR {- Note [An alternative story for the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (This entire note is just background, left here in case we ever want to return the previous state of affairs) We used (GHC 7.8) to have this story for the inert substitution inert_eqs * 'a' is not in fvs(ty) * They are *inert* in the weaker sense that there is no infinite chain of (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc This means that rewriting must be recursive, but it does allow [G] a ~ [b] [G] b ~ Maybe c This avoids "saturating" the Givens, which can save a modest amount of work. It is easy to implement, in GHC.Tc.Solver.InertSet.kickOutRewritableLHS, by only kicking out an inert only if (a) the work item can rewrite the inert AND (b) the inert cannot rewrite the work item This is significantly harder to think about. It can save a LOT of work in occurs-check cases, but we don't care about them much. #5837 is an example, but it causes trouble only with the old (pre-Fall 2020) rewriting story. It is unclear if there is any gain w.r.t. to the new story. -} -------------------------------------- -- Utilities -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at -- least one named binder. split_pi_tys' :: Type -> ([PiTyBinder], Type, Bool) split_pi_tys' :: Xi -> ([PiTyBinder], Xi, Bool) split_pi_tys' Xi ty = Xi -> Xi -> ([PiTyBinder], Xi, Bool) split Xi ty Xi ty where -- put common cases first split :: Xi -> Xi -> ([PiTyBinder], Xi, Bool) split Xi _ (ForAllTy TyVarBinder b Xi res) = let -- This bang is necessary lest we see rather -- terrible reboxing, as noted in #19102. !([PiTyBinder] bs, Xi ty, Bool _) = Xi -> Xi -> ([PiTyBinder], Xi, Bool) split Xi res Xi res in (TyVarBinder -> PiTyBinder Named TyVarBinder b PiTyBinder -> [PiTyBinder] -> [PiTyBinder] forall a. a -> [a] -> [a] : [PiTyBinder] bs, Xi ty, Bool True) split Xi _ (FunTy { ft_af :: Xi -> FunTyFlag ft_af = FunTyFlag af, ft_mult :: Xi -> Xi ft_mult = Xi w, ft_arg :: Xi -> Xi ft_arg = Xi arg, ft_res :: Xi -> Xi ft_res = Xi res }) = let -- See #19102 !([PiTyBinder] bs, Xi ty, Bool named) = Xi -> Xi -> ([PiTyBinder], Xi, Bool) split Xi res Xi res in (Scaled Xi -> FunTyFlag -> PiTyBinder Anon (Xi -> Xi -> Scaled Xi forall a. Xi -> a -> Scaled a mkScaled Xi w Xi arg) FunTyFlag af PiTyBinder -> [PiTyBinder] -> [PiTyBinder] forall a. a -> [a] -> [a] : [PiTyBinder] bs, Xi ty, Bool named) split Xi orig_ty Xi ty | Just Xi ty' <- Xi -> Maybe Xi coreView Xi ty = Xi -> Xi -> ([PiTyBinder], Xi, Bool) split Xi orig_ty Xi ty' split Xi orig_ty Xi _ = ([], Xi orig_ty, Bool False) {-# INLINE split_pi_tys' #-} -- | Like 'tyConBindersPiTyBinders' but you also get a 'Bool' which is true iff -- there is at least one named binder. ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool) ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool) ty_con_binders_ty_binders' = (TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool)) -> ([PiTyBinder], Bool) -> [TyConBinder] -> ([PiTyBinder], Bool) forall a b. (a -> b -> b) -> b -> [a] -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool) go ([], Bool False) where go :: TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool) go (Bndr TcTyVar tv (NamedTCB ForAllTyFlag vis)) ([PiTyBinder] bndrs, Bool _) = (TyVarBinder -> PiTyBinder Named (TcTyVar -> ForAllTyFlag -> TyVarBinder forall var argf. var -> argf -> VarBndr var argf Bndr TcTyVar tv ForAllTyFlag vis) PiTyBinder -> [PiTyBinder] -> [PiTyBinder] forall a. a -> [a] -> [a] : [PiTyBinder] bndrs, Bool True) go (Bndr TcTyVar tv TyConBndrVis AnonTCB) ([PiTyBinder] bndrs, Bool n) = (Scaled Xi -> FunTyFlag -> PiTyBinder Anon (Xi -> Scaled Xi forall a. a -> Scaled a tymult (TcTyVar -> Xi tyVarKind TcTyVar tv)) FunTyFlag FTF_T_T PiTyBinder -> [PiTyBinder] -> [PiTyBinder] forall a. a -> [a] -> [a] : [PiTyBinder] bndrs, Bool n) {-# INLINE go #-} {-# INLINE ty_con_binders_ty_binders' #-}