ghc-tcplugin-api-0.4.0.0: src/GHC/TcPlugin/API/Internal.hs
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# 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
, askRewriteEnv
, askDeriveds
, askEvBinds
, mkTcPlugin
, mkTcPluginErrorTy
)
where
-- base
import Data.Coerce
( Coercible )
import Data.Kind
( Constraint, 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, tcTypeKind )
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 )
-- 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.
type TcPluginM :: TcPluginStage -> ( Type -> Type )
data family TcPluginM s
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.
type MonadTcPlugin :: ( Type -> Type ) -> Constraint
class ( Monad m, ( forall x y. Coercible x y => Coercible (m x) (m y) ) ) => MonadTcPlugin m 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@:
--
-- <https://lexi-lambda.github.io/blog/2019/09/07/demystifying-monadbasecontrol/ Demystifying 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
( GHC.runTcPluginM
#ifdef HAS_DERIVEDS
. ( \ f -> f builtinDefs evBinds deriveds )
#else
. ( \ f -> f builtinDefs evBinds )
#endif
. 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
adaptUserSolve :: ( userDefs -> TcPluginSolver )
-> TcPluginDefs userDefs
-> GHC.EvBindsVar
-> GHC.TcPluginSolver
adaptUserSolve userSolve ( TcPluginDefs { tcPluginUserDefs, tcPluginBuiltinDefs } )
evBindsVar
#ifdef HAS_DERIVEDS
= \ givens deriveds wanteds -> do
tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
tcPluginBuiltinDefs evBindsVar deriveds
#else
= \ givens _deriveds wanteds -> do
tcPluginSolveM ( userSolve tcPluginUserDefs givens wanteds )
tcPluginBuiltinDefs evBindsVar
#endif
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.
type MonadTcPluginWork :: ( Type -> Type ) -> Constraint
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 ]
--------------------------------------------------------------------------------
-- 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.tcTypeKind 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 ]