remove trailing newlines from Display etc

nikomatsakis · nikomatsakis · commit 54c85447ca64 · 2024-01-02T06:45:24.000-05:00
These trailing newlines mess with `expect_test`
which has some bugs in this area.

It also just seems better.
diff --git 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<String> = 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<T: Debug> std::fmt::Display for ProvenSet<T> {
             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<T: Debug> std::fmt::Display for ProvenSet<T> {
 
 fn indent(s: impl std::fmt::Display) -> String {
     let s = s.to_string();
-    s.lines()
+    let lines: Vec<String> = 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
@@ -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
@@ -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 <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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
@@ -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
@@ -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 <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
                       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 <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
-    "#]]);
+                        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 <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
 }
 
 #[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 <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
                                   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 <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
-    "#]]);
+                                    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 <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
 }
diff --git 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
@@ -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 <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> 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 <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> 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 <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> 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 <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> 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 <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> 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 <ty> , trait Magic <ty> where {Copy(^ty0_0)}], [impl <ty> 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
@@ -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>`
-            "#]]);
+                                    `?ty_0` occurs in `Vec<?ty_0>`"#]]);
 }
 
 /// Test that `X = Vec<Y>` 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>`
-    "#]]);
+                                    `?ty_0` occurs in `Vec<?ty_0>`"#]]);
 }
 
 /// Test that `X = Vec<X>` 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>`
-    "#]]);
+                                    `?ty_0` occurs in `Vec<?ty_0>`"#]]);
 }
diff --git 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
@@ -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
@@ -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
@@ -12,4 +12,3 @@ Caused by:
                    judgment `prove_wc { goal: B(!ty_0), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 <ty, ty> ], [impl <ty> 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
@@ -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
@@ -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 <ty, const> 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
@@ -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 <ty> 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 <ty> where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }`
-       
diff --git 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
@@ -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 <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {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()`
-       

Original file line number	Diff line number	Diff line change
`@@ -51,8 +51,7 @@ fn judgment() {`
`51`	`51`	`transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"`
`52`	`52`	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):
`53`	`53`	`the rule "base" failed at step #1 (src/file.rs:LL:CC) because`
`54`		- condition evaluted to false: `b % 2 == 0`
`55`		`- "#]]);`
	`54`	+ condition evaluted to false: `b % 2 == 0`"#]]);
`56`	`55`
`57`	`56`	`transitive_reachable(&graph, 2).assert_ok(expect_test::expect![[r#"`
`58`	`57`	`{`
Original file line number	Diff line number	Diff line change
`@@ -63,6 +63,5 @@ fn not_well_formed_adt() {`
`63`	`63`	`the rule "some" failed at step #0 (src/file.rs:LL:CC) because`
`64`	`64`	judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
`65`	`65`	`the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because`
`66`		- expression evaluated to an empty collection: `decls.trait_invariants()`
`67`		`- "#]]);`
	`66`	+ expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
`68`	`67`	`}`
Original file line number	Diff line number	Diff line change
`@@ -192,8 +192,7 @@ fn test_normalize_assoc_ty_existential0() {`
`192`	`192`	`the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because`
`193`	`193`	condition evaluted to false: `env.universe(p) < env.universe(v)`
`194`	`194`	`the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because`
`195`		- expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`
`196`		`- "#]]);`
	`195`	+ expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]);
`197`	`196`	`}`
`198`	`197`
`199`	`198`	`#[test]`
Original file line number	Diff line number	Diff line change
`@@ -21,8 +21,7 @@ fn test_forall_not_local() {`
`21`	`21`	`the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because`
`22`	`22`	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):
`23`	`23`	`the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because`
`24`		- condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
`25`		`- "#]]);`
	`24`	+ condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`"#]]);
`26`	`25`	`}`
`27`	`26`
`28`	`27`	`#[test]`
Original file line number	Diff line number	Diff line change
`@@ -26,8 +26,7 @@ fn exists_u_for_t() {`
`26`	`26`	`the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because`
`27`	`27`	pattern `None` did not match value `Some(!ty_1)`
`28`	`28`	`the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because`
`29`		- condition evaluted to false: `env.universe(p) < env.universe(v)`
`30`		`- "#]]);`
	`29`	+ condition evaluted to false: `env.universe(p) < env.universe(v)`"#]]);
`31`	`30`	`}`
`32`	`31`
`33`	`32`	`/// There is U that is equal to some T.`