TcMType

Documentation

type TcTyVar = Var

Type variable that might be a metavariable

type TcKind = Kind

type TcType = Type

type TcTauType = TcType

type TcThetaType = ThetaType

type TcTyVarSet = TyVarSet

newFlexiTyVar :: Kind -> TcM TcTyVar

newFlexiTyVarTy :: Kind -> TcM TcType

newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]

newOpenFlexiTyVarTy :: TcM TcType

Create a tyvar that can be a lifted or unlifted type. Returns alpha :: TYPE kappa, where both alpha and kappa are fresh

newOpenTypeKind :: TcM TcKind

newMetaKindVar :: TcM TcKind

newMetaKindVars :: Int -> TcM [TcKind]

newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType

cloneMetaTyVar :: TcTyVar -> TcM TcTyVar

newFmvTyVar :: TcType -> TcM TcTyVar

newFskTyVar :: TcType -> TcM TcTyVar

readMetaTyVar :: TyVar -> TcM MetaDetails

writeMetaTyVar :: TcTyVar -> TcType -> TcM ()

writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()

newMetaDetails :: MetaInfo -> TcM TcTyVarDetails

isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type)

isFilledMetaTyVar :: TyVar -> TcM Bool

isUnfilledMetaTyVar :: TyVar -> TcM Bool

data ExpType

An expected type to check against during type-checking. See Note [ExpType] in TcMType, where you'll also find manipulators.

Constructors

Check TcType

Infer !InferResult

Instances

Outputable ExpType

Defined in TcType

Methods

ppr :: ExpType -> SDoc

pprPrec :: Rational -> ExpType -> SDoc

type ExpSigmaType = ExpType

type ExpRhoType = ExpType

mkCheckExpType :: TcType -> ExpType

Make an ExpType suitable for checking.

newInferExpType :: Bool -> TcM ExpType

newInferExpTypeInst :: TcM ExpRhoType

newInferExpTypeNoInst :: TcM ExpSigmaType

Make an ExpType suitable for inferring a type of kind * or #.

readExpType :: ExpType -> TcM TcType

Extract a type out of an ExpType. Otherwise, panics.

readExpType_maybe :: ExpType -> TcM (Maybe TcType)

Extract a type out of an ExpType, if one exists. But one should always exist. Unless you're quite sure you know what you're doing.

expTypeToType :: ExpType -> TcM TcType

Extracts the expected type if there is one, or generates a new TauTv if there isn't.

checkingExpType_maybe :: ExpType -> Maybe TcType

Returns the expected type when in checking mode.

checkingExpType :: String -> ExpType -> TcType

Returns the expected type when in checking mode. Panics if in inference mode.

tauifyExpType :: ExpType -> TcM ExpType

Turn a (Infer hole) type into a (Check alpha), where alpha is a fresh unification variable

inferResultToType :: InferResult -> TcM Type

newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar

newEvVars :: TcThetaType -> TcM [EvVar]

newDict :: Class -> [TcType] -> TcM DictId

newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence

newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]

newHoleCt :: Hole -> Id -> Type -> TcM Ct

Create a new CHoleCan Ct.

cloneWanted :: Ct -> TcM Ct

cloneWC :: WantedConstraints -> TcM WantedConstraints

emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm

Emits a new Wanted. Deals with both equalities and non-equalities.

emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion

Emits a new equality constraint

emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar

Creates a new EvVar and immediately emits it as a Wanted. No equality predicates here.

emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]

emitDerivedEqs :: CtOrigin -> [(TcType, TcType)] -> TcM ()

newTcEvBinds :: TcM EvBindsVar

newNoTcEvBinds :: TcM EvBindsVar

Creates an EvBindsVar incapable of holding any bindings. It still tracks covar usages (see comments on ebv_tcvs in TcEvidence), thus must be made monadically

addTcEvBind :: EvBindsVar -> EvBind -> TcM ()

newCoercionHole :: TcPredType -> TcM CoercionHole

fillCoercionHole :: CoercionHole -> Coercion -> TcM ()

Put a value in a coercion hole

isFilledCoercionHole :: CoercionHole -> TcM Bool

Is a coercion hole filled in?

unpackCoercionHole :: CoercionHole -> TcM Coercion

Retrieve the contents of a coercion hole. Panics if the hole is unfilled

unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)

Retrieve the contents of a coercion hole, if it is filled

checkCoercionHole :: CoVar -> Coercion -> TcM Coercion

Check that a coercion is appropriate for filling a hole. (The hole itself is needed only for printing. Always returns the checked coercion, but this return value is necessary so that the input coercion is forced only when the output is forced.

newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])

newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)

newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])

newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])

newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)

newTyVarTyVar :: Name -> Kind -> TcM TcTyVar

newTauTyVar :: Name -> Kind -> TcM TcTyVar

newSkolemTyVar :: Name -> Kind -> TcM TcTyVar

newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)

tcInstType

Arguments

:: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))

How to instantiate the type variables

-> Id

Type to instantiate

-> TcM ([(Name, TcTyVar)], TcThetaType, TcType)

Result (type vars, preds (incl equalities), rho)

tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])

Given a list of [TyVar], skolemize the type variables, returning a substitution mapping the original tyvars to the skolems, and the list of newly bound skolems.

tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])

tcInstSkolTyVarsAt :: TcLevel -> Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])

tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)

tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])

tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])

freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])

Give fresh uniques to a bunch of TyVars, but they stay as TyVars, rather than becoming TcTyVars Used in FamInst.newFamInst, and Inst.newClsInst

freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])

Give fresh uniques to a bunch of CoVars Used in FamInst.newFamInst

zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)

zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])

zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)

tidyEvVar :: TidyEnv -> EvVar -> EvVar

tidyCt :: TidyEnv -> Ct -> Ct

tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo

zonkTcTyVar :: TcTyVar -> TcM TcType

zonkTcTyVars :: [TcTyVar] -> TcM [TcType]

zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar

zonkTyVarTyVarPairs :: [(Name, TcTyVar)] -> TcM [(Name, TcTyVar)]

zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet

zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet

zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]

candidateQTyVarsOfType :: TcType -> TcM CandidatesQTvs

Gathers free variables to use as quantification candidates (in quantifyTyVars). This might output the same var in both sets, if it's used in both a type and a kind. The variables to quantify must have a TcLevel strictly greater than the ambient level. (See Wrinkle in Note [Naughty quantification candidates]) See Note [CandidatesQTvs determinism and order] See Note [Dependent type variables]

candidateQTyVarsOfKind :: TcKind -> TcM CandidatesQTvs

Like candidateQTyVarsOfType, but consider every free variable to be dependent. This is appropriate when generalizing a *kind*, instead of a type. (That way, -XNoPolyKinds will default the variables to Type.)

candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs

Like candidateQTyVarsOfType, but over a list of types The variables to quantify must have a TcLevel strictly greater than the ambient level. (See Wrinkle in Note [Naughty quantification candidates])

candidateQTyVarsOfKinds :: [TcKind] -> TcM CandidatesQTvs

data CandidatesQTvs

Constructors

DV

Fields

• dv_kvs :: DTyVarSet
• dv_tvs :: DTyVarSet
• dv_cvs :: CoVarSet

Instances

Semigroup CandidatesQTvs

Defined in TcMType

Methods

(<>) :: CandidatesQTvs -> CandidatesQTvs -> CandidatesQTvs

sconcat :: NonEmpty CandidatesQTvs -> CandidatesQTvs

stimes :: Integral b => b -> CandidatesQTvs -> CandidatesQTvs

Monoid CandidatesQTvs

Defined in TcMType

Methods

mempty :: CandidatesQTvs

mappend :: CandidatesQTvs -> CandidatesQTvs -> CandidatesQTvs

mconcat :: [CandidatesQTvs] -> CandidatesQTvs

Outputable CandidatesQTvs

Defined in TcMType

Methods

ppr :: CandidatesQTvs -> SDoc

pprPrec :: Rational -> CandidatesQTvs -> SDoc

delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs

candidateKindVars :: CandidatesQTvs -> TyVarSet

skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar

defaultTyVar :: Bool -> TcTyVar -> TcM Bool

quantifyTyVars :: TcTyCoVarSet -> CandidatesQTvs -> TcM [TcTyVar]

zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar

zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder]

zonkTcType :: TcType -> TcM TcType

zonkTcTypes :: [TcType] -> TcM [TcType]

zonkCo :: Coercion -> TcM Coercion

Zonk a coercion -- really, just zonk any types in the coercion

zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar

zonkEvVar :: EvVar -> TcM EvVar

zonkWC :: WantedConstraints -> TcM WantedConstraints

zonkSimples :: Cts -> TcM Cts

zonkId :: TcId -> TcM TcId

zonkCoVar :: CoVar -> TcM CoVar

zonkCt :: Ct -> TcM Ct

zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo

tcGetGlobalTyCoVars :: TcM TcTyVarSet

tcGetGlobalTyCoVars returns a fully-zonked set of *scoped* tyvars free in the environment. To improve subsequent calls to the same function it writes the zonked set back into the environment. Note that this returns all variables free in anything (term-level or type-level) in scope. We thus don't have to worry about clashes with things that are not in scope, because if they are reachable, then they'll be returned here. NB: This is closed over kinds, so it can return unification variables mentioned in the kinds of in-scope tyvars.

ensureNotLevPoly :: Type -> SDoc -> TcM ()

According to the rules around representation polymorphism (see https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds), no binder can have a representation-polymorphic type. This check ensures that we respect this rule. It is a bit regrettable that this error occurs in zonking, after which we should have reported all errors. But it's hard to see where else to do it, because this can be discovered only after all solving is done. And, perhaps most importantly, this isn't really a compositional property of a type system, so it's not a terrible surprise that the check has to go in an awkward spot.

checkForLevPoly :: SDoc -> Type -> TcM ()

checkForLevPolyX :: Monad m => (SDoc -> m ()) -> SDoc -> Type -> m ()

formatLevPolyErr :: Type -> SDoc