GHC.Tc.Utils.Unify

Type subsumption and unification

Documentation

tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)

tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)

tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc -> TcRhoType -> ExpRhoType -> TcM (HsExpr GhcTc)

tcTopSkolemise

Arguments

:: UserTypeCtxt

-> TcSigmaType

-> (TcType -> TcM result)

-> TcM (HsWrapper, result)

The wrapper has type: spec_ty ~> expected_ty See Note [Skolemisation] for the differences between tcSkolemiseScoped and tcTopSkolemise

tcSkolemiseScoped

Arguments

:: UserTypeCtxt

-> TcSigmaType

-> (TcType -> TcM result)

-> TcM (HsWrapper, result)

The wrapper has type: spec_ty ~> expected_ty See Note [Skolemisation] for the differences between tcSkolemiseScoped and tcTopSkolemise

tcSkolemiseExpType :: UserTypeCtxt -> ExpSigmaType -> (ExpRhoType -> TcM result) -> TcM (HsWrapper, result)

Variant of tcTopSkolemise that takes an ExpType

tcSubType

Arguments

:: CtOrigin

-> UserTypeCtxt

-> TcSigmaType

Actual

-> ExpRhoType

Expected

-> TcM HsWrapper

tcSubTypeNC

Arguments

:: CtOrigin

Used when instantiating

-> UserTypeCtxt

Used when skolemising

-> Maybe TypedThing

The expression that has type actual (if known)

-> TcSigmaType

Actual type

-> ExpRhoType

Expected type

-> TcM HsWrapper

tcSubTypeSigma :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper

tcSubTypePat :: CtOrigin -> UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper

tcSubTypeAmbiguity :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper

tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper

checkConstraints :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM result -> TcM (TcEvBinds, result)

checkTvConstraints :: SkolemInfo -> [TcTyVar] -> TcM result -> TcM result

buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> WantedConstraints -> TcM (Bag Implication, TcEvBinds)

buildTvImplication :: SkolemInfoAnon -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication

emitResidualTvConstraint :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()

unifyType

Arguments

:: Maybe TypedThing

If present, the thing that has type ty1

-> TcTauType

-> TcTauType

-> TcM TcCoercionN

unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN

unifyExpectedType :: HsExpr GhcRn -> TcRhoType -> ExpRhoType -> TcM TcCoercionN

uType :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN

promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)

swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool

startSolvingByUnification :: MetaInfo -> TcType -> TcM Bool

Checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of Note [Unification preconditions]; returns True if these conditions are satisfied. But see the Note for other preconditions, too.

tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)

Infer a type using a fresh ExpType See also Note [ExpType] in GHC.Tc.Utils.TcMType

Use tcInferFRR if you require the type to have a fixed runtime representation.

matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)

matchExpectedTyConApp :: TyCon -> TcRhoType -> TcM (TcCoercionN, [TcSigmaType])

matchExpectedAppTy :: TcRhoType -> TcM (TcCoercion, (TcSigmaType, TcSigmaType))

matchExpectedFunTys :: forall a. ExpectedFunTyOrigin -> UserTypeCtxt -> Arity -> ExpRhoType -> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a)

Use this function to split off arguments types when you have an "expected" type.

This function skolemises at each polytype.

Invariant: this function only applies the provided function to a list of argument types which all have a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. See Note [Return arguments with a fixed RuntimeRep].

matchExpectedFunKind

Arguments

:: TypedThing

type, only for errors

-> Arity

n: number of desired arrows

-> TcKind

fun_ kind

-> TcM Coercion

co :: fun_kind ~ (arg1 -> ... -> argn -> res)

Breaks apart a function kind into its pieces.

matchActualFunTySigma

Arguments

:: ExpectedFunTyOrigin

See Note [Herald for matchExpectedFunTys]

-> Maybe TypedThing

The thing with type TcSigmaType

-> (Arity, [Scaled TcSigmaType])

Total number of value args in the call, and types of values args to which function has been applied already (reversed) (Both are used only for error messages)

-> TcRhoType

Type to analyse: a TcRhoType

-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)

matchActualFunTySigma looks for just one function arrow, returning an uninstantiated sigma-type.

Invariant: the returned argument type has a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.

See Note [Return arguments with a fixed RuntimeRep].

matchActualFunTysRho

Arguments

:: ExpectedFunTyOrigin

See Note [Herald for matchExpectedFunTys]

-> CtOrigin

-> Maybe TypedThing

the thing with type TcSigmaType

-> Arity

-> TcSigmaType

-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)

Like matchExpectedFunTys, but used when you have an "actual" type, for example in function application.

INVARIANT: the returned arguemnt types all have a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. See Note [Return arguments with a fixed RuntimeRep].

checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult

checkTyFamEq :: TyCon -> [TcType] -> TcType -> CheckTyEqResult

checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult