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

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

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

tcSubTypeDS :: HsExpr GhcRn -> TcRhoType -> ExpRhoType -> 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

unifyInvisibleType :: TcTauType -> TcTauType -> TcM TcCoercionN

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

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

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

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

touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool

data UnifyEnv

Constructors

UE

Fields

• u_role :: Role
• u_loc :: CtLoc
• u_rewriters :: RewriterSet
• u_defer :: TcRef (Bag Ct)
• u_unified :: Maybe (TcRef [TcTyVar])

updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv

setUEnvRole :: UnifyEnv -> Role -> UnifyEnv

uType :: UnifyEnv -> TcType -> TcType -> TcM CoercionN

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 :: 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 argument 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].

checkTyEqRhs :: TyEqFlags a -> TcType -> TcM (PuResult a Reduction)

recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)

data PuResult a b

Constructors

PuFail CheckTyEqResult

PuOK (Bag a) b

Instances

Applicative (PuResult a)

Defined in GHC.Tc.Utils.Unify

Methods

pure :: a0 -> PuResult a a0

(<*>) :: PuResult a (a0 -> b) -> PuResult a a0 -> PuResult a b

liftA2 :: (a0 -> b -> c) -> PuResult a a0 -> PuResult a b -> PuResult a c

(*>) :: PuResult a a0 -> PuResult a b -> PuResult a b

(<*) :: PuResult a a0 -> PuResult a b -> PuResult a a0

Functor (PuResult a)

Defined in GHC.Tc.Utils.Unify

Methods

fmap :: (a0 -> b) -> PuResult a a0 -> PuResult a b

(<$) :: a0 -> PuResult a b -> PuResult a a0

(Outputable a, Outputable b) => Outputable (PuResult a b)

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: PuResult a b -> SDoc

failCheckWith :: CheckTyEqResult -> TcM (PuResult a b)

okCheckRefl :: TcType -> TcM (PuResult a Reduction)

mapCheck :: (x -> TcM (PuResult a Reduction)) -> [x] -> TcM (PuResult a Reductions)

data TyEqFlags a

Options describing how to deal with a type equality in the pure unifier. See checkTyEqRhs

Constructors

TEF

Fields

• tef_foralls :: Bool
• tef_lhs :: CanEqLHS
• tef_unifying :: AreUnifying
• tef_fam_app :: TyEqFamApp a
• tef_occurs :: CheckTyEqProblem

Instances

Outputable (TyEqFlags a)

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: TyEqFlags a -> SDoc

data TyEqFamApp a

What to do when encountering a type-family application while processing a type equality in the pure unifier.

See Note [Family applications in canonical constraints]

Constructors

TEFA_Fail

TEFA_Recurse

TEFA_Break (FamAppBreaker a)

Instances

Outputable (TyEqFamApp a)

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: TyEqFamApp a -> SDoc

data AreUnifying

Constructors

Unifying MetaInfo TcLevel LevelCheck

NotUnifying

Instances

Outputable AreUnifying

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: AreUnifying -> SDoc

data LevelCheck

Constructors

LC_None

LC_Check

LC_Promote

Instances

Outputable LevelCheck

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: LevelCheck -> SDoc

type FamAppBreaker a = TcType -> TcM (PuResult a Reduction)

famAppArgFlags :: TyEqFlags a -> TyEqFlags a

simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool

checkPromoteFreeVars :: CheckTyEqProblem -> TcTyVar -> TcLevel -> TyCoVarSet -> TcM CheckTyEqResult