...  ...  @@ 48,7 +48,10 @@ Meanwhile others have been adding new features. 





 **Rebindable list syntax.** A GHC extension called [overloaded lists](overloadedlists) 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 builtin 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 listlike 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 typelevel natural numbers. This allows simplifying and reasoning about typelevel 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 typelevel 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 `typenats` 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 valuelevelconstructors are declared, and it also allows the constructors to mention other kinds that do not have corresponding typelevel representation (e.g., `*`).






 **Ordered overlapping type family instances.** Richard Eisenberg has implemented support for ordered overlapping type family instances, called *branched* instances. This allows typelevel functions to use patterns in a similar way to termlevel functions. For example:




...  ...  