GHC.TcPlugin.API.Internal

This module provides operations to directly lift and unlift computations in GHC's 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 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.

Internal functions and types

class (Monad m, forall x y. Coercible x y => Coercible (m x) (m y)) => MonadTcPlugin (m :: Type -> Type) where

A MonadTcPlugin is essentially a reader monad over GHC's 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.

Minimal complete definition

liftTcPluginM, unsafeWithRunInTcM

Methods

liftTcPluginM :: TcPluginM a -> m a

Lift a computation from GHC's TcPluginM monad.

unsafeLiftTcM :: TcM a -> m a

Lift a computation from the TcM monad.

unsafeWithRunInTcM :: ((forall a. m a -> TcM a) -> TcM b) -> m b

Unlift a computation from the TcM monad.

If this type signature seems confusing, I recommend reading Alexis King's excellent blog post on MonadBaseControl:

Demystifying MonadBaseControl

Instances

MonadTcPlugin (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Init a

unsafeLiftTcM :: TcM a -> TcPluginM 'Init a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Init a -> TcM a) -> TcM b) -> TcPluginM 'Init b

MonadTcPlugin (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Rewrite a

unsafeLiftTcM :: TcM a -> TcPluginM 'Rewrite a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b) -> TcPluginM 'Rewrite b

MonadTcPlugin (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Solve a

unsafeLiftTcM :: TcM a -> TcPluginM 'Solve a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Solve a -> TcM a) -> TcM b) -> TcPluginM 'Solve b

MonadTcPlugin (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Stop a

unsafeLiftTcM :: TcM a -> TcPluginM 'Stop a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Stop a -> TcM a) -> TcM b) -> TcPluginM 'Stop b

class MonadTcPlugin m => MonadTcPluginWork m

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 emitWork for functions which require this typeclass.

Instances

(TypeError ('Text "Cannot emit new work in 'tcPluginInit'.") :: Constraint) => MonadTcPluginWork (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Init BuiltinDefs

MonadTcPluginWork (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Rewrite BuiltinDefs

MonadTcPluginWork (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Solve BuiltinDefs

(TypeError ('Text "Cannot emit new work in 'tcPluginStop'.") :: Constraint) => MonadTcPluginWork (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Stop BuiltinDefs

unsafeLiftThroughTcM :: MonadTcPlugin m => (TcM a -> TcM b) -> m a -> m b

Take a function whose argument and result types are both within the 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.

Re-exported functions and types

data TcPlugin

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 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 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 = ...

Constructors

forall s. TcPlugin

Fields

• 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 -> 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 const emptyUFM if your plugin does not provide this functionality.

• tcPluginStop :: s -> TcPluginM Stop ()

  Clean up after the plugin, when exiting the type-checker.

data TcPluginStage

Stage of a type-checking plugin, used as a data kind.

Constructors

Init

Solve

Rewrite

Stop

type TcPluginSolver

Arguments

 = [Ct]

Givens

-> [Ct]

Wanteds

-> TcPluginM Solve TcPluginSolveResult

The solve function of a type-checking plugin takes in Given and Wanted constraints, and should return a TcPluginSolveResult indicating which Wanted constraints it could solve, or whether any are insoluble.

data family TcPluginM (s :: TcPluginStage) :: Type -> Type

The monad used for a type-checker plugin, parametrised by the TcPluginStage of the plugin.

Instances

Applicative (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

pure :: a -> TcPluginM 'Init a

(<*>) :: TcPluginM 'Init (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b

liftA2 :: (a -> b -> c) -> TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init c

(*>) :: TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b

(<*) :: TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init a

Applicative (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

pure :: a -> TcPluginM 'Rewrite a

(<*>) :: TcPluginM 'Rewrite (a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b

liftA2 :: (a -> b -> c) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite c

(*>) :: TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b

(<*) :: TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a

Applicative (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

pure :: a -> TcPluginM 'Solve a

(<*>) :: TcPluginM 'Solve (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b

liftA2 :: (a -> b -> c) -> TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve c

(*>) :: TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b

(<*) :: TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve a

Applicative (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

pure :: a -> TcPluginM 'Stop a

(<*>) :: TcPluginM 'Stop (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b

liftA2 :: (a -> b -> c) -> TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop c

(*>) :: TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b

(<*) :: TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop a

Functor (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

fmap :: (a -> b) -> TcPluginM 'Init a -> TcPluginM 'Init b

(<$) :: a -> TcPluginM 'Init b -> TcPluginM 'Init a

Functor (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

fmap :: (a -> b) -> TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b

(<$) :: a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite a

Functor (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

fmap :: (a -> b) -> TcPluginM 'Solve a -> TcPluginM 'Solve b

(<$) :: a -> TcPluginM 'Solve b -> TcPluginM 'Solve a

Functor (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

fmap :: (a -> b) -> TcPluginM 'Stop a -> TcPluginM 'Stop b

(<$) :: a -> TcPluginM 'Stop b -> TcPluginM 'Stop a

Monad (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

(>>=) :: TcPluginM 'Init a -> (a -> TcPluginM 'Init b) -> TcPluginM 'Init b

(>>) :: TcPluginM 'Init a -> TcPluginM 'Init b -> TcPluginM 'Init b

return :: a -> TcPluginM 'Init a

Monad (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

(>>=) :: TcPluginM 'Rewrite a -> (a -> TcPluginM 'Rewrite b) -> TcPluginM 'Rewrite b

(>>) :: TcPluginM 'Rewrite a -> TcPluginM 'Rewrite b -> TcPluginM 'Rewrite b

return :: a -> TcPluginM 'Rewrite a

Monad (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

(>>=) :: TcPluginM 'Solve a -> (a -> TcPluginM 'Solve b) -> TcPluginM 'Solve b

(>>) :: TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b

return :: a -> TcPluginM 'Solve a

Monad (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

(>>=) :: TcPluginM 'Stop a -> (a -> TcPluginM 'Stop b) -> TcPluginM 'Stop b

(>>) :: TcPluginM 'Stop a -> TcPluginM 'Stop b -> TcPluginM 'Stop b

return :: a -> TcPluginM 'Stop a

(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) => MonadThings (TcPluginM s)

Defined in GHC.TcPlugin.API.Internal

Methods

lookupThing :: Name -> TcPluginM s TyThing

lookupId :: Name -> TcPluginM s Id

lookupDataCon :: Name -> TcPluginM s DataCon

lookupTyCon :: Name -> TcPluginM s TyCon

MonadTcPlugin (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Init a

unsafeLiftTcM :: TcM a -> TcPluginM 'Init a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Init a -> TcM a) -> TcM b) -> TcPluginM 'Init b

MonadTcPlugin (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Rewrite a

unsafeLiftTcM :: TcM a -> TcPluginM 'Rewrite a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Rewrite a -> TcM a) -> TcM b) -> TcPluginM 'Rewrite b

MonadTcPlugin (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Solve a

unsafeLiftTcM :: TcM a -> TcPluginM 'Solve a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Solve a -> TcM a) -> TcM b) -> TcPluginM 'Solve b

MonadTcPlugin (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

liftTcPluginM :: TcPluginM0 a -> TcPluginM 'Stop a

unsafeLiftTcM :: TcM a -> TcPluginM 'Stop a

unsafeWithRunInTcM :: ((forall a. TcPluginM 'Stop a -> TcM a) -> TcM b) -> TcPluginM 'Stop b

(TypeError ('Text "Cannot emit new work in 'tcPluginInit'.") :: Constraint) => MonadTcPluginWork (TcPluginM 'Init)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Init BuiltinDefs

MonadTcPluginWork (TcPluginM 'Rewrite)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Rewrite BuiltinDefs

MonadTcPluginWork (TcPluginM 'Solve)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Solve BuiltinDefs

(TypeError ('Text "Cannot emit new work in 'tcPluginStop'.") :: Constraint) => MonadTcPluginWork (TcPluginM 'Stop)

Defined in GHC.TcPlugin.API.Internal

Methods

askBuiltins :: TcPluginM 'Stop BuiltinDefs

newtype TcPluginM 'Init a

Defined in GHC.TcPlugin.API.Internal

newtype TcPluginM 'Init a = TcPluginInitM {

• tcPluginInitM :: TcPluginM a

}

newtype TcPluginM 'Rewrite a

Defined in GHC.TcPlugin.API.Internal

newtype TcPluginM 'Rewrite a = TcPluginRewriteM {

• tcPluginRewriteM :: BuiltinDefs -> RewriteEnv -> TcPluginM a

}

newtype TcPluginM 'Solve a

Defined in GHC.TcPlugin.API.Internal

newtype TcPluginM 'Solve a = TcPluginSolveM {

• tcPluginSolveM :: BuiltinDefs -> EvBindsVar -> [Ct] -> TcPluginM a

}

newtype TcPluginM 'Stop a

Defined in GHC.TcPlugin.API.Internal

newtype TcPluginM 'Stop a = TcPluginStopM {

• tcPluginStopM :: TcPluginM a

}

data TcPluginErrorMessage

Use this type like 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 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 setCtLocM.

Constructors

Txt !String

Show the text as is.

PrintType !Type

Pretty print the given type.

(:|:) !TcPluginErrorMessage !TcPluginErrorMessage infixl 5

Put two messages side by side.

(:-:) !TcPluginErrorMessage !TcPluginErrorMessage infixl 6

Stack two messages vertically.

type TcPluginRewriter

Arguments

 = [Ct]

Givens

-> [Type]

Type family arguments (saturated)

-> TcPluginM Rewrite TcPluginRewriteResult

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.

class Monad m => MonadThings (m :: Type -> Type) where

Class that abstracts out the common ability of the monads in GHC to lookup a TyThing in the monadic environment by Name. Provides a number of related convenience functions for accessing particular kinds of TyThing

Minimal complete definition

lookupThing

Methods

lookupThing :: Name -> m TyThing

lookupId :: Name -> m Id

lookupDataCon :: Name -> m DataCon

lookupTyCon :: Name -> m TyCon

Instances

MonadThings TcS

Defined in GHC.Tc.Solver.Monad

Methods

lookupThing :: Name -> TcS TyThing

lookupId :: Name -> TcS Id

lookupDataCon :: Name -> TcS DataCon

lookupTyCon :: Name -> TcS TyCon

(Monad (TcPluginM s), MonadTcPlugin (TcPluginM s)) => MonadThings (TcPluginM s)

Defined in GHC.TcPlugin.API.Internal

Methods

lookupThing :: Name -> TcPluginM s TyThing

lookupId :: Name -> TcPluginM s Id

lookupDataCon :: Name -> TcPluginM s DataCon

lookupTyCon :: Name -> TcPluginM s TyCon

MonadThings m => MonadThings (ReaderT s m)

Defined in GHC.Types.TyThing

Methods

lookupThing :: Name -> ReaderT s m TyThing

lookupId :: Name -> ReaderT s m Id

lookupDataCon :: Name -> ReaderT s m DataCon

lookupTyCon :: Name -> ReaderT s m TyCon

askRewriteEnv :: TcPluginM Rewrite RewriteEnv

Ask for the current rewriting environment.

Only available in the rewriter part of the type-checking plugin.

askDeriveds :: TcPluginM Solve [Ct]

Ask for the Derived constraints that the solver was provided with.

Always returns the empty list on GHC 9.4 or above.

askEvBinds :: TcPluginM Solve EvBindsVar

Ask for the evidence currently gathered by the type-checker.

Only available in the solver part of the type-checking plugin.

mkTcPlugin

Arguments

:: TcPlugin

type-checking plugin written with this library

-> TcPlugin

type-checking plugin for GHC

Use this function to create a type-checker plugin to pass to GHC.

mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m PredType

Create an error type with the desired error message.

The result can be paired with a CtLoc in order to throw a type error, for instance by using newWanted.