Add an extra rule for rigidty

Author: tiif

crates/formality-prove/src/prove/prove_wc.rs

@@ -149,6 +149,13 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c)
         )
 
+        (
+            (if ty.is_rigid())!
+            (is_int(&decl, &env, assumptions, ty) => c)
+            ----------------------------- ("rigidty is int")
+            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
+        )
+
         (
             (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))
             (let assumptions = c1.substitution().apply(&assumptions))

src/test/mir_fn_bodies.rs

@@ -663,7 +663,7 @@ fn test_invalid_value_in_switch_terminator() {
                 judgment `prove_wc_list { goal: {@ is_int(bool)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                   the rule "some" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `prove_wc { goal: @ is_int(bool), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
-                      the rule "ty is int" failed at step #0 (src/file.rs:LL:CC) because
+                      the rule "rigidty is int" failed at step #1 (src/file.rs:LL:CC) because
                         judgment `is_int { goal: bool, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s):
                           the rule "is int" failed at step #0 (src/file.rs:LL:CC) because
                             condition evaluted to false: `id.is_int()`