Safe Haskell	None
Language	GHC2021

GHC.Core.TyCo.Rep

Contents

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

Synopsis

data Type
- = TyVarTy Var
- | AppTy Type Type
- | TyConApp TyCon [KindOrType]
- | ForAllTy !ForAllTyBinder Type
- | FunTy {
  - ft_af :: FunTyFlag
  - ft_mult :: Mult
  - ft_arg :: Type
  - ft_res :: Type
  }
- | LitTy TyLit
- | CastTy Type KindCoercion
- | CoercionTy Coercion
data TyLit
- = NumTyLit Integer
- | StrTyLit FastString
- | CharTyLit Char
type KindOrType = Type
type Kind = Type
type RuntimeRepType = Type
type LevityType = Type
type KnotTied (ty :: k) = ty
type PredType = Type
type ThetaType = [PredType]
type FRRType = Type
data ForAllTyFlag where
- Invisible !Specificity
- Required
- pattern Inferred :: ForAllTyFlag
- pattern Specified :: ForAllTyFlag
data FunTyFlag
- = FTF_T_T
- | FTF_T_C
- | FTF_C_T
- | FTF_C_C
data Coercion
- = Refl Type
- | GRefl Role Type MCoercionN
- | TyConAppCo Role TyCon [Coercion]
- | AppCo Coercion CoercionN
- | ForAllCo {
  - fco_tcv :: TyCoVar
  - fco_visL :: !ForAllTyFlag
  - fco_visR :: !ForAllTyFlag
  - fco_kind :: KindCoercion
  - fco_body :: Coercion
  }
- | FunCo {
  - fco_role :: Role
  - fco_afl :: FunTyFlag
  - fco_afr :: FunTyFlag
  - fco_mult :: CoercionN
  - fco_arg :: Coercion
  - fco_res :: Coercion
  }
- | CoVarCo CoVar
- | AxiomCo CoAxiomRule [Coercion]
- | UnivCo {
  - uco_prov :: UnivCoProvenance
  - uco_role :: Role
  - uco_lty :: Type
  - uco_rty :: Type
  - uco_deps :: [Coercion]
  }
- | SymCo Coercion
- | TransCo Coercion Coercion
- | SelCo CoSel Coercion
- | LRCo LeftOrRight CoercionN
- | InstCo Coercion CoercionN
- | KindCo Coercion
- | SubCo CoercionN
- | HoleCo CoercionHole
data CoSel
- = SelTyCon Int Role
- | SelFun FunSel
- | SelForAll
data FunSel
- = SelMult
- | SelArg
- | SelRes
data UnivCoProvenance
- = PhantomProv
- | ProofIrrelProv
- | PluginProv String
data CoercionHole = CoercionHole {
- ch_co_var :: CoVar
- ch_ref :: IORef (Maybe Coercion)
}
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
mkNakedTyConTy :: TyCon -> Type
mkTyVarTy :: TyVar -> Type
mkTyVarTys :: [TyVar] -> [Type]
mkTyCoVarTy :: TyCoVar -> Type
mkTyCoVarTys :: [TyCoVar] -> [Type]
mkFunTy :: HasDebugCallStack => FunTyFlag -> Mult -> Type -> Type -> Type
mkNakedFunTy :: FunTyFlag -> Kind -> Kind -> Kind
mkVisFunTy :: HasDebugCallStack => Mult -> Type -> Type -> Type
mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type
mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type
mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type
tcMkVisFunTy :: Mult -> Type -> Type -> Type
tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
tcMkScaledFunTy :: Scaled Type -> Type -> Type
tcMkScaledFunTys :: [Scaled Type] -> Type -> Type
mkForAllTy :: ForAllTyBinder -> Type -> Type
mkForAllTys :: [ForAllTyBinder] -> Type -> Type
mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
mkPiTy :: HasDebugCallStack => PiTyBinder -> Type -> Type
mkPiTys :: HasDebugCallStack => [PiTyBinder] -> Type -> Type
mkVisFunTyMany :: HasDebugCallStack => Type -> Type -> Type
mkVisFunTysMany :: [Type] -> Type -> Type
nonDetCmpTyLit :: TyLit -> TyLit -> Ordering
cmpTyLit :: TyLit -> TyLit -> Ordering
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 -> ForAllTyFlag -> env
}
foldTyCo :: Monoid a => TyCoFolder env a -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
noView :: Type -> Maybe Type
typeSize :: Type -> Int
typesSize :: [Type] -> Int
coercionSize :: Coercion -> 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

Types

data Type #

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 !ForAllTyBinder Type
FunTy	FUN m t1 t2 Very common, so an important special case See Note [Function types]
Fields ft_af :: FunTyFlag 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 (EQ2) INVARIANT: The Type is not a CastTy (use TransCo instead) (EQ3) INVARIANT: The Type is not a ForAllTy over a tyvar (EQ4) See Note [Respecting definitional equality]
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

Outputable Type #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: Type -> SDoc #
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 #
Eq (DeBruijn Type) #
Instance details Defined in GHC.Core.Map.Type Methods (==) :: DeBruijn Type -> DeBruijn Type -> Bool Source # (/=) :: DeBruijn Type -> DeBruijn Type -> Bool Source #

data TyLit #

Constructors

NumTyLit Integer
StrTyLit FastString
CharTyLit Char

Instances

Instances details

Outputable TyLit #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: TyLit -> SDoc #
Eq TyLit #
Instance details Defined in GHC.Core.TyCo.Rep Methods (==) :: TyLit -> TyLit -> Bool Source # (/=) :: TyLit -> TyLit -> Bool Source #
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 #

type KindOrType = Type #

The key representation of types within the compiler

type Kind = Type #

The key type representing kinds in the compiler.

type RuntimeRepType = Type #

Type synonym used for types of kind RuntimeRep.

type LevityType = Type #

Type synonym used for types of kind Levity.

type KnotTied (ty :: k) = ty #

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 #

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] #

A collection of PredTypes

type FRRType = Type #

data ForAllTyFlag #

ForAllTyFlag

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, ForAllTyBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep

Constructors

Invisible !Specificity
Required

Bundled Patterns

pattern Inferred :: ForAllTyFlag
pattern Specified :: ForAllTyFlag

Instances

Instances details

NFData ForAllTyFlag #
Instance details Defined in GHC.Hs.Specificity Methods rnf :: ForAllTyFlag -> () Source #
Binary ForAllTyFlag #
Instance details Defined in GHC.Hs.Specificity Methods put_ :: WriteBinHandle -> ForAllTyFlag -> IO () # put :: WriteBinHandle -> ForAllTyFlag -> IO (Bin ForAllTyFlag) # get :: ReadBinHandle -> IO ForAllTyFlag #
Outputable ForAllTyFlag #
Instance details Defined in GHC.Hs.Specificity Methods ppr :: ForAllTyFlag -> SDoc #
Eq ForAllTyFlag #
Instance details Defined in Language.Haskell.Syntax.Specificity Methods (==) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source # (/=) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source #
Ord ForAllTyFlag #
Instance details Defined in Language.Haskell.Syntax.Specificity Methods compare :: ForAllTyFlag -> ForAllTyFlag -> Ordering Source # (<) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source # (<=) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source # (>) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source # (>=) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source # max :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag Source # min :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag Source #
Data ForAllTyFlag #
Instance details Defined in Language.Haskell.Syntax.Specificity Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ForAllTyFlag -> c ForAllTyFlag Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ForAllTyFlag Source # toConstr :: ForAllTyFlag -> Constr Source # dataTypeOf :: ForAllTyFlag -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ForAllTyFlag) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ForAllTyFlag) Source # gmapT :: (forall b. Data b => b -> b) -> ForAllTyFlag -> ForAllTyFlag Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ForAllTyFlag -> r Source # gmapQ :: (forall d. Data d => d -> u) -> ForAllTyFlag -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> ForAllTyFlag -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ForAllTyFlag -> m ForAllTyFlag Source #
OutputableBndrFlag ForAllTyFlag p #
Instance details Defined in GHC.Hs.Type Methods pprTyVarBndr :: HsTyVarBndr ForAllTyFlag (GhcPass p) -> SDoc
Outputable tv => Outputable (VarBndr tv ForAllTyFlag) #
Instance details Defined in GHC.Types.Var Methods ppr :: VarBndr tv ForAllTyFlag -> SDoc #

data FunTyFlag #

The non-dependent version of ForAllTyFlag. See Note [FunTyFlag] Appears here partly so that it's together with its friends ForAllTyFlag and ForallVisFlag, but also because it is used in IfaceType, rather early in the compilation chain

Constructors

FTF_T_T
FTF_T_C
FTF_C_T
FTF_C_C

Instances

Instances details

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

Coercions

data Coercion #

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
Fields fco_tcv :: TyCoVar fco_visL :: !ForAllTyFlag fco_visR :: !ForAllTyFlag fco_kind :: KindCoercion fco_body :: Coercion
FunCo
Fields fco_role :: Role fco_afl :: FunTyFlag fco_afr :: FunTyFlag fco_mult :: CoercionN fco_arg :: Coercion fco_res :: Coercion
CoVarCo CoVar
AxiomCo CoAxiomRule [Coercion]
UnivCo
Fields uco_prov :: UnivCoProvenance uco_role :: Role uco_lty :: Type uco_rty :: Type uco_deps :: [Coercion]
SymCo Coercion
TransCo Coercion Coercion
SelCo CoSel Coercion
LRCo LeftOrRight CoercionN
InstCo Coercion CoercionN
KindCo Coercion
SubCo CoercionN
HoleCo CoercionHole	See Note [Coercion holes] Only present during typechecking

Instances

Instances details

Outputable Coercion #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: Coercion -> SDoc #
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 #
Eq (DeBruijn Coercion) #
Instance details Defined in GHC.Core.Map.Type Methods (==) :: DeBruijn Coercion -> DeBruijn Coercion -> Bool Source # (/=) :: DeBruijn Coercion -> DeBruijn Coercion -> Bool Source #

data CoSel #

Constructors

SelTyCon Int Role
SelFun FunSel
SelForAll

Instances

Instances details

NFData CoSel #
Instance details Defined in GHC.Core.TyCo.Rep Methods rnf :: CoSel -> () Source #
Binary CoSel #
Instance details Defined in GHC.Core.TyCo.Rep Methods put_ :: WriteBinHandle -> CoSel -> IO () # put :: WriteBinHandle -> CoSel -> IO (Bin CoSel) # get :: ReadBinHandle -> IO CoSel #
Outputable CoSel #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: CoSel -> SDoc #
Eq CoSel #
Instance details Defined in GHC.Core.TyCo.Rep Methods (==) :: CoSel -> CoSel -> Bool Source # (/=) :: CoSel -> CoSel -> Bool Source #
Ord CoSel #
Instance details Defined in GHC.Core.TyCo.Rep Methods compare :: CoSel -> CoSel -> Ordering Source # (<) :: CoSel -> CoSel -> Bool Source # (<=) :: CoSel -> CoSel -> Bool Source # (>) :: CoSel -> CoSel -> Bool Source # (>=) :: CoSel -> CoSel -> Bool Source # max :: CoSel -> CoSel -> CoSel Source # min :: CoSel -> CoSel -> CoSel Source #
Data CoSel #
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) -> CoSel -> c CoSel Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoSel Source # toConstr :: CoSel -> Constr Source # dataTypeOf :: CoSel -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoSel) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoSel) Source # gmapT :: (forall b. Data b => b -> b) -> CoSel -> CoSel Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r Source # gmapQ :: (forall d. Data d => d -> u) -> CoSel -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoSel -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoSel -> m CoSel Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoSel -> m CoSel Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoSel -> m CoSel Source #

data FunSel #

Constructors

SelMult
SelArg
SelRes

Instances

Instances details

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

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.

Constructors

PhantomProv	See Note [Phantom coercions]. Only in Phantom roled coercions
ProofIrrelProv	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 and the variable set are for the use by the plugin.

Instances

Instances details

NFData UnivCoProvenance #
Instance details Defined in GHC.Core.TyCo.Rep Methods rnf :: UnivCoProvenance -> () Source #
Binary UnivCoProvenance #
Instance details Defined in GHC.Core.TyCo.Rep Methods put_ :: WriteBinHandle -> UnivCoProvenance -> IO () # put :: WriteBinHandle -> UnivCoProvenance -> IO (Bin UnivCoProvenance) # get :: ReadBinHandle -> IO UnivCoProvenance #
Outputable UnivCoProvenance #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: UnivCoProvenance -> SDoc #
Eq UnivCoProvenance #
Instance details Defined in GHC.Core.TyCo.Rep Methods (==) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source # (/=) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source #
Ord UnivCoProvenance #
Instance details Defined in GHC.Core.TyCo.Rep Methods compare :: UnivCoProvenance -> UnivCoProvenance -> Ordering Source # (<) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source # (<=) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source # (>) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source # (>=) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source # max :: UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance Source # min :: UnivCoProvenance -> UnivCoProvenance -> UnivCoProvenance Source #
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 #

data CoercionHole #

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

Constructors

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

Instances

Instances details

Uniquable CoercionHole #
Instance details Defined in GHC.Core.TyCo.Rep Methods getUnique :: CoercionHole -> Unique #
Outputable CoercionHole #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: CoercionHole -> SDoc #
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 #

coHoleCoVar :: CoercionHole -> CoVar #

setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole #

type CoercionN = Coercion #

type CoercionR = Coercion #

type CoercionP = Coercion #

type KindCoercion = CoercionN #

data MCoercion #

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

Constructors

MRefl
MCo Coercion

Instances

Instances details

Outputable MCoercion #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: MCoercion -> SDoc #
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 #

type MCoercionR = MCoercion #

type MCoercionN = MCoercion #

Functions over types

mkNakedTyConTy :: TyCon -> Type #

mkNakedTyConTy creates a nullary TyConApp. In general you should rather use mkTyConTy, which picks the shared nullary TyConApp from inside the TyCon (via tyConNullaryTy. But we have to build the TyConApp tc [] in that TyCon field; that's what mkNakedTyConTy is for.

mkTyVarTy :: TyVar -> Type #

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

mkTyCoVarTy :: TyCoVar -> Type #

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

mkFunTy :: HasDebugCallStack => FunTyFlag -> Mult -> Type -> Type -> Type infixr 3 #

mkNakedFunTy :: FunTyFlag -> Kind -> Kind -> Kind #

mkVisFunTy :: HasDebugCallStack => Mult -> Type -> Type -> Type #

mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type #

mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type infixr 3 #

mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type #

tcMkVisFunTy :: Mult -> Type -> Type -> Type #

tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type #

tcMkScaledFunTy :: Scaled Type -> Type -> Type #

tcMkScaledFunTys :: [Scaled Type] -> Type -> Type #

mkForAllTy :: ForAllTyBinder -> Type -> Type #

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

mkForAllTys :: [ForAllTyBinder] -> 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 :: HasDebugCallStack => PiTyBinder -> Type -> Type #

mkPiTys :: HasDebugCallStack => [PiTyBinder] -> Type -> Type #

mkVisFunTyMany :: HasDebugCallStack => Type -> Type -> Type infixr 3 #

Make nested arrow types | Special, common, case: Arrow type with mult Many

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

nonDetCmpTyLit :: TyLit -> TyLit -> Ordering #

cmpTyLit :: TyLit -> TyLit -> Ordering #

Functions over coercions

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

Analyzing types

data TyCoFolder env a #

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 -> ForAllTyFlag -> 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) #

noView :: Type -> Maybe Type #

A view function that looks through nothing.

Sizes

typeSize :: Type -> Int #

typesSize :: [Type] -> Int #

coercionSize :: Coercion -> Int #

Multiplicities

data Scaled a #

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

Constructors

Scaled !Mult a

Instances

Instances details

Outputable a => Outputable (Scaled a) #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: Scaled a -> SDoc #
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 #

scaledMult :: Scaled a -> Mult #

scaledThing :: Scaled a -> a #

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

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

type Mult = Type #

Mult is a type alias for Type.

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

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

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