[danidiaz]

If the project had no existing dependent types at all, couldn't you just perform a runtime check before calling the library? The check would return evidence that [i: i%2 == 0] for the particular i, or fail at runtime. If it succeeded, then you could invoke the library using the new evidence.

One appealing aspect of dependent types is that they let you decouple validation of inputs from the function calls themselves, while still disallowing passing wrong inputs to the function by mistake.

[bjz_]

Yup, lots of people are under the impression that you need to prove everything when it comes to DTs. That's not true - you can indeed push these checks to runtime, and just have the compiler make ensure you do it.