Right. I'm not saying there is no advantage to putting the machinery in place so that chunks of size 9, 10, 11, etc. are easier to express in the type system. T

Right. I'm not saying there is no advantage to putting the machinery in place so that chunks of size 9, 10, 11, etc. are easier to express in the type system. The problem I have with this is that there is a bit of dependent type theory envy going on and if you watch the talk linked in the article the required boilerplate is non-trivial.