The following (compile-fail/loop-pred-constraints.rs) should not compile: ``` fn print_even(y: int) : even(y) { log(debug, y); } pure fn even(y: int) -> bool { true } fn main() { let mut y = 42; check (even(y)); loop { print_even(y); loop { y += 1; break; } } } ``` Removing the inner `loop` or changing it to a `do` (back when `do existed) gives the correct error.