GHC.TypeLits.Normalise.Unify

SOP with TyVar variables

Convert a type of kind Nat to an SOP term

Applies normaliseNat and simplifySOP to type or predicates to reduce any occurrences of sub-terms of kind Nat. If the result is the same as input, returns Nothing.

Convert a SOP term back to a type of kind Nat

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.

Apply a substitution to a single normalised SOP term

Apply a substitution to a substitution

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

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, where u and v are only equal when the returned CoreSubst holds.

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]

Find the TyVar in a CoreSOP

Subtract an inequality, in order to either:

• See if the smallest solution is a natural number

• Cancel sums, i.e. monotonicity of addition

subtractIneq (2*y <=? 3*x ~ True)  = 3*x + (-2)*y
subtractIneq (2*y <=? 3*x ~ False) = -3*x + (-2)*y

Try to solve inequalities

Give the smallest solution for an inequality

Try to instantly solve an inequality by using the inequality solver using 1 <=? 1 ~ True as the given constraint.

Is this a natural number?

• Just True = definitely a natural number

• Just False = definitely not a natural number

• Nothing = not sure

The 'Set CType' writer accumulator returns inner types that must also be positive for the overall CoreSOP to be positive.