Ssa warn for constraints that will always succeed/fail

[jfecher]

It is possible that code like constrain a != 0 can be known to always fail if the ssa pass evaluates a to 0, resulting in constrain 0 != 0. Before, the ssa code would crash with a failed assert that a != b, but PR #223 removed most of these in favor of having the code fail to verify instead.

Can we give better warning messages here that points users to the correct location in the source code?

[jfecher]

It would be possible to give better diagnostics if the arguments to a constrain have const types during type checking, letting users know it will either always succeed/fail. We can issue a warning for the always succeed case and an error for the always fail case.

This would trigger the warning not only for things like constrain 0 < 5 but also:

for i in 2..10 {
    let i2 = i / 2;
    constrain i2 >= 1;
}

The main case this would fail to catch are cases using private variables that reduce to the two sides being equivalent:

fn foo(x: Field) {
    let y = x;
    constrain x == y; // no warning...
}

[kevaundray]

The new ssa code contains source location information, so closing this. We can open a new issue if we need the new SSA to improve in its current functionality