Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.
How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.