From 11949cfdd102f9129861ac3ee4e3376f89d4deaf Mon Sep 17 00:00:00 2001 From: lcnr Date: Tue, 14 May 2024 05:06:08 -0400 Subject: [PATCH 01/10] wip: flip polarity in `may_not_be_provable` --- crates/formality-check/src/coherence.rs | 7 ++++++ crates/formality-prove/src/prove/is_local.rs | 26 +++++++++++--------- src/test/coherence_orphan.rs | 4 +-- 3 files changed, 24 insertions(+), 13 deletions(-) diff --git a/crates/formality-check/src/coherence.rs b/crates/formality-check/src/coherence.rs index 7f679a9a..5da2a98a 100644 --- a/crates/formality-check/src/coherence.rs +++ b/crates/formality-check/src/coherence.rs @@ -53,6 +53,13 @@ impl Check<'_> { let a = env.instantiate_universally(&impl_a.binder); let trait_ref = a.trait_ref(); + // The orphan check passes if + // ∀P. ⌐ (coherence_mode => (wf(Ts) && cannot_be_proven(is_local_trait_ref))) + // + // TODO: feels like we do want a general "not goal", flipping existentials + // and universals and the coherence mode + // self.prove_not_goal(&env, &(Wcs::wf)) + self.prove_goal( &env.with_coherence_mode(true), &a.where_clauses, diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 265a27b1..27c2c257 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -51,6 +51,7 @@ judgment_fn! { goal: TraitRef, ) => () { debug(assumptions, goal, decls, env) + assert(env.is_in_coherence_mode()) ( (may_be_downstream_trait_ref(decls, env, assumptions, goal) => ()) @@ -61,7 +62,7 @@ judgment_fn! { ( // In principle this rule could be removed and preserve soundness, // but then we would accept code that is very prone to semver failures. - (may_not_be_provable(is_local_trait_ref(decls, env, assumptions, goal)) => ()) + (may_not_be_provable(&env, |env| is_local_trait_ref(decls, &env, assumptions, goal)) => ()) --- ("may be added by upstream in a minor release") (may_be_remote(decls, env, assumptions, goal) => ()) ) @@ -77,7 +78,7 @@ judgment_fn! { goal: TraitRef, ) => () { debug(goal, assumptions, env, decls) - + assert(env.is_in_coherence_mode()) ( // There may be a downstream parameter at position i... (&goal.parameters => p) @@ -96,7 +97,7 @@ judgment_fn! { parameter: Parameter, ) => () { debug(parameter, assumptions, env, decls) - + assert(env.is_in_coherence_mode()) ( // existential variables *could* be inferred to downstream types; depends on the substitution // we ultimately have. @@ -116,7 +117,9 @@ judgment_fn! { (if may_contain_downstream_type(&decls, &env, &assumptions, p)) // (b) the alias cannot be normalized to something that may not be downstream - (may_not_be_provable(normalizes_to_not_downstream(&decls, &env, &assumptions, AliasTy { name: name.clone(), parameters: parameters.clone() })) => ()) + (may_not_be_provable(&env, |env| + normalizes_to_not_downstream(&decls, &env, &assumptions, AliasTy { name: name.clone(), parameters: parameters.clone() }) + ) => ()) --- ("via normalize") (may_be_downstream_parameter(decls, env, assumptions, AliasTy { name, parameters }) => ()) ) @@ -170,8 +173,10 @@ fn may_contain_downstream_type( } } -fn may_not_be_provable(op: ProvenSet) -> ProvenSet<()> { - if let Some(constraints) = op +// FIXME: This should be a more general concept and not limited ot `is_local` +fn may_not_be_provable(env: &Env, op: impl FnOnce(Env) -> ProvenSet) -> ProvenSet<()> { + assert!(env.is_in_coherence_mode()); + if let Some(constraints) = op(env.with_coherence_mode(false)) .iter() .find(|constraints| constraints.unconditionally_true()) { @@ -211,7 +216,7 @@ judgment_fn! { goal: TraitRef, ) => Constraints { debug(goal, assumptions, env, decls) - + // assert(!env.is_in_coherence_mode()) TODO ( (if decls.is_local_trait_id(&goal.trait_id)) --- ("local trait") @@ -248,6 +253,7 @@ judgment_fn! { parameter: Parameter, ) => Constraints { debug(parameter, assumptions, env, decls) + // assert(!env.is_in_coherence_mode()) // TODO ( // Since https://rust-lang.github.io/rfcs/2451-re-rebalancing-coherence.html, @@ -279,13 +285,11 @@ judgment_fn! { goal: Parameter, ) => Constraints { debug(goal, assumptions, env, decls) - - assert(env.is_in_coherence_mode()) + // assert(!env.is_in_coherence_mode()) TODO // If we can normalize `goal` to something else, check if that normalized form is local. ( - (prove_normalize(&decls, env.with_coherence_mode(false), &assumptions, goal) => (c1, p)) - (let c1 = c1.with_coherence_mode(true)) + (prove_normalize(&decls, env, &assumptions, goal) => (c1, p)) (let assumptions = c1.substitution().apply(&assumptions)) (is_local_parameter(&decls, c1.env(), assumptions, p) => c2) --- ("local parameter") diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index 9a7835f4..caa80109 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -75,7 +75,7 @@ fn mirror_CoreStruct() { 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 (src/file.rs:LL:CC) 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): - the rule "local parameter" failed at step #3 (src/file.rs:LL:CC) because + the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because 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 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` @@ -202,7 +202,7 @@ fn alias_to_unit() { 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 (src/file.rs:LL:CC) 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): - the rule "local parameter" failed at step #3 (src/file.rs:LL:CC) because + the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because 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 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` From 4ef962aae00eb8446db6ceeb427c31ee05e79cb0 Mon Sep 17 00:00:00 2001 From: lcnr Date: Tue, 14 May 2024 05:11:09 -0400 Subject: [PATCH 02/10] add coherence tests --- crates/formality-prove/src/prove/is_local.rs | 4 +- src/test/coherence_orphan.rs | 28 +++++++- src/test/coherence_overlap.rs | 67 ++++++++++++++++++++ 3 files changed, 96 insertions(+), 3 deletions(-) diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 27c2c257..685b6b68 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -173,7 +173,9 @@ fn may_contain_downstream_type( } } -// FIXME: This should be a more general concept and not limited ot `is_local` +// FIXME(@lcnr): This should be a more general concept and not limited ot `is_local` +// +// Also, I think this should flip quantification from existential to universal again fn may_not_be_provable(env: &Env, op: impl FnOnce(Env) -> ProvenSet) -> ProvenSet<()> { assert!(env.is_in_coherence_mode()); if let Some(constraints) = op(env.with_coherence_mode(false)) diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index caa80109..7dce968d 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -95,7 +95,6 @@ fn mirror_CoreStruct() { #[test] fn mirror_FooStruct() { crate::assert_ok!( - //@check-pass [ crate core { trait CoreTrait {} @@ -121,7 +120,6 @@ fn mirror_FooStruct() { #[test] fn covered_VecT() { crate::assert_ok!( - //@check-pass [ crate core { trait CoreTrait {} @@ -255,3 +253,29 @@ fn CoreTrait_for_CoreStruct_in_Foo() { &goal.trait_id = CoreTrait"#]] ) } + +#[test] +fn CoreTraitLocal_for_AliasToKnown_in_Foo() { + // TODO: see comment in `orphan_check` from prev commit + crate::assert_ok!( + [ + crate core { + trait CoreTrait {} + + trait Unit { + type Assoc : []; + } + + impl Unit for T { + type Assoc = (); + } + }, + crate foo { + struct FooStruct {} + impl CoreTrait for <() as Unit>::Assoc {} + } + ] + + expect_test::expect!["()"] + ) +} diff --git a/src/test/coherence_overlap.rs b/src/test/coherence_overlap.rs index 2aab654b..b3efd5ea 100644 --- a/src/test/coherence_overlap.rs +++ b/src/test/coherence_overlap.rs @@ -275,3 +275,70 @@ fn T_and_Local_Bar_T() { impl Foo for ^ty0_0 where LocalType : Bar <^ty0_0> { }"#]] } } + +#[test] +fn is_local_unknowable_trait_ref() { + crate::assert_ok! { + [ + crate core { + trait Project { + type Assoc: []; + } + + impl Project for T { + type Assoc = T; + } + + trait Foo { } + }, + crate foo { + struct LocalType {} + + trait Overlap {} + impl Overlap for T + where + ::Assoc: Foo {} + impl Overlap for () {} + } + ] + + expect_test::expect!["()"] + } +} + +#[test] +fn is_local_with_unconstrained_self_ty_blanket_impl() { + // TODO: this test should pass imho + crate::assert_err! { + [ + crate core { + trait Project { + type Assoc: []; + } + + impl Project for T { + type Assoc = (); + } + + trait Foo { } + }, + crate foo { + struct LocalType {} + impl Foo for () {} + + trait Overlap {} + impl Overlap for T + where + ::Assoc: Foo {} + impl Overlap for T {} + } + ] + + [ ] + + expect_test::expect![[r#" + impls may overlap: + impl Overlap <^ty0_1> for ^ty0_0 where <^ty0_0 as Project>::Assoc : Foo <^ty0_1> { } + impl Overlap for ^ty0_0 { }"#]] + } +} From 9d7ec869d61d4fa691c13e695ebeebea6f4175ef Mon Sep 17 00:00:00 2001 From: lcnr Date: Tue, 14 May 2024 05:42:07 -0400 Subject: [PATCH 03/10] via normalize for `is_not_downstream` --- crates/formality-prove/src/prove/is_local.rs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 685b6b68..9d723357 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -257,6 +257,12 @@ judgment_fn! { debug(parameter, assumptions, env, decls) // assert(!env.is_in_coherence_mode()) // TODO + ( + // Lifetimes are not relevant. + --- ("lifetime") + (is_not_downstream(_decls, env, _assumptions, _l: Lt) => Constraints::none(env)) + ) + ( // Since https://rust-lang.github.io/rfcs/2451-re-rebalancing-coherence.html, // any rigid type is adequate. @@ -265,9 +271,11 @@ judgment_fn! { ) ( - // Lifetimes are not relevant. - --- ("lifetime") - (is_not_downstream(_decls, env, _assumptions, _l: Lt) => Constraints::none(env)) + (prove_normalize(&decls, env, &assumptions, parameter) => (c1, p)) + (let assumptions = c1.substitution().apply(&assumptions)) + (is_not_downstream(&decls, c1.env(), assumptions, p) => c2) + --- ("via normalize") + (is_not_downstream(decls, env, assumptions, parameter) => c1.seq(c2)) ) ( From e01c2046aa88142b7b2e257d63fb6ff7626a8b1e Mon Sep 17 00:00:00 2001 From: lcnr Date: Fri, 31 May 2024 18:32:16 +0200 Subject: [PATCH 04/10] coherence_mode -> bias --- crates/formality-check/src/coherence.rs | 14 ++----- crates/formality-check/src/lib.rs | 13 +++--- crates/formality-prove/src/lib.rs | 2 +- crates/formality-prove/src/prove.rs | 2 +- .../formality-prove/src/prove/constraints.rs | 7 ---- crates/formality-prove/src/prove/env.rs | 42 ++++++++++++++++--- crates/formality-prove/src/prove/is_local.rs | 20 ++++----- crates/formality-prove/src/prove/prove_wc.rs | 4 +- crates/formality-prove/src/test_util.rs | 7 ++-- src/test/coherence_orphan.rs | 42 +++++++++---------- src/test/coherence_overlap.rs | 4 +- src/test/consts.rs | 34 +++++++-------- src/test/functions.rs | 6 +-- src/test/mod.rs | 16 +++---- tests/associated_type_normalization.rs | 2 +- tests/projection.rs | 18 ++++---- 16 files changed, 126 insertions(+), 107 deletions(-) diff --git a/crates/formality-check/src/coherence.rs b/crates/formality-check/src/coherence.rs index 5da2a98a..e003490a 100644 --- a/crates/formality-check/src/coherence.rs +++ b/crates/formality-check/src/coherence.rs @@ -60,11 +60,7 @@ impl Check<'_> { // and universals and the coherence mode // self.prove_not_goal(&env, &(Wcs::wf)) - self.prove_goal( - &env.with_coherence_mode(true), - &a.where_clauses, - trait_ref.is_local(), - ) + self.prove_goal(&env, &a.where_clauses, trait_ref.is_local()) } #[context("orphan_check_neg({impl_a:?})")] @@ -74,11 +70,7 @@ impl Check<'_> { let a = env.instantiate_universally(&impl_a.binder); let trait_ref = a.trait_ref(); - self.prove_goal( - &env.with_coherence_mode(true), - &a.where_clauses, - trait_ref.is_local(), - ) + self.prove_goal(&env, &a.where_clauses, trait_ref.is_local()) } #[tracing::instrument(level = "Debug", skip(self))] @@ -107,7 +99,7 @@ impl Check<'_> { // // ∀P_a, ∀P_b. ⌐ (coherence_mode => (Ts_a = Ts_b && WC_a && WC_b)) if let Ok(()) = self.prove_not_goal( - &env.with_coherence_mode(true), + &env, (), ( Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters), diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs index 01b2d324..03e6bfbc 100644 --- a/crates/formality-check/src/lib.rs +++ b/crates/formality-check/src/lib.rs @@ -3,7 +3,7 @@ use std::{collections::VecDeque, fmt::Debug}; use anyhow::bail; -use formality_prove::{Decls, Env}; +use formality_prove::{Bias, Decls, Env}; use formality_rust::{ grammar::{Crate, CrateItem, Program, Test, TestBoundData}, prove::ToWcs, @@ -127,16 +127,19 @@ impl Check<'_> { tracing::debug!("assumptions = {assumptions:?}"); tracing::debug!("goal = {goal:?}"); + assert!(env.bias() == Bias::Soundness); assert!(env.only_universal_variables()); assert!(env.encloses((&assumptions, &goal))); // Proving `∀X. not(F(X))` is the same as proving: `not(∃X. F(X))`. // Therefore, since we have only universal variables, we can change them all to // existential and then try to prove. If we get back no solutions, we know that - // we've proven the negation. (This is called the "negation as failure" property, - // and it relies on our solver being complete -- i.e., if there is a solution, - // we'll find it, or at least return ambiguous.) - let mut existential_env = Env::default().with_coherence_mode(env.is_in_coherence_mode()); + // we've proven the negation. + // + // This is called the "negation as failure" property, and it relies on our solver + // being complete -- i.e., if there is a solution, we'll find it, or at least + // return ambiguous. + let mut existential_env = Env::default().with_bias(Bias::Completeness); let universal_to_existential: Substitution = env .variables() .iter() diff --git a/crates/formality-prove/src/lib.rs b/crates/formality-prove/src/lib.rs index f41ef19b..edbf576a 100644 --- a/crates/formality-prove/src/lib.rs +++ b/crates/formality-prove/src/lib.rs @@ -8,7 +8,7 @@ mod prove; pub use decls::*; pub use prove::prove; pub use prove::Constraints; -pub use prove::Env; +pub use prove::{Bias, Env}; #[cfg(test)] mod test; diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 3ea99ec6..22900b36 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -19,7 +19,7 @@ use tracing::Level; use crate::decls::Decls; -pub use self::env::Env; +pub use self::env::{Bias, Env}; use self::prove_wc_list::prove_wc_list; /// Top-level entry point for proving things; other rules recurse to this one. diff --git a/crates/formality-prove/src/prove/constraints.rs b/crates/formality-prove/src/prove/constraints.rs index 42f7cb3b..495183f5 100644 --- a/crates/formality-prove/src/prove/constraints.rs +++ b/crates/formality-prove/src/prove/constraints.rs @@ -30,13 +30,6 @@ impl Constraints { Self::from(env, v) } - pub fn with_coherence_mode(self, b: bool) -> Self { - Self { - env: self.env.with_coherence_mode(b), - ..self - } - } - pub fn unconditionally_true(&self) -> bool { self.known_true && self.substitution.is_empty() } diff --git a/crates/formality-prove/src/prove/env.rs b/crates/formality-prove/src/prove/env.rs index d29e6a46..67f30c15 100644 --- a/crates/formality-prove/src/prove/env.rs +++ b/crates/formality-prove/src/prove/env.rs @@ -7,10 +7,40 @@ use formality_types::{ rust::{Fold, Visit}, }; +/// Whether the solver has to be sound or complete. While it should +/// ideally be both at all times, we have some rules which break these +/// properties, so we have to make sure they are only used while in +/// the proper `Env`. Regardless of the current bias, it's always valid +/// to return an ambiguous result. +#[derive(Default, Debug, Clone, Copy, Hash, Ord, Eq, PartialEq, PartialOrd)] +pub enum Bias { + /// Whenever we're able to prove something, it has to definitely be + /// *truly true*. We must never be able to prove somethingwhich is not + /// *truly true*. This is the default unless we're currently trying to + /// prove the negation via "negation as failure". + /// + /// By convention, functions which may only be used with a bias + /// for soundness are called `fn is_X` or `fn is_definitely_X`. + #[default] + Soundness, + /// If we are unable to find a solution for some goal, this goal must + /// definitely not be proveable, it is known to not be *truly true*. This + /// implies that we must only add constraints if they are definitely + /// necessary as we can otherwise use these constraints to incorrectly + /// disprove something. + /// + /// Most notably, this is used by coherence checking to make sure that impls + /// definitely do not overlap. + /// + /// By convention, functions which may only be used with a bias for + /// completeness are called `fn may_X`. + Completeness, +} + #[derive(Default, Debug, Clone, Hash, Ord, Eq, PartialEq, PartialOrd)] pub struct Env { variables: Vec, - coherence_mode: bool, + bias: Bias, } impl Env { @@ -18,13 +48,13 @@ impl Env { self.variables.iter().all(|v| v.is_universal()) } - pub fn is_in_coherence_mode(&self) -> bool { - self.coherence_mode + pub fn bias(&self) -> Bias { + self.bias } - pub fn with_coherence_mode(&self, b: bool) -> Env { + pub fn with_bias(&self, bias: Bias) -> Env { Env { - coherence_mode: b, + bias, ..self.clone() } } @@ -208,7 +238,7 @@ impl Env { .iter() .map(|&v| vs.map_var(v).unwrap_or(v)) .collect(), - coherence_mode: self.coherence_mode, + bias: self.bias, } } diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 9d723357..0d12645a 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -5,7 +5,7 @@ use formality_types::grammar::{ use crate::{ decls::Decls, - prove::{combinators::for_all, prove_normalize::prove_normalize, Constraints}, + prove::{combinators::for_all, env::Bias, prove_normalize::prove_normalize, Constraints}, Env, }; @@ -51,7 +51,7 @@ judgment_fn! { goal: TraitRef, ) => () { debug(assumptions, goal, decls, env) - assert(env.is_in_coherence_mode()) + assert(env.bias() == Bias::Completeness) ( (may_be_downstream_trait_ref(decls, env, assumptions, goal) => ()) @@ -78,7 +78,7 @@ judgment_fn! { goal: TraitRef, ) => () { debug(goal, assumptions, env, decls) - assert(env.is_in_coherence_mode()) + assert(env.bias() == Bias::Completeness) ( // There may be a downstream parameter at position i... (&goal.parameters => p) @@ -97,7 +97,7 @@ judgment_fn! { parameter: Parameter, ) => () { debug(parameter, assumptions, env, decls) - assert(env.is_in_coherence_mode()) + assert(env.bias() == Bias::Completeness) ( // existential variables *could* be inferred to downstream types; depends on the substitution // we ultimately have. @@ -132,7 +132,7 @@ fn may_contain_downstream_type( assumptions: &Wcs, parameter: impl Upcast, ) -> bool { - assert!(env.is_in_coherence_mode()); + assert!(env.bias() == Bias::Completeness); let parameter = parameter.upcast(); let Parameter::Ty(ty) = parameter else { @@ -177,8 +177,8 @@ fn may_contain_downstream_type( // // Also, I think this should flip quantification from existential to universal again fn may_not_be_provable(env: &Env, op: impl FnOnce(Env) -> ProvenSet) -> ProvenSet<()> { - assert!(env.is_in_coherence_mode()); - if let Some(constraints) = op(env.with_coherence_mode(false)) + assert!(env.bias() == Bias::Completeness); + if let Some(constraints) = op(env.with_bias(Bias::Soundness)) .iter() .find(|constraints| constraints.unconditionally_true()) { @@ -218,7 +218,7 @@ judgment_fn! { goal: TraitRef, ) => Constraints { debug(goal, assumptions, env, decls) - // assert(!env.is_in_coherence_mode()) TODO + assert(env.bias() == Bias::Soundness) ( (if decls.is_local_trait_id(&goal.trait_id)) --- ("local trait") @@ -255,7 +255,7 @@ judgment_fn! { parameter: Parameter, ) => Constraints { debug(parameter, assumptions, env, decls) - // assert(!env.is_in_coherence_mode()) // TODO + assert(env.bias() == Bias::Soundness) ( // Lifetimes are not relevant. @@ -295,7 +295,7 @@ judgment_fn! { goal: Parameter, ) => Constraints { debug(goal, assumptions, env, decls) - // assert(!env.is_in_coherence_mode()) TODO + assert(env.bias() == Bias::Soundness) // If we can normalize `goal` to something else, check if that normalized form is local. ( diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index f51e55cb..204a4f65 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -4,7 +4,7 @@ use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs}; use crate::{ decls::Decls, prove::{ - env::Env, + env::{Bias, Env}, is_local::{is_local_trait_ref, may_be_remote}, prove, prove_after::prove_after, @@ -60,7 +60,7 @@ judgment_fn! { ) ( - (if env.is_in_coherence_mode())! + (if env.bias() == Bias::Completeness)! (may_be_remote(decls, &env, assumptions, trait_ref) => ()) ----------------------------- ("coherence / remote impl") (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => Constraints::none(&env).ambiguous()) diff --git a/crates/formality-prove/src/test_util.rs b/crates/formality-prove/src/test_util.rs index 24b6884d..a5c7bfd4 100644 --- a/crates/formality-prove/src/test_util.rs +++ b/crates/formality-prove/src/test_util.rs @@ -1,8 +1,8 @@ -use std::sync::Arc; - +use crate::prove::Bias; use formality_core::ProvenSet; use formality_macros::term; use formality_types::grammar::{Binder, Wcs}; +use std::sync::Arc; use crate::{ decls::Decls, @@ -49,8 +49,9 @@ pub fn test_prove(decls: Decls, mut assertion: Arc) -> ProvenSet< return prove(decls, env, assumptions, goals); } + // FIXME(@lcnr): This should be "negation-by-failure" or sth. TestAssertion::CoherenceMode(assertion1) => { - env = env.with_coherence_mode(true); + env = env.with_bias(Bias::Completeness); assertion = assertion1.clone(); } } diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index 7dce968d..a4e1807b 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -19,13 +19,13 @@ fn neg_CoreTrait_for_CoreStruct_in_Foo() { orphan_check_neg(impl ! CoreTrait for CoreStruct {}) 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): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) 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): + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) @@ -68,15 +68,15 @@ fn mirror_CoreStruct() { orphan_check(impl CoreTrait for ::Assoc { }) 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): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 #2 (src/file.rs:LL:CC) because - 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): + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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 ], {}, {}) @@ -154,11 +154,11 @@ fn uncovered_T() { orphan_check(impl CoreTrait for ^ty0_0 { }) 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): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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}) @@ -193,15 +193,15 @@ fn alias_to_unit() { orphan_check(impl CoreTrait for ::Assoc { }) 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): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 #2 (src/file.rs:LL:CC) because - 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): + judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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}) @@ -232,13 +232,13 @@ fn CoreTrait_for_CoreStruct_in_Foo() { orphan_check(impl CoreTrait for CoreStruct { }) 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): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) 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): + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) diff --git a/src/test/coherence_overlap.rs b/src/test/coherence_overlap.rs index b3efd5ea..c8b26ef9 100644 --- a/src/test/coherence_overlap.rs +++ b/src/test/coherence_overlap.rs @@ -28,7 +28,7 @@ fn u32_not_u32_impls() { given {} got - {Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }}"#]] + {Constraints { env: Env { variables: [], bias: Completeness }, known_true: true, substitution: {} }}"#]] ) } @@ -111,7 +111,7 @@ fn T_where_Foo_not_u32_impls() { given {Foo(!ty_1)} got - {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => u32} }}"#]] + {Constraints { env: Env { variables: [?ty_1], bias: Completeness }, known_true: true, substitution: {?ty_1 => u32} }}"#]] ) } diff --git a/src/test/consts.rs b/src/test/consts.rs index 127744fd..f988af36 100644 --- a/src/test/consts.rs +++ b/src/test/consts.rs @@ -18,25 +18,25 @@ fn nonsense_rigid_const_bound() { Caused by: 0: prove_where_clause_well_formed(type_of_const value(0, bool) is u32) - 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): + 1: judgment `prove_wc_list { goal: {u32 = bool}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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}, {}) }` + 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: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) 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): + judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, 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}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: bool, b: 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): + judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: 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): + judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - 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}, {}) }` + 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: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) 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}, {}) }`"#]] + cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }`"#]] ) } @@ -74,9 +74,9 @@ fn mismatch() { check_trait_impl(impl Foo for u32 { }) 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): + judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) @@ -131,15 +131,15 @@ fn generic_mismatch() { check_trait_impl(impl Foo for u32 where type_of_const ^const0_0 is u32 { }) 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): + judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, 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 (src/file.rs:LL:CC) because pattern `Some((_, const_ty))` did not match value `None` the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because diff --git a/src/test/functions.rs b/src/test/functions.rs index 8f000174..ac4eabda 100644 --- a/src/test/functions.rs +++ b/src/test/functions.rs @@ -42,10 +42,10 @@ fn lifetime() { [ /* TODO */ ] expect_test::expect![[r#" - 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): + judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) 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, [], [], [], [], [], [], {}, {}) }`"#]] + judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }`"#]] ) } diff --git a/src/test/mod.rs b/src/test/mod.rs index d926aae3..b525f96e 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -46,13 +46,13 @@ fn hello_world_fail() { Caused by: 0: prove_where_clause_well_formed(!ty_2 : Bar ) - 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): + 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], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) @@ -122,13 +122,13 @@ fn basic_where_clauses_fail() { Caused by: 0: prove_where_clause_well_formed(for u32 : A <^ty0_0>) 1: prove_where_clause_well_formed(u32 : A ) - 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): + 2: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(A(u32, !ty_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) 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): + judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs index 475ba569..18ab49a1 100644 --- a/tests/associated_type_normalization.rs +++ b/tests/associated_type_normalization.rs @@ -16,6 +16,6 @@ const MIRROR: &str = "[ #[test] fn test_mirror_normalizes_u32_to_u32() { test_where_clause(MIRROR, "exists {} => {::Assoc = T}").assert_ok( - expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => ::Assoc} }}"], + expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => ::Assoc} }}"], ); } diff --git a/tests/projection.rs b/tests/projection.rs index 9b02170e..780394ee 100644 --- a/tests/projection.rs +++ b/tests/projection.rs @@ -23,38 +23,38 @@ fn normalize_basic() { NORMALIZE_BASIC, "forall exists {} => { as Iterator>::Item = U }", ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]); + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]); test_where_clause( NORMALIZE_BASIC, "forall {} => { Iterator(Vec), as Iterator>::Item = T }", ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], coherence_mode: false }, known_true: true, substitution: {} }}"]); + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }}"]); test_where_clause( NORMALIZE_BASIC, "forall { Iterator(T), ::Item = Foo } => { ::Item = Foo }", ).assert_ok( - expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], coherence_mode: false }, known_true: true, substitution: {} }}"] + expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }}"] ); test_where_clause( NORMALIZE_BASIC, "forall exists { Iterator(T) } => { ::Item = U }", ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => ::Item} }}"]); + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => ::Item} }}"]); test_where_clause( NORMALIZE_BASIC, "forall { Iterator(T) } => { ::Item = ::Item }", ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], coherence_mode: false }, known_true: true, substitution: {} }}"]); + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }}"]); test_where_clause( NORMALIZE_BASIC, "forall exists { Iterator(T) } => { ::Item = ::Item }", ).assert_ok( - expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => Vec<::Item>, ?ty_3 => ::Item} }}"]); + expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => Vec<::Item>, ?ty_3 => ::Item} }}"]); } const NORMALIZE_INTO_ITERATOR: &str = "[ @@ -87,7 +87,7 @@ fn normalize_into_iterator() { NORMALIZE_INTO_ITERATOR, "forall exists {} => { as IntoIterator>::Item = U }", ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => as IntoIterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]); + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => as IntoIterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]); } const PROJECTION_EQUALITY: &str = "[ @@ -110,9 +110,9 @@ fn projection_equality() { PROJECTION_EQUALITY, "exists {} => { Trait1(S), >::Type = U }", ) - .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => ::Type} }}"]); + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => ::Type} }}"]); test_where_clause(PROJECTION_EQUALITY, "exists {} => { Trait2(S, U) }").assert_ok( - expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => ::Type} }}"], + expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => ::Type} }}"], ); } From 05290fb23e6cfbaf32204acdff5c00435b60e179 Mon Sep 17 00:00:00 2001 From: lcnr Date: Fri, 31 May 2024 19:54:45 +0200 Subject: [PATCH 05/10] make negation a first-class operation --- book/src/formality_core/judgment_fn.md | 2 +- crates/formality-check/src/lib.rs | 61 +++-------- crates/formality-core/src/visit.rs | 2 +- crates/formality-prove/src/lib.rs | 1 + crates/formality-prove/src/prove.rs | 2 + crates/formality-prove/src/prove/env.rs | 21 ++-- crates/formality-prove/src/prove/is_local.rs | 57 ++++------- crates/formality-prove/src/prove/negation.rs | 101 +++++++++++++++++++ crates/formality-prove/src/prove/prove_wc.rs | 4 +- crates/formality-prove/src/test_util.rs | 37 ++++--- src/test/coherence_overlap.rs | 16 +-- 11 files changed, 181 insertions(+), 123 deletions(-) create mode 100644 crates/formality-prove/src/prove/negation.rs diff --git a/book/src/formality_core/judgment_fn.md b/book/src/formality_core/judgment_fn.md index eabbd3a6..b812a75a 100644 --- a/book/src/formality_core/judgment_fn.md +++ b/book/src/formality_core/judgment_fn.md @@ -1,6 +1,6 @@ # Judgment functions and inference rules -The next thing is the `judgement_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things: +The next thing is the `judgment_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things: ``` premise1 diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs index 03e6bfbc..b94a7def 100644 --- a/crates/formality-check/src/lib.rs +++ b/crates/formality-check/src/lib.rs @@ -3,7 +3,7 @@ use std::{collections::VecDeque, fmt::Debug}; use anyhow::bail; -use formality_prove::{Bias, Decls, Env}; +use formality_prove::{is_definitely_not_proveable, Bias, Decls, Env}; use formality_rust::{ grammar::{Crate, CrateItem, Program, Test, TestBoundData}, prove::ToWcs, @@ -115,61 +115,24 @@ impl Check<'_> { } #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))] - fn prove_not_goal( - &self, - env: &Env, - assumptions: impl ToWcs, - goal: impl ToWcs + Debug, - ) -> Fallible<()> { + fn prove_not_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> { let goal: Wcs = goal.to_wcs(); let assumptions: Wcs = assumptions.to_wcs(); - tracing::debug!("assumptions = {assumptions:?}"); - tracing::debug!("goal = {goal:?}"); - - assert!(env.bias() == Bias::Soundness); assert!(env.only_universal_variables()); assert!(env.encloses((&assumptions, &goal))); - // Proving `∀X. not(F(X))` is the same as proving: `not(∃X. F(X))`. - // Therefore, since we have only universal variables, we can change them all to - // existential and then try to prove. If we get back no solutions, we know that - // we've proven the negation. - // - // This is called the "negation as failure" property, and it relies on our solver - // being complete -- i.e., if there is a solution, we'll find it, or at least - // return ambiguous. - let mut existential_env = Env::default().with_bias(Bias::Completeness); - let universal_to_existential: Substitution = env - .variables() - .iter() - .map(|v| { - assert!(v.is_universal()); - let v1 = existential_env.fresh_existential(v.kind()); - (v, v1) - }) - .collect(); - - let existential_assumptions = universal_to_existential.apply(&assumptions); - let existential_goal = universal_to_existential.apply(&goal); - - let cs = formality_prove::prove( - self.decls, - &existential_env, - existential_assumptions.to_wcs(), - &existential_goal, + let cs = is_definitely_not_proveable( + env, + &assumptions, + goal.clone(), + |env, assumptions, goal| formality_prove::prove(self.decls, env, &assumptions, &goal), ); - - match cs.into_set() { - Ok(proofs) => { - bail!( - "failed to disprove\n {goal:?}\ngiven\n {assumptions:?}\ngot\n{proofs:?}" - ) - } - Err(err) => { - tracing::debug!("Proved not goal, error = {err}"); - return Ok(()); - } + let cs = cs.into_set()?; + if cs.iter().any(|c| c.unconditionally_true()) { + return Ok(()); } + + bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}") } } diff --git a/crates/formality-core/src/visit.rs b/crates/formality-core/src/visit.rs index 2f31114d..0cdcf004 100644 --- a/crates/formality-core/src/visit.rs +++ b/crates/formality-core/src/visit.rs @@ -2,7 +2,7 @@ use std::sync::Arc; use crate::{collections::Set, language::Language, variable::CoreVariable}; -pub trait CoreVisit { +pub trait CoreVisit: std::fmt::Debug { /// Extract the list of free variables (for the purposes of this function, defined by `Variable::is_free`). /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important). fn free_variables(&self) -> Vec>; diff --git a/crates/formality-prove/src/lib.rs b/crates/formality-prove/src/lib.rs index edbf576a..65a2745d 100644 --- a/crates/formality-prove/src/lib.rs +++ b/crates/formality-prove/src/lib.rs @@ -8,6 +8,7 @@ mod prove; pub use decls::*; pub use prove::prove; pub use prove::Constraints; +pub use prove::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure}; pub use prove::{Bias, Env}; #[cfg(test)] diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 22900b36..8b204d7c 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -3,6 +3,7 @@ mod constraints; mod env; mod is_local; mod minimize; +mod negation; mod prove_after; mod prove_eq; mod prove_normalize; @@ -21,6 +22,7 @@ use crate::decls::Decls; pub use self::env::{Bias, Env}; use self::prove_wc_list::prove_wc_list; +pub use negation::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure}; /// Top-level entry point for proving things; other rules recurse to this one. pub fn prove( diff --git a/crates/formality-prove/src/prove/env.rs b/crates/formality-prove/src/prove/env.rs index 67f30c15..bb1250bd 100644 --- a/crates/formality-prove/src/prove/env.rs +++ b/crates/formality-prove/src/prove/env.rs @@ -44,6 +44,13 @@ pub struct Env { } impl Env { + pub fn new_with_bias(bias: Bias) -> Self { + Env { + variables: Default::default(), + bias, + } + } + pub fn only_universal_variables(&self) -> bool { self.variables.iter().all(|v| v.is_universal()) } @@ -51,13 +58,6 @@ impl Env { pub fn bias(&self) -> Bias { self.bias } - - pub fn with_bias(&self, bias: Bias) -> Env { - Env { - bias, - ..self.clone() - } - } } cast_impl!(Env); @@ -105,6 +105,13 @@ impl Env { v } + pub fn fresh_universal(&mut self, kind: ParameterKind) -> UniversalVar { + let var_index = self.fresh_index(); + let v = UniversalVar { kind, var_index }; + self.variables.push(v.upcast()); + v + } + pub fn insert_fresh_before(&mut self, kind: ParameterKind, rank: Universe) -> ExistentialVar { let var_index = self.fresh_index(); let v = ExistentialVar { kind, var_index }; diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 0d12645a..9dd398ce 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -1,11 +1,14 @@ -use formality_core::{judgment_fn, ProvenSet, Upcast}; +use formality_core::{judgment_fn, Upcast}; use formality_types::grammar::{ AliasTy, BoundVar, Lt, Parameter, RigidName, RigidTy, TraitRef, TyData, Variable, Wcs, }; use crate::{ decls::Decls, - prove::{combinators::for_all, env::Bias, prove_normalize::prove_normalize, Constraints}, + prove::{ + combinators::for_all, env::Bias, negation::may_not_be_provable, + prove_normalize::prove_normalize, Constraints, + }, Env, }; @@ -49,22 +52,22 @@ judgment_fn! { env: Env, assumptions: Wcs, goal: TraitRef, - ) => () { + ) => Constraints { debug(assumptions, goal, decls, env) assert(env.bias() == Bias::Completeness) ( - (may_be_downstream_trait_ref(decls, env, assumptions, goal) => ()) + (may_be_downstream_trait_ref(decls, env, assumptions, goal) => c) --- ("may be defined downstream") - (may_be_remote(decls, env, assumptions, goal) => ()) + (may_be_remote(decls, env, assumptions, goal) => c) ) ( // In principle this rule could be removed and preserve soundness, // but then we would accept code that is very prone to semver failures. - (may_not_be_provable(&env, |env| is_local_trait_ref(decls, &env, assumptions, goal)) => ()) + (may_not_be_provable(&env, assumptions, goal, |env, assumptions, goal| is_local_trait_ref(decls, &env, assumptions, goal)) => c) --- ("may be added by upstream in a minor release") - (may_be_remote(decls, env, assumptions, goal) => ()) + (may_be_remote(decls, env, assumptions, goal) => c) ) } } @@ -76,15 +79,15 @@ judgment_fn! { env: Env, assumptions: Wcs, goal: TraitRef, - ) => () { + ) => Constraints { debug(goal, assumptions, env, decls) assert(env.bias() == Bias::Completeness) ( // There may be a downstream parameter at position i... (&goal.parameters => p) - (may_be_downstream_parameter(&decls, &env, &assumptions, p) => ()) + (may_be_downstream_parameter(&decls, &env, &assumptions, p) => c) --- ("may_be_downstream_trait_ref") - (may_be_downstream_trait_ref(decls, env, assumptions, goal) => ()) + (may_be_downstream_trait_ref(decls, env, assumptions, goal) => c) ) } } @@ -95,14 +98,15 @@ judgment_fn! { env: Env, assumptions: Wcs, parameter: Parameter, - ) => () { + ) => Constraints { debug(parameter, assumptions, env, decls) assert(env.bias() == Bias::Completeness) ( // existential variables *could* be inferred to downstream types; depends on the substitution // we ultimately have. --- ("type variable") - (may_be_downstream_parameter(_decls, _env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => ()) + (may_be_downstream_parameter(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) + => Constraints::none(env)) ) // If `parameter` is an alias which refers a type which may be @@ -117,11 +121,11 @@ judgment_fn! { (if may_contain_downstream_type(&decls, &env, &assumptions, p)) // (b) the alias cannot be normalized to something that may not be downstream - (may_not_be_provable(&env, |env| - normalizes_to_not_downstream(&decls, &env, &assumptions, AliasTy { name: name.clone(), parameters: parameters.clone() }) - ) => ()) + (may_not_be_provable(&env, &assumptions, AliasTy::new(&name, ¶meters), |env, assumptions, alias| + normalizes_to_not_downstream(&decls, &env, &assumptions, &alias) + ) => c) --- ("via normalize") - (may_be_downstream_parameter(decls, env, assumptions, AliasTy { name, parameters }) => ()) + (may_be_downstream_parameter(decls, env, assumptions, AliasTy { name, parameters }) => c) ) } } @@ -173,24 +177,6 @@ fn may_contain_downstream_type( } } -// FIXME(@lcnr): This should be a more general concept and not limited ot `is_local` -// -// Also, I think this should flip quantification from existential to universal again -fn may_not_be_provable(env: &Env, op: impl FnOnce(Env) -> ProvenSet) -> ProvenSet<()> { - assert!(env.bias() == Bias::Completeness); - if let Some(constraints) = op(env.with_bias(Bias::Soundness)) - .iter() - .find(|constraints| constraints.unconditionally_true()) - { - ProvenSet::failed( - "may_not_be_provable", - format!("found a solution {constraints:?}"), - ) - } else { - ProvenSet::singleton(()) - } -} - judgment_fn! { fn normalizes_to_not_downstream( decls: Decls, @@ -282,7 +268,8 @@ judgment_fn! { // existential variables *could* be inferred to downstream types; depends on the substitution // we ultimately have. --- ("type variable") - (is_not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous()) + (is_not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) + => Constraints::none(env).ambiguous()) ) } } diff --git a/crates/formality-prove/src/prove/negation.rs b/crates/formality-prove/src/prove/negation.rs new file mode 100644 index 00000000..143e00cf --- /dev/null +++ b/crates/formality-prove/src/prove/negation.rs @@ -0,0 +1,101 @@ +use crate::{Bias, Constraints, Env}; +use formality_core::{fold::CoreFold, ProvenSet, Upcast}; +use formality_types::{ + grammar::{Substitution, Variable, Wcs}, + rust::FormalityLang, +}; + +/// This succeeds if `f` definitely fails: there are no possible +/// ways to prove its body. +/// +/// This fails if `f' is ambiguous, so it is biases towards soundness. +/// It never succeeds if `f` may actually hold, but may fail even if +/// `f` does not hold. For this to be correct the body of `f` must +/// be complete: it must only fail if there is definitely no solution. +/// +/// Proving `∀X. not(F(X))` is the same as proving `not(∃X. F(X))`, so +/// this replaces all universal variables with existantials. +#[tracing::instrument(level = "Debug", skip_all)] +pub fn is_definitely_not_proveable>( + env: &Env, + assumptions: impl Upcast, + data: T, + f: impl FnOnce(Env, Wcs, T) -> ProvenSet, +) -> ProvenSet { + assert!(env.bias() == Bias::Soundness); + // FIXME(@lcnr): why do we care about only having universal variables + // here. + assert!(env.only_universal_variables()); + negation_via_failure(env, assumptions, data, f) +} + +/// This fails if `f` definitely succeeds. There is no way to prove `f`. +/// This should only be used if we're currently biased towards completeness +/// as it returns success even if there's still ambiguity. +#[tracing::instrument(level = "Debug", skip_all)] +pub fn may_not_be_provable>( + env: &Env, + assumptions: impl Upcast, + data: T, + f: impl FnOnce(Env, Wcs, T) -> ProvenSet, +) -> ProvenSet { + assert!(env.bias() == Bias::Completeness); + negation_via_failure(env, assumptions, data, f) +} + +pub fn negation_via_failure>( + env: &Env, + assumptions: impl Upcast, + data: T, + f: impl FnOnce(Env, Wcs, T) -> ProvenSet, +) -> ProvenSet { + let assumptions: Wcs = assumptions.upcast(); + tracing::debug!(?assumptions, ?data); + + let flipped_bias = match env.bias() { + Bias::Soundness => Bias::Completeness, + Bias::Completeness => Bias::Soundness, + }; + + // As we prove the negation, we have to flip the bias and + // quantifiers of all variables. + let mut flipped_env = Env::new_with_bias(flipped_bias); + let flip_quantification: Substitution = env + .variables() + .iter() + .map(|v| { + let v1: Variable = if v.is_universal() { + flipped_env.fresh_existential(v.kind()).upcast() + } else { + flipped_env.fresh_universal(v.kind()).upcast() + }; + (v, v1) + }) + .collect(); + + let flipped_assumptions = flip_quantification.apply(&assumptions); + let flipped_data = flip_quantification.apply(&data); + + let cs = f(flipped_env, flipped_assumptions, flipped_data); + match cs.into_set() { + Ok(s) => { + if let Some(constraints) = s + .iter() + .find(|constraints| constraints.unconditionally_true()) + { + ProvenSet::failed( + "negation_via_failure", + format!("found an unconditionally true solution {constraints:?}"), + ) + } else { + tracing::debug!("ambiguous `negation_via_failure`, solutions: {s:?}"); + ProvenSet::singleton(Constraints::none(env).ambiguous()) + } + } + + Err(err) => { + tracing::debug!("Proved `negation_via_failure`, error = {err}"); + ProvenSet::singleton(Constraints::none(env)) + } + } +} diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 204a4f65..47e6bca2 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -61,9 +61,9 @@ judgment_fn! { ( (if env.bias() == Bias::Completeness)! - (may_be_remote(decls, &env, assumptions, trait_ref) => ()) + (may_be_remote(decls, &env, assumptions, trait_ref) => c) ----------------------------- ("coherence / remote impl") - (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => Constraints::none(&env).ambiguous()) + (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c) ) ( diff --git a/crates/formality-prove/src/test_util.rs b/crates/formality-prove/src/test_util.rs index a5c7bfd4..a91a23f9 100644 --- a/crates/formality-prove/src/test_util.rs +++ b/crates/formality-prove/src/test_util.rs @@ -11,49 +11,54 @@ use crate::{ /// Useful assertions for use in tests. #[term] -pub enum TestAssertion { - #[grammar(coherence_mode $v0)] - CoherenceMode(Arc), +pub enum TestAssertionPart { #[grammar(forall $v0)] - ForAll(Binder>), + ForAll(Binder>), #[grammar(exists $v0)] - Exists(Binder>), + Exists(Binder>), #[grammar($v0 => $v1)] Prove(Wcs, Wcs), } +#[term] +pub enum TestAssertion { + #[cast] + Default(Arc), + #[grammar(coherence_mode $v0)] + CoherenceMode(Arc), +} + /// `t` represents some set of existential bindings combined with (assumptions, goals). /// Returns the constraints that result from proving assumptions/goals. These will reference /// existential variables created for the bindings, so they're really just suitable for /// using with expect. -pub fn test_prove(decls: Decls, mut assertion: Arc) -> ProvenSet { - let mut env = Env::default(); +pub fn test_prove(decls: Decls, assertion: Arc) -> ProvenSet { + let (mut assertion, bias) = match &*assertion { + TestAssertion::Default(assertion) => (assertion.clone(), Bias::Soundness), + TestAssertion::CoherenceMode(assertion) => (assertion.clone(), Bias::Completeness), + }; + + let mut env = Env::new_with_bias(bias); loop { match &*assertion { - TestAssertion::ForAll(binder) => { + TestAssertionPart::ForAll(binder) => { let (env1, subst) = env.universal_substitution(binder); let assertion1 = binder.instantiate_with(&subst).unwrap(); env = env1; assertion = assertion1; } - TestAssertion::Exists(binder) => { + TestAssertionPart::Exists(binder) => { let (env1, subst) = env.existential_substitution(binder); let assertion1 = binder.instantiate_with(&subst).unwrap(); env = env1; assertion = assertion1; } - TestAssertion::Prove(assumptions, goals) => { + TestAssertionPart::Prove(assumptions, goals) => { return prove(decls, env, assumptions, goals); } - - // FIXME(@lcnr): This should be "negation-by-failure" or sth. - TestAssertion::CoherenceMode(assertion1) => { - env = env.with_bias(Bias::Completeness); - assertion = assertion1.clone(); - } } } } diff --git a/src/test/coherence_overlap.rs b/src/test/coherence_overlap.rs index c8b26ef9..0eeb7544 100644 --- a/src/test/coherence_overlap.rs +++ b/src/test/coherence_overlap.rs @@ -23,12 +23,9 @@ fn u32_not_u32_impls() { check_trait_impl(impl Foo for u32 { }) Caused by: - failed to disprove - {! Foo(u32)} - given - {} - got - {Constraints { env: Env { variables: [], bias: Completeness }, known_true: true, substitution: {} }}"#]] + judgment `negation_via_failure` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + found an unconditionally true solution Constraints { env: Env { variables: [], bias: Completeness }, known_true: true, substitution: {} }"#]] ) } @@ -106,12 +103,7 @@ fn T_where_Foo_not_u32_impls() { check_trait_impl(impl Foo for ^ty0_0 where ^ty0_0 : Foo { }) Caused by: - failed to disprove - {! Foo(!ty_1)} - given - {Foo(!ty_1)} - got - {Constraints { env: Env { variables: [?ty_1], bias: Completeness }, known_true: true, substitution: {?ty_1 => u32} }}"#]] + failed to prove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: false, substitution: {} }}"#]] ) } From 2c1d634add68374ee85fcc9d4971031f75d453d0 Mon Sep 17 00:00:00 2001 From: lcnr Date: Fri, 31 May 2024 20:38:20 +0200 Subject: [PATCH 06/10] update more tests --- crates/formality-check/src/lib.rs | 4 +- .../src/prove/minimize/test.rs | 6 +- crates/formality-prove/src/test/adt_wf.rs | 14 +-- .../src/test/eq_assumptions.rs | 112 +++++++++--------- .../formality-prove/src/test/eq_partial_eq.rs | 54 ++++----- .../src/test/exists_constraints.rs | 2 +- crates/formality-prove/src/test/expanding.rs | 2 +- crates/formality-prove/src/test/is_local.rs | 8 +- crates/formality-prove/src/test/magic_copy.rs | 110 ++++++++--------- .../formality-prove/src/test/occurs_check.rs | 36 +++--- .../formality-prove/src/test/simple_impl.rs | 4 +- crates/formality-prove/src/test/universes.rs | 14 +-- tests/coherence_overlap.rs | 6 +- 13 files changed, 185 insertions(+), 187 deletions(-) diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs index b94a7def..ddd88479 100644 --- a/crates/formality-check/src/lib.rs +++ b/crates/formality-check/src/lib.rs @@ -3,12 +3,12 @@ use std::{collections::VecDeque, fmt::Debug}; use anyhow::bail; -use formality_prove::{is_definitely_not_proveable, Bias, Decls, Env}; +use formality_prove::{is_definitely_not_proveable, Decls, Env}; use formality_rust::{ grammar::{Crate, CrateItem, Program, Test, TestBoundData}, prove::ToWcs, }; -use formality_types::grammar::{Fallible, Substitution, Wcs}; +use formality_types::grammar::{Fallible, Wcs}; /// Check all crates in the program. The crates must be in dependency order /// such that any prefix of the crates is a complete program. diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs index c62e9e8f..8f55e46b 100644 --- a/crates/formality-prove/src/prove/minimize/test.rs +++ b/crates/formality-prove/src/prove/minimize/test.rs @@ -17,12 +17,12 @@ fn minimize_a() { let (env, subst) = env.existential_substitution(&term); let term = term.instantiate_with(&subst).unwrap(); - expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], coherence_mode: false }, [?ty_1, ?ty_3])"] + expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness }, [?ty_1, ?ty_3])"] .assert_eq(&format!("{:?}", (&env, &term))); let (mut env_min, term_min, m) = minimize(env, term); - expect!["(Env { variables: [?ty_0, ?ty_1], coherence_mode: false }, [?ty_0, ?ty_1])"] + expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness }, [?ty_0, ?ty_1])"] .assert_eq(&format!("{:?}", (&env_min, &term_min))); let ty0 = term_min[0].as_variable().unwrap(); @@ -50,7 +50,7 @@ fn minimize_a() { ?ty_4, ?ty_3, ], - coherence_mode: false, + bias: Soundness, }, known_true: true, substitution: { diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs index 6a9dc5ce..9cb90867 100644 --- a/crates/formality-prove/src/test/adt_wf.rs +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -31,7 +31,7 @@ fn well_formed_adt() { Constraints { env: Env { variables: [], - coherence_mode: false, + bias: Soundness, }, known_true: true, substitution: {}, @@ -51,17 +51,17 @@ fn not_well_formed_adt() { assumptions, Relation::WellFormed(goal), ).assert_err(expect![[r#" - judgment `prove_wc_list { goal: {@ wf(X)}, 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): + judgment `prove_wc_list { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ wf(X), 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): + judgment `prove_wc { goal: @ wf(X), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wf { goal: X, 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): + judgment `prove_wf { goal: X, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { 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): + judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): 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): + judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness }, 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()`"#]]); } diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs index dd77a9a1..abba6ed0 100644 --- a/crates/formality-prove/src/test/eq_assumptions.rs +++ b/crates/formality-prove/src/test/eq_assumptions.rs @@ -14,7 +14,7 @@ fn test_a() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, } "#]]); } @@ -27,7 +27,7 @@ fn test_b() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_2, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => u32} }, + Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => u32} }, } "#]]); } @@ -40,7 +40,7 @@ fn test_normalize_assoc_ty() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, } "#]]); } @@ -52,37 +52,37 @@ fn test_normalize_assoc_ty_existential0() { term("exists {} => {for if { ::Item = u32 } ::Item = u32}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: if {::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_1, b: ?ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_1, b: ?ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): 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)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): 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 @@ -90,61 +90,61 @@ fn test_normalize_assoc_ty_existential0() { 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)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, known_true: true, substitution: {} }, goal: {::Item = ::Item}, assumptions: {::Item = u32}, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, known_true: true, substitution: {} }, goal: {::Item = ::Item}, assumptions: {::Item = u32}, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ::Item = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: ::Item = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` 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-l" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, known_true: true, substitution: {} }, goal: {u32 = ::Item}, assumptions: {::Item = u32}, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {u32 = ::Item}, assumptions: {::Item = u32}, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: u32 = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: u32 = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because @@ -152,41 +152,41 @@ fn test_normalize_assoc_ty_existential0() { 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)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_1 = !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_1 = !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` 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-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` 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 "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because @@ -208,7 +208,7 @@ fn test_normalize_assoc_ty_existential1() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, + Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, } "#]]); } diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index 149f0b9f..224a08e2 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -28,7 +28,7 @@ fn eq_implies_partial_eq() { Constraints { env: Env { variables: [], - coherence_mode: false, + bias: Soundness, }, known_true: true, substitution: {}, @@ -44,17 +44,17 @@ fn not_partial_eq_implies_eq() { prove(decls(), (), (), goal) .assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {PartialEq(^ty0_0)} Eq(^ty0_0), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for if {PartialEq(^ty0_0)} Eq(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): 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 ], [], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness }, 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], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }`"#]]); } #[test] @@ -63,43 +63,43 @@ fn universals_not_eq() { prove(decls(), (), (), goal) .assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {Eq(^ty0_0)} PartialEq(^ty0_1), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for if {Eq(^ty0_0)} PartialEq(^ty0_1), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], coherence_mode: false }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!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: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], coherence_mode: false }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)}, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)}, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Eq(!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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), 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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = !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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = !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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = !ty_1, via: Eq(!ty_0), 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 ], [], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, 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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Eq(!ty_0), 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 ], [], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_1, b: !ty_0, 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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_1, b: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !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 ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_1, via: Eq(!ty_0), 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 ], [], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` 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 ], [], [], [], [], [], {}, {}) }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, 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], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }`"#]]); } diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs index 97b36674..17c71fab 100644 --- a/crates/formality-prove/src/test/exists_constraints.rs +++ b/crates/formality-prove/src/test/exists_constraints.rs @@ -20,7 +20,7 @@ fn decls() -> Decls { fn exists_u_for_t() { test_prove(decls(), term("exists {} => {Foo(U)}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_2, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => Vec} }, + Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec} }, } "#]]); } diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs index 05ec0eb2..4c3426ea 100644 --- a/crates/formality-prove/src/test/expanding.rs +++ b/crates/formality-prove/src/test/expanding.rs @@ -19,7 +19,7 @@ fn decls() -> Decls { fn expanding() { test_prove(decls(), term("exists {} => {Debug(T)}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_0], coherence_mode: false }, known_true: false, substitution: {} }, + Constraints { env: Env { variables: [?ty_0], bias: Soundness }, known_true: false, substitution: {} }, } "#]]); } diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index adcafefc..b981e88b 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -10,7 +10,7 @@ use crate::test_util::test_prove; fn test_forall_not_local() { test_prove( Decls::empty(), - term("coherence_mode {} => {for @IsLocal(Debug(T))}"), + term("{} => {} => for {@IsLocal(Debug(T))}"), ).assert_err( expect![[r#" judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): @@ -30,11 +30,11 @@ fn test_forall_not_local() { fn test_exists_not_local() { test_prove( Decls::empty(), - term("coherence_mode exists {} => {@IsLocal(Debug(T))}"), + term("exists {} => {@IsLocal(Debug(T))}"), ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_1], coherence_mode: true }, known_true: false, substitution: {} }, + Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: false, substitution: {} }, } - "#]]) // FIXME: really this should be ambiguous, not sure if it matters + "#]]) } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 1bb5172d..1765a3aa 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -25,118 +25,118 @@ fn decls() -> Decls { fn all_t_not_magic() { test_prove(decls(), term("{} => {for Magic(T)}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for Magic(^ty0_0), assumptions: {}, env: Env { variables: [], 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for Magic(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_1), assumptions: {}, env: Env { variables: [!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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Copy(?ty_2)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Copy(?ty_2)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Copy(!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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {Copy(!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)], [], [], [], [], {}, {}) }` + cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, 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], bias: Soundness }, 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], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }`"#]]); } #[test] fn all_t_not_copy() { test_prove(decls(), term("{} => {for Copy(T)}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for Copy(^ty0_0), assumptions: {}, env: Env { variables: [], 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for Copy(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_1), assumptions: {}, env: Env { variables: [!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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Copy(!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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, 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)], [], [], [], [], {}, {}) }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, 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 #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {}, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): 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)], [], [], [], [], {}, {}) }` + cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, 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], bias: Soundness }, 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 57df5325..f44e0666 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -20,13 +20,13 @@ fn decls() -> Decls { fn direct_cycle() { test_prove(decls(), term("exists {} => {A = Vec}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): 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 @@ -38,7 +38,7 @@ fn direct_cycle() { fn eq_variable_to_rigid() { test_prove(decls(), term("exists {} => {X = Vec}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, + Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, } "#]]); } @@ -48,7 +48,7 @@ fn eq_variable_to_rigid() { fn eq_rigid_to_variable() { test_prove(decls(), term("exists {} => {Vec = X}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], coherence_mode: false }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, + Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, } "#]]); } @@ -61,17 +61,17 @@ fn indirect_cycle_1() { term("exists {} => {A = Vec, B = A}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): 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 @@ -86,17 +86,17 @@ fn indirect_cycle_2() { term("exists {} => {B = A, A = Vec}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {}, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): 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 diff --git a/crates/formality-prove/src/test/simple_impl.rs b/crates/formality-prove/src/test/simple_impl.rs index 4af1484b..3c2a66a0 100644 --- a/crates/formality-prove/src/test/simple_impl.rs +++ b/crates/formality-prove/src/test/simple_impl.rs @@ -22,7 +22,7 @@ fn vec_u32_debug() { let goal: Wc = term("Debug(Vec)"); prove(decls(), (), (), goal).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, } "#]]); } @@ -32,7 +32,7 @@ fn vec_vec_u32_debug() { let goal: Wc = term("Debug(Vec>)"); prove(decls(), (), (), goal).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, } "#]]); } diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index f091a6af..88511bd1 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -12,17 +12,17 @@ fn exists_u_for_t() { let decls = Decls::empty(); test_prove(decls, term("exists {} => {for T = U}")).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for ^ty0_0 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for ^ty0_0 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_1, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: !ty_1, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): 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 @@ -40,7 +40,7 @@ fn for_t_exists_u() { test_prove(decls, term("{} => {for Test(T, T)}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, } "#]]); } diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index 2be9a922..d549c796 100644 --- a/tests/coherence_overlap.rs +++ b/tests/coherence_overlap.rs @@ -99,10 +99,8 @@ fn test_overlap_alias_not_normalizable() { // ...and if there is at least one Iterator impl, we also 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 { }"# - ]]); + impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"#]]); } From 5e0ac3daf4a86e6869de2bd993074bbb7355117b Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 18 Jun 2024 11:06:16 -0400 Subject: [PATCH 07/10] update pre-existing test to parse correctly --- crates/formality-prove/src/test/is_local.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index b981e88b..0c269e54 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -10,16 +10,16 @@ use crate::test_util::test_prove; fn test_forall_not_local() { test_prove( Decls::empty(), - term("{} => {} => for {@IsLocal(Debug(T))}"), + term("{} => {for @IsLocal(Debug(T))}"), ).assert_err( expect![[r#" - judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for @ IsLocal(Debug(^ty0_0)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for @ IsLocal(Debug(^ty0_0)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): 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): + judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness }, 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)` decls = decls(222, [], [], [], [], [], [], {}, {}) From a950442fcf34c705890308dda83100d9eb9412cc Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Thu, 20 Jun 2024 18:23:35 -0400 Subject: [PATCH 08/10] answer lcnr's question (somewhat) --- crates/formality-prove/src/prove/negation.rs | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/crates/formality-prove/src/prove/negation.rs b/crates/formality-prove/src/prove/negation.rs index 143e00cf..6881affa 100644 --- a/crates/formality-prove/src/prove/negation.rs +++ b/crates/formality-prove/src/prove/negation.rs @@ -23,8 +23,21 @@ pub fn is_definitely_not_proveable>( f: impl FnOnce(Env, Wcs, T) -> ProvenSet, ) -> ProvenSet { assert!(env.bias() == Bias::Soundness); - // FIXME(@lcnr): why do we care about only having universal variables - // here. + + // Require only universal variables, so e.g. `forall not (T: Foo)`. + // For those, we can convert universal and existential and try to prove + // the inverse (so try to prove `exists (T: Foo)`, with a bias towards + // completeness. If that fails, then we know that for all `T`, `T: Foo` is false. + // + // But with existential we can do no such trick. Given `exists not (T: Foo)`, + // certainly if we can prove `forall (T: Foo)` then we know this is false. + // But if we can't prove it, it doesn't tell us that there exists a `T` + // where `not (T: Foo)`, only that we could not prove it is true for all `T` + // (put another way, it may still be true for all T, we just couldn't prove it). + // + // (FIXME(nikomatsakis): This sounds suspicious, if we *truly* handle bias correctly, + // this might not hold; I suspect we do not, which is why I wonder if we can + // frame this another way, such as "known not to hold".) assert!(env.only_universal_variables()); negation_via_failure(env, assumptions, data, f) } From 3b4839461d4193f34ddc835e25dd19d6ae82fd4c Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Mon, 24 Jun 2024 15:54:31 -0400 Subject: [PATCH 09/10] cargo fmt --- tests/coherence_overlap.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index d549c796..2be9a922 100644 --- a/tests/coherence_overlap.rs +++ b/tests/coherence_overlap.rs @@ -99,8 +99,10 @@ fn test_overlap_alias_not_normalizable() { // ...and if there is at least one Iterator impl, we also 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 { }"#]]); + impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"# + ]]); } From 48556d9a34096aa016a3cd016d10705b6c3771b9 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Mon, 24 Jun 2024 16:57:19 -0400 Subject: [PATCH 10/10] generalize the regex to support windows paths Hopefully this won't get us into trouble. We could make platform dependent paths if needed. --- 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 c7a401ed..d8df1fc2 100644 --- a/crates/formality-core/src/test_util.rs +++ b/crates/formality-core/src/test_util.rs @@ -41,7 +41,7 @@ use std::fmt::{Debug, Display}; /// with `"src/file.rs:LL:CC"`. This makes error messages resilient against changes to the source code. pub fn normalize_paths(s: impl Display) -> String { let s = s.to_string(); - let re = regex::Regex::new(r"\([^():]+.rs:\d+:\d+\)").unwrap(); + let re = regex::Regex::new(r"\([^()]+.rs:\d+:\d+\)").unwrap(); re.replace_all(&s, "(src/file.rs:LL:CC)").to_string() }