ghc-8.0.2: The GHC API

Safe HaskellNone
LanguageHaskell2010

Unify

Contents

Synopsis

Documentation

tcMatchTy :: Type -> Type -> Maybe TCvSubst Source #

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.

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.

tcMatchTys Source #

Arguments

:: [Type]

Template

-> [Type]

Target

-> Maybe TCvSubst

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

Like tcMatchTy but over a list of types.

tcMatchTyX Source #

Arguments

:: TCvSubst

Substitution to extend

-> Type

Template

-> Type

Target

-> Maybe TCvSubst 

This is similar to tcMatchTy, but extends a substitution

tcMatchTysX Source #

Arguments

:: TCvSubst

Substitution to extend

-> [Type]

Template

-> [Type]

Target

-> Maybe TCvSubst

One-shot substitution

Like tcMatchTys, but extending a substitution

tcUnifyTyWithTFs Source #

Arguments

:: Bool

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

-> Type 
-> Type 
-> Maybe TCvSubst 

Unify two types, treating type family applications as possibly unifying with anything and looking through injective type family applications.

ruleMatchTyX Source #

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

Rough matching

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

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

tcUnifyTys Source #

Arguments

:: (TyCoVar -> BindFlag) 
-> [Type] 
-> [Type] 
-> Maybe TCvSubst

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

tcUnifyTysFG :: (TyVar -> BindFlag) -> [Type] -> [Type] -> UnifyResult Source #

tcUnifyTysFG bind_tv tys1 tys2 attepts 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.

data BindFlag Source #

Constructors

BindMe 
Skolem 

Instances

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

liftCoMatch is sort of inverse to liftCoSubst. In particular, if liftCoMatch vars ty co == Just s, then tyCoSubst s ty == co, where == there means that the result of tyCoSubst 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.