Comment by throwthrow0987

>It has been some time I worked seriously in a dependently-typed language, but I recall coming to the conclusion that dependent types are best used as little as possible, for exactly this reason.

For which reason sorry?