include condition argument values in the output

nikomatsakis · nikomatsakis · commit f913710b0203 · 2024-01-03T06:26:02.000-05:00
diff --git a/crates/formality-core/src/judgment.rs b/crates/formality-core/src/judgment.rs
@@ -288,33 +288,104 @@ macro_rules! push_rules {
     // expression `v` is carried in from the conclusion and forms the final
     // output of this rule, once all the conditions are evaluated.
 
-    (@body $args:tt; $inputs:tt; $step_index:expr; (if $c:expr) $($m:tt)*) => {
-        if $c {
+    (@body $args:tt; $inputs:tt; $step_index:expr; (if let $p:pat = $e:expr) $($m:tt)*) => {
+        let value = &$e;
+        if let $p = Clone::clone(value) {
             $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
         } else {
-            $crate::push_rules!(@record_failure $inputs; $step_index, $c; $crate::judgment::RuleFailureCause::IfFalse {
-                expr: stringify!($c).to_string(),
+            $crate::push_rules!(@record_failure $inputs; $step_index, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
+                pattern: stringify!($p).to_string(),
+                value: format!("{:?}", value),
             });
         }
     };
 
-    (@body $args:tt; $inputs:tt; $step_index:expr; (assert $c:expr) $($m:tt)*) => {
-        assert!($c);
-        $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+    // For `(if ...)`, we have special treatment to try and extract the arguments so we can give better information
+    // about why the expression evaluated to false.
+    (@body $args:tt; $inputs:tt; $step_index:expr; (if $($c:tt)*) $($m:tt)*) => {
+        $crate::push_rules!(@body_if $args; $inputs; $step_index; $($c)*; $($c)*; $($m)*)
     };
 
-    (@body $args:tt; $inputs:tt; $step_index:expr; (if let $p:pat = $e:expr) $($m:tt)*) => {
-        let value = &$e;
-        if let $p = Clone::clone(value) {
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); arg0.$method(); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); !arg0.$method(); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0.$method(arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); !arg0.$method(arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( $arg1:expr, $arg2:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1, arg2 = $arg2); arg0.$method(arg1, arg2); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( $arg1:expr, $arg2:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1, arg2 = $arg2); !arg0.$method(arg1, arg2); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $func:ident ( $arg0:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); $func(arg0); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $func:ident ( $arg0:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); !$func(arg0); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $func:ident ( $arg0:expr, $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); $func(arg0, arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; ! $func:ident ( $arg0:expr, $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); ! $func(arg0, arg1); $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident == $arg1:ident; $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0 == arg1; $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident != $arg1:ident; $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0 != arg1; $origcond; $($m)*)
+    };
+
+    (@body_if $args:tt; $inputs:tt; $step_index:expr; $e:expr; $origcond:expr; $($m:tt)*) => {
+        $crate::push_rules!(@structured_if $args; $inputs; $step_index; (); $e; $origcond; $($m)*)
+    };
+
+    (@structured_if $args:tt; $inputs:tt; $step_index:expr; ($($argn:ident = $arge:expr),*); $cond:expr; $origcond:expr; $($m:tt)*) => {
+        $(
+            let $argn = &$arge;
+        )*
+        if {
+            $(
+                let $argn = Clone::clone($argn);
+            )*
+            $cond
+        } {
             $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
         } else {
-            $crate::push_rules!(@record_failure $inputs; $step_index, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
-                pattern: stringify!($p).to_string(),
-                value: format!("{:?}", value),
+            $crate::push_rules!(@record_failure $inputs; $step_index, $origcond; $crate::judgment::RuleFailureCause::IfFalse {
+                expr: stringify!($origcond).to_string(),
+                args: vec![
+                    $(
+                        (stringify!($arge).to_string(), format!("{:?}", $argn)),
+                    )*
+                ],
             });
         }
     };
 
+    (@body $args:tt; $inputs:tt; $step_index:expr; (assert $c:expr) $($m:tt)*) => {
+        assert!($c);
+        $crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
+    };
+
     (@body $args:tt; $inputs:tt; $step_index:expr; ($i:expr => $p:pat) $($m:tt)*) => {
         // Explicitly calling `into_iter` silences some annoying lints
         // in the case where `$i` is an `Option` or a `Result`
diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs
@@ -1,4 +1,4 @@
-use crate::{set, Set, SetExt};
+use crate::{set, Set};
 use std::{
     fmt::Debug,
     hash::{Hash, Hasher},
@@ -385,7 +385,14 @@ impl FailedRule {
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug)]
 pub enum RuleFailureCause {
     /// The rule did not succeed because an `(if X)` condition evaluated to false.
-    IfFalse { expr: String },
+    IfFalse {
+        /// The stringified form of the expression.
+        expr: String,
+
+        /// A set of pairs with the stringified form of arguments within the expression plus the debug representation of its value.
+        /// This is a best effort extraction via the macro.
+        args: Vec<(String, String)>,
+    },
 
     /// The rule did not succeed because an `(if let)` pattern failed to match.
     IfLetDidNotMatch { pattern: String, value: String },
@@ -466,8 +473,12 @@ impl std::fmt::Display for FailedRule {
 impl std::fmt::Display for RuleFailureCause {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
-            RuleFailureCause::IfFalse { expr } => {
-                write!(f, "condition evaluted to false: `{expr}`")
+            RuleFailureCause::IfFalse { expr, args } => {
+                write!(f, "condition evaluted to false: `{expr}`")?;
+                for (arg_expr, arg_value) in args {
+                    write!(f, "\n  {arg_expr} = {arg_value}")?;
+                }
+                Ok(())
             }
             RuleFailureCause::IfLetDidNotMatch { pattern, value } => {
                 write!(f, "pattern `{pattern}` did not match value `{value}`")
diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs
@@ -21,7 +21,9 @@ fn test_forall_not_local() {
                   the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because
                     judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
                       the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because
-                        condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`"#]]);
+                        condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
+                          decls = decls(222, [], [], [], [], [], [], {}, {})
+                          &goal.trait_id = Debug"#]]);
 }
 
 #[test]
diff --git a/tests/judgment-error-reporting/cyclic_judgment.rs b/tests/judgment-error-reporting/cyclic_judgment.rs
@@ -74,7 +74,9 @@ fn test() {
       expect_test::expect![[r#"
           judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
             the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
-              condition evaluted to false: `name_a == name_b`"#]]
+              condition evaluted to false: `name_a == name_b`
+                name_a = Foo
+                name_b = Bar"#]]
     );
 }
 
@@ -93,37 +95,51 @@ fn test1() {
               judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                 the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
                   condition evaluted to false: `name_a == name_b`
+                    name_a = Foo
+                    name_b = Bar
             the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
               judgment `sub { a: class(Foo), b: my(class(Bar)) }` failed at the following rule(s):
                 the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
                   judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                     the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
                       condition evaluted to false: `name_a == name_b`
+                        name_a = Foo
+                        name_b = Bar
                 the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
                   judgment `sub { a: my(class(Foo)), b: my(class(Bar)) }` failed at the following rule(s):
                     the rule "both my" failed at step #0 (src/file.rs:LL:CC) because
                       judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                         the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
                           condition evaluted to false: `name_a == name_b`
+                            name_a = Foo
+                            name_b = Bar
                     the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
                       judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                         the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
                           condition evaluted to false: `name_a == name_b`
+                            name_a = Foo
+                            name_b = Bar
             the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
               judgment `sub { a: my(class(Foo)), b: my(class(Bar)) }` failed at the following rule(s):
                 the rule "both my" failed at step #0 (src/file.rs:LL:CC) because
                   judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                     the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
                       condition evaluted to false: `name_a == name_b`
+                        name_a = Foo
+                        name_b = Bar
                 the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
                   judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                     the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
                       condition evaluted to false: `name_a == name_b`
+                        name_a = Foo
+                        name_b = Bar
                 the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
                   judgment `sub { a: class(Foo), b: my(class(Bar)) }` failed at the following rule(s):
                     the rule "equivalent" failed at step #3 (src/file.rs:LL:CC) because
                       judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
                         the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
-                          condition evaluted to false: `name_a == name_b`"#]]
+                          condition evaluted to false: `name_a == name_b`
+                            name_a = Foo
+                            name_b = Bar"#]]
     );
 }
diff --git a/tests/judgment-error-reporting/fallible.rs b/tests/judgment-error-reporting/fallible.rs
@@ -44,5 +44,7 @@ fn test() {
         Caused by:
             judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
               the rule "same class" failed at step #0 (src/file.rs:LL:CC) because
-                condition evaluted to false: `name_a == name_b`"#]]);
+                condition evaluted to false: `name_a == name_b`
+                  name_a = Foo
+                  name_b = Bar"#]]);
 }
diff --git a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr
@@ -10,7 +10,13 @@ Caused by:
                 judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait <ty> ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s):
                   the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because
                     condition evaluted to false: `is_fundamental(&decls, &name)`
+                      &decls = decls(222, [trait CoreTrait <ty> ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {})
+                      &name = (adt CoreStruct)
                   the rule "local rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:156:17) because
                     condition evaluted to false: `decls.is_local_adt_id(&a)`
+                      decls = decls(222, [trait CoreTrait <ty> ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {})
+                      &a = CoreStruct
               the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because
                 condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
+                  decls = decls(222, [trait CoreTrait <ty> ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {})
+                  &goal.trait_id = CoreTrait
diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr
@@ -12,5 +12,9 @@ Caused by:
                     judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait <ty> , trait Unit <ty> ], [impl <ty> Unit(^ty0_0), impl CoreTrait(<FooStruct as Unit>::Assoc)], [], [alias <ty> <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s):
                       the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because
                         condition evaluted to false: `is_fundamental(&decls, &name)`
+                          &decls = decls(222, [trait CoreTrait <ty> , trait Unit <ty> ], [impl <ty> Unit(^ty0_0), impl CoreTrait(<FooStruct as Unit>::Assoc)], [], [alias <ty> <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct})
+                          &name = tuple(0)
               the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because
                 condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
+                  decls = decls(222, [trait CoreTrait <ty> , trait Unit <ty> ], [impl <ty> Unit(^ty0_0), impl CoreTrait(<FooStruct as Unit>::Assoc)], [], [alias <ty> <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct})
+                  &goal.trait_id = CoreTrait
diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
@@ -12,7 +12,13 @@ Caused by:
                     judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait <ty> , trait Mirror <ty> ], [impl <ty> Mirror(^ty0_0), impl CoreTrait(<CoreStruct as Mirror>::Assoc)], [], [alias <ty> <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s):
                       the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because
                         condition evaluted to false: `is_fundamental(&decls, &name)`
+                          &decls = decls(222, [trait CoreTrait <ty> , trait Mirror <ty> ], [impl <ty> Mirror(^ty0_0), impl CoreTrait(<CoreStruct as Mirror>::Assoc)], [], [alias <ty> <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {})
+                          &name = (adt CoreStruct)
                       the rule "local rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:156:17) because
                         condition evaluted to false: `decls.is_local_adt_id(&a)`
+                          decls = decls(222, [trait CoreTrait <ty> , trait Mirror <ty> ], [impl <ty> Mirror(^ty0_0), impl CoreTrait(<CoreStruct as Mirror>::Assoc)], [], [alias <ty> <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {})
+                          &a = CoreStruct
               the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because
                 condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
+                  decls = decls(222, [trait CoreTrait <ty> , trait Mirror <ty> ], [impl <ty> Mirror(^ty0_0), impl CoreTrait(<CoreStruct as Mirror>::Assoc)], [], [alias <ty> <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {})
+                  &goal.trait_id = CoreTrait
diff --git a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr
@@ -10,7 +10,13 @@ Caused by:
                 judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait <ty> ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s):
                   the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because
                     condition evaluted to false: `is_fundamental(&decls, &name)`
+                      &decls = decls(222, [trait CoreTrait <ty> ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {})
+                      &name = (adt CoreStruct)
                   the rule "local rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:156:17) because
                     condition evaluted to false: `decls.is_local_adt_id(&a)`
+                      decls = decls(222, [trait CoreTrait <ty> ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {})
+                      &a = CoreStruct
               the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because
                 condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
+                  decls = decls(222, [trait CoreTrait <ty> ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {})
+                  &goal.trait_id = CoreTrait
diff --git a/tests/ui/coherence_orphan/uncovered_T.stderr b/tests/ui/coherence_orphan/uncovered_T.stderr

Original file line number	Diff line number	Diff line change
`@@ -44,5 +44,7 @@ fn test() {`
`44`	`44`	`Caused by:`
`45`	`45`	judgment `sub { a: class(Foo), b: class(Bar) }` failed at the following rule(s):
`46`	`46`	`the rule "same class" failed at step #0 (src/file.rs:LL:CC) because`
`47`		- condition evaluted to false: `name_a == name_b`"#]]);
	`47`	+ condition evaluted to false: `name_a == name_b`
	`48`	`+ name_a = Foo`
	`49`	`+ name_b = Bar"#]]);`
`48`	`50`	`}`