Slightly tweak the logic

Author: tiif

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

@@ -150,17 +150,17 @@ judgment_fn! {
         )
 
         (
-            (if ty.is_rigid())!
             (is_int(&decl, &env, assumptions, ty) => c)
-            ----------------------------- ("rigidty is int")
+            ----------------------------- ("ty is int")
             (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c)
         )
 
         (
+            (if ty.is_alias())!
             (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))
             (let assumptions = c1.substitution().apply(&assumptions))
             (is_int(&decl, &env, assumptions, p) => c2)
-            ----------------------------- ("ty is int")
+            ----------------------------- ("aliasty is int")
             (prove_wc(decl, env, assumptions, Relation::IsInt(ty)) => c2)
         )
     }

crates/formality-types/src/grammar/ty.rs

@@ -40,8 +40,8 @@ impl Ty {
         }
     }
 
-    pub fn is_rigid(&self) -> bool {
-        matches!(self.data(), TyData::RigidTy(_))
+    pub fn is_alias(&self) -> bool {
+        matches!(self.data(), TyData::AliasTy(_))
     }
 
     pub fn rigid(name: impl Upcast<RigidName>, parameters: impl Upcast<Vec<Parameter>>) -> Self {

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 "rigidty is int" failed at step #1 (src/file.rs:LL:CC) because
+                      the rule "ty is int" failed at step #0 (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()`