GHC.TypeLits.Normalise.Unify

Nat expressions <-> SOP terms

newtype CType

Constructors

CType

Fields

• unCType :: Type

Instances

Eq CType

Defined in GHC.TypeLits.Normalise.Unify

Methods

(==) :: CType -> CType -> Bool

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

Ord CType

Defined in GHC.TypeLits.Normalise.Unify

Methods

compare :: CType -> CType -> Ordering

(<) :: CType -> CType -> Bool

(<=) :: CType -> CType -> Bool

(>) :: CType -> CType -> Bool

(>=) :: CType -> CType -> Bool

max :: CType -> CType -> CType

min :: CType -> CType -> CType

Outputable CType

Defined in GHC.TypeLits.Normalise.Unify

Methods

ppr :: CType -> SDoc

pprPrec :: Rational -> CType -> SDoc

type CoreSOP = SOP TyVar CType

SOP with TyVar variables

normaliseNat :: Type -> Writer [(Type, 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 (+,-,*,^)

normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)

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.

normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type

reifySOP :: CoreSOP -> Type

Convert a SOP term back to a type of kind Nat

Substitution on SOP terms

data UnifyItem v c

Constructors

SubstItem

Fields

• siVar :: v
• siSOP :: SOP v c

UnifyItem

Fields

• siLHS :: SOP v c
• siRHS :: SOP v c

Instances

(Eq v, Eq c) => Eq (UnifyItem v c)

Defined in GHC.TypeLits.Normalise.Unify

Methods

(==) :: UnifyItem v c -> UnifyItem v c -> Bool

(/=) :: UnifyItem v c -> UnifyItem v c -> Bool

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

Defined in GHC.TypeLits.Normalise.Unify

Methods

ppr :: UnifyItem v c -> SDoc

pprPrec :: Rational -> UnifyItem v c -> SDoc

type CoreUnify = UnifyItem TyVar CType

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) => [UnifyItem v c] -> SOP v c -> SOP v c

Apply a substitution to a single normalised SOP term

substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]

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]

Two terms are only equal if the given substitution holds

Instances

Outputable UnifyResult

Defined in GHC.TypeLits.Normalise.Unify

Methods

ppr :: UnifyResult -> SDoc

pprPrec :: Rational -> UnifyResult -> SDoc

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]

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

Inequalities

subtractIneq :: (CoreSOP, CoreSOP, Bool) -> 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)  = (-2*y + 3*x)
subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y)

solveIneq

Arguments

:: Word

Solving depth

-> Ineq

Inequality we want to solve

-> Ineq

Given/proven inequality

-> WriterT (Set CType) Maybe Bool

Solver result

• Nothing: exhausted solver steps
• Just True: inequality is solved
• Just False: solver is unable to solve inequality, note that this does not mean the wanted inequality does not hold.

Try to solve inequalities

ineqToSubst :: Ineq -> Maybe CoreUnify

Give the smallest solution for an inequality

subtractionToPred :: (Type, Type) -> (PredType, Kind)

instantSolveIneq

Arguments

:: Word

Solving depth

-> Ineq

Inequality we want to solve

-> WriterT (Set CType) Maybe Bool

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

solvedInEqSmallestConstraint :: [(Bool, Set a)] -> (Bool, Set a)

Properties

isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool