Version 1 (modified by chak, 8 years ago) (diff) |
---|

# Normalising and Solving Type Equalities

The following is based on ideas for the new, post-ICFP'08 solving algorithm. Most of the code is in the module `TcTyFuns`.

## Normal equalities

Central to the algorithm are **normal equalities**, which can be regarded as a set of rewrite rules. Normal equalities are carefully oriented and contain applications of synonym family applications only in outermost positions of left-hand sides. They assume one of the following three forms:

`co :: F t1..tn ~ t`,`co :: x ~ t`, where`x`is a flexible type variable, or`co :: a ~ t`, where`a`is a rigid type variable (skolem) and`t`is*not*a flexible type variable.

and `t`, `t1`, ..., `tn` contain no applications of synonym families. Coercions `co` are either wanteds (represented by a flexible type variable) or givens (represented by type term of kind CO).

NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.