diff options
| author | Iavor S. Diatchki <iavor.diatchki@gmail.com> | 2013-09-12 23:19:21 -0700 |
|---|---|---|
| committer | Iavor S. Diatchki <iavor.diatchki@gmail.com> | 2013-09-12 23:19:21 -0700 |
| commit | 1f77a5341cbd6649a6bc2af868002728cd79b9d7 (patch) | |
| tree | 66daf8120722af710af7d99530d142993d9ddb44 /compiler/deSugar | |
| parent | ad15c2b4bd37082ce989268b3d2f86a2cd34386a (diff) | |
| download | haskell-1f77a5341cbd6649a6bc2af868002728cd79b9d7.tar.gz | |
Add support for evaluation of type-level natural numbers.
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`.
Diffstat (limited to 'compiler/deSugar')
| -rw-r--r-- | compiler/deSugar/DsBinds.lhs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs index 617516bd97..a1f5e77b5f 100644 --- a/compiler/deSugar/DsBinds.lhs +++ b/compiler/deSugar/DsBinds.lhs @@ -847,6 +847,11 @@ ds_tc_coercion subst role tc_co go r (TcCastCo co1 co2) = maybeSubCo r $ mkCoCast (go Nominal co1) (go Nominal co2) go r (TcCoVarCo v) = maybeSubCo r $ ds_ev_id subst v + go _ (TcAxiomRuleCo co ts cs) = AxiomRuleCo co + (map (Coercion.substTy subst) ts) + (map (go Nominal) cs) + + ds_co_binds :: TcEvBinds -> CvSubst ds_co_binds (EvBinds bs) = foldl ds_scc subst (sccEvBinds bs) |