| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
GHC.TcPlugin.API
Description
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.
Synopsis
- data TcPlugin = forall s.TcPlugin {
- tcPluginInit :: TcPluginM Init s
- tcPluginSolve :: s -> TcPluginSolver
- tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter
- tcPluginStop :: s -> TcPluginM Stop ()
- mkTcPlugin :: TcPlugin -> TcPlugin
- data TcPluginStage
- class Monad m => MonadTcPlugin m
- data family TcPluginM s
- tcPluginIO :: MonadTcPlugin m => IO a -> m a
- class MonadTcPlugin m => MonadTcPluginWork m
- data TcPluginErrorMessage
- mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m PredType
- findImportedModule :: MonadTcPlugin m => ModuleName -> Maybe FastString -> m FindResult
- fsLit :: String -> FastString
- mkModuleName :: String -> ModuleName
- type Module = GenModule Unit
- data ModuleName
- data FindResult
- = Found ModLocation Module
- | NoPackage Unit
- | FoundMultiple [(Module, ModuleOrigin)]
- | NotFound {
- fr_paths :: [FilePath]
- fr_pkg :: Maybe Unit
- fr_mods_hidden :: [Unit]
- fr_pkgs_hidden :: [Unit]
- fr_unusables :: [(Unit, UnusableUnitReason)]
- fr_suggestions :: [ModuleSuggestion]
- mkVarOcc :: String -> OccName
- mkDataOcc :: String -> OccName
- mkTyVarOcc :: String -> OccName
- mkTcOcc :: String -> OccName
- mkClsOcc :: String -> OccName
- lookupOrig :: MonadTcPlugin m => Module -> OccName -> m Name
- tcLookupTyCon :: MonadTcPlugin m => Name -> m TyCon
- tcLookupDataCon :: MonadTcPlugin m => Name -> m DataCon
- tcLookupClass :: MonadTcPlugin m => Name -> m Class
- tcLookupGlobal :: MonadTcPlugin m => Name -> m TyThing
- tcLookup :: MonadTcPlugin m => Name -> m TcTyThing
- tcLookupId :: MonadTcPlugin m => Name -> m Id
- promoteDataCon :: DataCon -> TyCon
- type TcPluginSolver = [Ct] -> [Ct] -> TcPluginM Solve TcPluginSolveResult
- data TcPluginSolveResult
- = TcPluginContradiction [Ct]
- | TcPluginOk {
- tcPluginSolvedCts :: [(EvTerm, Ct)]
- tcPluginNewCts :: [Ct]
- tcPluginTrace :: MonadTcPlugin m => String -> SDoc -> m ()
- mkNonCanonical :: CtEvidence -> Ct
- classifyPredType :: PredType -> Pred
- ctPred :: Ct -> PredType
- eqType :: Type -> Type -> Bool
- ctLoc :: Ct -> CtLoc
- ctEvidence :: Ct -> CtEvidence
- ctFlavour :: Ct -> CtFlavour
- ctEqRel :: Ct -> EqRel
- ctOrigin :: Ct -> CtOrigin
- mkPluginUnivCo :: String -> Role -> TcType -> TcType -> Coercion
- newCoercionHole :: PredType -> TcPluginM Solve CoercionHole
- mkReflCo :: Role -> Type -> Coercion
- mkSymCo :: Coercion -> Coercion
- mkTransCo :: Coercion -> Coercion -> Coercion
- mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
- mkCoercionTy :: Coercion -> Type
- isCoercionTy :: Type -> Bool
- isCoercionTy_maybe :: Type -> Maybe Coercion
- pattern Coercion :: Coercion -> Expr b
- mkPluginUnivEvTerm :: String -> Role -> TcType -> TcType -> EvTerm
- newEvVar :: PredType -> TcPluginM Solve EvVar
- setEvBind :: EvBind -> TcPluginM Solve ()
- evCoercion :: TcCoercion -> EvTerm
- evCast :: EvExpr -> TcCoercion -> EvTerm
- ctEvExpr :: CtEvidence -> EvExpr
- pattern Type :: Type -> Expr b
- classDataCon :: Class -> DataCon
- module GHC.Core.Make
- getInstEnvs :: MonadTcPlugin m => m InstEnvs
- newWanted :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence
- newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM Solve CtEvidence
- mkClassPred :: Class -> [Type] -> PredType
- mkPrimEqPredRole :: Role -> Type -> Type -> PredType
- askDeriveds :: TcPluginM Solve [Ct]
- newDerived :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence
- setCtLocM :: MonadTcPluginWork m => CtLoc -> m a -> m a
- setCtLocRewriteM :: TcPluginM Rewrite a -> TcPluginM Rewrite a
- bumpCtLocDepth :: CtLoc -> CtLoc
- type TcPluginRewriter = [Ct] -> [Type] -> TcPluginM Rewrite TcPluginRewriteResult
- data TcPluginRewriteResult
- matchFam :: MonadTcPlugin m => TyCon -> [TcType] -> m (Maybe Reduction)
- getFamInstEnvs :: MonadTcPlugin m => m (FamInstEnv, FamInstEnv)
- type FamInstEnv = UniqDFM TyCon FamilyInstEnv
- askRewriteEnv :: TcPluginM Rewrite RewriteEnv
- rewriteEnvCtLoc :: RewriteEnv -> CtLoc
- data RewriteEnv
- mkTyFamAppReduction :: String -> Role -> TyCon -> [TcType] -> TcType -> Reduction
- data Reduction = Reduction {}
- newUnique :: MonadTcPlugin m => m Unique
- newFlexiTyVar :: MonadTcPlugin m => Kind -> m TcTyVar
- isTouchableTcPluginM :: MonadTcPlugin m => TcTyVar -> m Bool
- mkTyVarTy :: TyVar -> Type
- mkTyVarTys :: [TyVar] -> [Type]
- isTyVarTy :: Type -> Bool
- getTyVar_maybe :: Type -> Maybe TyVar
- type TcType = Type
- type TcTyVar = Var
- data Unique
- type Kind = Type
- mkTyConTy :: TyCon -> Type
- mkTyConApp :: TyCon -> [Type] -> Type
- splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
- mkAppTy :: Type -> Type -> Type
- mkAppTys :: Type -> [Type] -> Type
- data AnonArgFlag
- type Mult = Type
- mkFunTy :: AnonArgFlag -> Mult -> Type -> Type -> Type
- mkVisFunTy :: Mult -> Type -> Type -> Type
- mkInvisFunTy :: Mult -> Type -> Type -> Type
- mkVisFunTys :: [Scaled Type] -> Type -> Type
- mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
- mkForAllTys :: [TyCoVarBinder] -> Type -> Type
- mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
- mkPiTy :: TyCoBinder -> Type -> Type
- mkPiTys :: [TyCoBinder] -> Type -> Type
- mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type
- mkScaledFunTy :: AnonArgFlag -> Scaled Type -> Type -> Type
- mkVisFunTyMany :: Type -> Type -> Type
- mkVisFunTysMany :: [Type] -> Type -> Type
- mkInvisFunTyMany :: Type -> Type -> Type
- mkInvisFunTysMany :: [Type] -> Type -> Type
- zonkTcType :: MonadTcPluginWork m => TcType -> m TcType
- zonkCt :: MonadTcPluginWork m => Ct -> m Ct
- data UniqDFM key ele
- lookupUDFM :: Uniquable key => UniqDFM key elt -> key -> Maybe elt
- lookupUDFM_Directly :: UniqDFM key elt -> Unique -> Maybe elt
- elemUDFM :: Uniquable key => key -> UniqDFM key elt -> Bool
- data UniqFM key ele
- emptyUFM :: UniqFM key elt
- listToUFM :: Uniquable key => [(key, elt)] -> UniqFM key elt
- getEnvs :: MonadTcPlugin m => m (TcGblEnv, TcLclEnv)
- module GHC.Builtin.Types
- data Name
- data OccName
- data TyThing
- data TcTyThing
- data Class
- data DataCon
- data TyCon
- type Id = Var
- data FastString
- data Pred
- data EqRel
- type FunDep a = ([a], [a])
- data CtFlavour
- data Ct
- data CtLoc
- data CtEvidence
- data CtOrigin
- data QCInst
- data CanEqLHS
- data Type
- type PredType = Type
- data InstEnvs
- data TcLevel
- data Coercion
- data Role
- data UnivCoProvenance
- data CoercionHole
- data EvBind
- data EvTerm
- type EvVar = EvId
- type EvExpr = CoreExpr
- data EvBindsVar
- data TcGblEnv
- data TcLclEnv
- data SDoc
- class Outputable a where
Basic TcPlugin functionality
The TcPlugin type
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
| |
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.
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).
data TcPluginStage Source #
Stage of a type-checking plugin, used as a data kind.
class Monad m => MonadTcPlugin m Source #
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
Instances
| MonadTcPlugin (TcPluginM 'Init) Source # | |
Defined in GHC.TcPlugin.API.Internal | |
| MonadTcPlugin (TcPluginM 'Rewrite) Source # | |
Defined in GHC.TcPlugin.API.Internal | |
| MonadTcPlugin (TcPluginM 'Solve) Source # | |
Defined in GHC.TcPlugin.API.Internal | |
| MonadTcPlugin (TcPluginM 'Stop) Source # | |
Defined in GHC.TcPlugin.API.Internal | |
data family TcPluginM s Source #
The monad used for a type-checker plugin, parametrised by
the TcPluginStage of the plugin.
Instances
tcPluginIO :: MonadTcPlugin m => IO a -> m a Source #
Run an IO computation within the plugin.
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.
class MonadTcPlugin m => MonadTcPluginWork m Source #
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) Source # | |
Defined in GHC.TcPlugin.API.Internal Methods askBuiltins :: TcPluginM 'Init BuiltinDefs | |
| MonadTcPluginWork (TcPluginM 'Rewrite) Source # | |
Defined in GHC.TcPlugin.API.Internal Methods askBuiltins :: TcPluginM 'Rewrite BuiltinDefs | |
| MonadTcPluginWork (TcPluginM 'Solve) Source # | |
Defined in GHC.TcPlugin.API.Internal Methods askBuiltins :: TcPluginM 'Solve BuiltinDefs | |
| (TypeError ('Text "Cannot emit new work in 'tcPluginStop'.") :: Constraint) => MonadTcPluginWork (TcPluginM 'Stop) Source # | |
Defined in GHC.TcPlugin.API.Internal Methods askBuiltins :: TcPluginM 'Stop BuiltinDefs | |
data TcPluginErrorMessage Source #
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. |
mkTcPluginErrorTy :: MonadTcPluginWork m => TcPluginErrorMessage -> m PredType Source #
Name resolution
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.
For instance, to lookup the type family MyFam in module MyModule in package my-pkg:
lookupMyModule :: MonadTcPlugin m => m Module
lookupMyModule = do
findResult <- findImportedModule ( mkModuleName "MyModule" ) ( Just $ fsLit "my-pkg" )
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.
Packages and modules
Use these functions to lookup a module, from the current package or imported packages.
Arguments
| :: MonadTcPlugin m | |
| => ModuleName | Module name, e.g. |
| -> Maybe FastString | Package name, e.g. |
| -> m FindResult |
Lookup a Haskell module from the given package.
fsLit :: String -> FastString #
mkModuleName :: String -> ModuleName #
data ModuleName #
A ModuleName is essentially a simple string, e.g. Data.List.
Instances
data 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
| Found ModLocation Module | The module was found |
| NoPackage Unit | The requested unit was not found |
| FoundMultiple [(Module, ModuleOrigin)] | _Error_: both in multiple packages |
| NotFound | Not found |
Fields
| |
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).
mkTyVarOcc :: String -> OccName #
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.
lookupOrig :: MonadTcPlugin m => Module -> OccName -> m Name Source #
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.
tcLookupTyCon :: MonadTcPlugin m => Name -> m TyCon Source #
Lookup a type constructor from its name (datatype, type synonym or type family).
tcLookupDataCon :: MonadTcPlugin m => Name -> m DataCon Source #
tcLookupClass :: MonadTcPlugin m => Name -> m Class Source #
Lookup a typeclass from its name.
tcLookupGlobal :: MonadTcPlugin m => Name -> m TyThing Source #
Lookup a global typecheckable-thing from its name.
tcLookup :: MonadTcPlugin m => Name -> m TcTyThing Source #
Lookup a typecheckable-thing available in a local context, such as a local type variable.
tcLookupId :: MonadTcPlugin m => Name -> m Id Source #
Lookup an identifier, such as a type variable.
promoteDataCon :: DataCon -> TyCon #
Constraint solving
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.
type TcPluginSolver Source #
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 TcPluginSolveResult #
Constructors
| TcPluginContradiction [Ct] | 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. |
| TcPluginOk | The first field is for constraints that were solved. These are removed from the inert set, and the evidence for them is recorded. The second field contains new work, that should be processed by the constraint solver. |
Fields
| |
The tcPluginSolve method of a typechecker plugin will be invoked
in two different ways:
- to simplify Given constraints. In this case, the
tcPluginSolvefunction will not be passed any Wanted constraints, and - to solve Wanted constraints.
The plugin can then respond in one of two ways:
- with
TcPluginOk solved new, wheresolvedis a list of solved constraints andnewis a list of new constraints for GHC to process; - with
TcPluginContradiction contras, wherecontrasis 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.
Arguments
| :: MonadTcPlugin m | |
| => String | Text at the top of the debug message. |
| -> SDoc | Formatted document to print (use the |
| -> m () |
Output some debugging information within the plugin.
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.
mkNonCanonical :: CtEvidence -> Ct #
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
NominalorRepresentationalrole? - a type-class constraint? for which class?
- an irreducible constraint, e.g. something of the form
c a? - a quantified constraint?
classifyPredType :: PredType -> Pred #
Some further functions for inspecting constraints
eqType :: Type -> Type -> Bool #
Type equality on source types. Does not look through newtypes or
PredTypes, but it does look through type synonyms.
This first checks that the kinds of the types are equal and then
checks whether the types are equal, ignoring casts and coercions.
(The kind check is a recursive call, but since all kinds have type
Type, there is no need to check the types of kinds.)
See also Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep.
ctEvidence :: Ct -> CtEvidence #
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.
Arguments
| :: String | Name of equality (for the plugin's internal use, or for debugging) |
| -> Role | |
| -> TcType | LHS |
| -> TcType | RHS |
| -> Coercion |
Conjure up a coercion witnessing an equality between two types
at the given Role (Nominal or Representational).
This amounts to telling GHC "believe me, these things are equal".
The plugin is responsible for not emitting any unsound coercions,
such as a coercion between Int and Float.
newCoercionHole :: PredType -> TcPluginM Solve CoercionHole Source #
Create a fresh coercion hole.
mkSymCo :: 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.
Arguments
| :: UnivCoProvenance | |
| -> Role | role of the built coercion, "r" |
| -> Type | t1 :: k1 |
| -> Type | t2 :: k2 |
| -> Coercion | :: t1 ~r t2 |
Make a universal coercion between two arbitrary types.
mkCoercionTy :: Coercion -> Type #
isCoercionTy :: Type -> Bool #
isCoercionTy_maybe :: Type -> Maybe Coercion #
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.
Arguments
| :: String | Name of equality (for the plugin's internal use, or for debugging) |
| -> Role | |
| -> TcType | LHS |
| -> TcType | RHS |
| -> 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.
evCoercion :: TcCoercion -> EvTerm #
evCast :: EvExpr -> TcCoercion -> EvTerm #
d |> co
ctEvExpr :: CtEvidence -> EvExpr #
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, re-exported here, will be useful for
constructing the necessary terms, e.g. mkCoreApp for an application.
classDataCon :: Class -> DataCon #
module GHC.Core.Make
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.
getInstEnvs :: MonadTcPlugin m => m InstEnvs Source #
Obtain all currently-reachable typeclass instances.
Emitting new constraints
newWanted :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence Source #
Create a new derived 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).
newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM Solve CtEvidence Source #
Create a new given constraint.
Unlike newWanted and newDerived, we need to supply evidence
for this constraint.
Use setCtLocM to pass along the location information,
as only the CtOrigin gets taken into account here.
The following functions allow plugins to create constraints for typeclasses and type equalities.
mkClassPred :: Class -> [Type] -> PredType #
mkPrimEqPredRole :: Role -> Type -> Type -> PredType #
Makes a lifted equality predicate at the given role
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.
askDeriveds :: TcPluginM Solve [Ct] Source #
Ask for the Derived constraints that the solver was provided with.
Always returns the empty list on GHC 9.4 or above.
newDerived :: MonadTcPluginWork m => CtLoc -> PredType -> m CtEvidence Source #
Create a new derived constraint. See also newWanted.
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.
setCtLocM :: MonadTcPluginWork m => CtLoc -> m a -> m a Source #
Set the location information for a computation, so that the constraint solver reports an error at the given location.
setCtLocRewriteM :: TcPluginM Rewrite a -> TcPluginM Rewrite a Source #
Use the RewriteEnv to set the CtLoc for a computation.
bumpCtLocDepth adds one to the "depth" of the constraint.
Can help avoid loops, by triggering a "maximum depth exceeded" error.
bumpCtLocDepth :: CtLoc -> CtLoc #
Rewriting type-family applications
type TcPluginRewriter Source #
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.
data TcPluginRewriteResult #
Constructors
| TcPluginNoRewrite | The plugin does not rewrite the type family application. |
| TcPluginRewriteTo | The plugin rewrites the type family application providing a rewriting together with evidence. The plugin can also emit additional wanted constraints. |
Fields
| |
Querying for type family reductions
matchFam :: MonadTcPlugin m => TyCon -> [TcType] -> m (Maybe Reduction) Source #
Ask GHC what a type family application reduces to.
Warning: can cause a loop when used within tcPluginRewrite.
getFamInstEnvs :: MonadTcPlugin m => m (FamInstEnv, FamInstEnv) Source #
Obtain all currently-reachable data/type family instances.
First result: external instances. Second result: instances in the current home package.
type FamInstEnv = UniqDFM TyCon FamilyInstEnv #
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
Coercionproving 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.
askRewriteEnv :: TcPluginM Rewrite RewriteEnv Source #
Ask for the current rewriting environment.
Only available in the rewriter part of the type-checking plugin.
rewriteEnvCtLoc :: RewriteEnv -> CtLoc Source #
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.
data RewriteEnv #
Arguments
| :: String | Name of reduction (for debugging) |
| -> Role | Role of reduction ( |
| -> TyCon | Type family |
| -> [TcType] | Type family arguments |
| -> TcType | The type that the type family application reduces to |
| -> 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.
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
| Reduction | |
Fields | |
Instances
| Outputable Reduction | |
Defined in GHC.Core.Reduction | |
Handling Haskell types
Type variables
newUnique :: MonadTcPlugin m => m Unique Source #
Create a new unique. Useful for generating new variables in the plugin.
newFlexiTyVar :: MonadTcPlugin m => Kind -> m TcTyVar Source #
Create a new meta-variable (unification variable) of the given kind.
isTouchableTcPluginM :: MonadTcPlugin m => TcTyVar -> m Bool Source #
Query whether a type variable is touchable:
- is it a unification variable (and not a skolem variable)?
- is it actually unifiable given the current TcLevel?
mkTyVarTys :: [TyVar] -> [Type] #
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.
Instances
| Show Unique | |
| Uniquable Unique | |
Defined in GHC.Types.Unique | |
| Outputable Unique | |
Defined in GHC.Types.Unique | |
| Eq Unique | |
Creating and decomposing applications
Create the plain type constructor type which has been applied to no type arguments at all.
mkTyConApp :: TyCon -> [Type] -> Type #
splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) #
Attempts to tease a type apart into a type constructor and the application of a number of arguments to that constructor
Function types
data AnonArgFlag #
The non-dependent version of ArgFlag.
See Note [AnonArgFlag]
Appears here partly so that it's together with its friends ArgFlag
and ForallVisFlag, but also because it is used in IfaceType, rather
early in the compilation chain
Constructors
| VisArg | Used for |
| InvisArg | Used for |
Instances
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.
mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type #
Like mkTyCoForAllTy, but does not check the occurrence of the binder
See Note [Unused coercion variable in ForAllTy]
mkForAllTys :: [TyCoVarBinder] -> Type -> Type #
Wraps foralls over the type using the provided TyCoVars from left to right
mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type #
Wraps foralls over the type using the provided InvisTVBinders from left to right
mkPiTy :: TyCoBinder -> Type -> Type #
mkPiTys :: [TyCoBinder] -> Type -> Type #
mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type #
mkScaledFunTy :: AnonArgFlag -> Scaled Type -> Type -> Type #
mkVisFunTyMany :: Type -> Type -> Type infixr 3 #
Special, common, case: Arrow type with mult Many
mkVisFunTysMany :: [Type] -> Type -> Type #
mkInvisFunTyMany :: Type -> Type -> Type infixr 3 #
mkInvisFunTysMany :: [Type] -> Type -> Type #
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.
zonkTcType :: MonadTcPluginWork m => TcType -> m TcType Source #
Zonk the given type, which takes the metavariables in the type and substitutes their actual value.
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.
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.
Instances
| Foldable (UniqDFM key) | Deterministic, in O(n log n). |
Defined in GHC.Types.Unique.DFM Methods fold :: Monoid m => UniqDFM key m -> m # foldMap :: Monoid m => (a -> m) -> UniqDFM key a -> m # foldMap' :: Monoid m => (a -> m) -> UniqDFM key a -> m # foldr :: (a -> b -> b) -> b -> UniqDFM key a -> b # foldr' :: (a -> b -> b) -> b -> UniqDFM key a -> b # foldl :: (b -> a -> b) -> b -> UniqDFM key a -> b # foldl' :: (b -> a -> b) -> b -> UniqDFM key a -> b # foldr1 :: (a -> a -> a) -> UniqDFM key a -> a # foldl1 :: (a -> a -> a) -> UniqDFM key a -> a # toList :: UniqDFM key a -> [a] # null :: UniqDFM key a -> Bool # length :: UniqDFM key a -> Int # elem :: Eq a => a -> UniqDFM key a -> Bool # maximum :: Ord a => UniqDFM key a -> a # minimum :: Ord a => UniqDFM key a -> a # | |
| Traversable (UniqDFM key) | Deterministic, in O(n log n). |
Defined in GHC.Types.Unique.DFM | |
| Functor (UniqDFM key) | |
| Uniquable key => TrieMap (UniqDFM key) | |
| (Data key, Data ele) => Data (UniqDFM key ele) | |
Defined in GHC.Types.Unique.DFM Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UniqDFM key ele -> c (UniqDFM key ele) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (UniqDFM key ele) # toConstr :: UniqDFM key ele -> Constr # dataTypeOf :: UniqDFM key ele -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (UniqDFM key ele)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (UniqDFM key ele)) # gmapT :: (forall b. Data b => b -> b) -> UniqDFM key ele -> UniqDFM key ele # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniqDFM key ele -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniqDFM key ele -> r # gmapQ :: (forall d. Data d => d -> u) -> UniqDFM key ele -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UniqDFM key ele -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniqDFM key ele -> m (UniqDFM key ele) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniqDFM key ele -> m (UniqDFM key ele) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniqDFM key ele -> m (UniqDFM key ele) # | |
| Outputable a => Outputable (UniqDFM key a) | |
Defined in GHC.Types.Unique.DFM | |
| type Key (UniqDFM key) | |
Defined in GHC.Data.TrieMap | |
lookupUDFM :: Uniquable key => UniqDFM key elt -> key -> Maybe elt #
lookupUDFM_Directly :: UniqDFM key elt -> Unique -> Maybe elt #
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.
Instances
| Functor (UniqFM key) | |
| (Data key, Data ele) => Data (UniqFM key ele) | |
Defined in GHC.Types.Unique.FM Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UniqFM key ele -> c (UniqFM key ele) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (UniqFM key ele) # toConstr :: UniqFM key ele -> Constr # dataTypeOf :: UniqFM key ele -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (UniqFM key ele)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (UniqFM key ele)) # gmapT :: (forall b. Data b => b -> b) -> UniqFM key ele -> UniqFM key ele # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniqFM key ele -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniqFM key ele -> r # gmapQ :: (forall d. Data d => d -> u) -> UniqFM key ele -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UniqFM key ele -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniqFM key ele -> m (UniqFM key ele) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniqFM key ele -> m (UniqFM key ele) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniqFM key ele -> m (UniqFM key ele) # | |
| Monoid (UniqFM key a) | |
| Semigroup (UniqFM key a) | |
| Outputable a => Outputable (UniqFM key a) | |
Defined in GHC.Types.Unique.FM | |
| Eq ele => Eq (UniqFM key ele) | |
The type-checking environment
getEnvs :: MonadTcPlugin m => m (TcGblEnv, TcLclEnv) Source #
Obtain the current global and local type-checking environments.
Built-in types
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.
module GHC.Builtin.Types
GHC types
These are the types that the plugin will inspect and manipulate.
END OF API DOCUMENTATION, RE-EXPORTS FOLLOW
Names
A unique, unambiguous name for something, containing information about where that thing originated.
Instances
| Data Name | |
Defined in GHC.Types.Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name # dataTypeOf :: Name -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) # gmapT :: (forall b. Data b => b -> b) -> Name -> Name # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name # | |
| NFData Name | |
Defined in GHC.Types.Name | |
| NamedThing Name | |
Defined in GHC.Types.Name | |
| HasOccName Name | |
Defined in GHC.Types.Name | |
| Uniquable Name | |
Defined in GHC.Types.Name | |
| Binary Name | Assumes that the |
| Outputable Name | |
Defined in GHC.Types.Name | |
| OutputableBndr Name | |
Defined in GHC.Types.Name Methods pprBndr :: BindingSite -> Name -> SDoc # pprPrefixOcc :: Name -> SDoc # pprInfixOcc :: Name -> SDoc # bndrIsJoin_maybe :: Name -> Maybe Int # | |
| Eq Name | |
| Ord Name | Caution: This instance is implemented via See |
| type Anno Name | |
Defined in GHC.Hs.Extension | |
| type Anno (LocatedN Name) | |
Defined in GHC.Hs.Binds | |
| type Anno [LocatedN Name] | |
Defined in GHC.Hs.Binds | |
Occurrence Name
In this context that means: "classified (i.e. as a type name, value name, etc) but not qualified and not yet resolved"
Instances
| Data OccName | |
Defined in GHC.Types.Name.Occurrence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OccName -> c OccName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OccName # toConstr :: OccName -> Constr # dataTypeOf :: OccName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OccName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OccName) # gmapT :: (forall b. Data b => b -> b) -> OccName -> OccName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OccName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OccName -> r # gmapQ :: (forall d. Data d => d -> u) -> OccName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> OccName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> OccName -> m OccName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OccName -> m OccName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OccName -> m OccName # | |
| NFData OccName | |
Defined in GHC.Types.Name.Occurrence | |
| HasOccName OccName | |
Defined in GHC.Types.Name.Occurrence | |
| Uniquable OccName | |
Defined in GHC.Types.Name.Occurrence | |
| Binary OccName | |
| Outputable OccName | |
Defined in GHC.Types.Name.Occurrence | |
| OutputableBndr OccName | |
Defined in GHC.Types.Name.Occurrence Methods pprBndr :: BindingSite -> OccName -> SDoc # pprPrefixOcc :: OccName -> SDoc # pprInfixOcc :: OccName -> SDoc # bndrIsJoin_maybe :: OccName -> Maybe Int # | |
| Eq OccName | |
| Ord OccName | |
Defined in GHC.Types.Name.Occurrence | |
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.
Instances
| NamedThing TyThing | |
Defined in GHC.Types.TyThing | |
| Outputable TyThing | |
Defined in GHC.Types.TyThing | |
A typecheckable thing available in a local context. Could be
AGlobal TyThing, but also lexically scoped variables, etc.
See GHC.Tc.Utils.Env for how to retrieve a TyThing given a Name.
Instances
| Outputable TcTyThing | |
Defined in GHC.Tc.Types | |
Instances
| Data Class | |
Defined in GHC.Core.Class Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Class -> c Class # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Class # dataTypeOf :: Class -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Class) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Class) # gmapT :: (forall b. Data b => b -> b) -> Class -> Class # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Class -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Class -> r # gmapQ :: (forall d. Data d => d -> u) -> Class -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Class -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Class -> m Class # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Class -> m Class # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Class -> m Class # | |
| NamedThing Class | |
Defined in GHC.Core.Class | |
| Uniquable Class | |
Defined in GHC.Core.Class | |
| Outputable Class | |
Defined in GHC.Core.Class | |
| Eq Class | |
A data constructor
Instances
| Data DataCon | |
Defined in GHC.Core.DataCon Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataCon -> c DataCon # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataCon # toConstr :: DataCon -> Constr # dataTypeOf :: DataCon -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataCon) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataCon) # gmapT :: (forall b. Data b => b -> b) -> DataCon -> DataCon # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataCon -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataCon -> r # gmapQ :: (forall d. Data d => d -> u) -> DataCon -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataCon -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataCon -> m DataCon # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataCon -> m DataCon # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataCon -> m DataCon # | |
| NamedThing DataCon | |
Defined in GHC.Core.DataCon | |
| Uniquable DataCon | |
Defined in GHC.Core.DataCon | |
| Outputable DataCon | |
Defined in GHC.Core.DataCon | |
| OutputableBndr DataCon | |
Defined in GHC.Core.DataCon Methods pprBndr :: BindingSite -> DataCon -> SDoc # pprPrefixOcc :: DataCon -> SDoc # pprInfixOcc :: DataCon -> SDoc # bndrIsJoin_maybe :: DataCon -> Maybe Int # | |
| Eq DataCon | |
TyCons represent type constructors. Type constructors are introduced by things such as:
1) Data declarations: data Foo = ... creates the Foo type constructor of
kind *
2) Type synonyms: type Foo = ... creates the Foo type constructor
3) Newtypes: newtype Foo a = MkFoo ... creates the Foo type constructor
of kind * -> *
4) Class declarations: class Foo where creates the Foo type constructor
of kind *
This data type also encodes a number of primitive, built in type constructors such as those for function and tuple types.
Instances
| Data TyCon | |
Defined in GHC.Core.TyCon Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyCon -> c TyCon # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyCon # dataTypeOf :: TyCon -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyCon) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCon) # gmapT :: (forall b. Data b => b -> b) -> TyCon -> TyCon # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyCon -> r # gmapQ :: (forall d. Data d => d -> u) -> TyCon -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyCon -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyCon -> m TyCon # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyCon -> m TyCon # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyCon -> m TyCon # | |
| NamedThing TyCon | |
Defined in GHC.Core.TyCon | |
| Uniquable TyCon | |
Defined in GHC.Core.TyCon | |
| Outputable TyCon | |
Defined in GHC.Core.TyCon | |
| Eq TyCon | |
data FastString #
A FastString is a 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.
Instances
Constraints
A predicate in the solver. The solver tries to prove Wanted predicates from Given ones.
A choice of equality relation. This is separate from the type Role
because Phantom does not define a (non-trivial) equality relation.
Instances
| Outputable EqRel | |
Defined in GHC.Core.Predicate | |
| Eq EqRel | |
| Ord EqRel | |
Instances
| Outputable Ct | |
Defined in GHC.Tc.Types.Constraint | |
data CtEvidence #
Instances
| Outputable CtEvidence | |
Defined in GHC.Tc.Types.Constraint Methods ppr :: CtEvidence -> SDoc # | |
Instances
| Outputable CtOrigin | |
Defined in GHC.Tc.Types.Origin | |
Instances
| Outputable QCInst | |
Defined in GHC.Tc.Types.Constraint | |
A CanEqLHS is a type that can appear on the left of a canonical
equality: a type variable or exactly-saturated type family application.
Instances
| Outputable CanEqLHS | |
Defined in GHC.Tc.Types.Constraint | |
Instances
| Data Type | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type # dataTypeOf :: Type -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) # gmapT :: (forall b. Data b => b -> b) -> Type -> Type # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r # gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type # | |
| Outputable Type | |
Defined in GHC.Core.TyCo.Rep | |
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"
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.
Instances
| Outputable TcLevel | |
Defined in GHC.Tc.Utils.TcType | |
| Eq TcLevel | |
| Ord TcLevel | |
Coercions and evidence
A Coercion is concrete evidence of the equality/convertibility
of two types.
Instances
| Data Coercion | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Coercion -> c Coercion # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Coercion # toConstr :: Coercion -> Constr # dataTypeOf :: Coercion -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Coercion) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion) # gmapT :: (forall b. Data b => b -> b) -> Coercion -> Coercion # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r # gmapQ :: (forall d. Data d => d -> u) -> Coercion -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion # | |
| Outputable Coercion | |
Defined in GHC.Core.TyCo.Rep | |
Constructors
| Nominal | |
| Representational | |
| Phantom |
Instances
| Data Role | |
Defined in GHC.Core.Coercion.Axiom Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role # dataTypeOf :: Role -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) # gmapT :: (forall b. Data b => b -> b) -> Role -> Role # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # | |
| Binary Role | |
| Outputable Role | |
Defined in GHC.Core.Coercion.Axiom | |
| Eq Role | |
| Ord Role | |
| type Anno (Maybe Role) | |
Defined in GHC.Hs.Decls | |
| type Anno (Maybe Role) | |
Defined in GHC.Hs.Decls | |
data 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.
Instances
| Data UnivCoProvenance | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnivCoProvenance # toConstr :: UnivCoProvenance -> Constr # dataTypeOf :: UnivCoProvenance -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnivCoProvenance) # gmapT :: (forall b. Data b => b -> b) -> UnivCoProvenance -> UnivCoProvenance # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r # gmapQ :: (forall d. Data d => d -> u) -> UnivCoProvenance -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance # | |
| Outputable UnivCoProvenance | |
Defined in GHC.Core.TyCo.Rep Methods ppr :: UnivCoProvenance -> SDoc # | |
data CoercionHole #
A coercion to be filled in by the type-checker. See Note [Coercion holes]
Instances
| Data CoercionHole | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoercionHole -> c CoercionHole # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole # toConstr :: CoercionHole -> Constr # dataTypeOf :: CoercionHole -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoercionHole) # gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r # gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole # | |
| Uniquable CoercionHole | |
Defined in GHC.Core.TyCo.Rep Methods getUnique :: CoercionHole -> Unique # | |
| Outputable CoercionHole | |
Defined in GHC.Core.TyCo.Rep Methods ppr :: CoercionHole -> SDoc # | |
Instances
| Outputable EvBind | |
Defined in GHC.Tc.Types.Evidence | |
Instances
| Data EvTerm | |
Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTerm -> c EvTerm # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTerm # toConstr :: EvTerm -> Constr # dataTypeOf :: EvTerm -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTerm) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm) # gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> EvTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm # | |
| Outputable EvTerm | |
Defined in GHC.Tc.Types.Evidence | |
data EvBindsVar #
Instances
| Uniquable EvBindsVar | |
Defined in GHC.Tc.Types.Evidence Methods getUnique :: EvBindsVar -> Unique # | |
| Outputable EvBindsVar | |
Defined in GHC.Tc.Types.Evidence Methods ppr :: EvBindsVar -> SDoc # | |
The type-checking environment
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).
Instances
| ContainsModule TcGblEnv | |
Defined in GHC.Tc.Types Methods extractModule :: TcGblEnv -> Module # | |
Pretty-printing
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.
Instances
| IsString SDoc | |
Defined in GHC.Utils.Outputable Methods fromString :: String -> SDoc # | |
| Outputable SDoc | |
Defined in GHC.Utils.Outputable | |
| OutputableP env SDoc | |
Defined in GHC.Utils.Outputable | |
class Outputable a where #
Class designating that some type has an SDoc representation