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 ()
- 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
- 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 {}
- updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
- setUEnvRole :: UnifyEnv -> Role -> UnifyEnv
- uType :: UnifyEnv -> TcType -> TcType -> TcM CoercionN
- mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst
- makeTypeConcrete :: FastString -> ConcreteTvOrigin -> TcType -> TcM (TcCoercion, Cts)
- 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 :: Monad m => TyEqFlags m a -> TcType -> m (PuResult a Reduction)
- recurseIntoTyConApp :: Monad m => TyEqFlags m a -> TyCon -> [TcType] -> m (PuResult a Reduction)
- recurseIntoFamTyConApp :: Monad m => TyEqFlags m a -> TyCon -> [TcType] -> m (PuResult a Reduction)
- data PuResult a b
- = PuFail CheckTyEqResult
- | PuOK (Bag a) b
- okCheckRefl :: TcType -> PuResult a Reduction
- mapCheck :: Monad m => (x -> m (PuResult a Reduction)) -> [x] -> m (PuResult a Reductions)
- data TyEqFlags (m :: Type -> Type) a
- notUnifying_TEFTask :: forall (m :: Type -> Type) a. CheckTyEqProblem -> CanEqLHS -> TyEqFlags m a
- unifyingLHSMetaTyVar_TEFTask :: CtEvidence -> TcTyVar -> TyEqFlags TcM Ct
- defaulting_TEFTask :: TcTyVar -> TyEqFlags TcM a
- pureTyEqFlags_LHSMetaTyVar :: TyVar -> TyEqFlags Identity ()
- mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp TcM a
- data OccursCheck where
- OC_None :: OccursCheck
- OC_Check :: {..} -> OccursCheck
- data LevelCheck (m :: Type -> Type) where
- LC_None :: forall (m :: Type -> Type). LevelCheck m
- LC_Check :: forall (m :: Type -> Type). {..} -> LevelCheck m
- LC_Promote :: {..} -> LevelCheck (IOEnv (Env TcGblEnv TcLclEnv))
- data ConcreteCheck (m :: Type -> Type) where
- CC_None :: forall (m :: Type -> Type). ConcreteCheck m
- CC_Check :: forall (m :: Type -> Type). ConcreteCheck m
- CC_Promote :: ConcreteTvOrigin -> ConcreteCheck (IOEnv (Env TcGblEnv TcLclEnv))
- data TyEqFamApp (m :: Type -> Type) a where
- TEFA_Fail :: forall (m :: Type -> Type) a. TyEqFamApp m a
- TEFA_Recurse :: forall (m :: Type -> Type) a. TyEqFamApp m a
- TEFA_Break :: forall a. FamAppBreaker a -> TyEqFamApp (IOEnv (Env TcGblEnv TcLclEnv)) a
- data FamAppBreaker a where
- BreakGiven :: FamAppBreaker (TcTyVar, TcType)
- BreakWanted :: CtEvidence -> TcTyVar -> FamAppBreaker Ct
- checkPromoteFreeVars :: CheckTyEqProblem -> Name -> TcLevel -> TyCoVarSet -> TcM CheckTyEqResult
- simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
- data UnifyCheckCaller
- 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 #
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 #
tcSubTypeAmbiguity :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper 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 #
Instances
Outputable DeepSubsumptionFlag Source # | |
Defined in GHC.Tc.Utils.Unify Methods ppr :: DeepSubsumptionFlag -> SDoc 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 #
Arguments
:: Maybe TypedThing | If present, the thing that has type ty1 |
-> TcTauType | |
-> TcTauType | |
-> TcM TcCoercionN |
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 #
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 #
mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst Source #
makeTypeConcrete :: FastString -> ConcreteTvOrigin -> TcType -> TcM (TcCoercion, Cts) Source #
Try to turn the provided type into a concrete type, by ensuring unfilled metavariables are appropriately marked as concrete.
Returns a coercion whose RHS is a zonked type which is "as concrete as possible", and a collection of Wanted equality constraints that are necessary to make the type concrete.
For example, for an input TYPE a[sk]
we will return a coercion with RHS
TYPE gamma[conc]
together with the Wanted equality constraint a ~# gamma
.
INVARIANT: the RHS type of the returned coercion is equal to the input type, up to zonking and the returned Wanted equality constraints.
INVARIANT: if this function returns an empty list of constraints then the RHS type of the returned coercion is concrete, in the sense of Note [Concrete types].
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].
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.
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].
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].
recurseIntoTyConApp :: Monad m => TyEqFlags m a -> TyCon -> [TcType] -> m (PuResult a Reduction) Source #
recurseIntoFamTyConApp :: Monad m => TyEqFlags m a -> TyCon -> [TcType] -> m (PuResult a Reduction) Source #
Constructors
PuFail CheckTyEqResult | |
PuOK (Bag a) b |
Instances
Applicative (PuResult a) Source # | |
Defined in GHC.Tc.Utils.Unify | |
Functor (PuResult a) Source # | |
Foldable (PuResult a) Source # | |
Defined in GHC.Tc.Utils.Unify Methods fold :: Monoid m => PuResult a m -> m # foldMap :: Monoid m => (a0 -> m) -> PuResult a a0 -> m # foldMap' :: Monoid m => (a0 -> m) -> PuResult a a0 -> m # foldr :: (a0 -> b -> b) -> b -> PuResult a a0 -> b # foldr' :: (a0 -> b -> b) -> b -> PuResult a a0 -> b # foldl :: (b -> a0 -> b) -> b -> PuResult a a0 -> b # foldl' :: (b -> a0 -> b) -> b -> PuResult a a0 -> b # foldr1 :: (a0 -> a0 -> a0) -> PuResult a a0 -> a0 # foldl1 :: (a0 -> a0 -> a0) -> PuResult a a0 -> a0 # toList :: PuResult a a0 -> [a0] # null :: PuResult a a0 -> Bool # length :: PuResult a a0 -> Int # elem :: Eq a0 => a0 -> PuResult a a0 -> Bool # maximum :: Ord a0 => PuResult a a0 -> a0 # minimum :: Ord a0 => PuResult a a0 -> a0 # | |
Traversable (PuResult a) Source # | |
Defined in GHC.Tc.Utils.Unify | |
(Outputable a, Outputable b) => Outputable (PuResult a b) Source # | |
data TyEqFlags (m :: Type -> Type) a Source #
Options describing how to deal with a type equality
in the pure unifier. See checkTyEqRhs
Constructors
TEFTyFam | LHS is a type family application; we are not unifying. |
Fields
| |
TEFTyVar | LHS is a |
Fields
|
Instances
Outputable (TyEqFlags m a) Source # | |
notUnifying_TEFTask :: forall (m :: Type -> Type) a. CheckTyEqProblem -> CanEqLHS -> TyEqFlags m a Source #
pureTyEqFlags_LHSMetaTyVar :: TyVar -> TyEqFlags Identity () Source #
TyEqFlags
for a pure call of checkTyEqRhs
.
A call to checkTyEqRhs
with these TyEqFlags
will perform an optimistic
check: it will return PuFail
if there is definitely a problem, but it
might return PuOK
if it isn't entirely sure.
mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp TcM a Source #
data OccursCheck where Source #
Constructors
OC_None :: OccursCheck | No occurs check. |
OC_Check | Do an occurs check between the LHS tyvar and the RHS. |
Fields
|
Instances
Outputable OccursCheck Source # | |
Defined in GHC.Tc.Utils.Unify Methods ppr :: OccursCheck -> SDoc Source # |
data LevelCheck (m :: Type -> Type) where Source #
What level check to perform, in a call to the pure unifier?
A defunctionalisation of the possible level-check functions
Interpreter: tyVarLevelCheck
Constructors
LC_None :: forall (m :: Type -> Type). LevelCheck m | No level check. |
LC_Check | Do a level check between the LHS tyvar and the occurrence tyvar. Fail if the level check fails. True = lenient check, e.g. the levels have a chance of working out after promotion. |
Fields
| |
LC_Promote | Do a level check between the LHS tyvar and the occurrence tyvar. If the level check fails, and the occurrence is a unification variable, promote it. |
Instances
Outputable (LevelCheck m) Source # | |
Defined in GHC.Tc.Utils.Unify Methods ppr :: LevelCheck m -> SDoc Source # |
data ConcreteCheck (m :: Type -> Type) where Source #
Constructors
CC_None :: forall (m :: Type -> Type). ConcreteCheck m | No concreteness check. |
CC_Check :: forall (m :: Type -> Type). ConcreteCheck m | Simple check for concreteness, leniently returning |
CC_Promote :: ConcreteTvOrigin -> ConcreteCheck (IOEnv (Env TcGblEnv TcLclEnv)) | Proper concreteness check: promote non-concrete metavariables, failing if there are any problems. |
Instances
Outputable (ConcreteCheck m) Source # | |
Defined in GHC.Tc.Utils.Unify Methods ppr :: ConcreteCheck m -> SDoc Source # |
data TyEqFamApp (m :: Type -> Type) a where 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 :: forall (m :: Type -> Type) a. TyEqFamApp m a | Always fail |
TEFA_Recurse :: forall (m :: Type -> Type) a. TyEqFamApp m a | Just recurse |
TEFA_Break :: forall a. FamAppBreaker a -> TyEqFamApp (IOEnv (Env TcGblEnv TcLclEnv)) a | Recurse, but replace with cycle breaker if fails,
using the specified |
Instances
Outputable (TyEqFamApp m a) Source # | |
Defined in GHC.Tc.Utils.Unify Methods ppr :: TyEqFamApp m a -> SDoc Source # |
data FamAppBreaker a where Source #
A defunctionalisation of family application breaker functions.
Interpreter: famAppBreaker
Constructors
BreakGiven :: FamAppBreaker (TcTyVar, TcType) | |
BreakWanted :: CtEvidence -> TcTyVar -> FamAppBreaker Ct |
Instances
Outputable (FamAppBreaker a) Source # | |
Defined in GHC.Tc.Utils.Unify Methods ppr :: FamAppBreaker a -> SDoc Source # |
checkPromoteFreeVars :: CheckTyEqProblem -> Name -> 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: