{-# LANGUAGE BlockArguments #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-| Module: GHC.TcPlugin.API.Internal This module provides operations to directly lift and unlift computations in GHC's 'GHC.Tc.TcM' monad to the various type-checking plugin monads, in the form of the functions > unsafeLiftTcM :: TcM a -> m a > unsafeWithRunInTcM :: ( ( forall a. m a -> TcM a ) -> TcM b ) -> m b Here 'GHC.Tc.TcM' is GHC's internal type-checker monad. It also exposes extra environment available in the solving/rewriting stages: > askRewriteEnv :: TcPluginM Rewrite RewriteEnv > askEvBinds :: TcPluginM Solve EvBindsVar It is hoped that none of these internal operations are necessary, and that users can fulfill their needs without importing this internal module. Please file a bug on the issue tracker if you have encountered a situation which requires the import of this module. -} module GHC.TcPlugin.API.Internal ( -- * Internal functions and types MonadTcPlugin(..), MonadTcPluginWork , unsafeLiftThroughTcM -- * Re-exported functions and types , TcPlugin(..), TcPluginStage(..) , TcPluginSolver , TcPluginM(..) , TcPluginErrorMessage(..) , TcPluginRewriter , MonadThings(..) , askRewriteEnv , askDeriveds , askEvBinds , mkTcPlugin , mkTcPluginErrorTy ) where -- base import Data.Coerce ( Coercible ) import Data.Kind ( Type ) import GHC.TypeLits ( TypeError, ErrorMessage(..) ) -- transformers import Control.Monad.Trans.Reader ( ReaderT(..) ) -- ghc import qualified GHC.Builtin.Names as GHC.TypeLits ( errorMessageTypeErrorFamName , typeErrorTextDataConName , typeErrorAppendDataConName , typeErrorVAppendDataConName , typeErrorShowTypeDataConName ) import qualified GHC.Builtin.Types as GHC ( constraintKind ) import qualified GHC.Core.DataCon as GHC ( promoteDataCon ) import qualified GHC.Core.TyCon as GHC ( TyCon ) import qualified GHC.Core.TyCo.Rep as GHC ( PredType, Type(..), TyLit(..) ) import qualified GHC.Core.Type as GHC ( mkTyConApp, typeKind ) import qualified GHC.Data.FastString as GHC ( fsLit ) import qualified GHC.Tc.Plugin as GHC ( tcLookupDataCon, tcLookupTyCon ) import qualified GHC.Tc.Types as GHC ( TcM, TcPlugin(..), TcPluginM , TcPluginSolver #ifdef HAS_REWRITING , TcPluginRewriter #else , getEvBindsTcPluginM #endif , runTcPluginM, unsafeTcPluginTcM ) #ifdef HAS_REWRITING import GHC.Tc.Types ( TcPluginSolveResult , TcPluginRewriteResult , RewriteEnv ) #endif import qualified GHC.Tc.Types.Constraint as GHC ( Ct ) import qualified GHC.Tc.Types.Evidence as GHC ( EvBindsVar ) import qualified GHC.Types.Unique.FM as GHC ( UniqFM ) #if MIN_VERSION_ghc(9,1,0) import GHC.Types.TyThing ( MonadThings(..) ) #else import GHC.Driver.Types ( MonadThings(..) ) #endif -- ghc-tcplugin-api #ifndef HAS_REWRITING import GHC.TcPlugin.API.Internal.Shim ( TcPluginSolveResult, TcPluginRewriteResult(..) , RewriteEnv , shimRewriter ) #endif -------------------------------------------------------------------------------- -- Public types and functions. -- | Stage of a type-checking plugin, used as a data kind. data TcPluginStage = Init | Solve | Rewrite | Stop -- | The @solve@ function of a type-checking plugin takes in Given and Wanted -- constraints, and should return a 'GHC.Tc.Types.TcPluginSolveResult' -- indicating which Wanted constraints it could solve, or whether any are -- insoluble. type TcPluginSolver = [GHC.Ct] -- ^ Givens -> [GHC.Ct] -- ^ Wanteds -> TcPluginM Solve TcPluginSolveResult -- | For rewriting type family applications, a type-checking plugin provides -- a function of this type for each type family 'GHC.Core.TyCon.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 = [GHC.Ct] -- ^ Givens -> [GHC.Type] -- ^ Type family arguments (saturated) -> TcPluginM Rewrite TcPluginRewriteResult -- | A record containing all the stages necessary for the -- operation of a type-checking plugin, as defined in this API. -- -- __Note__: this is not the same record as GHC's built-in -- 'GHC.Tc.Types.TcPlugin' record. Use 'mkTcPlugin' for the conversion. -- -- To create a type-checking plugin, define something of this type -- and then call 'mkTcPlugin' on the result. -- This will return something that can be passed to 'GHC.Plugins.Plugin': -- -- > plugin :: GHC.Plugins.Plugin -- > plugin = -- > GHC.Plugins.defaultPlugin -- > { GHC.Plugins.tcPlugin = -- > \ args -> Just $ -- > GHC.TcPlugin.API.mkTcPlugin ( myTcPlugin args ) -- > } -- > -- > myTcPlugin :: [String] -> GHC.TcPlugin.API.TcPlugin -- > myTcPlugin args = ... data TcPlugin = forall s. TcPlugin { tcPluginInit :: TcPluginM Init s -- ^ Initialise plugin, when entering type-checker. , tcPluginSolve :: s -> TcPluginSolver -- ^ Solve some constraints. -- -- This function will be invoked at two points in the constraint solving -- process: once to manipulate 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 wanted constraints. -- -- Use @ \\ _ _ _ -> pure $ TcPluginOK [] [] @ if your plugin -- does not provide this functionality. , tcPluginRewrite :: s -> GHC.UniqFM #if MIN_VERSION_ghc(9,0,0) GHC.TyCon #endif 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 'GHC.Core.TyCon.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 @ const emptyUFM @ if your plugin does not provide this functionality. , tcPluginStop :: s -> TcPluginM Stop () -- ^ Clean up after the plugin, when exiting the type-checker. } -- | The monad used for a type-checker plugin, parametrised by -- the 'TcPluginStage' of the plugin. data family TcPluginM (s :: TcPluginStage) :: Type -> Type newtype instance TcPluginM Init a = TcPluginInitM { tcPluginInitM :: GHC.TcPluginM a } deriving newtype ( Functor, Applicative, Monad ) #ifdef HAS_DERIVEDS newtype instance TcPluginM Solve a = TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> [GHC.Ct] -> GHC.TcPluginM a } deriving ( Functor, Applicative, Monad ) via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar ( ReaderT [GHC.Ct] GHC.TcPluginM ) ) ) #else newtype instance TcPluginM Solve a = TcPluginSolveM { tcPluginSolveM :: BuiltinDefs -> GHC.EvBindsVar -> GHC.TcPluginM a } deriving ( Functor, Applicative, Monad ) via ( ReaderT BuiltinDefs ( ReaderT GHC.EvBindsVar GHC.TcPluginM ) ) #endif newtype instance TcPluginM Rewrite a = TcPluginRewriteM { tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> GHC.TcPluginM a } deriving ( Functor, Applicative, Monad ) via ( ReaderT BuiltinDefs ( ReaderT RewriteEnv GHC.TcPluginM ) ) newtype instance TcPluginM Stop a = TcPluginStopM { tcPluginStopM :: GHC.TcPluginM a } deriving newtype ( Functor, Applicative, Monad ) -- | Ask for the evidence currently gathered by the type-checker. -- -- Only available in the solver part of the type-checking plugin. askEvBinds :: TcPluginM Solve GHC.EvBindsVar askEvBinds = TcPluginSolveM \ _defs evBinds #ifdef HAS_DERIVEDS _deriveds #endif -> pure evBinds -- | Ask for the Derived constraints that the solver was provided with. -- -- Always returns the empty list on GHC 9.4 or above. askDeriveds :: TcPluginM Solve [GHC.Ct] askDeriveds = #ifdef HAS_DERIVEDS TcPluginSolveM \ _defs _evBinds deriveds -> pure deriveds #else pure [] #endif -- | Ask for the current rewriting environment. -- -- Only available in the rewriter part of the type-checking plugin. askRewriteEnv :: TcPluginM Rewrite RewriteEnv askRewriteEnv = TcPluginRewriteM ( \ _ rewriteEnv -> pure rewriteEnv ) -- | A 'MonadTcPlugin' is essentially a reader monad over GHC's 'GHC.Tc.TcM' monad. -- -- This means we have both a @lift@ and an @unlift@ operation, -- similar to @MonadUnliftIO@ or @MonadBaseControl@. -- -- See for instance 'unsafeLiftThroughTcM', which is an example of function that -- one would not be able to write using only a @lift@ operation. -- -- Note that you must import the internal module in order to access the methods. -- Please report a bug if you find yourself needing this functionality. class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin (m :: Type -> Type) where {-# MINIMAL liftTcPluginM, unsafeWithRunInTcM #-} -- N.B.: these methods are not re-exported from the main module. -- | Lift a computation from GHC's 'GHC.TcPluginM' monad. liftTcPluginM :: GHC.TcPluginM a -> m a -- | Lift a computation from the 'GHC.Tc.TcM' monad. unsafeLiftTcM :: GHC.TcM a -> m a unsafeLiftTcM = liftTcPluginM . GHC.unsafeTcPluginTcM -- | Unlift a computation from the 'GHC.Tc.TcM' monad. -- -- If this type signature seems confusing, I recommend reading Alexis King's -- excellent blog post on @MonadBaseControl@: -- -- unsafeWithRunInTcM :: ( ( forall a. m a -> GHC.TcM a ) -> GHC.TcM b ) -> m b instance MonadTcPlugin ( TcPluginM Init ) where liftTcPluginM = TcPluginInitM unsafeWithRunInTcM runInTcM = unsafeLiftTcM $ runInTcM #ifdef HAS_REWRITING ( GHC.runTcPluginM . tcPluginInitM ) #else ( ( `GHC.runTcPluginM` ( error "tcPluginInit: cannot access EvBindsVar" ) ) . tcPluginInitM ) #endif instance MonadTcPlugin ( TcPluginM Solve ) where liftTcPluginM = TcPluginSolveM #ifdef HAS_DERIVEDS . ( \ ma _defs _evBinds _deriveds -> ma ) #else . ( \ ma _defs _evBinds -> ma ) #endif unsafeWithRunInTcM runInTcM = TcPluginSolveM \ builtinDefs evBinds #ifdef HAS_DERIVEDS deriveds #endif -> GHC.unsafeTcPluginTcM $ runInTcM #ifdef HAS_REWRITING -- (no deriveds) ( GHC.runTcPluginM . ( \ f -> f builtinDefs evBinds ) . tcPluginSolveM ) #else ( ( `GHC.runTcPluginM` evBinds ) . ( \ f -> f builtinDefs evBinds deriveds ) . tcPluginSolveM ) #endif instance MonadTcPlugin ( TcPluginM Rewrite ) where liftTcPluginM = TcPluginRewriteM . ( \ ma _ _ -> ma ) unsafeWithRunInTcM runInTcM = TcPluginRewriteM \ builtinDefs rewriteEnv -> GHC.unsafeTcPluginTcM $ runInTcM #ifdef HAS_REWRITING ( GHC.runTcPluginM #else ( ( `GHC.runTcPluginM` ( error "tcPluginRewrite: cannot access EvBindsVar" ) ) #endif . ( \ f -> f builtinDefs rewriteEnv ) . tcPluginRewriteM ) instance MonadTcPlugin ( TcPluginM Stop ) where liftTcPluginM = TcPluginStopM unsafeWithRunInTcM runInTcM = unsafeLiftTcM $ runInTcM #ifdef HAS_REWRITING ( GHC.runTcPluginM . tcPluginStopM ) #else ( ( `GHC.runTcPluginM` ( error "tcPluginStop: cannot access EvBindsVar" ) ) . tcPluginStopM ) #endif -- | Take a function whose argument and result types are both within the 'GHC.Tc.TcM' monad, -- and return a function that works within a type-checking plugin monad. -- -- Please report a bug if you find yourself needing to use this function. unsafeLiftThroughTcM :: MonadTcPlugin m => ( GHC.TcM a -> GHC.TcM b ) -> m a -> m b unsafeLiftThroughTcM f ma = unsafeWithRunInTcM \ runInTcM -> f ( runInTcM ma ) -- | Use this function to create a type-checker plugin to pass to GHC. mkTcPlugin :: TcPlugin -- ^ type-checking plugin written with this library -> GHC.TcPlugin -- ^ type-checking plugin for GHC mkTcPlugin ( TcPlugin { tcPluginInit = tcPluginInit :: TcPluginM Init userDefs , tcPluginSolve , tcPluginRewrite , tcPluginStop } ) = GHC.TcPlugin { GHC.tcPluginInit = adaptUserInit tcPluginInit #ifdef HAS_REWRITING , GHC.tcPluginSolve = adaptUserSolve tcPluginSolve , GHC.tcPluginRewrite = adaptUserRewrite tcPluginRewrite #else , GHC.tcPluginSolve = adaptUserSolveAndRewrite tcPluginSolve tcPluginRewrite #endif , GHC.tcPluginStop = adaptUserStop tcPluginStop } where adaptUserInit :: TcPluginM Init userDefs -> GHC.TcPluginM ( TcPluginDefs userDefs ) adaptUserInit userInit = do tcPluginBuiltinDefs <- initBuiltinDefs tcPluginUserDefs <- tcPluginInitM userInit pure ( TcPluginDefs { tcPluginBuiltinDefs, tcPluginUserDefs }) #ifdef HAS_REWRITING -- (no deriveds) adaptUserSolve :: ( userDefs -> TcPluginSolver ) -> TcPluginDefs userDefs -> GHC.TcPluginSolver adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) = \ evBindsVar givens wanteds -> do tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds ) tcPluginBuiltinDefs evBindsVar adaptUserRewrite :: ( userDefs -> GHC.UniqFM GHC.TyCon TcPluginRewriter ) -> TcPluginDefs userDefs -> GHC.UniqFM GHC.TyCon GHC.TcPluginRewriter adaptUserRewrite userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs }) = fmap ( \ userRewriter rewriteEnv givens tys -> tcPluginRewriteM ( userRewriter givens tys ) tcPluginBuiltinDefs rewriteEnv ) ( userRewrite tcPluginUserDefs ) #else adaptUserSolveAndRewrite :: ( userDefs -> TcPluginSolver ) -> ( userDefs -> GHC.UniqFM #if MIN_VERSION_ghc(9,0,0) GHC.TyCon #endif TcPluginRewriter ) -> TcPluginDefs userDefs -> GHC.TcPluginSolver adaptUserSolveAndRewrite userSolve userRewrite ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } ) = \ givens deriveds wanteds -> do evBindsVar <- GHC.getEvBindsTcPluginM shimRewriter givens deriveds wanteds ( fmap ( \ userRewriter rewriteEnv gs tys -> tcPluginRewriteM ( userRewriter gs tys ) tcPluginBuiltinDefs rewriteEnv ) ( userRewrite tcPluginUserDefs ) ) ( \ gs ds ws -> tcPluginSolveM ( userSolve tcPluginUserDefs gs ws ) tcPluginBuiltinDefs evBindsVar ds ) #endif adaptUserStop :: ( userDefs -> TcPluginM Stop () ) -> TcPluginDefs userDefs -> GHC.TcPluginM () adaptUserStop userStop ( TcPluginDefs { tcPluginUserDefs } ) = tcPluginStopM $ userStop tcPluginUserDefs -- | Monads for type-checking plugins which are able to emit new constraints -- and throw errors. -- -- These operations are supported by the monads that 'tcPluginSolve' -- and 'tcPluginRewrite' use; it is not possible to emit work or -- throw type errors in 'tcPluginInit' or 'tcPluginStop'. -- -- See 'mkTcPluginErrorTy' and 'GHC.TcPlugin.API.emitWork' for functions -- which require this typeclass. class MonadTcPlugin m => MonadTcPluginWork m where {-# MINIMAL #-} -- to avoid the methods appearing in the haddocks askBuiltins :: m BuiltinDefs askBuiltins = error "askBuiltins: no default implementation" instance MonadTcPluginWork ( TcPluginM Solve ) where askBuiltins = TcPluginSolveM \ builtinDefs _evBinds #ifdef HAS_DERIVEDS _deriveds #endif -> pure builtinDefs instance MonadTcPluginWork ( TcPluginM Rewrite ) where askBuiltins = TcPluginRewriteM \ builtinDefs _evBinds -> pure builtinDefs instance TypeError ( 'Text "Cannot emit new work in 'tcPluginInit'." ) => MonadTcPluginWork ( TcPluginM Init ) where askBuiltins = error "Cannot emit new work in 'tcPluginInit'." instance TypeError ( 'Text "Cannot emit new work in 'tcPluginStop'." ) => MonadTcPluginWork ( TcPluginM Stop ) where askBuiltins = error "Cannot emit new work in 'tcPluginStop'." -- | Use this type like 'GHC.TypeLits.ErrorMessage' to write an error message. -- This error message can then be thrown at the type-level by the plugin, -- by emitting a wanted constraint whose predicate is obtained from 'mkTcPluginErrorTy'. -- -- A 'GHC.Tc.Types.Constraint.CtLoc' will still need to be provided in order to inform GHC of the -- origin of the error (e.g.: which part of the source code should be -- highlighted?). See 'GHC.TcPlugin.API.setCtLocM'. data TcPluginErrorMessage = Txt !String -- ^ Show the text as is. | PrintType !GHC.Type -- ^ Pretty print the given type. | (:|:) !TcPluginErrorMessage !TcPluginErrorMessage -- ^ Put two messages side by side. | (:-:) !TcPluginErrorMessage !TcPluginErrorMessage -- ^ Stack two messages vertically. infixl 5 :|: infixl 6 :-: -- | Create an error type with the desired error message. -- -- The result can be paired with a 'GHC.Tc.Types.Constraint.CtLoc' in order to throw a type error, -- for instance by using 'GHC.TcPlugin.API.newWanted'. mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m GHC.PredType mkTcPluginErrorTy msg = do builtinDefs@( BuiltinDefs { typeErrorTyCon } ) <- askBuiltins let errorMsgTy :: GHC.PredType errorMsgTy = interpretErrorMessage builtinDefs msg pure $ GHC.mkTyConApp typeErrorTyCon [ GHC.constraintKind, errorMsgTy ] instance ( Monad (TcPluginM s), MonadTcPlugin (TcPluginM s) ) => MonadThings (TcPluginM s) where lookupThing = unsafeLiftTcM . lookupThing -------------------------------------------------------------------------------- -- Private types and functions. -- Not exposed at all, even from the internal module. data BuiltinDefs = BuiltinDefs { typeErrorTyCon :: !GHC.TyCon , textTyCon :: !GHC.TyCon , showTypeTyCon :: !GHC.TyCon , concatTyCon :: !GHC.TyCon , vcatTyCon :: !GHC.TyCon } data TcPluginDefs s = TcPluginDefs { tcPluginBuiltinDefs :: !BuiltinDefs , tcPluginUserDefs :: !s } initBuiltinDefs :: GHC.TcPluginM BuiltinDefs initBuiltinDefs = do typeErrorTyCon <- GHC.tcLookupTyCon GHC.TypeLits.errorMessageTypeErrorFamName textTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorTextDataConName showTypeTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorShowTypeDataConName concatTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorAppendDataConName vcatTyCon <- GHC.promoteDataCon <$> GHC.tcLookupDataCon GHC.TypeLits.typeErrorVAppendDataConName pure ( BuiltinDefs { .. } ) interpretErrorMessage :: BuiltinDefs -> TcPluginErrorMessage -> GHC.PredType interpretErrorMessage ( BuiltinDefs { .. } ) = go where go :: TcPluginErrorMessage -> GHC.PredType go ( Txt str ) = GHC.mkTyConApp textTyCon [ GHC.LitTy . GHC.StrTyLit . GHC.fsLit $ str ] go ( PrintType ty ) = GHC.mkTyConApp showTypeTyCon [ GHC.typeKind ty, ty ] -- The kind gets ignored by GHC when printing the error message (see GHC.Core.Type.pprUserTypeErrorTy). -- However, including the wrong kind can lead to ASSERT failures, so we compute the kind and pass it. go ( msg1 :|: msg2 ) = GHC.mkTyConApp concatTyCon [ go msg1, go msg2 ] go ( msg1 :-: msg2 ) = GHC.mkTyConApp vcatTyCon [ go msg1, go msg2 ]