ghc-9.13: The GHC API
Safe HaskellNone
LanguageGHC2021

GHC.Tc.Utils.Unify

Description

Type subsumption and unification

Synopsis

Documentation

tcSubType Source #

Arguments

:: CtOrigin 
-> UserTypeCtxt 
-> TcSigmaType

Actual

-> ExpRhoType

Expected

-> TcM HsWrapper 

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

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

data DeepSubsumptionFlag Source #

Constructors

Deep 
Shallow 

Instances

Instances details
Outputable DeepSubsumptionFlag Source # 
Instance details

Defined in GHC.Tc.Utils.Unify

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

unifyType Source #

Arguments

:: Maybe TypedThing

If present, the thing that has type ty1

-> TcTauType 
-> TcTauType 
-> TcM TcCoercionN 

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.

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.

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

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 #

Foldable (PuResult a) Source # 
Instance details

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 #

sum :: Num a0 => PuResult a a0 -> a0 #

product :: Num a0 => PuResult a a0 -> a0 #

Traversable (PuResult a) Source # 
Instance details

Defined in GHC.Tc.Utils.Unify

Methods

traverse :: Applicative f => (a0 -> f b) -> PuResult a a0 -> f (PuResult a b) #

sequenceA :: Applicative f => PuResult a (f a0) -> f (PuResult a a0) #

mapM :: Monad m => (a0 -> m b) -> PuResult a a0 -> m (PuResult a b) #

sequence :: Monad m => PuResult a (m a0) -> m (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 #

mapCheck :: Monad m => (x -> m (PuResult a Reduction)) -> [x] -> m (PuResult a Reductions) 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 TyVar.

Fields

Instances

Instances details
Outputable (TyEqFlags m a) Source # 
Instance details

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: TyEqFlags m a -> SDoc Source #

notUnifying_TEFTask :: forall (m :: Type -> Type) a. CheckTyEqProblem -> CanEqLHS -> TyEqFlags m a Source #

Create a "not unifying" TyEqFlags from a CanEqLHS.

See use-case (1) in Note [TyEqFlags].

unifyingLHSMetaTyVar_TEFTask :: CtEvidence -> TcTyVar -> TyEqFlags TcM Ct Source #

Create "unifying" TyEqFlags from a TyVarLHS.

Invariant: the argument TcTyVar is a MetaTv.

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.

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

Instances details
Outputable OccursCheck Source # 
Instance details

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.

  • False = don't promote under type families (the common case)
  • True = promote even under type families (see Note [Defaulting equalities] in GHC.Tc.Solver)

Fields

Instances

Instances details
Outputable (LevelCheck m) Source # 
Instance details

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 OK if concreteness could be achieved after promotion.

CC_Promote :: ConcreteTvOrigin -> ConcreteCheck (IOEnv (Env TcGblEnv TcLclEnv))

Proper concreteness check: promote non-concrete metavariables, failing if there are any problems.

Instances

Instances details
Outputable (ConcreteCheck m) Source # 
Instance details

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 FamAppBreaker

Instances

Instances details
Outputable (TyEqFamApp m a) Source # 
Instance details

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

Instances

Instances details
Outputable (FamAppBreaker a) Source # 
Instance details

Defined in GHC.Tc.Utils.Unify

Methods

ppr :: FamAppBreaker a -> SDoc Source #

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.