It turned out that function preconditions weren't getting checked at all, so you could write a constraint on a fn decl that was total nonsense. Fixed now.