The paper mentions HList, the "heterogeneous list" package, which often gets used for extensible records and static duck typing; HList uses type-level numbers and lists, and extensive type-level computation. I've wanted to use HList in the past, but the sheer pain of the types involved made it not worth the trouble. It also includes several (incompatible) variations of internal implementations with different tradeoffs.
Several packages exist for "session typing", which allows specification of a communication protocol between functions by using complementary types. Those involve heavy type-level computation on families of related types; this extension would help greatly.
I've personally encountered multiple cases where I'd like to operate on an arbitrary function or type regardless of its arity (how many arguments it takes), but doing so typically requires writing a family of handlers for various argument lengths. This extension would allow handling all of the cases generically.
 J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. (Shamelessly copied from Wikipedia)
What I'm getting at is that there are plenty of parts of GHC's flavor of Haskell that you can't depend on type inference for. You have to give type signatures for polymorphic recursion, for instance.
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...
Types at the kind level and kind polymorphism is much more close to dependent type system.
Honestly, I cannot wait. ;)
Read about the async keyword in C# if you want to know why monads are useful. I'm not sure why MSFT decided to take a great thing like monads and only allow one type of monad instead of building in support for the general case, it seems so typical in imperative languages that the forest is missed for the trees. They'll take a great thing like generics and then screw it up by only allowing methods on classes which ruins type inference.
var a = new Array<int>(1,2,3,4);
var a = Array.new(1,2,3,4);
So, my question is how extending the type system might be turned into a concrete feature in a "mainstream" language. It's not too often that we need to prove things about red-black trees.
I'd say it's like only knowing what an array is instead of being able to generalize to an Enumerable/Iterable thing.