HORIZON HASKELLDocslts/ghc-9.14.x45dd5372026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 45dd537 · 2026-10-11

Moduleghc-tcplugin-api-0.20.1.0Haskell2010

GHC.TcPlugin.API

This module provides a unified interface for writing type-checking plugins for GHC.

It attempts to re-export all the functionality from GHC that is relevant to plugin authors, as well as providing utility functions to streamline certain common operations such as creating evidence (to solve constraints), rewriting type family applications, throwing custom type errors.

Consider making use of the table of contents to help navigate this documentation; don't hesitate to jump between sections to get an overview of the relevant aspects.

For an illustration of the functionality, check the examples in the associated GitHub repository.

The internal module GHC.TcPlugin.API.Internal can be used to directly lift and unlift computations in GHC's TcM monad, but it is hoped that the interface provided in this module is sufficient.

  • 74 types
  • 3 classes
  • 152 values

Basic TcPlugin functionality

0 declarations

The TcPlugin type

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

Constructors

  • forall s. TcPlugin
    • tcPluginInit :: TcPluginM 'Init s

      Initialize plugin (once per module), when starting the type-checker.

    • tcPluginSolve :: s -> TcPluginSolver

      Solve some constraints.

      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

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

    • tcPluginPostTc :: s -> TcPluginM 'PostTc ()

      Action to run at the end of typechecking a module, e.g. to intercept the final TcGblEnv/TcLclEnv at the end of typechecking, possibly modifying mutable fields.

      Should not terminate the plugin, as the plugin may continue to be invoked when desugaring the module (as the pattern-match checker may invoke the constraint solver).

    • tcPluginShutdown :: s -> IO ()

      Clean up after the plugin, when GHC is done processing the given module (e.g. after desugaring).

valuemkTcPlugin
  1. :: TcPlugin

    type-checking plugin written with this library

  2. -> TcPlugin

    type-checking plugin for GHC

#

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

Plugin state

A type-checker plugin can define its own state, corresponding to the existential parameter s in the definition of TcPlugin. This allows a plugin to look up information a single time on initialisation, and pass it on for access in all further invocations of the plugin.

For example:

data MyDefinitions { myTyFam :: !TyCon, myClass :: !Class }

Usually, the tcPluginInit part of the plugin looks up all this information and returns it:

myTcPluginInit :: TcPluginM Init MyDefinitions

This step should also be used to initialise any external tools, such as an external SMT solver.

This information will then be passed to other stages of the plugin:

myTcPluginSolve :: MyDefinitions -> TcPluginSolver

The type-checking plugin monads

Different stages of type-checking plugins have access to different information. For a unified interface, an MTL-style approach is used, with the MonadTcPlugin typeclass providing overloading (for operations that work in all stages).

datadata TcPluginStage
#

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

Constructors

classclass (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 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.

Instances4MonadTcPlugin
data familydata family TcPluginM (s :: TcPluginStage) :: Type -> Type
#

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

Instances25Monad, Functor, Applicative, MonadIO, MonadTcPlugin, MonadTcPluginWork, …

Emitting new work, and throwing type-errors

Some operations only make sense in the two main phases, solving and rewriting. This is captured by the MonadTcPluginWork typeclass, which allows emitting new work, including throwing type errors.

classclass MonadTcPlugin m => MonadTcPluginWork (m :: Type -> Type) where
#

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

See mkTcPluginErrorTy and GHC.TcPlugin.API.emitWork for functions which require this typeclass.

Instances4MonadTcPluginWork
datadata 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 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 setCtLocM.

Constructors

Name resolution

0 declarations

Name resolution is usually the first step in writing a type-checking plugin: plugins need to look up the names of the objects they want to manipulate.

The most convenient way to look up a Name is to bring the name into scope in the module defining the plugin, and use TemplateHaskellQuotes in conjunction with the lookupTHName function.

import Data.Maybe

lookupMaybeTyCon :: MonadTcPluginM m => m TyCon
lookupMaybeTyCon = lookupTHName ''Maybe >>= tcLookupTyCon

This is recommended over manually looking up the package and module name, because the manual method does not robustly deal with re-exports; one must specify the exact package/module which defines the identifier. For instance, to manually lookup the type family MyFam in module MyModule in package my-pkg:

lookupMyFam :: MonadTcPluginM m => m Name
lookupMyFam = do
   let modlName = mkModuleName "MyModule"
       pkgName  = Just $ fsLit "my-pkg"
   pkgQual    <- resolveImport      modlName pkgName
   findResult <- findImportedModule modlName pkgQual
   case findResult of
     Found _ myModule -> pure myModule
     _ -> error "MyPlugin couldn't find MyModule in my-pkg"

lookupMyFam :: MonadTcPlugin m => Module -> m TyCon
lookupMyFam myModule = tcLookupTyCon =<< lookupOrig myModule ( mkTcOcc "MyFam" )

Most of these operations should be performed in tcPluginInit, and passed on to the other stages: the plugin initialisation is called only once in each module that the plugin is used, whereas the solver and rewriter are usually called repeatedly.

Name resolution: TH method

Look up a Name from a Template Haskell Name (e.g. a Name constructed using TemplateHaskellQuotes).

Name resolution: manual method

Packages and modules

Use these functions to lookup a module, from the current package or imported packages.

newtypenewtype ModuleName
#

A ModuleName is essentially a simple string, e.g. Data.List.

Instances10Eq, Data, Ord, Show, NFData, Outputable, …
datadata FindResult
#

The result of searching for an imported module.

NB: FindResult manages both user source-import lookups (which can result in Module) as well as direct imports for interfaces (which always result in InstalledModule).

Constructors

newtypenewtype UnitId
#

A UnitId identifies a built library in a database and is used to generate unique symbols, etc. It's usually of the form:

pkgname-1.2:libname+hash

These UnitId are provided to us via the -this-unit-id flag.

The library in question may be definite or indefinite; if it is indefinite, none of the holes have been filled (we never install partially instantiated libraries as we can cheaply instantiate them on-the-fly, cf VirtUnit). Put another way, an installed unit id is either fully instantiated, or not instantiated at all.

Instances20Eq, Data, Ord, Show, NFData, Outputable, …
datadata PkgQual
#

Package-qualifier after renaming

Renaming detects if "this" or the unit-id of the home-unit was used as a package qualifier.

Instances5Eq, Data, Ord, Outputable, Binary

Names

Occurence names

The most basic type of name is the OccName, which is a simple textual name within a namespace (e.g. the class namespace), without any disambiguation (no module qualifier, etc).

Names

After having looked up the Module, we can obtain the full Name referred to by an OccName. This is fully unambiguous, as it contains a Unique identifier for the name.

Name resolution: resolving the Name to a TyCon, Class, DataCon, etc

Finally, we can obtain the actual objects we're interested in handling, such as classes, type families, data constructors... by looking them up using their Name.

Constraint solving

4 declarations

Type-checking plugins will often want to manipulate constraints, e.g. solve constraints that GHC can't solve on its own, or emit their own constraints.

There are two different constraint flavours:

  • Given constraints, which are already known and have evidence associated to them,

  • Wanted constraints, for which evidence has not yet been found.

When GHC can't solve a Wanted constraint, it will get reported to the user as a type error.

datadata TcPluginSolveResult
#

Result of running a solver plugin.

Constructors

  • TcPluginSolveResult
    • tcPluginInsolubleCts :: [Ct]

      Insoluble constraints found by the plugin.

      These constraints will be added to the inert set, and reported as insoluble to the user.

    • tcPluginSolvedCts :: [(EvTerm, Ct)]

      Solved constraints, together with their evidence.

      These are removed from the inert set, and the evidence for them is recorded.

    • tcPluginNewCts :: [Ct]

      New constraints that the plugin wishes to emit.

      These will be added to the work list.

patternpattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult
#

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.

patternpattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
#

The plugin has not found any contradictions,

The first field is for constraints that were solved. The second field contains new work, that should be processed by the constraint solver.

The tcPluginSolve method of a typechecker plugin will be invoked in two different ways:

  1. to simplify Given constraints. In this case, the tcPluginSolve function will not be passed any Wanted constraints, and

  2. to solve Wanted constraints.

The plugin can then respond in one of two ways:

  • with TcPluginOk solved new, where solved is a list of solved constraints and new is a list of new constraints for GHC to process;

  • with TcPluginContradiction contras, where contras is a list of impossible constraints, so that they can be turned into errors.

In both cases, the plugin must respond with constraints of the same flavour, i.e. in (1) it should return only Givens, and for (2) it should return only Wanteds; all other constraints will be ignored.

Getting started with constraint solving

To get started, it can be helpful to immediately print out all the constraints that the plugin is given, using tcPluginTrace:

solver _ givens wanteds = do
  tcPluginTrace "---Plugin start---" (ppr givens $$ ppr wanteds)
  pure $ TcPluginOk [] []

This creates a plugin that prints outs the constraints it is passed, without doing anything with them.

To see this output, you will need to pass the flags -ddump-tc-trace and -ddump-to-file to GHC. This will output the trace as a log file, and you can search for "---Plugin start---" to find the plugin inputs.

Note that pretty-printing in GHC is done using the Outputable type class. We use its ppr method to turn things into pretty-printable documents, and ($$) to combine documents vertically. If you need more capabilities for pretty-printing documents, import GHC's GHC.Utils.Outputable module.

Inspecting constraints & predicates

Canonical and non-canonical constraints

A constraint in GHC starts out as "non-canonical", which means that GHC doesn't know what type of constraint it is. GHC will inspect the constraint to turn it into a canonical form (class constraint, equality constraint, etc.) which satisfies certain invariants used during constraint solving.

Thus, whenever emitting new constraints, it is usually best to emit a non-canonical constraint, letting GHC canonicalise it.

Predicates

A type-checking plugin will usually need to inspect constraints, so that it can pick out the constraints it is going to interact with.

In general, type-checking plugins can encounter all sorts of constraints, whether in canonical form or not. In order to handle these constraints in a uniform manner, it is usually preferable to inspect each constraint's predicate, which can be obtained by using classifyPredType and ctPred.

This allows the plugin to determine what kind of constraints it is dealing with:

  • an equality constraint? at Nominal or Representational role?

  • a type-class constraint? for which class?

  • an irreducible constraint, e.g. something of the form c a?

  • a quantified constraint?

datadata Pred
#

A predicate in the solver. The solver tries to prove Wanted predicates from Given ones.

Handling type variables

typetype TyVar = Var
#

Type or kind Variable

typetype CoVar = Id
#

Coercion Variable

datadata MetaInfo
#

What restrictions are on this metavariable around unification? These are checked in GHC.Tc.Utils.Unify.checkTopShape

Instances1Outputable

Some further functions for inspecting constraints

valueeqType :: HasCallStack => Type -> Type -> Bool
#

Type equality comparing both visible and invisible arguments, expanding synonyms and respecting multiplicities.

valueisEqPred :: PredType -> Bool
#

Is this a primitive (unboxed) equality type, i.e. one of:

  • ~# (heterogeneous nominal unboxed equality),

  • ~R# (heterogeneous representational unboxed equality).

NB: returns False for **boxed** equalities such as (~), (~~) and Coercible. If you want to detect those, use isEqClassPred.

valueisEqClassPred :: PredType -> Bool
#

Is this a boxed equality type, i.e. one of:

  • (~) (homogeneous nominal boxed equality),

  • (~~) (heterogeneous nominal boxed equality),

  • Coercible (homogeneous boxed representational equality).

Constraint evidence

Coercions

Coercions are the evidence for type equalities. As such, when proving an equality, a type-checker plugin needs to construct the associated coercions.

valuemkSymCo :: Coercion -> Coercion
#

Create a symmetric version of the given Coercion that asserts equality between the same types but in the other "direction", so a kind of t1 ~ t2 becomes the kind t2 ~ t1.

Depending on outer Givens

When a plugin returns a coercion that depends on outer Given constraints, it should declare this dependency using the '[Coercion]' argument to functions such as mkPluginUnivCo, mkPluginUnivEvTerm and mkTyFamAppReduction in order to avoid this coercion getting floated out past such enclosing Givens.

You can use ctEvCoercion to obtain the coercion underlying an equality constraint (whether Given or Wanted). It is not possible to declare a dependency on non-equality constraints, and calling ctEvCoercion on a non-equality constraint will cause a crash.

Evidence terms

Typeclass constraints have a different notion of evidence: evidence terms.

A plugin that wants to solve a class constraint will need to provide an evidence term. Such evidence can be created from scratch, or it can be obtained by combining evidence that is already available.

valuemkPluginUnivEvTerm
  1. :: String

    Name of equality (for the plugin's internal use, or for debugging)

  2. -> Role
  3. -> [Coercion]

    Evidence that this proof term depends on (use ctEvCoercion)

  4. -> TcType

    LHS

  5. -> TcType

    RHS

  6. -> EvTerm
#

Conjure up an evidence term for an equality between two types at the given Role (Nominal or Representational).

This can be used to supply a proof of a wanted equality in TcPluginOk.

The plugin is responsible for not emitting any unsound equalities, such as an equality between Int and Float.

valueevDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
#

Apply an instance dictionary function to type and value arguments.

NB: different from evDFunApp defined in GHC, as this function returns an EvExpr rather than an EvTerm.

valueevDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvExpr
#

Apply a data constructor to type and value arguments.

NB: different from evDataConApp defined in GHC, as this function returns an EvExpr rather than an EvTerm.

valueevId :: EvId -> EvExpr
#

Any sort of evidence Id, including coercions

valueevCast :: EvExpr -> Coercion -> EvExpr
#

Cast an evidence expression by a coercion.

NB: different from evCast defined in GHC, as this function returns an EvExpr rather than an EvTerm.

Class dictionaries

To create evidence terms for class constraints, type-checking plugins need to be able to construct the appropriate dictionaries containing the values for the class methods.

The class dictionary constructor can be obtained using classDataCon. Functions from GHC.Core.Make, which is re-exported by this library, will be useful for constructing the necessary terms

For instance, we can apply the class data constructor using mkCoreConApps. Remember that the type-level arguments (the typeclass variables) come first, before the actual evidence term (the class dictionary expression).

Class instances

In some cases, a type-checking plugin might need to access the class instances that are currently in scope, e.g. to obtain certain evidence terms.

Emitting new constraints

valuenewWanted :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence
#

Create a new Wanted constraint.

Requires a location (so that error messages can say where the constraint came from, what things were in scope at that point, etc), as well as the actual constraint (encoded as a type).

The following functions allow plugins to create constraints for typeclasses and type equalities.

Deriveds

Derived constraints are like Wanted constraints, except that they don't require evidence in order to be solved, and won't be seen in error messages if they go unsolved.

Solver plugins usually ignore this type of constraint entirely. They occur mostly when dealing with functional dependencies and type-family injectivity annotations.

GHC 9.4 removes this flavour of constraints entirely, subsuming their uses into Wanted constraints.

valueaskDeriveds :: 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.

Location information and CtLocs

When creating new constraints, one still needs a mechanism allowing GHC to report a certain source location associated to them when throwing an error, as well as other information the type-checker was aware of at that point (e.g. available instances, given constraints, etc).

This is the purpose of CtLoc.

bumpCtLocDepth adds one to the "depth" of the constraint. Can help avoid loops, by triggering a "maximum depth exceeded" error.

Rewriting type-family applications

2 declarations
typetype TcPluginRewriter = [Ct] -> [Type] -> 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.

Querying for type family reductions

Specifying type family reductions

A plugin that wants to rewrite a type family application must provide two pieces of information:

  • the type that the type family application reduces to,

  • evidence for this reduction, i.e. a Coercion proving the equality.

In the rewriting stage, type-checking plugins have access to the rewriter environment RewriteEnv, which has information about the location of the type family application, the local type-checking environment, among other things.

Note that a plugin should provide a UniqFM from TyCon to rewriting functions, which specifies a rewriting function for each type family. Use emptyUFM or listToUFM to construct this map, or import the GHC module GHC.Types.Unique.FM for a more complete API.

valuerewriteEnvCtLoc :: RewriteEnv -> CtLoc
#

Obtain the CtLoc from a RewriteEnv.

This can be useful to obtain the location of the constraint currently being rewritten, so that newly emitted constraints can be given the same location information.

datadata RewriteEnv
#

A RewriteEnv carries the necessary context for performing rewrites (i.e. type family reductions and following filled-in metavariables) in the solver.

valuemkTyFamAppReduction
  1. :: String

    Name of reduction (for debugging)

  2. -> Role

    Role of reduction (Nominal or Representational)

  3. -> [Coercion]

    Evidence that this reduction depends on (use ctEvCoercion)

  4. -> TyCon

    Type family TyCon

  5. -> [TcType]

    Type family arguments

  6. -> TcType

    The type that the type family application reduces to

  7. -> Reduction
#

Provide a rewriting of a saturated type family application at the given Role (Nominal or Representational).

The result can be passed to TcPluginRewriteTo to specify the outcome of rewriting a type family application.

datadata Reduction
#

A Reduction is the result of an operation that rewrites a type ty_in. The Reduction includes the rewritten type ty_out and a Coercion co such that co :: ty_in ~ ty_out, where the role of the coercion is determined by the context. That is, the LHS type of the coercion is the original type ty_in, while its RHS type is the rewritten type ty_out.

A Reduction is always homogeneous, unless it is wrapped inside a HetReduction, which separately stores the kind coercion.

See Note [The Reduction type].

Constructors

Instances1Outputable

Handling Haskell types

0 declarations

Type variables

typetype TcTyVar = Var
#

Type variable that might be a metavariable

newtypenewtype Unique
#

Unique identifier.

The type of unique identifiers that are used in many places in GHC for fast ordering and equality tests. You should generate these with the functions from the UniqSupply module

These are sometimes also referred to as "keys" in comments in GHC.

Instances4Eq, Show, Outputable, Uniquable
typetype Kind = Type
#

The key type representing kinds in the compiler.

Type literals (natural numbers, type-level strings)

Creating and decomposing applications

valuemkTyConTy :: TyCon -> Type
#

(mkTyConTy tc) returns (TyConApp tc []) but arranges to share that TyConApp among all calls See Note [Sharing nullary TyConApps] So it's just an alias for tyConNullaryTy!

valuesplitAppTy_maybe :: Type -> Maybe (Type, Type)
#

Attempt to take a type application apart, whether it is a function, type constructor, or plain type application. Note that type family applications are NEVER unsaturated by this!

valuesplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
#

Recursively splits a type as far as is possible, leaving a residual type being applied to and the type arguments applied to it. Never fails, even if that means returning an empty list of type applications.

Data constructors

valuetyConSingleDataCon_maybe :: TyCon -> Maybe DataCon
#

If the given TyCon has a single data constructor, i.e. it is a data type with one alternative, a tuple type or a newtype then that constructor is returned. If the TyCon has more than one constructor, or represents a primitive or function type constructor then Nothing is returned.

Function types

valuemkForAllTy :: ForAllTyBinder -> Type -> Type
#

Like mkTyCoForAllTy, but does not check the occurrence of the binder See Note [Unused coercion variable in ForAllTy]

Kinds

typetype Mult = Type
#

Mult is a type alias for Type.

Mult must contain Type because multiplicity variables are mere type variables (of kind Multiplicity) in Haskell. So the simplest implementation is to make Mult be Type.

Multiplicities can be formed with: - One: GHC.Types.One (= oneDataCon) - Many: GHC.Types.Many (= manyDataCon) - Multiplication: GHC.Types.MultMul (= multMulTyCon)

So that Mult feels a bit more structured, we provide pattern synonyms and smart constructors for these.

Substitution

datadata Subst
#

Type & coercion & id substitution

The Subst data type defined in this module contains substitution for tyvar, covar and id. However, operations on IdSubstEnv (mapping from Id to CoreExpr) that require the definition of the Expr data type are defined in GHC.Core.Subst to avoid circular module dependency.

Instances1Outputable
valuemkTvSubstPrs :: [(TyVar, Type)] -> Subst
#

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No CoVars, please! The InScopeSet is just a thunk so with a bit of luck it'll never be evaluated

valueextendTvSubst :: Subst -> TyVar -> Type -> Subst
#

Add a substitution for a TyVar to the Subst The TyVar *must* be a real TyVar, and not a CoVar You must ensure that the in-scope set is such that Note [The substitution invariant] holds after extending the substitution like this.

valuectsSubst :: [Ct] -> Subst
#

Compute an idempotent substitution from a collection of constraints, in particular from inert Givens.

NB: don't pass any set of constraints to this function; they should form a terminating generalised substitution as in Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.InertSet.

Zonking

Zonking is the operation in which GHC actually switches out mutable unification variables for their actual filled in type.

See the Note [What is zonking?] in GHC's source code for more information.

Panicking

It is often better for type-checking plugins to panic when encountering a problem, as opposed to silently doing something wrong. Use pprPanic to throw an informative error message, so that users of your plugin can report an issue if a problem occurs.

Map-like data structures based on Uniques

Import GHC.Types.Unique.FM or GHC.Types.Unique.DFM for a more complete interface to maps whose keys are Uniques.

datadata UniqDFM (key :: k) ele
#

Type of unique deterministic finite maps

The key is just here to keep us honest. It's always safe to use a single type as key. If two types don't overlap in their uniques it's also safe to index the same map at multiple key types. But this is very much discouraged.

Instances7Functor, Foldable, Traversable, TrieMap, Data, Outputable, …
newtypenewtype UniqFM (key :: k) ele
#

A finite map from uniques of one type to elements in another type.

The key is just here to keep us honest. It's always safe to use a single type as key. If two types don't overlap in their uniques it's also safe to index the same map at multiple key types. But this is very much discouraged.

Instances6Functor, Eq, Data, Semigroup, Monoid, Outputable

The type-checking environment

1 declaration

Interacting with GHC's constraint solver

6 declarations
newtypenewtype TcS a
#
Instances10Monad, Functor, MonadFix, MonadFail, Applicative, MonadIO, …

Built-in types

0 declarations

This module also re-exports the built-in types that GHC already knows about.

This allows plugins to directly refer to e.g. the promoted data constructor True without having to look up its name.

Refer to GHC.Builtin.Names, GHC.Builtin.Types and GHC.Builtin.Types.Prim.

GHC types

49 declarations

These are the types that the plugin will inspect and manipulate.

END OF API DOCUMENTATION, RE-EXPORTS FOLLOW

Some basic types

typetype Arity = Int
#

The number of value arguments that can be applied to a value before it does "real work". So: fib 100 has arity 0 x -> fib x has arity 1 See also Note [Definition of arity] in GHC.Core.Opt.Arity

datadata Boxity
#
BoxedUnboxed
Instances4Eq, Data, Outputable, Binary
  • Eq BoxityDefined in ghc-9.14.1 · Language.Haskell.Syntax.Basic
  • Data BoxityDefined in ghc-9.14.1 · Language.Haskell.Syntax.Basic
  • Outputable BoxityDefined in ghc-9.14.1 · GHC.Types.Basic · orphan
  • Binary BoxityDefined in ghc-9.14.1 · GHC.Types.Basic · orphan
datadata PromotionFlag
#

Is a TyCon a promoted data constructor or just a normal type constructor?

NotPromotedIsPromoted
Instances6Eq, Data, Ord, NFData, Outputable, Binary

Names

datadata Name
#

A unique, unambiguous name for something, containing information about where that thing originated.

Instances17Eq, Data, Ord, NFData, NamedThing, Uniquable, …
datadata OccName
#

Occurrence Name

In this context that means: "classified (i.e. as a type name, value name, etc) but not qualified and not yet resolved"

Instances8Eq, Data, Ord, NFData, Outputable, Binary, …
datadata TyThing
#

A global typecheckable-thing, essentially anything that has a name. Not to be confused with a TcTyThing, which is also a typecheckable thing but in the *local* context. See GHC.Tc.Utils.Env for how to retrieve a TyThing given a Name.

Instances2NamedThing, Outputable
datadata Class
#
Instances6Eq, Data, NamedThing, Outputable, Uniquable, Lookupable
datadata DataCon
#

A data constructor

Instances8Eq, Data, NamedThing, Outputable, Uniquable, OutputableBndr, …
datadata TyCon
#

TyCons represent type constructors. Type constructors are introduced by things such as:

1) Data declarations: data Foo = ... creates the Foo type constructor of kind Type

2) Type synonyms: type Foo = ... creates the Foo type constructor

3) Newtypes: newtype Foo a = MkFoo ... creates the Foo type constructor of kind Type -> Type

4) Class declarations: class Foo where creates the Foo type constructor of kind Constraint

This data type also encodes a number of primitive, built in type constructors such as those for function and tuple types.

If you edit this type, you may need to update the GHC formalism See Note [GHC Formalism] in GHC.Core.Lint

Instances6Eq, Data, NamedThing, Outputable, Uniquable, Lookupable
typetype Id = Var
#

Identifier

datadata FastString
#

A FastString is a Modified UTF-8 encoded string together with a unique ID. All FastStrings are stored in a global hashtable to support fast O(1) comparison.

It is also associated with a lazy reference to the Z-encoding of this string which is used by the compiler internally.

Instances14Eq, Data, Show, IsString, Semigroup, Monoid, …

Constraints

datadata EqRel
#

A choice of equality relation. This is separate from the type Role because Phantom does not define a (non-trivial) equality relation.

NomEqReprEq
Instances3Eq, Ord, Outputable
  • Eq EqRelDefined in ghc-9.14.1 · GHC.Core.Predicate
  • Ord EqRelDefined in ghc-9.14.1 · GHC.Core.Predicate
  • Outputable EqRelDefined in ghc-9.14.1 · GHC.Core.Predicate
typetype FunDep a = ([a], [a])
#
datadata Ct
#

Constraint

Instances1Outputable
  • Outputable CtDefined in ghc-9.14.1 · GHC.Tc.Types.Constraint
datadata QCInst
#

A quantified constraint, also called a "local instance" (a simplified version of ClsInst).

See Note [Quantified constraints] in GHC.Tc.Solver.Solve

Instances1Outputable
datadata Type
#
Instances3Data, Outputable, Eq
typetype PredType = Type
#

A type of the form p of constraint kind represents a value whose type is the Haskell predicate p, where a predicate is what occurs before the => in a Haskell type.

We use PredType as documentation to mark those types that we guarantee to have this kind.

It can be expanded into its representation, but:

  • The type checker must treat it as opaque

  • The rest of the compiler treats it as transparent

Consider these examples:

f :: (Eq a) => a -> Int
g :: (?x :: Int -> Int) => a -> Int
h :: (r\l) => {r} => {l::Int | r}

Here the Eq a and ?x :: Int -> Int and rl are all called "predicates"

datadata InstEnvs
#

InstEnvs represents the combination of the global type class instance environment, the local type class instance environment, and the set of transitively reachable orphan modules (according to what modules have been directly imported) used to test orphan instance visibility.

Coercions and evidence
datadata Role
#

See Note [Roles] in GHC.Core.Coercion

Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.

NominalRepresentationalPhantom
Instances7Eq, Data, Ord, NFData, Outputable, Binary, …
  • Eq RoleDefined in ghc-9.14.1 · Language.Haskell.Syntax.Basic
  • Data RoleDefined in ghc-9.14.1 · Language.Haskell.Syntax.Basic
  • Ord RoleDefined in ghc-9.14.1 · Language.Haskell.Syntax.Basic
  • NFData RoleDefined in ghc-9.14.1 · GHC.Core.Coercion.Axiom · orphan
  • Outputable RoleDefined in ghc-9.14.1 · GHC.Core.Coercion.Axiom · orphan
  • Binary RoleDefined in ghc-9.14.1 · GHC.Core.Coercion.Axiom · orphan
  • type Anno (Maybe Role) = EpAnnCODefined in ghc-9.14.1 · GHC.Hs.Decls · orphan
datadata UnivCoProvenance
#

For simplicity, we have just one UnivCo that represents a coercion from some type to some other type, with (in general) no restrictions on the type. The UnivCoProvenance specifies more exactly what the coercion really is and why a program should (or shouldn't!) trust the coercion. It is reasonable to consider each constructor of UnivCoProvenance as a totally independent coercion form; their only commonality is that they don't tell you what types they coercion between. (That info is in the UnivCo constructor of Coercion.

Instances6Eq, Data, Ord, NFData, Outputable, Binary
datadata EvBind
#
Instances2Data, Outputable
datadata Expr b
#

This is the data type that represents GHCs core intermediate language. Currently GHC uses System FC https://www.microsoft.com/en-us/research/publication/system-f-with-type-equality-coercions/ for this purpose, which is closely related to the simpler and better known System F http://en.wikipedia.org/wiki/System_F.

We get from Haskell source to this Core language in a number of stages:

  1. The source code is parsed into an abstract syntax tree, which is represented by the data type GHC.Hs.Expr.HsExpr with the names being GHC.Types.Name.Reader.RdrNames

  2. This syntax tree is renamed, which attaches a Unique to every RdrName (yielding a Name) to disambiguate identifiers which are lexically identical. For example, this program:

     f x = let f x = x + 1
           in f (x - 2)

Would be renamed by having Uniques attached so it looked something like this:

     f_1 x_2 = let f_3 x_4 = x_4 + 1
               in f_3 (x_2 - 2)

But see Note [Shadowing in Core] below.

  1. The resulting syntax tree undergoes type checking (which also deals with instantiating type class arguments) to yield a GHC.Hs.Expr.HsExpr type that has GHC.Types.Id.Id as it's names.

  2. Finally the syntax tree is desugared from the expressive GHC.Hs.Expr.HsExpr type into this Expr type, which has far fewer constructors and hence is easier to perform optimization, analysis and code generation on.

The type parameter b is for the type of binders in the expression tree.

The language consists of the following elements:

  • Variables See Note [Variable occurrences in Core]

  • Primitive literals

  • Applications: note that the argument may be a Type. See Note [Representation polymorphism invariants]

  • Lambda abstraction See Note [Representation polymorphism invariants]

  • Recursive and non recursive lets. Operationally this corresponds to allocating a thunk for the things bound and then executing the sub-expression.

See Note [Core letrec invariant] See Note [Core let-can-float invariant] See Note [Representation polymorphism invariants] See Note [Core type and coercion invariant]

  • Case expression. Operationally this corresponds to evaluating the scrutinee (expression examined) to weak head normal form and then examining at most one level of resulting constructor (i.e. you cannot do nested pattern matching directly with this).

The binder gets bound to the value of the scrutinee, and the Type must be that of all the case alternatives

IMPORTANT: see Note [Case expression invariants]

  • Cast an expression to a particular type. This is used to implement newtypes (a newtype constructor or destructor just becomes a Cast in Core) and GADTs.

  • Ticks. These are used to represent all the source annotation we support: profiling SCCs, HPC ticks, and GHCi breakpoints.

  • A type: this should only show up at the top level of an Arg

  • A coercion

Constructors

Instances3Eq, Data, Outputable
typetype CoreBndr = Var
#

The common case for the type of binders and variables when we are manipulating the Core language within GHC

datadata TcEvDest
#

A place for type-checking evidence to go after it is generated.

  • Wanted equalities use HoleDest,

  • other Wanteds use EvVarDest.

Constructors

  • EvVarDest EvVar

    bind this var to the evidence EvVarDest is always used for non-type-equalities e.g. class constraints

  • HoleDest CoercionHole

    fill in this hole with the evidence HoleDest is always used for type-equalities See Note [Coercion holes] in GHC.Core.TyCo.Rep

Instances1Outputable

The type-checking environment

datadata TcGblEnv
#

TcGblEnv describes the top-level of the module at the point at which the typechecker is finished work. It is this structure that is handed on to the desugarer For state that needs to be updated during the typechecking phase and returned at end, use a TcRef (= IORef).

Instances3Quasi, ContainsModule, MonadThings

Source locations

datadata GenLocated l e
#

We attach SrcSpans to lots of things, so let's have a datatype for it.

Constructors

  • L l e
Instances179Semigroup, HasAnnotation, NoAnn, Functor, Foldable, Traversable, …

Pretty-printing

newtypenewtype SDoc
#

Represents a pretty-printable document.

To display an SDoc, use printSDoc, printSDocLn, bufLeftRenderSDoc, or renderWithContext. Avoid calling runSDoc directly as it breaks the abstraction layer.

Instances8IsString, Outputable, IsLine, IsDoc, IsOutput, JsRender, …
classclass Outputable a where
#

Class designating that some type has an SDoc representation

Methods

Instances900Outputable, …