Safe Haskell	None
Language	Haskell2010

GHC.Core.TyCo.Rep

Contents

Types
Coercions
Functions over types
Functions over binders
Functions over coercions
- Analyzing types
Sizes
Multiplicities

Synopsis

data TyThing
- = AnId Id
- | AConLike ConLike
- | ATyCon TyCon
- | ACoAxiom (CoAxiom Branched)
tyThingCategory :: TyThing -> String
pprTyThingCategory :: TyThing -> SDoc
pprShortTyThing :: TyThing -> SDoc
data Type
- = TyVarTy Var
- | AppTy Type Type
- | TyConApp TyCon [KindOrType]
- | ForAllTy !TyCoVarBinder Type
- | FunTy {
  - ft_af :: AnonArgFlag
  - ft_mult :: Mult
  - ft_arg :: Type
  - ft_res :: Type
  }
- | LitTy TyLit
- | CastTy Type KindCoercion
- | CoercionTy Coercion
data TyLit
- = NumTyLit Integer
- | StrTyLit FastString
type KindOrType = Type
type Kind = Type
type KnotTied ty = ty
type PredType = Type
type ThetaType = [PredType]
data ArgFlag where
- Invisible Specificity
- Required
- pattern Specified :: ArgFlag
- pattern Inferred :: ArgFlag
data AnonArgFlag
- = VisArg
- | InvisArg
data Coercion
- = Refl Type
- | GRefl Role Type MCoercionN
- | TyConAppCo Role TyCon [Coercion]
- | AppCo Coercion CoercionN
- | ForAllCo TyCoVar KindCoercion Coercion
- | FunCo Role CoercionN Coercion Coercion
- | CoVarCo CoVar
- | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
- | AxiomRuleCo CoAxiomRule [Coercion]
- | UnivCo UnivCoProvenance Role Type Type
- | SymCo Coercion
- | TransCo Coercion Coercion
- | NthCo Role Int Coercion
- | LRCo LeftOrRight CoercionN
- | InstCo Coercion CoercionN
- | KindCo Coercion
- | SubCo CoercionN
- | HoleCo CoercionHole
data UnivCoProvenance
- = PhantomProv KindCoercion
- | ProofIrrelProv KindCoercion
- | PluginProv String
data CoercionHole = CoercionHole {
- ch_co_var :: CoVar
- ch_blocker :: BlockSubstFlag
- ch_ref :: IORef (Maybe Coercion)
}
data BlockSubstFlag
- = YesBlockSubst
- | NoBlockSubst
coHoleCoVar :: CoercionHole -> CoVar
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
type CoercionN = Coercion
type CoercionR = Coercion
type CoercionP = Coercion
type KindCoercion = CoercionN
data MCoercion
- = MRefl
- | MCo Coercion
type MCoercionR = MCoercion
type MCoercionN = MCoercion
mkTyConTy :: TyCon -> Type
mkTyVarTy :: TyVar -> Type
mkTyVarTys :: [TyVar] -> [Type]
mkTyCoVarTy :: TyCoVar -> Type
mkTyCoVarTys :: [TyCoVar] -> [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
mkTyConApp :: TyCon -> [Type] -> Type
data TyCoBinder
- = Named TyCoVarBinder
- | Anon AnonArgFlag (Scaled Type)
type TyCoVarBinder = VarBndr TyCoVar ArgFlag
type TyBinder = TyCoBinder
binderVar :: VarBndr tv argf -> tv
binderVars :: [VarBndr tv argf] -> [tv]
binderType :: VarBndr TyCoVar argf -> Type
binderArgFlag :: VarBndr tv argf -> argf
delBinderVar :: VarSet -> TyCoVarBinder -> VarSet
isInvisibleArgFlag :: ArgFlag -> Bool
isVisibleArgFlag :: ArgFlag -> Bool
isInvisibleBinder :: TyCoBinder -> Bool
isVisibleBinder :: TyCoBinder -> Bool
isTyBinder :: TyCoBinder -> Bool
isNamedBinder :: TyCoBinder -> Bool
pickLR :: LeftOrRight -> (a, a) -> a
data TyCoFolder env a = TyCoFolder {
- tcf_view :: Type -> Maybe Type
- tcf_tyvar :: env -> TyVar -> a
- tcf_covar :: env -> CoVar -> a
- tcf_hole :: env -> CoercionHole -> a
- tcf_tycobinder :: env -> TyCoVar -> ArgFlag -> env
}
foldTyCo :: Monoid a => TyCoFolder env a -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
typeSize :: Type -> Int
coercionSize :: Coercion -> Int
provSize :: UnivCoProvenance -> Int
data Scaled a = Scaled Mult a
scaledMult :: Scaled a -> Mult
scaledThing :: Scaled a -> a
mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type
type Mult = Type

Documentation

data TyThing Source #

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.

Constructors

AnId Id
AConLike ConLike
ATyCon TyCon
ACoAxiom (CoAxiom Branched)

Instances

Instances details

Outputable TyThing #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: TyThing -> SDoc Source # pprPrec :: Rational -> TyThing -> SDoc Source #
NamedThing TyThing #
Instance details Defined in GHC.Core.TyCo.Rep Methods getOccName :: TyThing -> OccName Source # getName :: TyThing -> Name Source #

tyThingCategory :: TyThing -> String Source #

pprTyThingCategory :: TyThing -> SDoc Source #

pprShortTyThing :: TyThing -> SDoc Source #

Types

data Type Source #

Constructors

TyVarTy Var	Vanilla type or kind variable (never a coercion variable)
AppTy Type Type	Type application to something other than a `TyCon`. Parameters: 1) Function: must not be a `TyConApp` or `CastTy`, must be another `AppTy`, or `TyVarTy` See Note [Respecting definitional equality] (EQ1) about the no `CastTy` requirement 2) Argument type
TyConApp TyCon [KindOrType]	Application of a `TyCon`, including newtypes and synonyms. Invariant: saturated applications of `FunTyCon` must use `FunTy` and saturated synonyms must use their own constructors. However, unsaturated `FunTyCon`s do appear as `TyConApp`s. Parameters: 1) Type constructor being applied to. 2) Type arguments. Might not have enough type arguments here to saturate the constructor. Even type synonyms are not necessarily saturated; for example unsaturated type synonyms can appear as the right hand side of a type synonym.
ForAllTy !TyCoVarBinder Type	A Π type. INVARIANT: If the binder is a coercion variable, it must be mentioned in the Type. See Note [Unused coercion variable in ForAllTy]
FunTy	FUN m t1 t2 Very common, so an important special case See Note [Function types]
Fields ft_af :: AnonArgFlag ft_mult :: Mult ft_arg :: Type ft_res :: Type
LitTy TyLit	Type literals are similar to type constructors.
CastTy Type KindCoercion	A kind cast. The coercion is always nominal. INVARIANT: The cast is never reflexive INVARIANT: The Type is not a CastTy (use TransCo instead) INVARIANT: The Type is not a ForAllTy over a type variable See Note [Respecting definitional equality] (EQ2), (EQ3), (EQ4)
CoercionTy Coercion	Injection of a Coercion into a type This should only ever be used in the RHS of an AppTy, in the list of a TyConApp, when applying a promoted GADT data constructor

Instances

Instances details

Data Type #
Instance details 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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type Source # toConstr :: Type -> Constr Source # dataTypeOf :: Type -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) Source # gmapT :: (forall b. Data b => b -> b) -> Type -> Type Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type Source #
Outputable Type #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: Type -> SDoc Source # pprPrec :: Rational -> Type -> SDoc Source #

data TyLit Source #

Constructors

NumTyLit Integer
StrTyLit FastString

Instances

Instances details

Eq TyLit #
Instance details Defined in GHC.Core.TyCo.Rep Methods (==) :: TyLit -> TyLit -> Bool # (/=) :: TyLit -> TyLit -> Bool #
Data TyLit #
Instance details Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyLit -> c TyLit Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyLit Source # toConstr :: TyLit -> Constr Source # dataTypeOf :: TyLit -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyLit) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyLit) Source # gmapT :: (forall b. Data b => b -> b) -> TyLit -> TyLit Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyLit -> r Source # gmapQ :: (forall d. Data d => d -> u) -> TyLit -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyLit -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyLit -> m TyLit Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyLit -> m TyLit Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyLit -> m TyLit Source #
Ord TyLit #
Instance details Defined in GHC.Core.TyCo.Rep Methods compare :: TyLit -> TyLit -> Ordering # (<) :: TyLit -> TyLit -> Bool # (<=) :: TyLit -> TyLit -> Bool # (>) :: TyLit -> TyLit -> Bool # (>=) :: TyLit -> TyLit -> Bool # max :: TyLit -> TyLit -> TyLit # min :: TyLit -> TyLit -> TyLit #
Outputable TyLit #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: TyLit -> SDoc Source # pprPrec :: Rational -> TyLit -> SDoc Source #

type KindOrType = Type Source #

The key representation of types within the compiler

type Kind = Type Source #

The key type representing kinds in the compiler.

type KnotTied ty = ty Source #

A type labeled KnotTied might have knot-tied tycons in it. See Note [Type checking recursive type and class declarations] in GHC.Tc.TyCl

type PredType = Type Source #

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"

type ThetaType = [PredType] Source #

A collection of PredTypes

data ArgFlag Source #

Argument Flag

Is something required to appear in source Haskell (Required), permitted by request (Specified) (visible type application), or prohibited entirely from appearing in source Haskell (Inferred)? See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep

Constructors

Invisible Specificity
Required

Bundled Patterns

pattern Specified :: ArgFlag
pattern Inferred :: ArgFlag

Instances

Instances details

Eq ArgFlag #
Instance details Defined in GHC.Types.Var Methods (==) :: ArgFlag -> ArgFlag -> Bool # (/=) :: ArgFlag -> ArgFlag -> Bool #
Data ArgFlag #
Instance details Defined in GHC.Types.Var Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ArgFlag -> c ArgFlag Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgFlag Source # toConstr :: ArgFlag -> Constr Source # dataTypeOf :: ArgFlag -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgFlag) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgFlag) Source # gmapT :: (forall b. Data b => b -> b) -> ArgFlag -> ArgFlag Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgFlag -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgFlag -> r Source # gmapQ :: (forall d. Data d => d -> u) -> ArgFlag -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgFlag -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgFlag -> m ArgFlag Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgFlag -> m ArgFlag Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgFlag -> m ArgFlag Source #
Ord ArgFlag #
Instance details Defined in GHC.Types.Var Methods compare :: ArgFlag -> ArgFlag -> Ordering # (<) :: ArgFlag -> ArgFlag -> Bool # (<=) :: ArgFlag -> ArgFlag -> Bool # (>) :: ArgFlag -> ArgFlag -> Bool # (>=) :: ArgFlag -> ArgFlag -> Bool # max :: ArgFlag -> ArgFlag -> ArgFlag # min :: ArgFlag -> ArgFlag -> ArgFlag #
Outputable ArgFlag #
Instance details Defined in GHC.Types.Var Methods ppr :: ArgFlag -> SDoc Source # pprPrec :: Rational -> ArgFlag -> SDoc Source #
Binary ArgFlag #
Instance details Defined in GHC.Types.Var Methods put_ :: BinHandle -> ArgFlag -> IO () Source # put :: BinHandle -> ArgFlag -> IO (Bin ArgFlag) Source # get :: BinHandle -> IO ArgFlag Source #
Outputable tv => Outputable (VarBndr tv ArgFlag) #
Instance details Defined in GHC.Types.Var Methods ppr :: VarBndr tv ArgFlag -> SDoc Source # pprPrec :: Rational -> VarBndr tv ArgFlag -> SDoc Source #

data AnonArgFlag Source #

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 `(->)`: an ordinary non-dependent arrow. The argument is visible in source code.
InvisArg	Used for `(=>)`: a non-dependent predicate arrow. The argument is invisible in source code.

Instances

Instances details

Eq AnonArgFlag #
Instance details Defined in GHC.Types.Var Methods (==) :: AnonArgFlag -> AnonArgFlag -> Bool # (/=) :: AnonArgFlag -> AnonArgFlag -> Bool #
Data AnonArgFlag #
Instance details Defined in GHC.Types.Var Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnonArgFlag -> c AnonArgFlag Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AnonArgFlag Source # toConstr :: AnonArgFlag -> Constr Source # dataTypeOf :: AnonArgFlag -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AnonArgFlag) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AnonArgFlag) Source # gmapT :: (forall b. Data b => b -> b) -> AnonArgFlag -> AnonArgFlag Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnonArgFlag -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnonArgFlag -> r Source # gmapQ :: (forall d. Data d => d -> u) -> AnonArgFlag -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> AnonArgFlag -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnonArgFlag -> m AnonArgFlag Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnonArgFlag -> m AnonArgFlag Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnonArgFlag -> m AnonArgFlag Source #
Ord AnonArgFlag #
Instance details Defined in GHC.Types.Var Methods compare :: AnonArgFlag -> AnonArgFlag -> Ordering # (<) :: AnonArgFlag -> AnonArgFlag -> Bool # (<=) :: AnonArgFlag -> AnonArgFlag -> Bool # (>) :: AnonArgFlag -> AnonArgFlag -> Bool # (>=) :: AnonArgFlag -> AnonArgFlag -> Bool # max :: AnonArgFlag -> AnonArgFlag -> AnonArgFlag # min :: AnonArgFlag -> AnonArgFlag -> AnonArgFlag #
Outputable AnonArgFlag #
Instance details Defined in GHC.Types.Var Methods ppr :: AnonArgFlag -> SDoc Source # pprPrec :: Rational -> AnonArgFlag -> SDoc Source #
Binary AnonArgFlag #
Instance details Defined in GHC.Types.Var Methods put_ :: BinHandle -> AnonArgFlag -> IO () Source # put :: BinHandle -> AnonArgFlag -> IO (Bin AnonArgFlag) Source # get :: BinHandle -> IO AnonArgFlag Source #

Coercions

data Coercion Source #

A Coercion is concrete evidence of the equality/convertibility of two types.

Constructors

Refl Type
GRefl Role Type MCoercionN
TyConAppCo Role TyCon [Coercion]
AppCo Coercion CoercionN
ForAllCo TyCoVar KindCoercion Coercion
FunCo Role CoercionN Coercion Coercion
CoVarCo CoVar
AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
AxiomRuleCo CoAxiomRule [Coercion]
UnivCo UnivCoProvenance Role Type Type
SymCo Coercion
TransCo Coercion Coercion
NthCo Role Int Coercion
LRCo LeftOrRight CoercionN
InstCo Coercion CoercionN
KindCo Coercion
SubCo CoercionN
HoleCo CoercionHole	See Note [Coercion holes] Only present during typechecking

Instances

Instances details

Data Coercion #
Instance details 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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Coercion Source # toConstr :: Coercion -> Constr Source # dataTypeOf :: Coercion -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Coercion) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion) Source # gmapT :: (forall b. Data b => b -> b) -> Coercion -> Coercion Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Coercion -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion Source #
Outputable Coercion #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: Coercion -> SDoc Source # pprPrec :: Rational -> Coercion -> SDoc Source #

data UnivCoProvenance Source #

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.

Constructors

PhantomProv KindCoercion	See Note [Phantom coercions]. Only in Phantom roled coercions
ProofIrrelProv KindCoercion	From the fact that any two coercions are considered equivalent. See Note [ProofIrrelProv]. Can be used in Nominal or Representational coercions
PluginProv String	From a plugin, which asserts that this coercion is sound. The string is for the use of the plugin.

Instances

Instances details

Data UnivCoProvenance #
Instance details 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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnivCoProvenance Source # toConstr :: UnivCoProvenance -> Constr Source # dataTypeOf :: UnivCoProvenance -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnivCoProvenance) Source # gmapT :: (forall b. Data b => b -> b) -> UnivCoProvenance -> UnivCoProvenance Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r Source # gmapQ :: (forall d. Data d => d -> u) -> UnivCoProvenance -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance Source #
Outputable UnivCoProvenance #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: UnivCoProvenance -> SDoc Source # pprPrec :: Rational -> UnivCoProvenance -> SDoc Source #

data CoercionHole Source #

A coercion to be filled in by the type-checker. See Note [Coercion holes]

Constructors

CoercionHole
Fields ch_co_var :: CoVar ch_blocker :: BlockSubstFlag ch_ref :: IORef (Maybe Coercion)

Instances

Instances details

Data CoercionHole #
Instance details 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 Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole Source # toConstr :: CoercionHole -> Constr Source # dataTypeOf :: CoercionHole -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoercionHole) Source # gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r Source # gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source #
Outputable CoercionHole #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: CoercionHole -> SDoc Source # pprPrec :: Rational -> CoercionHole -> SDoc Source #

data BlockSubstFlag Source #

Constructors

YesBlockSubst
NoBlockSubst

Instances

Instances details

Outputable BlockSubstFlag #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: BlockSubstFlag -> SDoc Source # pprPrec :: Rational -> BlockSubstFlag -> SDoc Source #

coHoleCoVar :: CoercionHole -> CoVar Source #

setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole Source #

type CoercionN = Coercion Source #

type CoercionR = Coercion Source #

type CoercionP = Coercion Source #

type KindCoercion = CoercionN Source #

data MCoercion Source #

A semantically more meaningful type to represent what may or may not be a useful Coercion.

Constructors

MRefl
MCo Coercion

Instances

Instances details

Data MCoercion #
Instance details Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MCoercion -> c MCoercion Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MCoercion Source # toConstr :: MCoercion -> Constr Source # dataTypeOf :: MCoercion -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MCoercion) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion) Source # gmapT :: (forall b. Data b => b -> b) -> MCoercion -> MCoercion Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MCoercion -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MCoercion -> r Source # gmapQ :: (forall d. Data d => d -> u) -> MCoercion -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> MCoercion -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion Source #
Outputable MCoercion #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: MCoercion -> SDoc Source # pprPrec :: Rational -> MCoercion -> SDoc Source #

type MCoercionR = MCoercion Source #

type MCoercionN = MCoercion Source #

Functions over types

mkTyConTy :: TyCon -> Type Source #

Create the plain type constructor type which has been applied to no type arguments at all.

mkTyVarTy :: TyVar -> Type Source #

mkTyVarTys :: [TyVar] -> [Type] Source #

mkTyCoVarTy :: TyCoVar -> Type Source #

mkTyCoVarTys :: [TyCoVar] -> [Type] Source #

mkFunTy :: AnonArgFlag -> Mult -> Type -> Type -> Type infixr 3 Source #

mkVisFunTy :: Mult -> Type -> Type -> Type infixr 3 Source #

mkInvisFunTy :: Mult -> Type -> Type -> Type infixr 3 Source #

mkVisFunTys :: [Scaled Type] -> Type -> Type Source #

Make nested arrow types

mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type Source #

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

mkForAllTys :: [TyCoVarBinder] -> Type -> Type Source #

Wraps foralls over the type using the provided TyCoVars from left to right

mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type Source #

Wraps foralls over the type using the provided InvisTVBinders from left to right

mkPiTy :: TyCoBinder -> Type -> Type Source #

mkPiTys :: [TyCoBinder] -> Type -> Type Source #

mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type Source #

mkScaledFunTy :: AnonArgFlag -> Scaled Type -> Type -> Type Source #

mkVisFunTyMany :: Type -> Type -> Type infixr 3 Source #

Special, common, case: Arrow type with mult Many

mkVisFunTysMany :: [Type] -> Type -> Type Source #

mkInvisFunTyMany :: Type -> Type -> Type infixr 3 Source #

mkInvisFunTysMany :: [Type] -> Type -> Type Source #

mkTyConApp :: TyCon -> [Type] -> Type Source #

A key function: builds a TyConApp or FunTy as appropriate to its arguments. Applies its arguments to the constructor from left to right.

Functions over binders

data TyCoBinder Source #

A TyCoBinder represents an argument to a function. TyCoBinders can be dependent (Named) or nondependent (Anon). They may also be visible or not. See Note [TyCoBinders]

Constructors

Named TyCoVarBinder
Anon AnonArgFlag (Scaled Type)

Instances

Instances details

Data TyCoBinder #
Instance details Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyCoBinder -> c TyCoBinder Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyCoBinder Source # toConstr :: TyCoBinder -> Constr Source # dataTypeOf :: TyCoBinder -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyCoBinder) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyCoBinder) Source # gmapT :: (forall b. Data b => b -> b) -> TyCoBinder -> TyCoBinder Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyCoBinder -> r Source # gmapQ :: (forall d. Data d => d -> u) -> TyCoBinder -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> TyCoBinder -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyCoBinder -> m TyCoBinder Source #
Outputable TyCoBinder #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: TyCoBinder -> SDoc Source # pprPrec :: Rational -> TyCoBinder -> SDoc Source #

type TyCoVarBinder = VarBndr TyCoVar ArgFlag Source #

Variable Binder

A TyCoVarBinder is the binder of a ForAllTy It's convenient to define this synonym here rather its natural home in GHC.Core.TyCo.Rep, because it's used in GHC.Core.DataCon.hs-boot

A TyVarBinder is a binder with only TyVar

type TyBinder = TyCoBinder Source #

TyBinder is like TyCoBinder, but there can only be TyVarBinder in the Named field.

binderVar :: VarBndr tv argf -> tv Source #

binderVars :: [VarBndr tv argf] -> [tv] Source #

binderType :: VarBndr TyCoVar argf -> Type Source #

binderArgFlag :: VarBndr tv argf -> argf Source #

delBinderVar :: VarSet -> TyCoVarBinder -> VarSet Source #

Remove the binder's variable from the set, if the binder has a variable.

isInvisibleArgFlag :: ArgFlag -> Bool Source #

Does this ArgFlag classify an argument that is not written in Haskell?

isVisibleArgFlag :: ArgFlag -> Bool Source #

Does this ArgFlag classify an argument that is written in Haskell?

isInvisibleBinder :: TyCoBinder -> Bool Source #

Does this binder bind an invisible argument?

isVisibleBinder :: TyCoBinder -> Bool Source #

Does this binder bind a visible argument?

isTyBinder :: TyCoBinder -> Bool Source #

If its a named binder, is the binder a tyvar? Returns True for nondependent binder. This check that we're really returning a *Ty*Binder (as opposed to a coercion binder). That way, if/when we allow coercion quantification in more places, we'll know we missed updating some function.

isNamedBinder :: TyCoBinder -> Bool Source #

Functions over coercions

pickLR :: LeftOrRight -> (a, a) -> a Source #

Analyzing types

data TyCoFolder env a Source #

Constructors

TyCoFolder
Fields tcf_view :: Type -> Maybe Type tcf_tyvar :: env -> TyVar -> a tcf_covar :: env -> CoVar -> a tcf_hole :: env -> CoercionHole -> a What to do with coercion holes. See Note [Coercion holes] in GHC.Core.TyCo.Rep. tcf_tycobinder :: env -> TyCoVar -> ArgFlag -> env The returned env is used in the extended scope

foldTyCo :: Monoid a => TyCoFolder env a -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a) Source #

Sizes

typeSize :: Type -> Int Source #

coercionSize :: Coercion -> Int Source #

provSize :: UnivCoProvenance -> Int Source #

Multiplicities

data Scaled a Source #

A shorthand for data with an attached Mult element (the multiplicity).

Constructors

Scaled Mult a

Instances

Instances details

Data a => Data (Scaled a) #
Instance details Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Scaled a -> c (Scaled a) Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Scaled a) Source # toConstr :: Scaled a -> Constr Source # dataTypeOf :: Scaled a -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Scaled a)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scaled a)) Source # gmapT :: (forall b. Data b => b -> b) -> Scaled a -> Scaled a Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scaled a -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scaled a -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Scaled a -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Scaled a -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scaled a -> m (Scaled a) Source #
Outputable a => Outputable (Scaled a) #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: Scaled a -> SDoc Source # pprPrec :: Rational -> Scaled a -> SDoc Source #

scaledMult :: Scaled a -> Mult Source #

scaledThing :: Scaled a -> a Source #

mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type Source #

Apply a function to both the Mult and the Type in a 'Scaled Type'

type Mult = Type Source #

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.