ghc-lib-parser-9.12.2.20250421: The GHC API, decoupled from GHC versions

Safe Haskell | Ignore
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 Specified :: ForAllTyFlag
  - pattern Inferred :: 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)
  - ch_hetero_kind :: Bool
  }
- coHoleCoVar :: CoercionHole -> CoVar
- setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
- isHeteroKindCoHole :: CoercionHole -> Bool
- 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 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 !ForAllTyBinder Type | A Π type. See Note [Why ForAllTy can quantify over a coercion variable] 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 :: 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

Data Type Source # |

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

data TyLit Source #

Constructors

NumTyLit Integer |
StrTyLit FastString |
CharTyLit Char |

#### Instances

Instances details

Data TyLit Source # |

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 #

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

Type synonym used for types of kind RuntimeRep.

type LevityType = Type Source #

Type synonym used for types of kind Levity.

type KnotTied (ty :: k) = 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 `PredType`s

type FRRType = Type Source #

data ForAllTyFlag Source #

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 Specified :: ForAllTyFlag |
pattern Inferred :: ForAllTyFlag |

#### Instances

Instances details

NFData ForAllTyFlag Source # |
Instance details Defined in GHC.Hs.Specificity Methods rnf :: ForAllTyFlag -> () Source #
Data ForAllTyFlag Source # |

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 #

Binary ForAllTyFlag Source # |
Instance details Defined in GHC.Hs.Specificity Methods put_ :: WriteBinHandle -> ForAllTyFlag -> IO () Source # put :: WriteBinHandle -> ForAllTyFlag -> IO (Bin ForAllTyFlag) Source # get :: ReadBinHandle -> IO ForAllTyFlag Source #
Outputable ForAllTyFlag Source # |
Instance details Defined in GHC.Hs.Specificity Methods ppr :: ForAllTyFlag -> SDoc Source #
Eq ForAllTyFlag Source # |
Instance details Defined in Language.Haskell.Syntax.Specificity Methods (==) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source # (/=) :: ForAllTyFlag -> ForAllTyFlag -> Bool Source #
Ord ForAllTyFlag Source # |

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 #

Outputable tv => Outputable (VarBndr tv ForAllTyFlag) Source # |
Instance details Defined in GHC.Types.Var Methods ppr :: VarBndr tv ForAllTyFlag -> SDoc Source #

data FunTyFlag Source #

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

Data FunTyFlag Source # |

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 #

Binary FunTyFlag Source # |
Instance details Defined in GHC.Types.Var Methods put_ :: WriteBinHandle -> FunTyFlag -> IO () Source # put :: WriteBinHandle -> FunTyFlag -> IO (Bin FunTyFlag) Source # get :: ReadBinHandle -> IO FunTyFlag Source #
Outputable FunTyFlag Source # |
Instance details Defined in GHC.Types.Var Methods ppr :: FunTyFlag -> SDoc Source #
Eq FunTyFlag Source # |
Instance details Defined in GHC.Types.Var Methods (==) :: FunTyFlag -> FunTyFlag -> Bool Source # (/=) :: FunTyFlag -> FunTyFlag -> Bool Source #
Ord FunTyFlag Source # |
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 #

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

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

Data Coercion Source # |

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

data CoSel Source #

Constructors

SelTyCon Int Role |
SelFun FunSel |
SelForAll |

#### Instances

Instances details

NFData CoSel Source # |
Instance details Defined in GHC.Core.TyCo.Rep Methods rnf :: CoSel -> () Source #
Data CoSel Source # |

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 #

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

Constructors

SelMult |
SelArg |
SelRes |

#### Instances

Instances details

Data FunSel Source # |

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 #

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

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 #

Binary UnivCoProvenance Source # |
Instance details Defined in GHC.Core.TyCo.Rep Methods put_ :: WriteBinHandle -> UnivCoProvenance -> IO () Source # put :: WriteBinHandle -> UnivCoProvenance -> IO (Bin UnivCoProvenance) Source # get :: ReadBinHandle -> IO UnivCoProvenance Source #
Outputable UnivCoProvenance Source # |
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: UnivCoProvenance -> SDoc Source #
Eq UnivCoProvenance Source # |
Instance details Defined in GHC.Core.TyCo.Rep Methods (==) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source # (/=) :: UnivCoProvenance -> UnivCoProvenance -> Bool Source #
Ord UnivCoProvenance Source # |

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 CoercionHole Source #

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)
- ch_hetero_kind :: Bool

#### Instances

Instances details

Data CoercionHole Source # |

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 #

Uniquable CoercionHole Source # |
Instance details Defined in GHC.Core.TyCo.Rep Methods getUnique :: CoercionHole -> Unique Source #
Outputable CoercionHole Source # |
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: CoercionHole -> SDoc Source #

coHoleCoVar :: CoercionHole -> CoVar Source #

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

isHeteroKindCoHole :: CoercionHole -> Bool 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 Source # |

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

type MCoercionR = MCoercion Source #

type MCoercionN = MCoercion Source #

# Functions over types

mkNakedTyConTy :: TyCon -> Type Source #

`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 Source #

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

mkTyCoVarTy :: TyCoVar -> Type Source #

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

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

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

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

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

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

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

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

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

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

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

mkForAllTy :: ForAllTyBinder -> Type -> Type Source #

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

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

Wraps foralls over the type using the provided `TyCoVar`s from left to right

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

Wraps foralls over the type using the provided `InvisTVBinder`s from left to right

mkPiTy :: HasDebugCallStack => PiTyBinder -> Type -> Type Source #

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

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

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

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

nonDetCmpTyLit :: TyLit -> TyLit -> Ordering Source #

cmpTyLit :: TyLit -> TyLit -> Ordering 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 -> 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) Source #

noView :: Type -> Maybe Type Source #

A view function that looks through nothing.

# Sizes

typeSize :: Type -> Int Source #

typesSize :: [Type] -> Int Source #

coercionSize :: Coercion -> 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) Source # |

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