Safe Haskell	None
Language	Haskell2010

TyCoRep

Contents

Types
Coercions
Functions over types
Functions over binders
Functions over coercions
Sizes

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_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
- = Inferred
- | Specified
- | Required
data AnonArgFlag
- = VisArg
- | InvisArg
data ForallVisFlag
- = ForallVis
- | ForallInvis
data Coercion
- = Refl Type
- | GRefl Role Type MCoercionN
- | TyConAppCo Role TyCon [Coercion]
- | AppCo Coercion CoercionN
- | ForAllCo TyCoVar KindCoercion Coercion
- | FunCo Role 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
- = UnsafeCoerceProv
- | PhantomProv KindCoercion
- | ProofIrrelProv KindCoercion
- | 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
mkTyConTy :: TyCon -> Type
mkTyVarTy :: TyVar -> Type
mkTyVarTys :: [TyVar] -> [Type]
mkTyCoVarTy :: TyCoVar -> Type
mkTyCoVarTys :: [TyCoVar] -> [Type]
mkFunTy :: AnonArgFlag -> Type -> Type -> Type
mkVisFunTy :: Type -> Type -> Type
mkInvisFunTy :: Type -> Type -> Type
mkVisFunTys :: [Type] -> Type -> Type
mkInvisFunTys :: [Type] -> Type -> Type
mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
mkForAllTys :: [TyCoVarBinder] -> Type -> Type
mkPiTy :: TyCoBinder -> Type -> Type
mkPiTys :: [TyCoBinder] -> Type -> Type
data TyCoBinder
- = Named TyCoVarBinder
- | Anon AnonArgFlag 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
typeSize :: Type -> Int
coercionSize :: Coercion -> Int
provSize :: UnivCoProvenance -> Int

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 TcEnv 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 TyCoRep Methods ppr :: TyThing -> SDoc Source # pprPrec :: Rational -> TyThing -> SDoc Source #
NamedThing TyThing #
Instance details Defined in TyCoRep 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 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.
FunTy	t1 -> t2 Very common, so an important special case See Note [Function types]
Fields ft_af :: AnonArgFlag 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 refl. INVARIANT: The Type is not a CastTy (use TransCo instead) See Note Respecting definitional equality and (EQ3)
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 TyCoRep 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 TyCoRep 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 TyCoRep Methods (==) :: TyLit -> TyLit -> Bool # (/=) :: TyLit -> TyLit -> Bool #
Data TyLit #
Instance details Defined in TyCoRep 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 TyCoRep 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 TyCoRep 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 TcTyClsDecls

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 TyCoRep

Constructors

Inferred
Specified
Required

Instances

Instances details

Eq ArgFlag #
Instance details Defined in Var Methods (==) :: ArgFlag -> ArgFlag -> Bool # (/=) :: ArgFlag -> ArgFlag -> Bool #
Data ArgFlag #
Instance details Defined in 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 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 Var Methods ppr :: ArgFlag -> SDoc Source # pprPrec :: Rational -> ArgFlag -> SDoc Source #
Binary ArgFlag #
Instance details Defined in 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 Var Methods ppr :: VarBndr tv ArgFlag -> SDoc Source # pprPrec :: Rational -> VarBndr tv ArgFlag -> SDoc Source #

data AnonArgFlag Source #

The non-dependent version of ArgFlag.

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 Var Methods (==) :: AnonArgFlag -> AnonArgFlag -> Bool # (/=) :: AnonArgFlag -> AnonArgFlag -> Bool #
Data AnonArgFlag #
Instance details Defined in 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 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 Var Methods ppr :: AnonArgFlag -> SDoc Source # pprPrec :: Rational -> AnonArgFlag -> SDoc Source #
Binary AnonArgFlag #
Instance details Defined in Var Methods put_ :: BinHandle -> AnonArgFlag -> IO () Source # put :: BinHandle -> AnonArgFlag -> IO (Bin AnonArgFlag) Source # get :: BinHandle -> IO AnonArgFlag Source #

data ForallVisFlag Source #

Is a forall invisible (e.g., forall a b. {...}, with a dot) or visible (e.g., forall a b -> {...}, with an arrow)?

Constructors

ForallVis	A visible `forall` (with an arrow)
ForallInvis	An invisible `forall` (with a dot)

Instances

Instances details

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

UnsafeCoerceProv	From `unsafeCoerce#`. These are unsound.
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 TyCoRep 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 TyCoRep 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_ref :: IORef (Maybe Coercion)

Instances

Instances details

Data CoercionHole #
Instance details Defined in TyCoRep 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 TyCoRep Methods ppr :: CoercionHole -> SDoc Source # pprPrec :: Rational -> CoercionHole -> 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 TyCoRep 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 TyCoRep 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 -> Type -> Type -> Type infixr 3 Source #

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

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

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

Make nested arrow types

mkInvisFunTys :: [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

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

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

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 Type

Instances

Instances details

Data TyCoBinder #
Instance details Defined in TyCoRep 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 TyCoRep 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 TyCoRep, because it's used in 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 #

Sizes

typeSize :: Type -> Int Source #

coercionSize :: Coercion -> Int Source #

provSize :: UnivCoProvenance -> Int Source #