There's also a project for implementing a prolog like interpreter for doing type checking and other logic for Rust, I think it works on the MIR level, but could be wrong on that.