Commit 50e2b37d authored by sheaf's avatar sheaf
Browse files

Add rewriting to typechecking plugins

Includes some changes to the TcPlugin API, e.g. removal
of the EvBindsVar parameter to the TcPluginM monad.
parent 5850efa3
......@@ -3087,19 +3087,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)
......
......@@ -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
......@@ -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
......
......@@ -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
......
......@@ -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)
......@@ -697,9 +700,19 @@ 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.
STEP 2. Try top-level instances. Note that we haven't simplified the arguments
If any plugin rewrites the type family application, jump to FINISH.
If any plugin throws an error, jump to GIVEUP.
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))
......@@ -708,27 +721,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.)
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.
......@@ -736,11 +753,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.
-}
......@@ -767,15 +784,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 <-
......@@ -805,8 +826,11 @@ rewrite_exact_fam_app tc tys
= homogeniseHetRedn role
$ mkHetReduction kind_co
(args_co `mkTransRedn` redn)
give_up :: Reduction
give_up = homogenise $ mkReflRedn role reduced
where reduced = mkTyConApp tc xis
-- STEP 4: try the inerts
-- STEP 3: try the inerts
; result2 <- liftTcS $ lookupFamAppInert tc xis
; flavour <- getFlavour
; case result2 of
......@@ -826,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: GIVEUP.
_ -> return give_up }}}}}
where
-- call this if the above attempts made progress.
-- This recursively rewrites the result and then adds to the cache
......@@ -856,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
......@@ -876,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 (overRednCo mkSubCo redn) }
NomEq -> return redn
ReprEq -> return $ overRednCo mkSubCo 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
{-
************************************************************************
......
{-# 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.List ( sort )
......@@ -251,6 +254,20 @@ instance ContainsLogger (Env gbl lcl) where
instance ContainsModule gbl => ContainsModule (Env gbl lcl) where
extractModule env = extractModule (env_gbl env)
{-
************************************************************************
* *
* RewriteEnv
* The rewriting environment
* *
************************************************************************
-}
data RewriteEnv
= FE { fe_loc :: !CtLoc -- See Note [Rewriter CtLoc]
, fe_flavour :: !CtFlavour
, fe_eq_rel :: !EqRel -- See Note [Rewriter EqRels]
}
{-
************************************************************************
......@@ -573,8 +590,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.
......@@ -1666,66 +1688,103 @@ 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