Gradual Refinement Typing


If we ever want to add to Refinement Typing to Rust, I think it’s probably better to add them as gradual (like the gradual typing of Scheme), “Gradual Refinement Types”, by Nico Lehmann and Éric Tanter:

There are still some missing parts like the measures, but this helps introduce refinement types in older code, just in the parts where it matters.

You probably also want to add a compiler switch that prints all the spots where the compiler adds run-time tests where normal types and refined types interact.