From 6c6f20667f9c0e224a1815e220d8c83244dad73c Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 2 Jan 2024 05:27:46 -0500 Subject: [PATCH 1/7] normalize paths in `assert_err` (doh!) --- crates/formality-core/src/test_util.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/formality-core/src/test_util.rs b/crates/formality-core/src/test_util.rs index b9ee9a01..091d27d5 100644 --- a/crates/formality-core/src/test_util.rs +++ b/crates/formality-core/src/test_util.rs @@ -75,7 +75,7 @@ where match self { Ok(v) => panic!("expected `Err`, got `Ok`: {v:?}"), Err(e) => { - expect.assert_eq(&format!("{e:?}")); + expect.assert_eq(&normalize_paths(format!("{e:?}"))); } } } From 4285909a157d1077f017329c0dbe49a8d0ab4553 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 2 Jan 2024 05:29:11 -0500 Subject: [PATCH 2/7] add track_caller annotations --- crates/formality-core/src/test_util.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/crates/formality-core/src/test_util.rs b/crates/formality-core/src/test_util.rs index 091d27d5..c361a28b 100644 --- a/crates/formality-core/src/test_util.rs +++ b/crates/formality-core/src/test_util.rs @@ -60,6 +60,7 @@ where T: Debug, E: Debug, { + #[track_caller] fn assert_ok(self, expect: expect_test::Expect) { match self { Ok(v) => { @@ -71,6 +72,7 @@ where } } + #[track_caller] fn assert_err(self, expect: expect_test::Expect) { match self { Ok(v) => panic!("expected `Err`, got `Ok`: {v:?}"), From 29cb1c8785539001c92a4f0532ce58c98a977733 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 2 Jan 2024 05:51:45 -0500 Subject: [PATCH 3/7] improve the span for "wrong judgment name" error --- crates/formality-core/src/judgment.rs | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/crates/formality-core/src/judgment.rs b/crates/formality-core/src/judgment.rs index ffc687b8..48a099f0 100644 --- a/crates/formality-core/src/judgment.rs +++ b/crates/formality-core/src/judgment.rs @@ -178,15 +178,20 @@ macro_rules! push_rules { ) => { // Found the conclusion. { - // give the user a type error if the name they gave - // in the conclusion is not the same as the name of the - // function - #[allow(dead_code)] - struct WrongJudgmentNameInConclusion; - const _: WrongJudgmentNameInConclusion = { - let $judgment_name = WrongJudgmentNameInConclusion; + $crate::respan!( $conclusion_name - }; + ( + // give the user a type error if the name they gave + // in the conclusion is not the same as the name of the + // function + #[allow(dead_code)] + struct WrongJudgmentNameInConclusion; + const _: WrongJudgmentNameInConclusion = { + let $judgment_name = WrongJudgmentNameInConclusion; + $conclusion_name + }; + ) + ); if let Some(__JudgmentStruct($($input_names),*)) = Some($input_value) { $crate::push_rules!(@match From d12672a7bc5218e2d7ddd03df6e538e403b5be60 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 2 Jan 2024 06:43:40 -0500 Subject: [PATCH 4/7] add test demonstrating problems with formatting this test looks right, and if you run with `UPDATE_EXPECT=1` it is not changed, but if you run without it, you get an error --- tests/judgment-error-reporting/fallible.rs | 49 ++++++++++++++++++++++ tests/judgment-error-reporting/main.rs | 1 + 2 files changed, 50 insertions(+) create mode 100644 tests/judgment-error-reporting/fallible.rs diff --git a/tests/judgment-error-reporting/fallible.rs b/tests/judgment-error-reporting/fallible.rs new file mode 100644 index 00000000..87202ddb --- /dev/null +++ b/tests/judgment-error-reporting/fallible.rs @@ -0,0 +1,49 @@ +use anyhow::Context; +use formality_core::{judgment_fn, term, test, test_util::ResultTestExt, Fallible}; + +#[term] +enum Ty { + Class { name: ClassName }, +} + +formality_core::id!(ClassName); + +judgment_fn! { + fn sub( + a: Ty, + b: Ty, + ) => () { + debug(a, b) + + ( + (if name_a == name_b) + ---------------------- ("same class") + (sub(Ty::Class { name: name_a }, Ty::Class { name: name_b }) => ()) + ) + } +} + +fn check_sub(a: Ty, b: Ty) -> Fallible<()> { + Ok(sub(a, b) + .check_proven() + .with_context(|| format!("check_sub"))?) +} + +#[test] +fn test() { + let foo = Ty::Class { + name: ClassName::new("Foo"), + }; + let bar = Ty::Class { + name: ClassName::new("Bar"), + }; + // Demonstrates a multi-line error rendered by anyhow. + check_sub(foo, bar).assert_err(expect_test::expect![[r#" + check_sub + + 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` + "#]]); +} diff --git a/tests/judgment-error-reporting/main.rs b/tests/judgment-error-reporting/main.rs index d70762ee..da0b7a2f 100644 --- a/tests/judgment-error-reporting/main.rs +++ b/tests/judgment-error-reporting/main.rs @@ -20,6 +20,7 @@ formality_core::declare_language! { use jer::FormalityLang; mod cyclic_judgment; +mod fallible; mod grammar; fn main() -> Fallible<()> { From 54c85447ca64470a5e8d4e52a488483045d40ed6 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 2 Jan 2024 06:37:35 -0500 Subject: [PATCH 5/7] remove trailing newlines from Display etc These trailing newlines mess with `expect_test` which has some bugs in this area. It also just seems better. --- crates/formality-core/src/judgment/proven_set.rs | 16 +++++++--------- .../formality-core/src/judgment/test_filtered.rs | 3 +-- crates/formality-prove/src/test/adt_wf.rs | 3 +-- .../formality-prove/src/test/eq_assumptions.rs | 3 +-- crates/formality-prove/src/test/eq_partial_eq.rs | 6 ++---- crates/formality-prove/src/test/is_local.rs | 3 +-- crates/formality-prove/src/test/magic_copy.rs | 6 ++---- crates/formality-prove/src/test/occurs_check.rs | 9 +++------ crates/formality-prove/src/test/universes.rs | 3 +-- .../judgment-error-reporting/cyclic_judgment.rs | 6 ++---- tests/judgment-error-reporting/fallible.rs | 3 +-- tests/ui/basic_where_clauses_fail.stderr | 1 - .../CoreTrait_for_CoreStruct_in_Foo.stderr | 1 - tests/ui/coherence_orphan/alias_to_unit.stderr | 1 - .../ui/coherence_orphan/mirror_CoreStruct.stderr | 1 - .../neg_CoreTrait_for_CoreStruct_in_Foo.stderr | 1 - tests/ui/coherence_orphan/uncovered_T.stderr | 1 - tests/ui/consts/generic_mismatch.stderr | 1 - tests/ui/consts/mismatch.stderr | 1 - .../ui/consts/nonsense_rigid_const_bound.stderr | 1 - tests/ui/fn/lifetime.stderr | 1 - tests/ui/hello_world_fail.stderr | 1 - 22 files changed, 22 insertions(+), 50 deletions(-) diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs index 8fb5a012..2d83d9c7 100644 --- a/crates/formality-core/src/judgment/proven_set.rs +++ b/crates/formality-core/src/judgment/proven_set.rs @@ -426,8 +426,8 @@ impl std::fmt::Display for FailedJudgment { if failed_rules.is_empty() { write!(f, "judgment had no applicable rules: `{judgment}` ",) } else { - let rules: String = failed_rules.iter().map(|r| r.to_string()).collect(); - let rules = indent(rules); + let rules: Vec = failed_rules.iter().map(|r| r.to_string()).collect(); + let rules = indent(rules.join("\n")); write!( f, "judgment `{judgment}` failed at the following rule(s):\n{rules}" @@ -492,7 +492,7 @@ impl std::fmt::Display for ProvenSet { Data::Success(set) => { write!(f, "{{\n")?; for item in set { - write!(f, "{}", indent(format!("{item:?},\n")))?; + write!(f, "{},\n", indent(format!("{item:?}")))?; } write!(f, "}}\n")?; Ok(()) @@ -503,14 +503,12 @@ impl std::fmt::Display for ProvenSet { fn indent(s: impl std::fmt::Display) -> String { let s = s.to_string(); - s.lines() + let lines: Vec = s + .lines() .map(|l| format!(" {l}")) .map(|l| l.trim_end().to_string()) - .map(|mut l| { - l.push_str("\n"); - l - }) - .collect() + .collect(); + lines.join("\n") } /// This trait is used for the `(foo => bar)` patterns. diff --git a/crates/formality-core/src/judgment/test_filtered.rs b/crates/formality-core/src/judgment/test_filtered.rs index 600dc398..08995737 100644 --- a/crates/formality-core/src/judgment/test_filtered.rs +++ b/crates/formality-core/src/judgment/test_filtered.rs @@ -51,8 +51,7 @@ fn judgment() { transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#" judgment `transitive_reachable { node: 0, g: Graph { edges: [(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)] } }` failed at the following rule(s): the rule "base" failed at step #1 (src/file.rs:LL:CC) because - condition evaluted to false: `b % 2 == 0` - "#]]); + condition evaluted to false: `b % 2 == 0`"#]]); transitive_reachable(&graph, 2).assert_ok(expect_test::expect![[r#" { diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs index dd791af7..6a9dc5ce 100644 --- a/crates/formality-prove/src/test/adt_wf.rs +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -63,6 +63,5 @@ fn not_well_formed_adt() { the rule "some" failed at step #0 (src/file.rs:LL:CC) because judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because - expression evaluated to an empty collection: `decls.trait_invariants()` - "#]]); + expression evaluated to an empty collection: `decls.trait_invariants()`"#]]); } diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs index d6f41650..dd77a9a1 100644 --- a/crates/formality-prove/src/test/eq_assumptions.rs +++ b/crates/formality-prove/src/test/eq_assumptions.rs @@ -192,8 +192,7 @@ fn test_normalize_assoc_ty_existential0() { the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `env.universe(p) < env.universe(v)` the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because - expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` - "#]]); + expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]); } #[test] diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index fd953abc..149f0b9f 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -54,8 +54,7 @@ fn not_partial_eq_implies_eq() { the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - "#]]); + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }`"#]]); } #[test] @@ -102,6 +101,5 @@ fn universals_not_eq() { the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` - "#]]); + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }`"#]]); } diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index 23b6d070..8e86db91 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -21,8 +21,7 @@ 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)`"#]]); } #[test] diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 9faf0dc9..1bb5172d 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -69,8 +69,7 @@ fn all_t_not_magic() { the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - "#]]); + judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]); } #[test] @@ -139,6 +138,5 @@ fn all_t_not_copy() { the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` - "#]]); + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]); } diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index 4c7c836a..57df5325 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -30,8 +30,7 @@ fn direct_cycle() { the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because judgment `equate_variable` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - `?ty_0` occurs in `Vec` - "#]]); + `?ty_0` occurs in `Vec`"#]]); } /// Test that `X = Vec` can be solved @@ -76,8 +75,7 @@ fn indirect_cycle_1() { the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because judgment `equate_variable` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - `?ty_0` occurs in `Vec` - "#]]); + `?ty_0` occurs in `Vec`"#]]); } /// Test that `X = Vec` cannot be solved (when constructed over several steps) @@ -102,6 +100,5 @@ fn indirect_cycle_2() { the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because judgment `equate_variable` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - `?ty_0` occurs in `Vec` - "#]]); + `?ty_0` occurs in `Vec`"#]]); } diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index 804cc214..f091a6af 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -26,8 +26,7 @@ fn exists_u_for_t() { the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_1)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because - condition evaluted to false: `env.universe(p) < env.universe(v)` - "#]]); + condition evaluted to false: `env.universe(p) < env.universe(v)`"#]]); } /// There is U that is equal to some T. diff --git a/tests/judgment-error-reporting/cyclic_judgment.rs b/tests/judgment-error-reporting/cyclic_judgment.rs index 442d5283..7ded93a7 100644 --- a/tests/judgment-error-reporting/cyclic_judgment.rs +++ b/tests/judgment-error-reporting/cyclic_judgment.rs @@ -74,8 +74,7 @@ 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`"#]] ); } @@ -125,7 +124,6 @@ fn test1() { 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`"#]] ); } diff --git a/tests/judgment-error-reporting/fallible.rs b/tests/judgment-error-reporting/fallible.rs index 87202ddb..d8d36ad4 100644 --- a/tests/judgment-error-reporting/fallible.rs +++ b/tests/judgment-error-reporting/fallible.rs @@ -44,6 +44,5 @@ 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`"#]]); } diff --git a/tests/ui/basic_where_clauses_fail.stderr b/tests/ui/basic_where_clauses_fail.stderr index 7110b98c..c6b2630e 100644 --- a/tests/ui/basic_where_clauses_fail.stderr +++ b/tests/ui/basic_where_clauses_fail.stderr @@ -12,4 +12,3 @@ Caused by: judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because expression evaluated to an empty collection: `decls.trait_invariants()` - diff --git a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr index 82cef8b4..b462c9dd 100644 --- a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr +++ b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr @@ -14,4 +14,3 @@ Caused by: condition evaluted to false: `decls.is_local_adt_id(&a)` 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)` - diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr index 095587a6..41de190f 100644 --- a/tests/ui/coherence_orphan/alias_to_unit.stderr +++ b/tests/ui/coherence_orphan/alias_to_unit.stderr @@ -14,4 +14,3 @@ Caused by: condition evaluted to false: `is_fundamental(&decls, &name)` 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)` - diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr index 087dcc96..83c37dd4 100644 --- a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr +++ b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr @@ -16,4 +16,3 @@ Caused by: condition evaluted to false: `decls.is_local_adt_id(&a)` 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)` - 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 index b999aeda..dea5536b 100644 --- a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr +++ b/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr @@ -14,4 +14,3 @@ Caused by: condition evaluted to false: `decls.is_local_adt_id(&a)` 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)` - diff --git a/tests/ui/coherence_orphan/uncovered_T.stderr b/tests/ui/coherence_orphan/uncovered_T.stderr index 6129af51..ae01cdff 100644 --- a/tests/ui/coherence_orphan/uncovered_T.stderr +++ b/tests/ui/coherence_orphan/uncovered_T.stderr @@ -8,4 +8,3 @@ Caused by: judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): 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)` - diff --git a/tests/ui/consts/generic_mismatch.stderr b/tests/ui/consts/generic_mismatch.stderr index 8ca90a2e..882a9b77 100644 --- a/tests/ui/consts/generic_mismatch.stderr +++ b/tests/ui/consts/generic_mismatch.stderr @@ -14,4 +14,3 @@ Caused by: pattern `Some((_, const_ty))` did not match value `None` the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because expression evaluated to an empty collection: `decls.trait_invariants()` - diff --git a/tests/ui/consts/mismatch.stderr b/tests/ui/consts/mismatch.stderr index 408f4bd6..5462ed60 100644 --- a/tests/ui/consts/mismatch.stderr +++ b/tests/ui/consts/mismatch.stderr @@ -6,4 +6,3 @@ Caused by: judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because expression evaluated to an empty collection: `decls.trait_invariants()` - diff --git a/tests/ui/consts/nonsense_rigid_const_bound.stderr b/tests/ui/consts/nonsense_rigid_const_bound.stderr index 7ad682cb..a022eaef 100644 --- a/tests/ui/consts/nonsense_rigid_const_bound.stderr +++ b/tests/ui/consts/nonsense_rigid_const_bound.stderr @@ -21,4 +21,3 @@ Caused by: judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` the rule "symmetric" failed at step #0 (crates/formality-prove/src/prove/prove_eq.rs:38:14) because cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` - diff --git a/tests/ui/fn/lifetime.stderr b/tests/ui/fn/lifetime.stderr index 8163a002..937b530f 100644 --- a/tests/ui/fn/lifetime.stderr +++ b/tests/ui/fn/lifetime.stderr @@ -3,4 +3,3 @@ Error: judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, en judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "parameter well formed" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:117:14) because judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` - diff --git a/tests/ui/hello_world_fail.stderr b/tests/ui/hello_world_fail.stderr index edd01a3f..17442cc2 100644 --- a/tests/ui/hello_world_fail.stderr +++ b/tests/ui/hello_world_fail.stderr @@ -11,4 +11,3 @@ Caused by: judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because expression evaluated to an empty collection: `decls.trait_invariants()` - From 6d4aacd3fd159b0477ccb1bdf731eda5aeb2344d Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Wed, 3 Jan 2024 06:25:22 -0500 Subject: [PATCH 6/7] improve SetExt to operate on &Set and Set and do some mild renaming --- crates/formality-core/src/collections.rs | 46 +++++++++++++++---- .../formality-core/src/judgment/proven_set.rs | 9 ++-- 2 files changed, 43 insertions(+), 12 deletions(-) diff --git a/crates/formality-core/src/collections.rs b/crates/formality-core/src/collections.rs index 84c5053e..63792ad3 100644 --- a/crates/formality-core/src/collections.rs +++ b/crates/formality-core/src/collections.rs @@ -70,13 +70,37 @@ impl VecExt for Vec { } pub trait SetExt: Sized { - fn split_first(self) -> Option<(T, Self)>; + fn split_first(self) -> Option<(T, Set)>; - fn union_with(self, other: Self) -> Self; + fn union_with(self, other: impl Upcast>) -> Set; - fn plus(self, other: T) -> Self; + fn with_element(self, other: impl Upcast) -> Set; - fn split_nth(&self, i: usize) -> Option<(T, Self)>; + fn without_element(self, other: impl Upcast) -> Set; + + fn split_nth(&self, i: usize) -> Option<(T, Set)>; +} + +impl SetExt for &Set { + fn split_first(self) -> Option<(T, Set)> { + self.clone().split_first() + } + + fn union_with(self, other: impl Upcast>) -> Set { + self.clone().union_with(other) + } + + fn with_element(self, other: impl Upcast) -> Set { + self.clone().with_element(other) + } + + fn without_element(self, other: impl Upcast) -> Set { + self.clone().without_element(other) + } + + fn split_nth(&self, i: usize) -> Option<(T, Set)> { + >::split_nth(self, i) + } } impl SetExt for Set { @@ -87,22 +111,28 @@ impl SetExt for Set { Some((e, c)) } - fn split_nth(&self, i: usize) -> Option<(T, Self)> { + fn split_nth(&self, i: usize) -> Option<(T, Set)> { let mut s = self.clone(); let item = self.iter().skip(i).next()?; let item = s.take(item).unwrap(); Some((item, s)) } - fn union_with(mut self, other: Self) -> Self { + fn union_with(mut self, other: impl Upcast>) -> Set { + let other: Set = other.upcast(); for item in other { self.insert(item); } self } - fn plus(mut self, other: T) -> Self { - self.insert(other); + fn with_element(mut self, other: impl Upcast) -> Set { + self.insert(other.upcast()); + self + } + + fn without_element(mut self, other: impl Upcast) -> Set { + self.remove(&other.upcast()); self } } diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs index 2d83d9c7..db5781d6 100644 --- a/crates/formality-core/src/judgment/proven_set.rs +++ b/crates/formality-core/src/judgment/proven_set.rs @@ -316,11 +316,12 @@ impl FailedJudgment { // This will return a boolean indicating if all the failed rules // ultimately failed because of a cycle. + let mut stack1 = stack.clone(); + stack1.insert(&judgment.judgment); + let judgment_has_non_cycle; - (judgment.failed_rules, judgment_has_non_cycle) = Self::strip_cycles( - stack.clone().plus(&judgment.judgment), - judgment.failed_rules, - ); + (judgment.failed_rules, judgment_has_non_cycle) = + Self::strip_cycles(stack1, judgment.failed_rules); failed_rule.cause = RuleFailureCause::FailedJudgment(judgment); if judgment_has_non_cycle.0 { From f913710b020397c527a6a7db86a6f9d3e1266e82 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Wed, 3 Jan 2024 06:26:02 -0500 Subject: [PATCH 7/7] include condition argument values in the output --- crates/formality-core/src/judgment.rs | 97 ++++++++++++++++--- .../formality-core/src/judgment/proven_set.rs | 19 +++- crates/formality-prove/src/test/is_local.rs | 4 +- .../cyclic_judgment.rs | 20 +++- tests/judgment-error-reporting/fallible.rs | 4 +- .../CoreTrait_for_CoreStruct_in_Foo.stderr | 6 ++ .../ui/coherence_orphan/alias_to_unit.stderr | 4 + .../coherence_orphan/mirror_CoreStruct.stderr | 6 ++ ...neg_CoreTrait_for_CoreStruct_in_Foo.stderr | 6 ++ tests/ui/coherence_orphan/uncovered_T.stderr | 2 + 10 files changed, 147 insertions(+), 21 deletions(-) diff --git a/crates/formality-core/src/judgment.rs b/crates/formality-core/src/judgment.rs index 48a099f0..ef35435b 100644 --- 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 index db5781d6..8b2c2a71 100644 --- 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 index 8e86db91..adcafefc 100644 --- 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 index 7ded93a7..d7506776 100644 --- 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 index d8d36ad4..017c3968 100644 --- 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 index b462c9dd..034ac2ad 100644 --- 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 ], [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 ], [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 ], [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 ], [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 index 41de190f..c7493056 100644 --- 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 , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 index 83c37dd4..60113b62 100644 --- 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 , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^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 index dea5536b..8ea95ce3 100644 --- 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 ], [], [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 ], [], [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 ], [], [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 ], [], [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 index ae01cdff..2432395d 100644 --- a/tests/ui/coherence_orphan/uncovered_T.stderr +++ b/tests/ui/coherence_orphan/uncovered_T.stderr @@ -8,3 +8,5 @@ Caused by: judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): 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 ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) + &goal.trait_id = CoreTrait