You are answering a question you want to answer, not the one I asked! :)

Yes, dependent types can encode nice constraints, but so can asserts and assumes.

I am not seeing the fundamental difference in yeeting these constraints to a solver. Dafny seems to do the same thing with Z3.