I think it's a major step towards more pleasant type-level programming in haskel...

I think it's a major step towards more pleasant type-level programming in haskell. I recently worked on a very type-level heavy side-project and the matchability is a real issue.

I think this could drastically simplify the whole singletons-library and would also enable proving stuff via induction entirly in the type-level.