GHC.TypeLits.Normalise.Unify

Nat expressions <-> SOP terms

type CoreSOP = SOP TyVar Type

SOP with TyVar variables

normaliseNat :: Type -> CoreSOP

Convert a type of kind Nat to an SOP term, but only when the type is constructed out of:

• literals
• type variables
• Applications of the arithmetic operators (+,-,*,^)

reifySOP :: CoreSOP -> Type

Convert a SOP term back to a type of kind Nat

Substitution on SOP terms

data UnifyItem v c n

Constructors

SubstItem

Fields

siVar :: v

siSOP :: SOP v c

siNote :: n

UnifyItem

Fields

siLHS :: SOP v c

siRHS :: SOP v c

siNote :: n

Instances

(Outputable v, Outputable c) => Outputable (UnifyItem v c n)

type TyUnify v c n = [UnifyItem v c n]

type CoreUnify a = TyUnify TyVar Type a

A substitution is essentially a list of (variable, SOP) pairs, but we keep the original Ct that lead to the substitution being made, for use when turning the substitution back into constraints.

substsSOP :: (Ord v, Ord c) => TyUnify v c n -> SOP v c -> SOP v c

Apply a substitution to a single normalised SOP term

substsSubst :: (Ord v, Ord c) => TyUnify v c n -> TyUnify v c n -> TyUnify v c n

Apply a substitution to a substitution

Find unifiers

data UnifyResult

Result of comparing two SOP terms, returning a potential substitution list under which the two terms are equal.

Constructors

Win

Two terms are equal

Lose

Two terms are not equal

Draw (CoreUnify Ct)

Two terms are only equal if the given substitution holds

Instances

Outputable UnifyResult

unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult

Given two SOPs u and v, when their free variables (fvSOP) are the same, then we Win if u and v are equal, and Lose otherwise.

If u and v do not have the same free variables, we result in a Draw, ware u and v are only equal when the returned CoreSubst holds.

unifiers :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct

Find unifiers for two SOP terms

Can find the following unifiers:

t ~ a + b          ==>  [t := a + b]
a + b ~ t          ==>  [t := a + b]
(a + c) ~ (b + c)  ==>  [a := b]
(2*a) ~ (2*b)      ==>  [a := b]
(2 + a) ~ 5        ==>  [a := 3]
(i * a) ~ j        ==>  [a := div j i], when (mod j i == 0)

However, given a wanted:

[W] t ~ a + b

this function returns [], or otherwise we "solve" the constraint by finding a unifier equal to the constraint.

However, given a wanted:

[W] (a + c) ~ (b + c)

we do return the unifier:

[a := b]

Free variables in SOP terms

fvSOP :: CoreSOP -> UniqSet TyVar

Find the TyVar in a CoreSOP