These are refinement types, rather than dependent types. The main distinction as I understand it being that refinement types allow you to state assertions at a

These are refinement types, rather than dependent types. The main distinction as I understand it being that refinement types allow you to state assertions at a meta-level which are submitted to an SMT solver which may or may not prove them correct, dependent types on the other hand allow expression of arbitrary constraints within the types themselves, along with arbitrary proofs satisfying these types.