GHC.Core.Unify

Documentation

tcMatchTy :: Type -> Type -> Maybe Subst

tcMatchTy t1 t2 produces a substitution (over fvs(t1)) s such that s(t1) equals t2. The returned substitution might bind coercion variables, if the variable is an argument to a GADT constructor.

Precondition: typeKind ty1 eqType typeKind ty2

We don't pass in a set of "template variables" to be bound by the match, because tcMatchTy (and similar functions) are always used on top-level types, so we can bind any of the free variables of the LHS. See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTyKi :: Type -> Type -> Maybe Subst

Like tcMatchTy, but allows the kinds of the types to differ, and thus matches them as well. See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTys

Arguments

:: [Type]

Template

-> [Type]

Target

-> Maybe Subst

One-shot; in principle the template variables could be free in the target

Like tcMatchTy but over a list of types. See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTyKis

Arguments

:: [Type]

Template

-> [Type]

Target

-> Maybe Subst

One-shot substitution

Like tcMatchTyKi but over a list of types. See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTyX

Arguments

:: Subst

Substitution to extend

-> Type

Template

-> Type

Target

-> Maybe Subst

This is similar to tcMatchTy, but extends a substitution See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTysX

Arguments

:: Subst

Substitution to extend

-> [Type]

Template

-> [Type]

Target

-> Maybe Subst

One-shot substitution

Like tcMatchTys, but extending a substitution See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTyKisX

Arguments

:: Subst

Substitution to extend

-> [Type]

Template

-> [Type]

Target

-> Maybe Subst

One-shot substitution

Like tcMatchTyKis, but extending a substitution See also Note [tcMatchTy vs tcMatchTyKi]

tcMatchTyX_BM :: BindFun -> Subst -> Type -> Type -> Maybe Subst

ruleMatchTyKiX

Arguments

:: TyCoVarSet

template variables

-> RnEnv2

-> TvSubstEnv

type substitution to extend

-> Type

Template

-> Type

Target

-> Maybe TvSubstEnv

This one is called from the expression matcher, which already has a MatchEnv in hand

tcUnifyTy :: Type -> Type -> Maybe Subst

Simple unification of two types; all type variables are bindable Precondition: the kinds are already equal

tcUnifyTyKi :: Type -> Type -> Maybe Subst

Like tcUnifyTy, but also unifies the kinds

tcUnifyTys

Arguments

:: BindFun

-> [Type]

-> [Type]

-> Maybe Subst

A regular one-shot (idempotent) substitution that unifies the erased types. See comments for tcUnifyTysFG

tcUnifyTyKis :: BindFun -> [Type] -> [Type] -> Maybe Subst

Like tcUnifyTys but also unifies the kinds

tcUnifyTysFG :: BindFun -> [Type] -> [Type] -> UnifyResult

tcUnifyTysFG bind_tv tys1 tys2 attempts to find a substitution s (whose domain elements all respond BindMe to bind_tv) such that s(tys1) and that of s(tys2) are equal, as witnessed by the returned Coercions. This version requires that the kinds of the types are the same, if you unify left-to-right.

tcUnifyTyWithTFs

Arguments

:: Bool

True = do two-way unification; False = do one-way matching. See end of sec 5.2 from the paper

-> InScopeSet

-> Type

-> Type

-> Maybe Subst

Unify two types, treating type family applications as possibly unifying with anything and looking through injective type family applications. Precondition: kinds are the same

type BindFun = TyCoVar -> Type -> BindFlag

Some unification functions are parameterised by a BindFun, which says whether or not to allow a certain unification to take place. A BindFun takes the TyVar involved along with the Type it will potentially be bound to.

It is possible for the variable to actually be a coercion variable (Note [Matching coercion variables]), but only when one-way matching. In this case, the Type will be a CoercionTy.

data BindFlag

Constructors

BindMe

A regular type variable

Apart

Declare that this type variable is apart from the type provided. That is, the type variable will never be instantiated to that type. See also Note [Binding when looking up instances] in GHC.Core.InstEnv.

Instances

Eq BindFlag

Defined in GHC.Core.Unify

Methods

(==) :: BindFlag -> BindFlag -> Bool

(/=) :: BindFlag -> BindFlag -> Bool

matchBindFun :: TyCoVarSet -> BindFun

Allow binding only for any variable in the set. Variables may be bound to any type. Used when doing simple matching; e.g. can we find a substitution

S = [a :-> t1, b :-> t2] such that
    S( Maybe (a, b->Int )  =   Maybe (Bool, Char -> Int)

alwaysBindFun :: BindFun

Allow the binding of any variable to any type

type UnifyResult = UnifyResultM Subst

data UnifyResultM a

See Note [Unification result]

Constructors

Unifiable a

MaybeApart MaybeApartReason a

SurelyApart

Instances

Applicative UnifyResultM

Defined in GHC.Core.Unify

Methods

pure :: a -> UnifyResultM a

(<*>) :: UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b

liftA2 :: (a -> b -> c) -> UnifyResultM a -> UnifyResultM b -> UnifyResultM c

(*>) :: UnifyResultM a -> UnifyResultM b -> UnifyResultM b

(<*) :: UnifyResultM a -> UnifyResultM b -> UnifyResultM a

Functor UnifyResultM

Defined in GHC.Core.Unify

Methods

fmap :: (a -> b) -> UnifyResultM a -> UnifyResultM b

(<$) :: a -> UnifyResultM b -> UnifyResultM a

Monad UnifyResultM

Defined in GHC.Core.Unify

Methods

(>>=) :: UnifyResultM a -> (a -> UnifyResultM b) -> UnifyResultM b

(>>) :: UnifyResultM a -> UnifyResultM b -> UnifyResultM b

return :: a -> UnifyResultM a

Outputable a => Outputable (UnifyResultM a)

Defined in GHC.Core.Unify

Methods

ppr :: UnifyResultM a -> SDoc

data MaybeApartReason

Why are two types MaybeApart? MARInfinite takes precedence: This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint; it's really only MARInfinite that's interesting here.

Constructors

MARTypeFamily

matching e.g. F Int ~? Bool

MARInfinite

matching e.g. a ~? Maybe a

MARTypeVsConstraint

matching Type ~? Constraint or the arrow types See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim

Instances

Semigroup MaybeApartReason

Defined in GHC.Core.Unify

Methods

(<>) :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason

sconcat :: NonEmpty MaybeApartReason -> MaybeApartReason

stimes :: Integral b => b -> MaybeApartReason -> MaybeApartReason

Outputable MaybeApartReason

Defined in GHC.Core.Unify

Methods

ppr :: MaybeApartReason -> SDoc

typesCantMatch :: [(Type, Type)] -> Bool

Given a list of pairs of types, are any two members of a pair surely apart, even after arbitrary type function evaluation and substitution?

typesAreApart :: Type -> Type -> Bool

liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext

liftCoMatch is sort of inverse to liftCoSubst. In particular, if liftCoMatch vars ty co == Just s, then liftCoSubst s ty == co, where == there means that the result of liftCoSubst has the same type as the original co; but may be different under the hood. That is, it matches a type against a coercion of the same "shape", and returns a lifting substitution which could have been used to produce the given coercion from the given type. Note that this function is incomplete -- it might return Nothing when there does indeed exist a possible lifting context.

This function is incomplete in that it doesn't respect the equality in eqType. That is, it's possible that this will succeed for t1 and fail for t2, even when t1 eqType t2. That's because it depends on there being a very similar structure between the type and the coercion. This incompleteness shouldn't be all that surprising, especially because it depends on the structure of the coercion, which is a silly thing to do.

The lifting context produced doesn't have to be exacting in the roles of the mappings. This is because any use of the lifting context will also require a desired role. Thus, this algorithm prefers mapping to nominal coercions where it can do so.

flattenTys :: InScopeSet -> [Type] -> [Type]

flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))