Safe Haskell	None
Language	GHC2021

GHC.Tc.Utils.Unify

Description

Type subsumption and unification

Synopsis

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)
tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
tcSubTypeSigma :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypePat :: CtOrigin -> UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeDS :: HsExpr GhcRn -> TcRhoType -> TcRhoType -> TcM HsWrapper
tcSubTypeAmbiguity :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
tcSubMult' :: CtOrigin -> Mult -> Mult -> TcM MultiplicityCheckCoercions
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 ()
data DeepSubsumptionFlag
- = Deep
- | Shallow
getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag
isRhoTyDS :: DeepSubsumptionFlag -> TcType -> Bool
tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType -> (TcRhoType -> TcM result) -> TcM (HsWrapper, result)
tcSkolemiseCompleteSig :: TcCompleteSig -> ([ExpPatType] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result)
tcSkolemiseExpectedType :: TcSigmaType -> ([ExpPatType] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result)
unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercionN
unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN
unifyInvisibleType :: TcTauType -> TcTauType -> TcM TcCoercionN
unifyExpectedType :: HsExpr GhcRn -> TcRhoType -> ExpRhoType -> TcM TcCoercionN
unifyExprType :: HsExpr GhcRn -> TcType -> TcType -> 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
checkTopShape :: MetaInfo -> TcType -> Bool
lhsPriority :: TcTyVar -> Int
data UnifyEnv = UE {
- 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)
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
matchExpectedTyConApp :: TyCon -> TcRhoType -> TcM (TcCoercionN, [TcSigmaType])
matchExpectedAppTy :: TcRhoType -> TcM (TcCoercion, (TcSigmaType, TcSigmaType))
matchExpectedFunTys :: ExpectedFunTyOrigin -> UserTypeCtxt -> VisArity -> ExpSigmaType -> ([ExpPatType] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a)
matchExpectedFunKind :: TypedThing -> Arity -> TcKind -> TcM Coercion
matchActualFunTy :: ExpectedFunTyOrigin -> Maybe TypedThing -> (Arity, TcType) -> TcRhoType -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
matchActualFunTys :: ExpectedFunTyOrigin -> CtOrigin -> Arity -> TcSigmaType -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
checkTyEqRhs :: TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
data PuResult a b
- = PuFail CheckTyEqResult
- | PuOK (Bag a) b
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 = TEF {
- tef_foralls :: Bool
- tef_lhs :: CanEqLHS
- tef_unifying :: AreUnifying
- tef_fam_app :: TyEqFamApp a
- tef_occurs :: CheckTyEqProblem
}
data TyEqFamApp a
- = TEFA_Fail
- | TEFA_Recurse
- | TEFA_Break (FamAppBreaker a)
data AreUnifying
- = Unifying MetaInfo TcLevel LevelCheck
- | NotUnifying
data LevelCheck
- = LC_None
- | LC_Check
- | LC_Promote Bool
type FamAppBreaker a = TcType -> TcM (PuResult a Reduction)
famAppArgFlags :: TyEqFlags a -> TyEqFlags a
checkPromoteFreeVars :: CheckTyEqProblem -> TcTyVar -> TcLevel -> TyCoVarSet -> TcM CheckTyEqResult
simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
data UnifyCheckCaller
- = UC_OnTheFly
- | UC_QuickLook
- | UC_Solver
- | UC_Defaulting
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN

Documentation

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

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

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

tcSubType Source #

Arguments

:: CtOrigin
-> UserTypeCtxt
-> TcSigmaType	Actual
-> ExpRhoType	Expected
-> TcM HsWrapper

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

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

tcSubTypeDS :: HsExpr GhcRn -> TcRhoType -> TcRhoType -> TcM HsWrapper Source #

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

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

tcSubMult' :: CtOrigin -> Mult -> Mult -> TcM MultiplicityCheckCoercions Source #

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

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

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

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

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

data DeepSubsumptionFlag Source #

Constructors

Deep
Shallow

Instances

Instances details

Outputable DeepSubsumptionFlag Source #
Instance details Defined in GHC.Tc.Utils.Unify Methods ppr :: DeepSubsumptionFlag -> SDoc Source #

getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag Source #

isRhoTyDS :: DeepSubsumptionFlag -> TcType -> Bool Source #

tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType -> (TcRhoType -> TcM result) -> TcM (HsWrapper, result) Source #

tcSkolemiseCompleteSig :: TcCompleteSig -> ([ExpPatType] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) Source #

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

tcSkolemiseExpectedType :: TcSigmaType -> ([ExpPatType] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) Source #

unifyType Source #

Arguments

:: Maybe TypedThing	If present, the thing that has type ty1
-> TcTauType
-> TcTauType
-> TcM TcCoercionN

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

unifyInvisibleType :: TcTauType -> TcTauType -> TcM TcCoercionN Source #

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

unifyExprType :: HsExpr GhcRn -> TcType -> TcType -> TcM TcCoercionN Source #

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

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

swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool Source #

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

checkTopShape :: MetaInfo -> TcType -> Bool Source #

checkTopShape checks (TYVAR-TV) Note [Unification preconditions]; returns True if these conditions are satisfied. But see the Note for other preconditions, too.

lhsPriority :: TcTyVar -> Int Source #

data UnifyEnv Source #

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

setUEnvRole :: UnifyEnv -> Role -> UnifyEnv Source #

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

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

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

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

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

matchExpectedFunTys :: ExpectedFunTyOrigin -> UserTypeCtxt -> VisArity -> ExpSigmaType -> ([ExpPatType] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a) Source #

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

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.

matchActualFunTy Source #

Arguments

:: ExpectedFunTyOrigin	See Note [Herald for matchExpectedFunTys]
-> Maybe TypedThing	The thing with type TcSigmaType
-> (Arity, TcType)	Total number of value args in the call, and the original function type (Both are used only for error messages)
-> TcRhoType	Type to analyse: a TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)

matchActualFunTy 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].

matchActualFunTys Source #

Arguments

:: ExpectedFunTyOrigin	See Note [Herald for matchExpectedFunTys]
-> CtOrigin
-> 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) Source #

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

data PuResult a b Source #

Constructors

PuFail CheckTyEqResult
PuOK (Bag a) b

Instances

Instances details

Applicative (PuResult a) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in GHC.Tc.Utils.Unify Methods ppr :: PuResult a b -> SDoc Source #

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

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

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

data TyEqFlags a Source #

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

Instances details

Outputable (TyEqFlags a) Source #
Instance details Defined in GHC.Tc.Utils.Unify Methods ppr :: TyEqFlags a -> SDoc Source #

data TyEqFamApp a Source #

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

Instances details

Outputable (TyEqFamApp a) Source #
Instance details Defined in GHC.Tc.Utils.Unify Methods ppr :: TyEqFamApp a -> SDoc Source #

data AreUnifying Source #

Constructors

Unifying MetaInfo TcLevel LevelCheck
NotUnifying

Instances

Instances details

Outputable AreUnifying Source #
Instance details Defined in GHC.Tc.Utils.Unify Methods ppr :: AreUnifying -> SDoc Source #

data LevelCheck Source #

Constructors

LC_None
LC_Check
LC_Promote Bool

Instances

Instances details

Outputable LevelCheck Source #
Instance details Defined in GHC.Tc.Utils.Unify Methods ppr :: LevelCheck -> SDoc Source #

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

famAppArgFlags :: TyEqFlags a -> TyEqFlags a Source #

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

simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool Source #

data UnifyCheckCaller Source #

Constructors

UC_OnTheFly
UC_QuickLook
UC_Solver
UC_Defaulting

fillInferResult :: TcType -> InferResult -> TcM TcCoercionN Source #

Fill an InferResult with the given type.

If co = fillInferResult t1 infer_res, then co :: t1 ~# t2, where t2 is the type stored in the ir_ref field of infer_res.

This function enforces the following invariants:

Level invariant. The stored type t2 is at the same level as given by the ir_lvl field.
FRR invariant. Whenever the ir_frr field is not Nothing, t2 is guaranteed to have a syntactically fixed RuntimeRep, in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.