ghc-typelits-natnormalise-0.1: GHC typechecker plugin for types of kind GHC.TypeLits.Nat

Copyright(C) 2015, University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <>
Safe HaskellNone






Nat expressions <-> SOP terms

type CoreSOP = SOP TyVar Type Source

SOP with TyVar variables

normaliseNat :: Type -> CoreSOP Source

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 Source

Convert a SOP term back to a type of kind Nat

Substitution on SOP terms

data SubstItem v c n Source




siVar :: v
siSOP :: SOP v c
siNote :: n


type TySubst v c n = [SubstItem v c n] Source

type CoreSubst = TySubst TyVar Type Ct Source

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) => TySubst v c n -> SOP v c -> SOP v c Source

Apply a substitution to a single normalised SOP term

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

Apply a substitution to a substitution

Find unifiers

data UnifyResult Source

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



Two terms are equal


Two terms are not equal

Draw CoreSubst

Two terms are only equal if the given substitution holds

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

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

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]

However, given a wanted:

[W] t ~ a + b

this function returns [], or otherwise we "solve" the contstraint 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