This is true, and also applies to other systems with dependent types. Generally speaking, when you do this dance, it's best to work with total functions that te

This is true, and also applies to other systems with dependent types. Generally speaking, when you do this dance, it's best to work with total functions that terminate, i.e., algorithms. If in the chunk example, he used an option type to make the function total, the problem you pointed out would go away. And you would also be left in a better place than if you weren't using fancy types, as other functions can now use the fact that the result is a chunk of size eight.