Make is_int work with normalization

Author: tiif

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

@@ -10,6 +10,7 @@ use crate::{
         prove,
         prove_after::prove_after,
         prove_eq::prove_eq,
+        prove_normalize::prove_normalize,
         prove_via::prove_via,
         prove_wf::prove_wf,
     },
@@ -149,9 +150,11 @@ judgment_fn! {
         )
 
         (
-            (is_int(decl, env, assumptions, ty) => c)
+            (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))
+            (let assumptions = c1.substitution().apply(&assumptions))
+            (is_int(&decl, &env, assumptions, p) => c2)
             ----------------------------- ("ty is int")
-            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
+            (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c2)
         )
     }
 }

tests/projection.rs

@@ -141,12 +141,5 @@ fn test_ty_is_int() {
         TEST_TY_IS_INT,
         "{} => { @is_int(<u16 as Id>::This) }",
     )
-    .assert_err(expect_test::expect![[r#"
-        judgment `prove { goal: {@ is_int(<u16 as Id>::This)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Id <ty> ], [impl <ty> Id(^ty0_0)], [], [alias <ty> <^ty0_0 as Id>::This = ^ty0_0], [], [], {Id}, {}) }` failed at the following rule(s):
-          failed at (src/file.rs:LL:CC) because
-            judgment `prove_wc_list { goal: {@ is_int(<u16 as Id>::This)}, 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(<u16 as Id>::This), 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
-                    judgment had no applicable rules: `is_int { goal: <u16 as Id>::This, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }`"#]]);
+    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }}"]);
 }