diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Rewrite.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 195 |
1 files changed, 77 insertions, 118 deletions
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index b7573e7f09..6e8baf15a6 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -5,7 +5,7 @@ {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} module GHC.Tc.Solver.Rewrite( - rewrite, rewriteKind, rewriteArgsNom, + rewrite, rewriteArgsNom, rewriteType ) where @@ -34,15 +34,14 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Tc.Solver.Monad as TcS -import GHC.Tc.Solver.Types + import GHC.Utils.Misc import GHC.Data.Maybe import GHC.Exts (oneShot) import Control.Monad -import GHC.Utils.Monad ( zipWith3M ) -import Data.List.NonEmpty ( NonEmpty(..) ) import Control.Applicative (liftA3) import GHC.Builtin.Types.Prim (tYPETyCon) +import Data.List ( find ) {- ************************************************************************ @@ -82,18 +81,23 @@ liftTcS thing_inside -- convenient wrapper when you have a CtEvidence describing -- the rewriting operation -runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS a +runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet) runRewriteCtEv ev = runRewrite (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev) -- Run thing_inside (which does the rewriting) -runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a +-- 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 loc flav eq_rel thing_inside - = runRewriteM thing_inside fmode - where - fmode = FE { fe_loc = loc - , fe_flavour = flav - , fe_eq_rel = eq_rel } + = do { rewriters_ref <- newTcRef emptyRewriterSet + ; let fmode = RE { re_loc = loc + , re_flavour = flav + , re_eq_rel = eq_rel + , re_rewriters = rewriters_ref } + ; res <- runRewriteM thing_inside fmode + ; rewriters <- readTcRef rewriters_ref + ; return (res, rewriters) } traceRewriteM :: String -> SDoc -> RewriteM () traceRewriteM herald doc = liftTcS $ traceTcS herald doc @@ -108,13 +112,13 @@ getRewriteEnvField accessor = mkRewriteM $ \env -> return (accessor env) getEqRel :: RewriteM EqRel -getEqRel = getRewriteEnvField fe_eq_rel +getEqRel = getRewriteEnvField re_eq_rel getRole :: RewriteM Role getRole = eqRelRole <$> getEqRel getFlavour :: RewriteM CtFlavour -getFlavour = getRewriteEnvField fe_flavour +getFlavour = getRewriteEnvField re_flavour getFlavourRole :: RewriteM CtFlavourRole getFlavourRole @@ -123,7 +127,7 @@ getFlavourRole ; return (flavour, eq_rel) } getLoc :: RewriteM CtLoc -getLoc = getRewriteEnvField fe_loc +getLoc = getRewriteEnvField re_loc checkStackDepth :: Type -> RewriteM () checkStackDepth ty @@ -134,38 +138,32 @@ checkStackDepth ty setEqRel :: EqRel -> RewriteM a -> RewriteM a setEqRel new_eq_rel thing_inside = mkRewriteM $ \env -> - if new_eq_rel == fe_eq_rel env + if new_eq_rel == re_eq_rel env then runRewriteM thing_inside env - else runRewriteM thing_inside (env { fe_eq_rel = new_eq_rel }) + else runRewriteM thing_inside (env { re_eq_rel = new_eq_rel }) {-# INLINE setEqRel #-} --- | Make sure that rewriting actually produces a coercion (in other --- words, make sure our flavour is not Derived) --- Note [No derived kind equalities] -noBogusCoercions :: RewriteM a -> RewriteM a -noBogusCoercions thing_inside - = mkRewriteM $ \env -> - -- No new thunk is made if the flavour hasn't changed (note the bang). - let !env' = case fe_flavour env of - Derived -> env { fe_flavour = Wanted WDeriv } - _ -> env - in - runRewriteM thing_inside env' - bumpDepth :: RewriteM a -> RewriteM a bumpDepth (RewriteM thing_inside) = mkRewriteM $ \env -> do -- bumpDepth can be called a lot during rewriting so we force the -- new env to avoid accumulating thunks. - { let !env' = env { fe_loc = bumpCtLocDepth (fe_loc env) } + { let !env' = env { re_loc = bumpCtLocDepth (re_loc env) } ; thing_inside env' } +-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint +-- Precondition: the CtEvidence is a CtWanted of an equality +recordRewriter :: CtEvidence -> RewriteM () +recordRewriter (CtWanted { ctev_dest = HoleDest hole }) + = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriterSet` hole) +recordRewriter other = pprPanic "recordRewriter" (ppr other) + {- Note [Rewriter EqRels] ~~~~~~~~~~~~~~~~~~~~~~~ When rewriting, we need to know which equality relation -- nominal or representation -- we should be respecting. The only difference is -that we rewrite variables by representational equalities when fe_eq_rel +that we rewrite variables by representational equalities when re_eq_rel is ReprEq, and that we unwrap newtypes when rewriting w.r.t. representational equality. @@ -203,14 +201,6 @@ 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.) -Note [No derived kind equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A kind-level coercion can appear in types, via mkCastTy. So, whenever -we are generating a coercion in a dependent context (in other words, -in a kind) we need to make sure that our flavour is never Derived -(as Derived constraints have no evidence). The noBogusCoercions function -changes the flavour from Derived just for this purpose. - -} {- ********************************************************************* @@ -221,32 +211,21 @@ changes the flavour from Derived just for this purpose. -} -- | See Note [Rewriting]. --- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty +-- 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 + -> TcS (Reduction, RewriterSet) rewrite ev ty = do { traceTcS "rewrite {" (ppr ty) - ; redn <- runRewriteCtEv ev (rewrite_one ty) + ; result@(redn, _) <- runRewriteCtEv ev (rewrite_one ty) ; traceTcS "rewrite }" (ppr $ reductionReducedType redn) - ; return redn } - --- specialized to rewriting kinds: never Derived, always Nominal --- See Note [No derived kind equalities] --- See Note [Rewriting] -rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS ReductionN -rewriteKind loc flav ty - = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty) - ; let flav' = case flav of - Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not - _ -> flav - ; redn <- runRewrite loc flav' NomEq (rewrite_one ty) - ; traceTcS "rewriteKind }" (ppr redn) -- the coercion inside the reduction is never a panic - ; return redn } + ; return result } -- See Note [Rewriting] rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] - -> TcS Reductions + -> 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 @@ -255,15 +234,15 @@ rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -- 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) -- --- For Derived constraints the returned coercion may be undefined --- because rewriting may use a Derived equality ([D] a ~ ty) +-- Final return value returned which Wanteds rewrote another Wanted +-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint rewriteArgsNom ev tc tys = do { traceTcS "rewrite_args {" (vcat (map ppr tys)) - ; ArgsReductions redns@(Reductions _ tys') kind_co + ; (ArgsReductions redns@(Reductions _ tys') kind_co, rewriters) <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys) ; massert (isReflMCo kind_co) ; traceTcS "rewrite }" (vcat (map ppr tys')) - ; return redns } + ; 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 @@ -271,10 +250,10 @@ rewriteArgsNom ev tc tys -- only givens. rewriteType :: CtLoc -> TcType -> TcS TcType rewriteType loc ty - = do { redn <- runRewrite loc Given NomEq $ - rewrite_one ty + = do { (redn, _) <- runRewrite loc Given NomEq $ + rewrite_one ty -- use Given flavor so that it is rewritten - -- only w.r.t. Givens, never Wanteds/Deriveds + -- only w.r.t. Givens, never Wanteds -- (Shouldn't matter, if only Givens are present -- anyway) ; return $ reductionReducedType redn } @@ -462,38 +441,20 @@ rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet -> [Role] -> [Type] -> RewriteM ArgsReductions rewrite_args_slow binders inner_ki fvs roles tys --- Arguments used dependently must be rewritten with proper coercions, but --- we're not guaranteed to get a proper coercion when rewriting with the --- "Derived" flavour. So we must call noBogusCoercions when rewriting arguments --- corresponding to binders that are dependent. However, we might legitimately --- have *more* arguments than binders, in the case that the inner_ki is a variable --- that gets instantiated with a Π-type. We conservatively choose not to produce --- bogus coercions for these, too. Note that this might miss an opportunity for --- a Derived rewriting a Derived. The solution would be to generate evidence for --- Deriveds, thus avoiding this whole noBogusCoercions idea. See also --- Note [No derived kind equalities] - = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True) - roles tys - ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } + = do { rewritten_args <- zipWithM rw roles tys + ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) } where {-# INLINE rw #-} - rw :: Bool -- must we ensure to produce a real coercion here? - -- see comment at top of function - -> Role -> Type -> RewriteM Reduction - rw True r ty = noBogusCoercions $ rw1 r ty - rw False r ty = rw1 r ty - - {-# INLINE rw1 #-} - rw1 :: Role -> Type -> RewriteM Reduction - rw1 Nominal ty + rw :: Role -> Type -> RewriteM Reduction + rw Nominal ty = setEqRel NomEq $ rewrite_one ty - rw1 Representational ty + rw Representational ty = setEqRel ReprEq $ rewrite_one ty - rw1 Phantom ty + rw Phantom ty -- See Note [Phantoms in the rewriter] = do { ty <- liftTcS $ zonkTcType ty ; return $ mkReflRedn Phantom ty } @@ -859,17 +820,13 @@ rewrite_exact_fam_app tc tys where reduced = mkTyConApp tc xis -- STEP 3: try the inerts - ; result2 <- liftTcS $ lookupFamAppInert tc xis ; flavour <- getFlavour + ; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis ; case result2 of - { Just (redn, fr@(_, inert_eq_rel)) - - | fr `eqCanRewriteFR` (flavour, eq_rel) -> - do { traceRewriteM "rewrite family application with inert" $ - vcat [ ppr tc <+> ppr xis - , ppUnless (flavour == Derived) (ppr redn) ] - -- Deriveds have no evidence, so we can't print the reduction - ; finish True (homogenise downgraded_redn) } + { Just (redn, (inert_flavour, inert_eq_rel)) + -> do { traceRewriteM "rewrite family application with inert" + (ppr tc <+> ppr xis $$ ppr redn) + ; finish (inert_flavour == Given) (homogenise 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 @@ -890,18 +847,17 @@ rewrite_exact_fam_app tc tys -- 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 use_cache redn = do { -- rewrite the result: FINISH 1 final_redn <- rewrite_reduction redn ; eq_rel <- getEqRel - ; flavour <- getFlavour -- extend the cache: FINISH 2 - ; when (use_cache && eq_rel == NomEq && flavour /= Derived) $ + ; when (use_cache && eq_rel == NomEq) $ -- the cache only wants Nominal eqs - -- and Wanteds can rewrite Deriveds; the cache - -- has only Givens liftTcS $ extendFamAppCache tc tys final_redn ; return final_redn } {-# INLINE finish #-} @@ -1034,32 +990,35 @@ rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult rewrite_tyvar2 tv fr@(_, eq_rel) = do { ieqs <- liftTcS $ getInertEqs ; case lookupDVarEnv ieqs tv of - Just (EqualCtList (ct :| _)) -- If the first doesn't work, - -- the subsequent ones won't either - | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv + Just equal_ct_list + | Just ct <- find can_rewrite equal_ct_list + , CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct - , let ct_fr = (ctEvFlavour ctev, ct_eq_rel) - , ct_fr `eqCanRewriteFR` fr -- This is THE key call of eqCanRewriteFR - -> do { traceRewriteM "Following inert tyvar" - (ppr tv <+> - equals <+> - ppr rhs_ty $$ ppr ctev) - ; let rewriting_co1 = ctEvCoercion ctev - rewriting_co = case (ct_eq_rel, eq_rel) of - (ReprEq, _rel) -> assert (_rel == ReprEq ) - -- if this ASSERT fails, then + -> do { let wrw = isWantedCt ct + ; traceRewriteM "Following inert tyvar" $ + vcat [ ppr tv <+> equals <+> ppr rhs_ty + , ppr ctev + , text "wanted_rewrite_wanted:" <+> ppr wrw ] + ; when wrw $ recordRewriter ctev + + ; let rewriting_co1 = ctEvCoercion ctev + rewriting_co = case (ct_eq_rel, eq_rel) of + (ReprEq, _rel) -> assert (_rel == ReprEq) + -- if this assert fails, then -- eqCanRewriteFR answered incorrectly rewriting_co1 (NomEq, NomEq) -> rewriting_co1 (NomEq, ReprEq) -> mkSubCo rewriting_co1 - ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty } - -- NB: ct is Derived then fmode must be also, hence - -- we are not going to touch the returned coercion - -- so ctEvCoercion is fine. + ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty } _other -> return RTRNotFollowed } + where + can_rewrite :: Ct -> Bool + can_rewrite ct = ctFlavourRole ct `eqCanRewriteFR` fr + -- This is THE key call of eqCanRewriteFR + {- Note [An alternative story for the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |