From 65fe16abec0d6758121b866496976f1a9099b854 Mon Sep 17 00:00:00 2001 From: kadmin Date: Wed, 2 Aug 2023 07:01:02 +0000 Subject: [PATCH] Add new exhaustive covering predicate & Add additional tests --- .../formality-core/src/judgment/proven_set.rs | 8 + crates/formality-prove/src/prove/prove_wc.rs | 92 +++++++-- crates/formality-types/src/grammar/consts.rs | 4 + .../formality-types/src/grammar/formulas.rs | 13 ++ crates/formality-types/src/grammar/wc.rs | 39 +++- tests/coherence_overlap.rs | 16 +- tests/consts.rs | 183 ------------------ .../cyclic_judgment.rs | 6 +- tests/ui/basic_where_clauses_fail.stderr | 8 +- .../CoreTrait_for_CoreStruct_in_Foo.stderr | 2 +- .../ui/coherence_orphan/alias_to_unit.stderr | 2 +- .../coherence_orphan/mirror_CoreStruct.stderr | 2 +- ...neg_CoreTrait_for_CoreStruct_in_Foo.stderr | 2 +- tests/ui/coherence_orphan/uncovered_T.stderr | 2 +- "tests/ui/consts/double.\360\237\224\254" | 8 + tests/ui/consts/exhaustive.stderr | 30 +++ "tests/ui/consts/exhaustive.\360\237\224\254" | 12 ++ tests/ui/consts/generic_mismatch.stderr | 10 +- tests/ui/consts/mismatch.stderr | 6 +- .../consts/nonsense_rigid_const_bound.stderr | 4 +- tests/ui/consts/not_covering.stderr | 28 +++ .../ui/consts/not_covering.\360\237\224\254" | 10 + .../consts/trait_with_const.\360\237\224\254" | 11 ++ ...trait_with_generic_const.\360\237\224\254" | 11 ++ tests/ui/fn/lifetime.stderr | 2 +- tests/ui/hello_world_fail.stderr | 8 +- 26 files changed, 290 insertions(+), 229 deletions(-) delete mode 100644 tests/consts.rs create mode 100644 "tests/ui/consts/double.\360\237\224\254" create mode 100644 tests/ui/consts/exhaustive.stderr create mode 100644 "tests/ui/consts/exhaustive.\360\237\224\254" create mode 100644 tests/ui/consts/not_covering.stderr create mode 100644 "tests/ui/consts/not_covering.\360\237\224\254" create mode 100644 "tests/ui/consts/trait_with_const.\360\237\224\254" create mode 100644 "tests/ui/consts/trait_with_generic_const.\360\237\224\254" diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs index 8b2c2a71..f8498679 100644 --- a/crates/formality-core/src/judgment/proven_set.rs +++ b/crates/formality-core/src/judgment/proven_set.rs @@ -99,6 +99,14 @@ impl ProvenSet { } } + /// Convert to a non-empty set of proven results (if ok) or an error (otherwise). + pub fn into_iter(self) -> Box> where T: 'static { + match self.data { + Data::Failure(_) => Box::new(std::iter::empty()), + Data::Success(s) => Box::new(s.into_iter()), + } + } + /// For each item `t` that was proven, /// invoke `op(t)` to yield a new set of proven results /// and then flatten those into a new proven set. diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 3d63afdf..ed03e94d 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -1,20 +1,35 @@ -use formality_core::judgment_fn; -use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs}; - -use crate::{ - decls::Decls, - prove::{ - env::Env, - is_local::{is_local_trait_ref, may_be_remote}, - prove, - prove_after::prove_after, - prove_eq::prove_eq, - prove_via::prove_via, - prove_wf::prove_wf, - }, +use crate::prove; +use crate::prove::prove_eq::prove_eq; +use crate::prove::prove_wf::prove_wf; +use crate::prove::prove_after::prove_after; +use crate::prove::is_local::is_local_trait_ref; +use crate::prove::prove_via::prove_via; +use crate::prove::is_local::may_be_remote; +use crate::Env; +use crate::Decls; + +use crate::Constraints; +use formality_core::{judgment_fn, Upcasted, ProvenSet}; +use formality_types::grammar::{ + Const, ExhaustiveState, Parameter, Predicate, Relation, Scalar, Ty, Wc, WcData, Wcs, }; -use super::constraints::Constraints; +pub fn is_covering(vals: &[ExhaustiveState], params: &[Parameter]) -> Wcs { + assert_eq!(vals.len(), params.len()); + vals.iter() + .zip(params.iter()) + .filter_map(|(a, b)| match a { + ExhaustiveState::ExactMatch => None, + ExhaustiveState::ConstCover(cs) => { + let Parameter::Const(c) = b else { + todo!(); + }; + Some(Predicate::Covers(cs.clone(), c.clone())) + } + }) + .upcasted() + .collect() +} judgment_fn! { pub fn prove_wc( @@ -46,6 +61,34 @@ judgment_fn! { (prove_wc(decls, env, assumptions, WcData::PR(goal)) => c) ) + ( + (let mut covering_consts = vec![ExhaustiveState::ExactMatch; trait_ref.parameters.len()]) + (let asmp = &assumptions) + (let d = &decls) + (d.impl_decls(&trait_ref.trait_id).flat_map(|i| { + + let (env, subst) = env.clone().existential_substitution(&i.binder); + let i = i.binder.instantiate_with(&subst).unwrap(); + let co_assumptions = (asmp, &trait_ref); + let cs = prove( + &decls, env, &co_assumptions, + Wcs::eq_or_cover( + &i.trait_ref.parameters, &trait_ref.parameters, &mut covering_consts + ) + ); + let cs = cs.flat_map(move |c| prove_after(d, c, &co_assumptions, &i.where_clause)); + let cs = cs.flat_map(move |c| { + let t = d.trait_decl(&i.trait_ref.trait_id) + .binder.instantiate_with(&i.trait_ref.parameters).unwrap(); + prove_after(d, c, asmp, &t.where_clause) + }); + cs.into_iter().map(move |c| c.pop_subst(&subst)) + }).into_iter().collect::>() => c) + (prove_after(d, c, asmp, is_covering(&covering_consts, &trait_ref.parameters)) => c) + ----------------------------- ("exhaustive positive impl") + (prove_wc(_d, env, _asmp, Predicate::IsImplemented(trait_ref)) => c) + ) + ( (decls.impl_decls(&trait_ref.trait_id) => i)! (let (env, subst) = env.existential_substitution(&i.binder)) @@ -112,6 +155,25 @@ judgment_fn! { (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c) ) + ( + (let () = vals.sort_unstable()) + (prove(&decls, env, &assumptions, Predicate::ConstHasType(var, Ty::bool())) => c) + (vals.iter().cloned() => v) + (prove_after(&decls, &c, &assumptions, Predicate::ConstHasType(v, Ty::bool())) => c) + (if vals.len() == 2) + (let mut i = 0) + (vals.clone().into_iter().flat_map(|v| { + i += 1; + prove_after( + &decls, &c, &assumptions, + Relation::Equals(Parameter::Const(Const::valtree(Scalar::new(i as u128), + Ty::bool())), Parameter::Const(v)) + ).into_iter() + }).collect::>() => c) + ----------------------------- ("exhaustive bool values cover variable") + (prove_wc(decls, env, assumptions, Predicate::Covers(mut vals, var)) => c) + ) + ( (prove_wf(decls, env, assumptions, p) => c) diff --git a/crates/formality-types/src/grammar/consts.rs b/crates/formality-types/src/grammar/consts.rs index 4b46910f..b08512e2 100644 --- a/crates/formality-types/src/grammar/consts.rs +++ b/crates/formality-types/src/grammar/consts.rs @@ -26,6 +26,10 @@ impl Const { Self::new(ConstData::Value(vt.upcast(), ty.upcast())) } + pub fn is_variable(&self) -> bool { + matches!(self.data(), ConstData::Variable(_)) + } + pub fn as_variable(&self) -> Option { match self.data() { ConstData::Value(_, _) => None, diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 68f199dc..5912eeab 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -36,6 +36,9 @@ pub enum Predicate { #[grammar(@ConstHasType($v0, $v1))] ConstHasType(Const, Ty), + + #[grammar(@CoveringSet($v0, $v1))] + Covers(Vec, Const), } /// A coinductive predicate is one that can be proven via a cycle. @@ -94,6 +97,7 @@ pub enum Skeleton { Equals, Sub, Outlives, + Covered, } impl Predicate { @@ -136,6 +140,15 @@ impl Predicate { Skeleton::ConstHasType, vec![ct.clone().upcast(), ty.clone().upcast()], ), + Predicate::Covers(consts, c) => ( + Skeleton::Covered, + consts + .iter() + .cloned() + .chain(std::iter::once(c.clone())) + .map(|c| Parameter::Const(c)) + .collect::>(), + ), } } } diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs index ef31a4da..1c1d3a6e 100644 --- a/crates/formality-types/src/grammar/wc.rs +++ b/crates/formality-types/src/grammar/wc.rs @@ -6,7 +6,7 @@ use formality_core::{ use crate::grammar::PR; -use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef}; +use super::{Binder, BoundVar, Const, Parameter, Predicate, Relation, TraitRef}; #[term($set)] #[derive(Default)] @@ -14,6 +14,12 @@ pub struct Wcs { set: Set, } +#[derive(Debug, Clone, PartialEq)] +pub enum ExhaustiveState { + ExactMatch, + ConstCover(Vec), +} + impl Wcs { pub fn t() -> Self { set![].upcast() @@ -30,6 +36,37 @@ impl Wcs { .upcasted() .collect() } + /// Goal(s) to prove `a` and `b` are equal (they must have equal length) + pub fn eq_or_cover( + candidate: impl Upcast>, + trait_impl: impl Upcast>, + covering_items: &mut [ExhaustiveState], + ) -> Wcs { + let a: Vec = candidate.upcast(); + let b: Vec = trait_impl.upcast(); + assert_eq!(a.len(), b.len()); + a.into_iter() + .zip(b) + .enumerate() + .filter_map(|(i, (a, b))| match (&a, &b) { + (Parameter::Const(ct), Parameter::Const(param)) if param.is_variable() => { + if covering_items[i] == ExhaustiveState::ExactMatch { + covering_items[i] = ExhaustiveState::ConstCover(vec![]); + } + let ExhaustiveState::ConstCover(ref mut c) = &mut covering_items[i] else { + panic!(); + }; + c.push(ct.clone()); + None + } + _ => { + assert!(matches!(covering_items[i], ExhaustiveState::ExactMatch)); + Some(Relation::equals(a, b)) + } + }) + .upcasted() + .collect() + } } impl<'w> IntoIterator for &'w Wcs { diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index 0bc3a15b..c8cd5700 100644 --- a/tests/coherence_overlap.rs +++ b/tests/coherence_overlap.rs @@ -47,13 +47,11 @@ fn test_overlap_normalize_alias_to_LocalType() { // ...but it's an error if LocalType implements Iterator (figuring *this* out also // requires normalizing). - test_program_ok(&gen_program( - "impl Iterator for LocalType {}", - )).assert_err( + test_program_ok(&gen_program("impl Iterator for LocalType {}")).assert_err( expect_test::expect![[r#" impls may overlap: impl LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { } - impl LocalTrait for ::T { }"#]] + impl LocalTrait for ::T { }"#]], ); } @@ -103,12 +101,10 @@ fn test_overlap_alias_not_normalizable() { // ...as long as there is at least one Iterator impl, however, we do flag an error. - test_program_ok(&gen_program( - "impl Iterator for u32 {}", - )).assert_err( - expect_test::expect![[r#" + test_program_ok(&gen_program("impl Iterator for u32 {}")).assert_err(expect_test::expect![[ + r#" impls may overlap: impl LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { } - impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"#]] - ); // FIXME + impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"# + ]]); // FIXME } diff --git a/tests/consts.rs b/tests/consts.rs deleted file mode 100644 index c6d324d2..00000000 --- a/tests/consts.rs +++ /dev/null @@ -1,183 +0,0 @@ -use formality::test_program_ok; -use formality_macros::test; - -#[test] -fn test_ok() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - trait Bar where [type_of_const C is u32] {} - - impl Foo for u32 where [type_of_const C is bool] {} - } - ]", - )); -} - -#[test] -fn test_holds() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - impl<> Foo for u32 where [] {} - } - ]", - )); -} - -#[test] -fn test_mismatch() { - expect_test::expect![[r#" - Err( - Error { - context: "check_trait_impl(impl <> Foo < const 42_(rigid (scalar u32)) > for (rigid (scalar u32)) where [] { })", - source: "failed to prove {Foo((rigid (scalar u32)), const 42_(rigid (scalar u32)))} given {}, got {}", - }, - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - impl<> Foo for u32 where [] {} - } - ]", - )); -} - -#[test] -fn test_generic_mismatch() { - expect_test::expect![[r#" - Err( - Error { - context: "check_trait_impl(impl Foo < const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar u32))] { })", - source: "failed to prove {Foo((rigid (scalar u32)), const !const_1)} given {@ ConstHasType(!const_1 , (rigid (scalar u32)))}, got {}", - }, - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - impl Foo for u32 where [type_of_const C is u32] {} - } - ]", - )); -} - -#[test] -fn test_trait_with_const() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - trait Bar where [T: Foo] {} - - impl<> Foo for u32 where [] {} - impl<> Bar for u32 where [] {} - } - ]", - )); -} - -#[test] -fn test_trait_with_generic_const() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool] {} - - trait Bar where [T: Foo, type_of_const C is bool] {} - - impl Foo for u32 where [type_of_const C is bool] {} - impl Bar for u32 where [type_of_const C is bool] {} - } - ]", - )); -} - -#[test] -/// This test is the short version of `test_holds`, skipping -/// substituting and directly going to a rigid constant. -fn test_rigid_const_bound() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo<> where [type_of_const true is bool] {} - } - ]", - )); -} - -#[test] -/// This test is the short version of `test_generic_mismatch`, skipping -/// substituting and directly going to a wrong constant. -fn test_nonsense_rigid_const_bound() { - expect_test::expect![[r#" - Err( - Error { - context: "check_trait(Foo)", - source: Error { - context: "prove_where_clause_well_formed(type_of_const 0_(rigid (scalar bool)) is (rigid (scalar u32)))", - source: "failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(0_(rigid (scalar bool)) , (rigid (scalar u32)))}, got {}", - }, - }, - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo<> where [type_of_const true is u32] {} - } - ]", - )); -} - -#[test] -/// This test is wrong, but it's also not something rustc ever generates. -/// Types on const generics only get exactly one `type_of_const` bound. -fn test_multiple_type_of_const() { - expect_test::expect![[r#" - Ok( - (), - ) - "#]] - .assert_debug_eq(&test_program_ok( - "[ - crate Foo { - trait Foo where [type_of_const C is bool, type_of_const C is u32] {} - } - ]", - )); -} diff --git a/tests/judgment-error-reporting/cyclic_judgment.rs b/tests/judgment-error-reporting/cyclic_judgment.rs index d7506776..57064e4e 100644 --- a/tests/judgment-error-reporting/cyclic_judgment.rs +++ b/tests/judgment-error-reporting/cyclic_judgment.rs @@ -70,14 +70,12 @@ fn test() { let bar = Ty::Class { name: ClassName::new("Bar"), }; - sub(foo, bar).assert_err( - expect_test::expect![[r#" + sub(foo, bar).assert_err(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` name_a = Foo - name_b = Bar"#]] - ); + name_b = Bar"#]]); } #[test] diff --git a/tests/ui/basic_where_clauses_fail.stderr b/tests/ui/basic_where_clauses_fail.stderr index c6b2630e..1f0cce10 100644 --- a/tests/ui/basic_where_clauses_fail.stderr +++ b/tests/ui/basic_where_clauses_fail.stderr @@ -6,9 +6,13 @@ Caused by: 2: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(A(u32, !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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !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 well formed" failed at step #2 (crates/formality-prove/src/prove/prove_wc.rs:104:14) because + the rule "trait well formed" failed at step #2 (crates/formality-prove/src/prove/prove_wc.rs:147:14) because judgment `prove_wc_list { 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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because 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 + the rule "exhaustive positive impl" failed at step #3 (crates/formality-prove/src/prove/prove_wc.rs:68:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129: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 034ac2ad..f14ff1dc 100644 --- a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr +++ b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr @@ -4,7 +4,7 @@ Caused by: judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ IsLocal(CoreTrait(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 "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because + the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:153:14) because judgment `is_local_trait_ref { goal: CoreTrait(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 "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because 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): diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr index c7493056..702efee9 100644 --- a/tests/ui/coherence_orphan/alias_to_unit.stderr +++ b/tests/ui/coherence_orphan/alias_to_unit.stderr @@ -4,7 +4,7 @@ Caused by: judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, 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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), 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 "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because + the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:153:14) because judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), 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 "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because judgment `is_local_parameter { goal: ::Assoc, 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): diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr index 60113b62..8a85f9cf 100644 --- a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr +++ b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr @@ -4,7 +4,7 @@ Caused by: judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, 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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), 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 "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because + the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:153:14) because judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), 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 "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because judgment `is_local_parameter { goal: ::Assoc, 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): 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 8ea95ce3..769cccb1 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 @@ -4,7 +4,7 @@ Caused by: judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ IsLocal(CoreTrait(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 "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because + the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:153:14) because judgment `is_local_trait_ref { goal: CoreTrait(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 "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because 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): diff --git a/tests/ui/coherence_orphan/uncovered_T.stderr b/tests/ui/coherence_orphan/uncovered_T.stderr index 2432395d..af01fbca 100644 --- a/tests/ui/coherence_orphan/uncovered_T.stderr +++ b/tests/ui/coherence_orphan/uncovered_T.stderr @@ -4,7 +4,7 @@ Caused by: judgment `prove_wc_list { goal: {@ IsLocal(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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ IsLocal(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 "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because + the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:153:14) because 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/double.\360\237\224\254" "b/tests/ui/consts/double.\360\237\224\254" new file mode 100644 index 00000000..ff16792d --- /dev/null +++ "b/tests/ui/consts/double.\360\237\224\254" @@ -0,0 +1,8 @@ +//@check-pass +[ + crate Foo { + trait Foo where type_of_const C is bool, type_of_const D is bool {} + + impl Foo for u32 where type_of_const C is bool {} + } +] diff --git a/tests/ui/consts/exhaustive.stderr b/tests/ui/consts/exhaustive.stderr new file mode 100644 index 00000000..243d84c8 --- /dev/null +++ b/tests/ui/consts/exhaustive.stderr @@ -0,0 +1,30 @@ +Error: check_trait_impl(impl Bar for u32 where type_of_const ^const0_0 is bool { }) + +Caused by: + judgment `prove_wc_list { goal: {Bar(u32, u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because + judgment `prove_wc { goal: Bar(u32, u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "exhaustive positive impl" failed at step #3 (crates/formality-prove/src/prove/prove_wc.rs:68:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "positive impl" failed at step #7 (crates/formality-prove/src/prove/prove_wc.rs:100:14) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], coherence_mode: false }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {Foo(u32, const ?const_1), @ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , bool)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (crates/formality-prove/src/prove/prove_after.rs:19:14) because + judgment `prove_wc_list { goal: {Foo(u32, const !const_0), @ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because + judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "exhaustive positive impl" failed at step #4 (crates/formality-prove/src/prove/prove_wc.rs:87:14) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0], coherence_mode: false }, known_true: true, substitution: {} }, goal: {@ CoveringSet([value(0, bool), value(1, bool)] , !const_0)}, assumptions: {@ ConstHasType(!const_0 , bool)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (crates/formality-prove/src/prove/prove_after.rs:19:14) because + judgment `prove_wc_list { goal: {@ CoveringSet([value(0, bool), value(1, bool)] , !const_0)}, assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because + judgment `prove_wc { goal: @ CoveringSet([value(0, bool), value(1, bool)] , !const_0), assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Foo(u32, const value(1, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "exhaustive bool values cover variable" failed at step #6 (crates/formality-prove/src/prove/prove_wc.rs:165:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129:14) because + expression evaluated to an empty collection: `decls.trait_invariants()` + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129:14) because + expression evaluated to an empty collection: `decls.trait_invariants()` diff --git "a/tests/ui/consts/exhaustive.\360\237\224\254" "b/tests/ui/consts/exhaustive.\360\237\224\254" new file mode 100644 index 00000000..1a0149bd --- /dev/null +++ "b/tests/ui/consts/exhaustive.\360\237\224\254" @@ -0,0 +1,12 @@ +//@check-pass +[ + crate Foo { + trait Foo where type_of_const C is bool {} + + trait Bar where T: Foo, type_of_const C is bool {} + + impl<> Foo for u32 {} + impl<> Foo for u32 {} + impl Bar for u32 where type_of_const C is bool {} + } +] diff --git a/tests/ui/consts/generic_mismatch.stderr b/tests/ui/consts/generic_mismatch.stderr index 882a9b77..611c6942 100644 --- a/tests/ui/consts/generic_mismatch.stderr +++ b/tests/ui/consts/generic_mismatch.stderr @@ -4,13 +4,17 @@ Caused by: judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "positive impl" failed at step #7 (crates/formality-prove/src/prove/prove_wc.rs:57:14) because + the rule "exhaustive positive impl" failed at step #3 (crates/formality-prove/src/prove/prove_wc.rs:68:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "positive impl" failed at step #7 (crates/formality-prove/src/prove/prove_wc.rs:100:14) because judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], coherence_mode: false }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (crates/formality-prove/src/prove/prove_after.rs:19:14) because judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "const has ty" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:123:43) because + the rule "const has ty" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:185:43) because 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 + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129: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 5462ed60..87118209 100644 --- a/tests/ui/consts/mismatch.stderr +++ b/tests/ui/consts/mismatch.stderr @@ -4,5 +4,9 @@ Caused by: judgment `prove_wc_list { 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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because 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 + the rule "exhaustive positive impl" failed at step #3 (crates/formality-prove/src/prove/prove_wc.rs:68:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129: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 a022eaef..0020f879 100644 --- a/tests/ui/consts/nonsense_rigid_const_bound.stderr +++ b/tests/ui/consts/nonsense_rigid_const_bound.stderr @@ -5,9 +5,9 @@ Caused by: 1: judgment `prove_wc_list { goal: {u32 = 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}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: u32 = 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}, {}) }` failed at the following rule(s): - the rule "assumption" failed at step #1 (crates/formality-prove/src/prove/prove_wc.rs:44:14) because + the rule "assumption" failed at step #1 (crates/formality-prove/src/prove/prove_wc.rs:59:14) because judgment had no applicable rules: `prove_via { goal: u32 = 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 "eq" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:96:14) because + the rule "eq" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:139:14) because judgment `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}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (crates/formality-prove/src/prove/prove_eq.rs:68:14) because judgment `prove_normalize { p: 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}, {}) }` failed at the following rule(s): diff --git a/tests/ui/consts/not_covering.stderr b/tests/ui/consts/not_covering.stderr new file mode 100644 index 00000000..67f24c4e --- /dev/null +++ b/tests/ui/consts/not_covering.stderr @@ -0,0 +1,28 @@ +Error: check_trait_impl(impl Bar for u32 where type_of_const ^const0_0 is bool { }) + +Caused by: + judgment `prove_wc_list { goal: {Bar(u32, u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because + judgment `prove_wc { goal: Bar(u32, u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "exhaustive positive impl" failed at step #3 (crates/formality-prove/src/prove/prove_wc.rs:68:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "positive impl" failed at step #7 (crates/formality-prove/src/prove/prove_wc.rs:100:14) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], coherence_mode: false }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {Foo(u32, const ?const_1), @ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , bool)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (crates/formality-prove/src/prove/prove_after.rs:19:14) because + judgment `prove_wc_list { goal: {Foo(u32, const !const_0), @ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because + judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "exhaustive positive impl" failed at step #4 (crates/formality-prove/src/prove/prove_wc.rs:87:14) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0], coherence_mode: false }, known_true: true, substitution: {} }, goal: {@ CoveringSet([value(0, bool)] , !const_0)}, assumptions: {@ ConstHasType(!const_0 , bool)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (crates/formality-prove/src/prove/prove_after.rs:19:14) because + judgment `prove_wc_list { goal: {@ CoveringSet([value(0, bool)] , !const_0)}, assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because + judgment `prove_wc { goal: @ CoveringSet([value(0, bool)] , !const_0), assumptions: {@ ConstHasType(!const_0 , bool)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}, trait Bar where {Foo(^ty0_1, const ^const0_2), @ ConstHasType(^const0_2 , bool)}], [impl Foo(u32, const value(0, bool)), impl Bar(u32, u32, const ^const0_0) where {@ ConstHasType(^const0_0 , bool)}], [], [], [], [], {Bar, Foo}, {}) }` failed at the following rule(s): + the rule "exhaustive bool values cover variable" failed at step #4 (crates/formality-prove/src/prove/prove_wc.rs:163:17) because + condition evaluted to false: `vals.len() == 2` + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129:14) because + expression evaluated to an empty collection: `decls.trait_invariants()` + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129:14) because + expression evaluated to an empty collection: `decls.trait_invariants()` diff --git "a/tests/ui/consts/not_covering.\360\237\224\254" "b/tests/ui/consts/not_covering.\360\237\224\254" new file mode 100644 index 00000000..94cd64af --- /dev/null +++ "b/tests/ui/consts/not_covering.\360\237\224\254" @@ -0,0 +1,10 @@ +[ + crate Foo { + trait Foo where type_of_const C is bool {} + + trait Bar where T: Foo, type_of_const C is bool {} + + impl<> Foo for u32 {} + impl Bar for u32 where type_of_const C is bool {} + } +] diff --git "a/tests/ui/consts/trait_with_const.\360\237\224\254" "b/tests/ui/consts/trait_with_const.\360\237\224\254" new file mode 100644 index 00000000..da0298d4 --- /dev/null +++ "b/tests/ui/consts/trait_with_const.\360\237\224\254" @@ -0,0 +1,11 @@ +//@check-pass +[ + crate Foo { + trait Foo where type_of_const C is bool {} + + trait Bar where T: Foo {} + + impl<> Foo for u32 {} + impl<> Bar for u32 {} + } +] diff --git "a/tests/ui/consts/trait_with_generic_const.\360\237\224\254" "b/tests/ui/consts/trait_with_generic_const.\360\237\224\254" new file mode 100644 index 00000000..9a06601e --- /dev/null +++ "b/tests/ui/consts/trait_with_generic_const.\360\237\224\254" @@ -0,0 +1,11 @@ +//@check-pass +[ + crate Foo { + trait Foo where type_of_const C is bool {} + + trait Bar where T: Foo, type_of_const C is bool {} + + impl Foo for u32 where type_of_const C is bool {} + impl Bar for u32 where type_of_const C is bool {} + } +] diff --git a/tests/ui/fn/lifetime.stderr b/tests/ui/fn/lifetime.stderr index 937b530f..36ac6c9c 100644 --- a/tests/ui/fn/lifetime.stderr +++ b/tests/ui/fn/lifetime.stderr @@ -1,5 +1,5 @@ Error: judgment `prove_wc_list { 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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because 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 + the rule "parameter well formed" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:179: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 17442cc2..e37fe2cf 100644 --- a/tests/ui/hello_world_fail.stderr +++ b/tests/ui/hello_world_fail.stderr @@ -5,9 +5,13 @@ Caused by: 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !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 well formed" failed at step #2 (crates/formality-prove/src/prove/prove_wc.rs:104:14) because + the rule "trait well formed" failed at step #2 (crates/formality-prove/src/prove/prove_wc.rs:147:14) because judgment `prove_wc_list { 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 "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because 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 + the rule "exhaustive positive impl" failed at step #3 (crates/formality-prove/src/prove/prove_wc.rs:68:14) because + judgment `collect` failed at the following rule(s): + failed at (/Users/julian/Desktop/programming/oss/a-mir-formality/crates/formality-core/src/judgment/proven_set.rs:189:13) because + empty collection + the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:129:14) because expression evaluated to an empty collection: `decls.trait_invariants()`