I once coded red-black-trees in Haskell at the type level and yes, I had to write some type-level tests. In a real dependently-typed language the friction woul

I once coded red-black-trees in Haskell at the type level and yes, I had to write some type-level tests. In a real dependently-typed language the friction would be lower, because it's easier to put "normal code" at the type level. Perhaps I could have skipped some type-level tests by introducing more kind-safety...