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

GHC.TypeLits.Normalise.Unify

Description

Synopsis

# `Nat` expressions <-> `SOP` terms

`SOP` with `TyVar` variables

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 `(+,-,*,^)`

Convert a `SOP` term back to a type of kind `Nat`

# Substitution on `SOP` terms

data SubstItem v c n Source

Constructors

 SubstItem FieldssiVar :: v siSOP :: SOP v c siNote :: n

Instances

 (Outputable v, Outputable c) => Outputable (SubstItem v c n) Source

type TySubst v c n = [SubstItem v c n] 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

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 CoreSubst Two terms are only equal if the given substitution holds

Instances

 Source

Given two `SOP`s `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.

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

Find the `TyVar` in a `CoreSOP`