On: New extension to Haskell -- data types and polymorphism at the type level

[bremac]

Interesting. The extensions to the type system remind me of Ωmega (http://code.google.com/p/omega/), though without higher-order kinds.

EDIT: Turns out "Programming in Omega" is cited by the section on related work. No wonder the mention of proving red-black trees using type-level computation seemed familiar...

[thesz → bremac]

Omega became what called now "type families".

Types at the kind level and kind polymorphism is much more close to dependent type system.

Honestly, I cannot wait. ;)