GHC.TypeLits.Normalise.Unify

Nat expressions <-> SOP terms

newtype CType

Constructors

CType

Fields

• unCType :: Type

Instances

Eq CType

Methods

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

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

Ord CType

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

Methods

ppr :: CType -> SDoc

pprPrec :: Rational -> CType -> SDoc

type CoreSOP = SOP TyVar CType

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)

Methods

ppr :: UnifyItem v c n -> SDoc

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

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

type CoreUnify a = TyUnify TyVar CType 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

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 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

Properties

isNatural :: CoreSOP -> Maybe Bool