diff options
Diffstat (limited to 'compiler/GHC')
-rw-r--r-- | compiler/GHC/Tc/Module.hs | 19 | ||||
-rw-r--r-- | compiler/GHC/Tc/Plugin.hs | 61 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 27 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 141 | ||||
-rw-r--r-- | compiler/GHC/Tc/Types.hs | 168 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/Monad.hs | 4 | ||||
-rw-r--r-- | compiler/GHC/Types/Unique/FM.hs | 10 |
8 files changed, 297 insertions, 135 deletions
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index e0a4f58d39..bf190f059c 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -3088,19 +3088,24 @@ withTcPlugins hsc_env m = [] -> m -- Common fast case plugins -> do ev_binds_var <- newTcEvBinds - (solvers,stops) <- unzip `fmap` mapM (startPlugin ev_binds_var) plugins - -- This ensures that tcPluginStop is called even if a type + (solvers, rewriters, stops) <- + unzip3 `fmap` mapM (startPlugin ev_binds_var) plugins + let + rewritersUniqFM :: UniqFM TyCon [TcPluginRewriter] + !rewritersUniqFM = sequenceUFMList rewriters + -- The following ensures that tcPluginStop is called even if a type -- error occurs during compilation (Fix of #10078) eitherRes <- tryM $ - updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m - mapM_ (flip runTcPluginM ev_binds_var) stops + updGblEnv (\e -> e { tcg_tc_plugin_solvers = solvers + , tcg_tc_plugin_rewriters = rewritersUniqFM }) m + mapM_ runTcPluginM stops case eitherRes of Left _ -> failM Right res -> return res where - startPlugin ev_binds_var (TcPlugin start solve stop) = - do s <- runTcPluginM start ev_binds_var - return (solve s, stop s) + startPlugin ev_binds_var (TcPlugin start solve rewrite stop) = + do s <- runTcPluginM start + return (solve s ev_binds_var, rewrite s, stop s) getTcPlugins :: HscEnv -> [GHC.Tc.Utils.Monad.TcPlugin] getTcPlugins hsc_env = catMaybes $ mapPlugins hsc_env (\p args -> tcPlugin p args) diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs index 78a0ebd16a..a62ac86734 100644 --- a/compiler/GHC/Tc/Plugin.hs +++ b/compiler/GHC/Tc/Plugin.hs @@ -47,7 +47,6 @@ module GHC.Tc.Plugin ( -- * Manipulating evidence bindings newEvVar, setEvBind, - getEvBindsTcPluginM ) where import GHC.Prelude @@ -62,30 +61,30 @@ import qualified GHC.Unit.Finder as Finder import GHC.Core.FamInstEnv ( FamInstEnv ) import GHC.Tc.Utils.Monad ( TcGblEnv, TcLclEnv, TcPluginM - , unsafeTcPluginTcM, getEvBindsTcPluginM + , unsafeTcPluginTcM , liftIO, traceTc ) import GHC.Tc.Types.Constraint ( Ct, CtLoc, CtEvidence(..), ctLocOrigin ) import GHC.Tc.Utils.TcMType ( TcTyVar, TcType ) import GHC.Tc.Utils.Env ( TcTyThing ) import GHC.Tc.Types.Evidence ( CoercionHole, EvTerm(..) - , EvExpr, EvBind, mkGivenEvBind ) + , EvExpr, EvBindsVar, EvBind, mkGivenEvBind ) import GHC.Types.Var ( EvVar ) -import GHC.Unit.Module -import GHC.Types.Name -import GHC.Types.TyThing +import GHC.Unit.Module ( ModuleName, Module ) +import GHC.Types.Name ( OccName, Name ) +import GHC.Types.TyThing ( TyThing ) import GHC.Core.Reduction ( Reduction ) -import GHC.Core.TyCon -import GHC.Core.DataCon -import GHC.Core.Class -import GHC.Driver.Config.Finder -import GHC.Driver.Env -import GHC.Utils.Outputable -import GHC.Core.Type -import GHC.Types.Id -import GHC.Core.InstEnv -import GHC.Data.FastString -import GHC.Types.Unique +import GHC.Core.TyCon ( TyCon ) +import GHC.Core.DataCon ( DataCon ) +import GHC.Core.Class ( Class ) +import GHC.Driver.Config.Finder ( initFinderOpts ) +import GHC.Driver.Env ( HscEnv(..), hsc_home_unit, hsc_units ) +import GHC.Utils.Outputable ( SDoc ) +import GHC.Core.Type ( Kind, Type, PredType ) +import GHC.Types.Id ( Id ) +import GHC.Core.InstEnv ( InstEnvs ) +import GHC.Data.FastString ( FastString ) +import GHC.Types.Unique ( Unique ) -- | Perform some IO, typically to interact with an external tool. @@ -162,9 +161,8 @@ zonkTcType = unsafeTcPluginTcM . TcM.zonkTcType zonkCt :: Ct -> TcPluginM Ct zonkCt = unsafeTcPluginTcM . TcM.zonkCt - -- | Create a new wanted constraint. -newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence +newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence newWanted loc pty = unsafeTcPluginTcM (TcM.newWanted (ctLocOrigin loc) Nothing pty) @@ -172,26 +170,29 @@ newWanted loc pty newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence newDerived loc pty = return CtDerived { ctev_pred = pty, ctev_loc = loc } --- | Create a new given constraint, with the supplied evidence. This --- must not be invoked from 'tcPluginInit' or 'tcPluginStop', or it --- will panic. -newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence -newGiven loc pty evtm = do +-- | Create a new given constraint, with the supplied evidence. +-- +-- This should only be invoked within 'tcPluginSolve'. +newGiven :: EvBindsVar -> CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence +newGiven tc_evbinds loc pty evtm = do new_ev <- newEvVar pty - setEvBind $ mkGivenEvBind new_ev (EvExpr evtm) + setEvBind tc_evbinds $ mkGivenEvBind new_ev (EvExpr evtm) return CtGiven { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc } -- | Create a fresh evidence variable. +-- +-- This should only be invoked within 'tcPluginSolve'. newEvVar :: PredType -> TcPluginM EvVar newEvVar = unsafeTcPluginTcM . TcM.newEvVar -- | Create a fresh coercion hole. +-- This should only be invoked within 'tcPluginSolve'. newCoercionHole :: PredType -> TcPluginM CoercionHole newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole --- | Bind an evidence variable. This must not be invoked from --- 'tcPluginInit' or 'tcPluginStop', or it will panic. -setEvBind :: EvBind -> TcPluginM () -setEvBind ev_bind = do - tc_evbinds <- getEvBindsTcPluginM +-- | Bind an evidence variable. +-- +-- This should only be invoked within 'tcPluginSolve'. +setEvBind :: EvBindsVar -> EvBind -> TcPluginM () +setEvBind tc_evbinds ev_bind = do unsafeTcPluginTcM $ TcM.addTcEvBind tc_evbinds ev_bind diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 171cb958f2..98824022cd 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -192,11 +192,11 @@ solveSimples cts -- into the main solver. runTcPluginsGiven :: TcS [Ct] runTcPluginsGiven - = do { plugins <- getTcPlugins - ; if null plugins then return [] else + = do { solvers <- getTcPluginSolvers + ; if null solvers then return [] else do { givens <- getInertGivens ; if null givens then return [] else - do { p <- runTcPlugins plugins (givens,[],[]) + do { p <- runTcPluginSolvers solvers (givens,[],[]) ; let (solved_givens, _, _) = pluginSolvedCts p insols = pluginBadCts p ; updInertCans (removeInertCts solved_givens) @@ -213,13 +213,13 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 }) | isEmptyBag simples1 = return (False, wc) | otherwise - = do { plugins <- getTcPlugins - ; if null plugins then return (False, wc) else + = do { solvers <- getTcPluginSolvers + ; if null solvers then return (False, wc) else do { given <- getInertGivens ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs ; let (wanted, derived) = partition isWantedCt (bagToList simples1) - ; p <- runTcPlugins plugins (given, derived, wanted) + ; p <- runTcPluginSolvers solvers (given, derived, wanted) ; let (_, _, solved_wanted) = pluginSolvedCts p (_, unsolved_derived, unsolved_wanted) = pluginInputCts p new_wanted = pluginNewCts p @@ -260,11 +260,12 @@ data TcPluginProgress = TcPluginProgress -- ^ New constraints emitted by plugins } -getTcPlugins :: TcS [TcPluginSolver] -getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) } +getTcPluginSolvers :: TcS [TcPluginSolver] +getTcPluginSolvers + = do { tcg_env <- getGblEnv; return (tcg_tc_plugin_solvers tcg_env) } -- | Starting from a triple of (given, derived, wanted) constraints, --- invoke each of the typechecker plugins in turn and return +-- invoke each of the typechecker constraint-solving plugins in turn and return -- -- * the remaining unmodified constraints, -- * constraints that have been solved, @@ -276,16 +277,16 @@ getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) } -- re-invoked and they will see it later). There is no check that new -- work differs from the original constraints supplied to the plugin: -- the plugin itself should perform this check if necessary. -runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress -runTcPlugins plugins all_cts - = foldM do_plugin initialProgress plugins +runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress +runTcPluginSolvers solvers all_cts + = foldM do_plugin initialProgress solvers where do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress do_plugin p solver = do result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p)) return $ progress p result - progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress + progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress progress p (TcPluginContradiction bad_cts) = p { pluginInputCts = discard bad_cts (pluginInputCts p) , pluginBadCts = bad_cts ++ pluginBadCts p diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 750b21f9c5..5796e2bd6a 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -1255,7 +1255,7 @@ traceTcS herald doc = wrapTcS (TcM.traceTc herald doc) {-# INLINE traceTcS #-} -- see Note [INLINE conditional tracing utilities] runTcPluginTcS :: TcPluginM a -> TcS a -runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar +runTcPluginTcS = wrapTcS . runTcPluginM instance HasDynFlags TcS where getDynFlags = wrapTcS getDynFlags diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index cf95fd8b3a..82c6c580a4 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -12,6 +12,10 @@ module GHC.Tc.Solver.Rewrite( 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 @@ -21,6 +25,7 @@ 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 @@ -46,12 +51,6 @@ import Data.List.NonEmpty ( NonEmpty(..) ) ************************************************************************ -} -data RewriteEnv - = FE { fe_loc :: !CtLoc -- See Note [Rewriter CtLoc] - , fe_flavour :: !CtFlavour - , fe_eq_rel :: !EqRel -- See Note [Rewriter EqRels] - } - -- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv' newtype RewriteM a = RewriteM { runRewriteM :: RewriteEnv -> TcS a } @@ -98,6 +97,10 @@ traceRewriteM :: String -> SDoc -> RewriteM () traceRewriteM herald doc = liftTcS $ traceTcS herald doc {-# INLINE traceRewriteM #-} -- see Note [INLINE conditional tracing utilities] +getRewriteEnv :: RewriteM RewriteEnv +getRewriteEnv + = mkRewriteM $ \env -> return env + getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a getRewriteEnvField accessor = mkRewriteM $ \env -> return (accessor env) @@ -698,9 +701,16 @@ 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. -STEP 1. Try the famapp-cache. If we get a cache hit, jump to FINISH. +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 2. Try top-level instances. Note that we haven't simplified the arguments +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)) @@ -709,27 +719,31 @@ STEP 2. Try top-level instances. Note that we haven't simplified the arguments If an instance is found, jump to FINISH. -STEP 3. Rewrite all arguments. This might expose more information so that we - can use a top-level instance. - - Continue to the next step. +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 4. Try the inerts. Note that we try the inerts *after* rewriting the +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. -STEP 5. Try the famapp-cache again. Now that we've revealed more information - in the arguments, the cache might be helpful. +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 6. Try top-level instances, which might trigger now that we know more - about the argumnents. +STEP 4c. Try top-level instances again. If an instance is found, jump to FINISH. -STEP 7. No progress to be made. Return what we have. (Do not do 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. @@ -737,11 +751,11 @@ FINISH 1. We've made a reduction, but the new type may still have more FINISH 2. Add the result to the famapp-cache, connecting the type we started with to the one we ended with. -Because STEP 1/2 and STEP 5/6 happen the same way, they are abstracted into +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/2. So `finish` +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. -} @@ -768,15 +782,19 @@ rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction rewrite_exact_fam_app tc tys = do { checkStackDepth (mkTyConApp tc tys) - -- STEP 1/2. Try to reduce without reducing arguments first. - ; result1 <- try_to_reduce tc tys + -- Query the typechecking plugins for all their rewriting functions + -- which apply to a type family application headed by the TyCon 'tc'. + ; tc_rewriters <- getTcPluginRewritersForTyCon 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 redn -> finish False redn ; Nothing -> - -- That didn't work. So reduce the arguments, in STEP 3. + -- That didn't work. So reduce the arguments, in STEP 2. do { eq_rel <- getEqRel -- checking eq_rel == NomEq saves ~0.5% in T9872a ; ArgsReductions (Reductions cos xis) kind_co <- @@ -808,7 +826,11 @@ rewrite_exact_fam_app tc tys (args_co `mkTransRedn` redn) kind_co - -- STEP 4: try the inerts + give_up :: Reduction + give_up = homogenise $ mkReflRedn role reduced + where reduced = mkTyConApp tc xis + + -- STEP 3: try the inerts ; result2 <- liftTcS $ lookupFamAppInert tc xis ; flavour <- getFlavour ; case result2 of @@ -828,14 +850,12 @@ rewrite_exact_fam_app tc tys ; _ -> - -- inert didn't work. Try to reduce again, in STEP 5/6. - do { result3 <- try_to_reduce tc xis + -- inerts didn't work. Try to reduce again, in STEP 4. + do { result3 <- try_to_reduce tc xis tc_rewriters ; case result3 of Just redn -> finish True (homogenise redn) - Nothing -> -- we have made no progress at all: STEP 7. - return (homogenise $ mkReflRedn role reduced) - where - reduced = mkTyConApp tc xis }}}}} + -- we have made no progress at all: STEP 5 (GIVEUP). + _ -> return give_up }}}}} where -- call this if the above attempts made progress. -- This recursively rewrites the result and then adds to the cache @@ -858,17 +878,21 @@ rewrite_exact_fam_app tc tys -- 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] -> RewriteM (Maybe Reduction) -try_to_reduce tc tys - = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys -- STEP 5 - , matchFam tc tys ] -- STEP 6 - ; downgrade result } +try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter] + -> RewriteM (Maybe Reduction) +try_to_reduce tc tys tc_rewriters + = do { rewrite_env <- 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 :: Maybe Reduction -> RewriteM (Maybe Reduction) - downgrade Nothing = return Nothing - downgrade result@(Just redn) + downgrade :: Reduction -> RewriteM Reduction + downgrade redn = do { traceRewriteM "Eager T.F. reduction success" $ vcat [ ppr tc , ppr tys @@ -878,8 +902,45 @@ try_to_reduce tc tys -- manually doing it this way avoids allocation in the vastly -- common NomEq case ; case eq_rel of - NomEq -> return result - ReprEq -> return $ Just (mkSubRedn redn) } + NomEq -> return redn + ReprEq -> return $ mkSubRedn redn } + +-- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application +-- headed by the given 'TyCon`. +getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter] +getTcPluginRewritersForTyCon tc + = liftTcS $ do { rewriters <- tcg_tc_plugin_rewriters <$> 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 rewriterFunctions tys + | null rewriterFunctions + = return Nothing -- short-circuit for common case + | otherwise + = do { givens <- getInertGivens + ; runRewriters givens rewriterFunctions } + where + runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction) + runRewriters _ [] + = return Nothing + runRewriters givens (rewriter:rewriters) + = do + rewriteResult <- wrapTcS . runTcPluginM $ rewriter rewriteEnv givens tys + case rewriteResult of + TcPluginRewriteTo + { tcPluginReduction = redn + , tcRewriterNewWanteds = wanteds + } -> do { emitWork wanteds; return $ Just redn } + TcPluginNoRewrite {} -> runRewriters givens rewriters {- ************************************************************************ diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs index b3f47a8dc2..684bee4a59 100644 --- a/compiler/GHC/Tc/Types.hs +++ b/compiler/GHC/Tc/Types.hs @@ -1,6 +1,7 @@ -{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {- @@ -32,6 +33,7 @@ module GHC.Tc.Types( setLclEnvLoc, getLclEnvLoc, IfGblEnv(..), IfLclEnv(..), tcVisibleOrphanMods, + RewriteEnv(..), -- Frontend types (shouldn't really be here) FrontendResult(..), @@ -72,9 +74,9 @@ module GHC.Tc.Types( getPlatform, -- Constraint solver plugins - TcPlugin(..), TcPluginResult(..), TcPluginSolver, - TcPluginM, runTcPluginM, unsafeTcPluginTcM, - getEvBindsTcPluginM, + TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..), + TcPluginSolver, TcPluginRewriter, + TcPluginM(runTcPluginM), unsafeTcPluginTcM, -- Role annotations RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv, @@ -103,6 +105,7 @@ import GHC.Tc.Types.Evidence import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes ( HoleFitPlugin ) import GHC.Tc.Errors.Types +import GHC.Core.Reduction ( Reduction(..) ) import GHC.Core.Type import GHC.Core.TyCon ( TyCon, tyConKind ) import GHC.Core.PatSyn ( PatSyn ) @@ -110,6 +113,7 @@ import GHC.Core.Lint ( lintAxioms ) import GHC.Core.UsageEnv import GHC.Core.InstEnv import GHC.Core.FamInstEnv +import GHC.Core.Predicate import GHC.Types.Id ( idType, idName ) import GHC.Types.FieldLabel ( FieldLabel ) @@ -151,7 +155,6 @@ import GHC.Utils.Logger import GHC.Builtin.Names ( isUnboundName ) -import Control.Monad (ap) import Data.Set ( Set ) import qualified Data.Set as S import Data.Map ( Map ) @@ -250,6 +253,40 @@ instance ContainsLogger (Env gbl lcl) where instance ContainsModule gbl => ContainsModule (Env gbl lcl) where extractModule env = extractModule (env_gbl env) +{- +************************************************************************ +* * +* RewriteEnv +* The rewriting environment +* * +************************************************************************ +-} + +-- | A 'RewriteEnv' carries the necessary context for performing rewrites +-- (i.e. type family reductions and following filled-in metavariables) +-- in the solver. +data RewriteEnv + = FE { fe_loc :: !CtLoc + -- ^ In which context are we rewriting? + -- + -- Type-checking plugins might want to use this location information + -- when emitting new Wanted constraints when rewriting type family + -- applications. This ensures that such Wanted constraints will, + -- when unsolved, give rise to error messages with the + -- correct source location. + + -- Within GHC, we use this field to keep track of reduction depth. + -- See Note [Rewriter CtLoc] in GHC.Tc.Solver.Rewrite. + , fe_flavour :: !CtFlavour + , fe_eq_rel :: !EqRel + -- ^ At what role are we rewriting? + -- + -- See Note [Rewriter EqRels] in GHC.Tc.Solver.Rewrite + } +-- RewriteEnv is mostly used in @GHC.Tc.Solver.Rewrite@, but it is defined +-- here so that it can also be passed to rewriting plugins. +-- See the 'tcPluginRewrite' field of 'TcPlugin'. + {- ************************************************************************ @@ -572,8 +609,13 @@ data TcGblEnv -- are supplied (#19714), or if those reasons have already been -- reported by GHC.Driver.Main.markUnsafeInfer - tcg_tc_plugins :: [TcPluginSolver], - -- ^ A list of user-defined plugins for the constraint solver. + tcg_tc_plugin_solvers :: [TcPluginSolver], + -- ^ A list of user-defined type-checking plugins for constraint solving. + + tcg_tc_plugin_rewriters :: UniqFM TyCon [TcPluginRewriter], + -- ^ A collection of all the user-defined type-checking plugins for rewriting + -- type family applications, collated by their type family 'TyCon's. + tcg_hf_plugins :: [HoleFitPlugin], -- ^ A list of user-defined plugins for hole fit suggestions. @@ -1665,66 +1707,106 @@ Constraint Solver Plugins ------------------------- -} -type TcPluginSolver = [Ct] -- given - -> [Ct] -- derived - -> [Ct] -- wanted - -> TcPluginM TcPluginResult - -newtype TcPluginM a = TcPluginM (EvBindsVar -> TcM a) deriving (Functor) - -instance Applicative TcPluginM where - pure x = TcPluginM (const $ pure x) - (<*>) = ap - -instance Monad TcPluginM where - TcPluginM m >>= k = - TcPluginM (\ ev -> do a <- m ev - runTcPluginM (k a) ev) - -instance MonadFail TcPluginM where - fail x = TcPluginM (const $ fail x) - -runTcPluginM :: TcPluginM a -> EvBindsVar -> TcM a -runTcPluginM (TcPluginM m) = m +-- | The @solve@ function of a type-checking plugin takes in Given, Derived +-- and Wanted constraints, and should return a 'TcPluginSolveResult' +-- indicating which Wanted constraints it could solve, or whether any are +-- insoluble. +type TcPluginSolver = [Ct] -- ^ Givens + -> [Ct] -- ^ Deriveds + -> [Ct] -- ^ Wanteds + -> TcPluginM TcPluginSolveResult + +-- | For rewriting type family applications, a type-checking plugin provides +-- a function of this type for each type family 'TyCon'. +-- +-- The function is provided with the current set of Given constraints, together +-- with the arguments to the type family. +-- The type family application will always be fully saturated. +type TcPluginRewriter + = RewriteEnv -- ^ Rewriter environment + -> [Ct] -- ^ Givens + -> [TcType] -- ^ type family arguments + -> TcPluginM TcPluginRewriteResult + +-- | 'TcPluginM' is the monad in which type-checking plugins operate. +newtype TcPluginM a = TcPluginM { runTcPluginM :: TcM a } + deriving newtype (Functor, Applicative, Monad, MonadFail) -- | This function provides an escape for direct access to -- the 'TcM` monad. It should not be used lightly, and -- the provided 'TcPluginM' API should be favoured instead. unsafeTcPluginTcM :: TcM a -> TcPluginM a -unsafeTcPluginTcM = TcPluginM . const - --- | Access the 'EvBindsVar' carried by the 'TcPluginM' during --- constraint solving. Returns 'Nothing' if invoked during --- 'tcPluginInit' or 'tcPluginStop'. -getEvBindsTcPluginM :: TcPluginM EvBindsVar -getEvBindsTcPluginM = TcPluginM return - +unsafeTcPluginTcM = TcPluginM data TcPlugin = forall s. TcPlugin - { tcPluginInit :: TcPluginM s + { tcPluginInit :: TcPluginM s -- ^ Initialize plugin, when entering type-checker. - , tcPluginSolve :: s -> TcPluginSolver + , tcPluginSolve :: s -> EvBindsVar -> TcPluginSolver -- ^ Solve some constraints. - -- TODO: WRITE MORE DETAILS ON HOW THIS WORKS. - - , tcPluginStop :: s -> TcPluginM () + -- + -- This function will be invoked at two points in the constraint solving + -- process: once to simplify Given constraints, and once to solve + -- Wanted constraints. In the first case (and only in the first case), + -- no Wanted constraints will be passed to the plugin. + -- + -- The plugin can either return a contradiction, + -- or specify that it has solved some constraints (with evidence), + -- and possibly emit additional constraints. These returned constraints + -- must be Givens in the first case, and Wanteds in the second. + -- + -- Use @ \\ _ _ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin + -- does not provide this functionality. + + , tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter + -- ^ Rewrite saturated type family applications. + -- + -- The plugin is expected to supply a mapping from type family names to + -- rewriting functions. For each type family 'TyCon', the plugin should + -- provide a function which takes in the given constraints and arguments + -- of a saturated type family application, and return a possible rewriting. + -- See 'TcPluginRewriter' for the expected shape of such a function. + -- + -- Use @ \\ _ -> emptyUFM @ if your plugin does not provide this functionality. + + , tcPluginStop :: s -> TcPluginM () -- ^ Clean up after the plugin, when exiting the type-checker. } -data TcPluginResult +data TcPluginSolveResult = TcPluginContradiction [Ct] -- ^ The plugin found a contradiction. -- The returned constraints are removed from the inert set, -- and recorded as insoluble. + -- + -- The returned list of constraints should never be empty. - | TcPluginOk [(EvTerm,Ct)] [Ct] + | TcPluginOk + { tcPluginSolvedCts :: [(EvTerm,Ct)] + , tcPluginNewCts :: [Ct] } -- ^ The first field is for constraints that were solved. -- These are removed from the inert set, -- and the evidence for them is recorded. -- The second field contains new work, that should be processed by -- the constraint solver. + +data TcPluginRewriteResult + = + -- | The plugin does not rewrite the type family application. + TcPluginNoRewrite + + -- | The plugin rewrites the type family application + -- providing a rewriting together with evidence: a 'Reduction', + -- which contains the rewritten type together with a 'Coercion' + -- whose right-hand-side type is the rewritten type. + -- + -- The plugin can also emit additional Wanted constraints. + | TcPluginRewriteTo + { tcPluginReduction :: !Reduction + , tcRewriterNewWanteds :: [Ct] + } + {- ********************************************************************* * * Role annotations diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 3a38e56f6c..1645333f32 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -205,6 +205,7 @@ import GHC.Types.SrcLoc import GHC.Types.Name.Env import GHC.Types.Name.Set import GHC.Types.Name.Ppr +import GHC.Types.Unique.FM ( emptyUFM ) import GHC.Types.Unique.Supply import GHC.Types.Annotations import GHC.Types.Basic( TopLevelFlag, TypeOrKind(..) ) @@ -348,7 +349,8 @@ initTc hsc_env hsc_src keep_rn_syntax mod loc do_this tcg_safe_infer = infer_var, tcg_safe_infer_reasons = infer_reasons_var, tcg_dependent_files = dependent_files_var, - tcg_tc_plugins = [], + tcg_tc_plugin_solvers = [], + tcg_tc_plugin_rewriters = emptyUFM, tcg_hf_plugins = [], tcg_top_loc = loc, tcg_static_wc = static_wc_var, diff --git a/compiler/GHC/Types/Unique/FM.hs b/compiler/GHC/Types/Unique/FM.hs index 35a8a2b3fc..7c80359d0e 100644 --- a/compiler/GHC/Types/Unique/FM.hs +++ b/compiler/GHC/Types/Unique/FM.hs @@ -57,6 +57,7 @@ module GHC.Types.Unique.FM ( mergeUFM, plusMaybeUFM_C, plusUFMList, + sequenceUFMList, minusUFM, intersectUFM, intersectUFM_C, @@ -301,6 +302,15 @@ plusMaybeUFM_C f (UFM xm) (UFM ym) plusUFMList :: [UniqFM key elt] -> UniqFM key elt plusUFMList = foldl' plusUFM emptyUFM +sequenceUFMList :: forall key elt. [UniqFM key elt] -> UniqFM key [elt] +sequenceUFMList = foldr (plusUFM_CD2 cons) emptyUFM + where + cons :: Maybe elt -> Maybe [elt] -> [elt] + cons (Just x) (Just ys) = x : ys + cons Nothing (Just ys) = ys + cons (Just x) Nothing = [x] + cons Nothing Nothing = [] + minusUFM :: UniqFM key elt1 -> UniqFM key elt2 -> UniqFM key elt1 minusUFM (UFM x) (UFM y) = UFM (M.difference x y) |