Well yes, but those are still static types. :) And of course, you're not forced to use dependent types, so "regular" statically typed programs are just a subse

Well yes, but those are still static types. :) And of course, you're not forced to use dependent types, so "regular" statically typed programs are just a subset of dependently typed ones.