status/may13.md

@@ -48,7 +48,10 @@ Meanwhile others have been adding new features.
 
 - **Rebindable list syntax.** A GHC extension called [overloaded lists](overloaded-lists) was added by Achim Krause, George Giorgidze, and colleagues. When this is turned on, the way GHC desugars explicit lists and lists in arithmetic sequence notation is changed. Instead of directly desugaring to built-in lists, a polymorphic witness function is used, similar to the desugaring of numeric literals. This allows for a more flexible use of list notations, supporting many different list-like types. In addition, the functions used in this desugaring process are completely rebindable.
 
-- type level natural numbers \[**Iavor S. Diatchki**\]
+- **Type level natural numbers**.  Iavor S. Diatchki has been working on a solver for equations involving type-level natural numbers.  This allows simplifying and reasoning about type-level terms involving
+  arithmetic. Currently, the solver can evaluate equations and inequalities mentioning the type functions `(+)`, `(*)`, `(^)`, and `(<=)`.  The solver works pretty well when it can use evaluation to prove equalities (e.g., examples like `2 + 5 = x`, `2 + x = 5`).  There is also some support for taking advantage of the commutativity and associativity of `(+)`, `(*)`.   More experimental features include:  support for `(-)`, which, currently is implemented by desugaring to `(+)`;  the type-level function `FromNat1`, which has special support for working with natural number literals, and thus can be used to expose some of their inductive structure.  This work is currently on the `type-nats` branch, and the plan is to merge it into HEAD into the next few months.
+
+- **Kinds without data** Trevor Elliott, Eric Mertens, and Iavor Diatchki have began implementing support for "data kind" declarations, described in more detail on the GHC wiki:    [ http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData](http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData)   The idea is to allow a new form of declaration that introduces a new kind, whose members are described by the (type) constructors in the declaration.   This is similar to promoting `data` declarations, except that no new value-level-constructors are declared, and it also allows the constructors to mention other kinds that do not have corresponding type-level representation (e.g., `*`).
 
 - **Ordered overlapping type family instances.** Richard Eisenberg has implemented support for ordered overlapping type family instances, called *branched* instances. This allows type-level functions to use patterns in a similar way to term-level functions. For example: