Main functions for manipulating types and typerelated things
 data TyThing
 data Type
 data PredType
 type ThetaType = [PredType]
 mkTyVarTy :: TyVar > Type
 mkTyVarTys :: [TyVar] > [Type]
 getTyVar :: String > Type > TyVar
 getTyVar_maybe :: Type > Maybe TyVar
 mkAppTy :: Type > Type > Type
 mkAppTys :: Type > [Type] > Type
 splitAppTy :: Type > (Type, Type)
 splitAppTys :: Type > (Type, [Type])
 splitAppTy_maybe :: Type > Maybe (Type, Type)
 repSplitAppTy_maybe :: Type > Maybe (Type, Type)
 mkFunTy :: Type > Type > Type
 mkFunTys :: [Type] > Type > Type
 splitFunTy :: Type > (Type, Type)
 splitFunTy_maybe :: Type > Maybe (Type, Type)
 splitFunTys :: Type > ([Type], Type)
 splitFunTysN :: Int > Type > ([Type], Type)
 funResultTy :: Type > Type
 funArgTy :: Type > Type
 zipFunTys :: Outputable a => [a] > Type > ([(a, Type)], Type)
 mkTyConApp :: TyCon > [Type] > Type
 mkTyConTy :: TyCon > Type
 tyConAppTyCon :: Type > TyCon
 tyConAppArgs :: Type > [Type]
 splitTyConApp_maybe :: Type > Maybe (TyCon, [Type])
 splitTyConApp :: Type > (TyCon, [Type])
 mkForAllTy :: TyVar > Type > Type
 mkForAllTys :: [TyVar] > Type > Type
 splitForAllTy_maybe :: Type > Maybe (TyVar, Type)
 splitForAllTys :: Type > ([TyVar], Type)
 applyTy :: Type > Type > Type
 applyTys :: Type > [Type] > Type
 applyTysD :: SDoc > Type > [Type] > Type
 isForAllTy :: Type > Bool
 dropForAlls :: Type > Type
 newTyConInstRhs :: TyCon > [Type] > Type
 carefullySplitNewType_maybe :: [TyCon] > TyCon > [Type] > Maybe ([TyCon], Type)
 tyFamInsts :: Type > [(TyCon, [Type])]
 predFamInsts :: PredType > [(TyCon, [Type])]
 mkPredTy :: PredType > Type
 mkPredTys :: ThetaType > [Type]
 mkFamilyTyConApp :: TyCon > [Type] > Type
 isEqPred :: PredType > Bool
 coVarPred :: CoVar > PredType
 funTyCon :: TyCon
 isTyVarTy :: Type > Bool
 isFunTy :: Type > Bool
 isDictTy :: Type > Bool
 isUnLiftedType :: Type > Bool
 isUnboxedTupleType :: Type > Bool
 isAlgType :: Type > Bool
 isClosedAlgType :: Type > Bool
 isPrimitiveType :: Type > Bool
 isStrictType :: Type > Bool
 isStrictPred :: PredType > Bool
 type Kind = Type
 type SimpleKind = Kind
 type KindVar = TyVar
 liftedTypeKind :: Kind
 unliftedTypeKind :: Kind
 openTypeKind :: Kind
 argTypeKind :: Kind
 ubxTupleKind :: Kind
 tySuperKind :: SuperKind
 coSuperKind :: SuperKind
 liftedTypeKindTyCon :: TyCon
 openTypeKindTyCon :: TyCon
 unliftedTypeKindTyCon :: TyCon
 argTypeKindTyCon :: TyCon
 ubxTupleKindTyCon :: TyCon
 tyVarsOfType :: Type > TyVarSet
 tyVarsOfTypes :: [Type] > TyVarSet
 tyVarsOfPred :: PredType > TyVarSet
 tyVarsOfTheta :: ThetaType > TyVarSet
 expandTypeSynonyms :: Type > Type
 coreEqType :: Type > Type > Bool
 coreEqType2 :: RnEnv2 > Type > Type > Bool
 tcEqType :: Type > Type > Bool
 tcEqTypes :: [Type] > [Type] > Bool
 tcCmpType :: Type > Type > Ordering
 tcCmpTypes :: [Type] > [Type] > Ordering
 tcEqPred :: PredType > PredType > Bool
 tcEqPredX :: RnEnv2 > PredType > PredType > Bool
 tcCmpPred :: PredType > PredType > Ordering
 tcEqTypeX :: RnEnv2 > Type > Type > Bool
 tcPartOfType :: Type > Type > Bool
 tcPartOfPred :: Type > PredType > Bool
 seqType :: Type > ()
 seqTypes :: [Type] > ()
 coreView :: Type > Maybe Type
 tcView :: Type > Maybe Type
 kindView :: Kind > Maybe Kind
 repType :: Type > Type
 data PrimRep
 typePrimRep :: Type > PrimRep
 predTypeRep :: PredType > Type
 type TvSubstEnv = TyVarEnv Type
 data TvSubst = TvSubst InScopeSet TvSubstEnv
 emptyTvSubstEnv :: TvSubstEnv
 emptyTvSubst :: TvSubst
 mkTvSubst :: InScopeSet > TvSubstEnv > TvSubst
 mkOpenTvSubst :: TvSubstEnv > TvSubst
 zipOpenTvSubst :: [TyVar] > [Type] > TvSubst
 zipTopTvSubst :: [TyVar] > [Type] > TvSubst
 mkTopTvSubst :: [(TyVar, Type)] > TvSubst
 notElemTvSubst :: TyVar > TvSubst > Bool
 getTvSubstEnv :: TvSubst > TvSubstEnv
 setTvSubstEnv :: TvSubst > TvSubstEnv > TvSubst
 zapTvSubstEnv :: TvSubst > TvSubst
 getTvInScope :: TvSubst > InScopeSet
 extendTvInScope :: TvSubst > Var > TvSubst
 extendTvInScopeList :: TvSubst > [Var] > TvSubst
 extendTvSubst :: TvSubst > TyVar > Type > TvSubst
 extendTvSubstList :: TvSubst > [TyVar] > [Type] > TvSubst
 isInScope :: Var > TvSubst > Bool
 composeTvSubst :: InScopeSet > TvSubstEnv > TvSubstEnv > TvSubstEnv
 zipTyEnv :: [TyVar] > [Type] > TvSubstEnv
 isEmptyTvSubst :: TvSubst > Bool
 unionTvSubst :: TvSubst > TvSubst > TvSubst
 substTy :: TvSubst > Type > Type
 substTys :: TvSubst > [Type] > [Type]
 substTyWith :: [TyVar] > [Type] > Type > Type
 substTysWith :: [TyVar] > [Type] > [Type] > [Type]
 substTheta :: TvSubst > ThetaType > ThetaType
 substPred :: TvSubst > PredType > PredType
 substTyVar :: TvSubst > TyVar > Type
 substTyVars :: TvSubst > [TyVar] > [Type]
 substTyVarBndr :: TvSubst > TyVar > (TvSubst, TyVar)
 deShadowTy :: TyVarSet > Type > Type
 lookupTyVar :: TvSubst > TyVar > Maybe Type
 pprType :: Type > SDoc
 pprParendType :: Type > SDoc
 pprTypeApp :: NamedThing a => a > [Type] > SDoc
 pprTyThingCategory :: TyThing > SDoc
 pprTyThing :: TyThing > SDoc
 pprForAll :: [TyVar] > SDoc
 pprPred :: PredType > SDoc
 pprEqPred :: (Type, Type) > SDoc
 pprTheta :: ThetaType > SDoc
 pprThetaArrow :: ThetaType > SDoc
 pprClassPred :: Class > [Type] > SDoc
 pprKind :: Kind > SDoc
 pprParendKind :: Kind > SDoc
 pprSourceTyCon :: TyCon > SDoc
Main data types representing Types
Types are one of:
 Unboxed
 Iff its representation is other than a pointer Unboxed types are also unlifted.
 Lifted
 Iff it has bottom as an element. Closures always have lifted types: i.e. any letbound identifier in Core must have a lifted type. Operationally, a lifted object is one that can be entered. Only lifted types may be unified with a type variable.
 Algebraic
 Iff it is a type with one or more constructors, whether
declared with
data
ornewtype
. An algebraic type is one that can be deconstructed with a case expression. This is not the same as lifted types, because we also include unboxed tuples in this classification.  Data
 Iff it is a type declared with
data
, or a boxed tuple.  Primitive
 Iff it is a builtin type that can't be expressed in Haskell.
Currently, all primitive types are unlifted, but that's not necessarily
the case: for example, Int
could be primitive.
Some primitive types are unboxed, such as Int#
, whereas some are boxed
but unlifted (such as ByteArray#
). The only primitive types that we
classify as algebraic are the unboxed tuples.
Some examples of type classifications that may make this a bit clearer are:
Type primitive boxed lifted algebraic  Int# Yes No No No ByteArray# Yes Yes No No (# a, b #) Yes No No Yes ( a, b ) No Yes Yes Yes [a] No Yes Yes Yes
A source type is a type that is a separate type as far as the type checker is
concerned, but which has a more lowlevel representation as far as CoretoCore
passes and the rest of the back end is concerned. Notably, PredTy
s are removed
from the representation type while they do exist in the source types.
You don't normally have to worry about this, as the utility functions in this module will automatically convert a source into a representation type if they are spotted, to the best of it's abilities. If you don't want this to happen, use the equivalent functions from the TcType module.
A typecheckablething, essentially anything that has a name
The key representation of types within the compiler
A type of the form PredTy p
represents a value whose type is
the Haskell predicate p
, where a predicate is what occurs before
the =>
in a Haskell type.
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"
Constructing and deconstructing types
mkTyVarTys :: [TyVar] > [Type]Source
getTyVar :: String > Type > TyVarSource
Attempts to obtain the type variable underlying a Type
, and panics with the
given message if this is not a type variable type. See also getTyVar_maybe
splitAppTy :: Type > (Type, Type)Source
Attempts to take a type application apart, as in splitAppTy_maybe
,
and panics if this is not possible
splitAppTys :: Type > (Type, [Type])Source
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.
splitAppTy_maybe :: Type > Maybe (Type, Type)Source
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!
repSplitAppTy_maybe :: Type > Maybe (Type, Type)Source
Does the AppTy split as in splitAppTy_maybe
, but assumes that
any Core view stuff is already done
mkFunTy :: Type > Type > TypeSource
Creates a function type from the given argument and result type
splitFunTy :: Type > (Type, Type)Source
Attempts to extract the argument and result types from a type, and
panics if that is not possible. See also splitFunTy_maybe
splitFunTy_maybe :: Type > Maybe (Type, Type)Source
Attempts to extract the argument and result types from a type
splitFunTys :: Type > ([Type], Type)Source
splitFunTysN :: Int > Type > ([Type], Type)Source
Split off exactly the given number argument types, and panics if that is not possible
funResultTy :: Type > TypeSource
Extract the function result type and panic if that is not possible
zipFunTys :: Outputable a => [a] > Type > ([(a, Type)], Type)Source
Splits off argument types from the given type and associating them with the things in the input list from left to right. The final result type is returned, along with the resulting pairs of objects and types, albeit with the list of pairs in reverse order. Panics if there are not enough argument types for the input list.
mkTyConApp :: TyCon > [Type] > TypeSource
A key function: builds a TyConApp
or FunTy
as apppropriate to its arguments.
Applies its arguments to the constructor from left to right
mkTyConTy :: TyCon > TypeSource
Create the plain type constructor type which has been applied to no type arguments at all.
tyConAppTyCon :: Type > TyConSource
The same as fst . splitTyConApp
tyConAppArgs :: Type > [Type]Source
The same as snd . splitTyConApp
splitTyConApp_maybe :: Type > Maybe (TyCon, [Type])Source
Attempts to tease a type apart into a type constructor and the application of a number of arguments to that constructor
splitTyConApp :: Type > (TyCon, [Type])Source
Attempts to tease a type apart into a type constructor and the application
of a number of arguments to that constructor. Panics if that is not possible.
See also splitTyConApp_maybe
mkForAllTy :: TyVar > Type > TypeSource
mkForAllTys :: [TyVar] > Type > TypeSource
Wraps foralls over the type using the provided TyVar
s from left to right
splitForAllTy_maybe :: Type > Maybe (TyVar, Type)Source
Attempts to take a forall type apart, returning the bound type variable and the remainder of the type
splitForAllTys :: Type > ([TyVar], Type)Source
Attempts to take a forall type apart, returning all the immediate such bound
type variables and the remainder of the type. Always suceeds, even if that means
returning an empty list of TyVar
s
applyTy :: Type > Type > TypeSource
Instantiate a forall type with one or more type arguments. Used when we have a polymorphic function applied to type args:
f t1 t2
We use applyTys typeoff [t1,t2]
to compute the type of the expression.
Panics if no application is possible.
applyTys :: Type > [Type] > TypeSource
This function is interesting because:
 The function may have more foralls than there are args
 Less obviously, it may have fewer foralls
For case 2. think of:
applyTys (forall a.a) [forall b.b, Int]
This really can happen, via dressing up polymorphic types with newtype clothing. Here's an example:
newtype R = R (forall a. a>a) foo = case undefined :: R of R f > f ()
isForAllTy :: Type > BoolSource
dropForAlls :: Type > TypeSource
Equivalent to snd . splitForAllTys
newTyConInstRhs :: TyCon > [Type] > TypeSource
Unwrap one layer
of newtype on a type constructor and its arguments, using an
etareduced version of the newtype
if possible
tyFamInsts :: Type > [(TyCon, [Type])]Source
Finds type family instances occuring in a type after expanding synonyms.
predFamInsts :: PredType > [(TyCon, [Type])]Source
Finds type family instances occuring in a predicate type after expanding synonyms.
mkFamilyTyConApp :: TyCon > [Type] > TypeSource
Given a family instance TyCon and its arg types, return the corresponding family type. E.g:
data family T a data instance T (Maybe b) = MkT b
Where the instance tycon is :RTL, so:
mkFamilyTyConApp :RTL Int = T (Maybe Int)
Common type constructors
Predicates on types
isUnLiftedType :: Type > BoolSource
See Type for what an unlifted type is
isUnboxedTupleType :: Type > BoolSource
isAlgType :: Type > BoolSource
See Type for what an algebraic type is. Should only be applied to types, as opposed to e.g. partially saturated type constructors
isClosedAlgType :: Type > BoolSource
See Type for what an algebraic type is. Should only be applied to types, as opposed to e.g. partially saturated type constructors. Closed type constructors are those with a fixed right hand side, as opposed to e.g. associated types
isPrimitiveType :: Type > BoolSource
Returns true of types that are opaque to Haskell. Most of these are unlifted, but now that we interact with .NET, we may have primtive (foreignimported) types that are lifted
isStrictType :: Type > BoolSource
Computes whether an argument (or let right hand side) should
be computed strictly or lazily, based only on its type.
Works just like isUnLiftedType
, except that it has a special case
for dictionaries (i.e. does not work purely on representation types)
isStrictPred :: PredType > BoolSource
We may be strict in dictionary types, but only if it has more than one component.
(Being strict in a singlecomponent dictionary risks poking the dictionary component, which is wrong.)
Main data types representing Kinds
There's a little subtyping at the kind level:
? / \ / \ ?? (#) / \ * # . Where: * [LiftedTypeKind] means boxed type # [UnliftedTypeKind] means unboxed type (#) [UbxTupleKind] means unboxed tuple ?? [ArgTypeKind] is the lub of {*, #} ? [OpenTypeKind] means any type at all
In particular:
error :: forall a:?. String > a (>) :: ?? > ? > \* (\\(x::t) > ...)
Where in the last example t :: ??
(i.e. is not an unboxed tuple)
The key type representing kinds in the compiler. Invariant: a kind is always in one of these forms:
FunTy k1 k2 TyConApp PrimTyCon [...] TyVar kv  (during inference only) ForAll ...  (for toplevel coercions)
type SimpleKind = KindSource
Common Kinds and SuperKinds
tySuperKind :: SuperKindSource
coSuperKind :: SuperKindSource
Common Kind type constructors
Type free variables
tyVarsOfType :: Type > TyVarSetSource
NB: for type synonyms tyVarsOfType does not expand the synonym
tyVarsOfTypes :: [Type] > TyVarSetSource
expandTypeSynonyms :: Type > TypeSource
Expand out all type synonyms. Actually, it'd suffice to expand out just the ones that discard type variables (e.g. type Funny a = Int) But we don't know which those are currently, so we just expand all.
Type comparison
coreEqType :: Type > Type > BoolSource
Type equality test for Core types (i.e. ignores predicatetypes, synonyms etc.)
tcEqType :: Type > Type > BoolSource
Type equality on source types. Does not look through newtypes
or
PredType
s, but it does look through type synonyms.
tcCmpType :: Type > Type > OrderingSource
Type ordering on source types. Does not look through newtypes
or
PredType
s, but it does look through type synonyms.
tcCmpTypes :: [Type] > [Type] > OrderingSource
tcPartOfType :: Type > Type > BoolSource
Checks whether the second argument is a subterm of the first. (We don't care about binders, as we are only interested in syntactic subterms.)
tcPartOfPred :: Type > PredType > BoolSource
Forcing evaluation of types
Other views onto Types
coreView :: Type > Maybe TypeSource
In Core, we "look through" nonrecursive newtypes and PredTypes
: this
function tries to obtain a different view of the supplied type given this
Strips off the top layer only of a type to give its underlying representation type. Returns Nothing if there is nothing to look through.
In the case of newtype
s, it returns one of:
1) A vanilla TyConApp
(recursive newtype, or nonsaturated)
2) The newtype representation (otherwise), meaning the type written in the RHS of the newtype declaration, which may itself be a newtype
For example, with:
newtype R = MkR S newtype S = MkS T newtype T = MkT (T > T)
expandNewTcApp
on:

R
givesJust S
*S
givesJust T
*T
givesNothing
(no expansion)
tcView :: Type > Maybe TypeSource
Similar to coreView
, but for the type checker, which just looks through synonyms
Looks through:
 Foralls 2. Synonyms 3. Predicates 4. All newtypes, including recursive ones, but not newtype families
It's useful in the back end of the compiler.
Type representation for the code generator
A PrimRep
is an abstraction of a type. It contains information that
the code generator needs in order to pass arguments, return results,
and store values of this type.
typePrimRep :: Type > PrimRepSource
Discovers the primitive representation of a more abstract Type
predTypeRep :: PredType > TypeSource
Convert a PredType
to its representation type. However, it unwraps
only the outermost level; for example, the result might be a newtype application
Main type substitution data types
Type substitution
The following invariants must hold of a TvSubst
:
 The inscope set is needed only to guide the generation of fresh uniques
 In particular, the kind of the type variables in the inscope set is not relevant
 The substition is only applied ONCE! This is because in general such application will not reached a fixed point.
Manipulating type substitutions
mkTvSubst :: InScopeSet > TvSubstEnv > TvSubstSource
zipOpenTvSubst :: [TyVar] > [Type] > TvSubstSource
zipTopTvSubst :: [TyVar] > [Type] > TvSubstSource
mkTopTvSubst :: [(TyVar, Type)] > TvSubstSource
Called when doing toplevel substitutions. Here we expect that the free vars of the range of the substitution will be empty.
notElemTvSubst :: TyVar > TvSubst > BoolSource
setTvSubstEnv :: TvSubst > TvSubstEnv > TvSubstSource
extendTvInScope :: TvSubst > Var > TvSubstSource
extendTvInScopeList :: TvSubst > [Var] > TvSubstSource
composeTvSubst :: InScopeSet > TvSubstEnv > TvSubstEnv > TvSubstEnvSource
(compose env1 env2)(x)
is env1(env2(x))
; i.e. apply env2
then env1
.
It assumes that both are idempotent.
Typically, env1
is the refinement to a base substitution env2
zipTyEnv :: [TyVar] > [Type] > TvSubstEnvSource
isEmptyTvSubst :: TvSubst > BoolSource
unionTvSubst :: TvSubst > TvSubst > TvSubstSource
Performing substitution on types
substTyWith :: [TyVar] > [Type] > Type > TypeSource
Type substitution making use of an TvSubst
that
is assumed to be open, see zipOpenTvSubst
substTysWith :: [TyVar] > [Type] > [Type] > [Type]Source
Type substitution making use of an TvSubst
that
is assumed to be open, see zipOpenTvSubst
substTyVar :: TvSubst > TyVar > TypeSource
substTyVars :: TvSubst > [TyVar] > [Type]Source
deShadowTy :: TyVarSet > Type > TypeSource
Prettyprinting
pprParendType :: Type > SDocSource
pprTypeApp :: NamedThing a => a > [Type] > SDocSource
pprTyThing :: TyThing > SDocSource
pprThetaArrow :: ThetaType > SDocSource
pprClassPred :: Class > [Type] > SDocSource
pprParendKind :: Kind > SDocSource