It's also important to note that you can embed SMT-driven refinement types into a fully dependently typed language; that's what F* does. I wonder how feasible doing something similar in Idris via the elaborator reflection and type provider faculties is. I remember Brady did something following a similar principle in one of the elaborator reflection papers with automated proofs of termination, but without calling into an external SMT solver.