• Iavor S. Diatchki's avatar
    Add support for evaluation of type-level natural numbers. · 1f77a534
    Iavor S. Diatchki authored
    This patch implements some simple evaluation of type-level expressions
    featuring natural numbers.  We can evaluate *concrete* expressions that
    use the built-in type families (+), (*), (^), and (<=?), declared in
    GHC.TypeLits.   We can also do some type inference involving these
    functions.  For example, if we encounter a constraint such as `(2 + x) ~ 5`
    we can infer that `x` must be 3.  Note, however, this is used only to
    resolve unification variables (i.e., as a form of a constraint improvement)
    and not to generate new facts.  This is similar to how functional
    dependencies work in GHC.
    The patch adds a new form of coercion, `AxiomRuleCo`, which makes use
    of a new form of axiom called `CoAxiomRule`.  This is the form of evidence
    generate when we solve a constraint, such as `(1 + 2) ~ 3`.
    The patch also adds support for built-in type-families, by adding a new
    form of TyCon rhs: `BuiltInSynFamTyCon`.  such built-in type-family
    constructors contain a record with functions that are used by the
    constraint solver to simplify and improve constraints involving the
    built-in function (see `TcInteract`).  The record in defined in `FamInst`.
    The type constructors and rules for evaluating the type-level functions
    are in a new module called `TcTypeNats`.
Coercion.lhs 67.8 KB