Oh, I think I just confused refinement types with dependent types. The above still stands though.