Merge branch 'main' into fnty

crates/formality-prove/src/prove.rs

@@ -13,8 +13,9 @@ mod prove_wc_list;
 mod prove_wf;
 
 pub use constraints::Constraints;
+use formality_core::judgment::{FailedRule, TryIntoIter};
 use formality_core::visit::CoreVisit;
-use formality_core::{ProvenSet, Upcast};
+use formality_core::{set, ProvenSet, Upcast};
 use formality_types::grammar::Wcs;
 use tracing::Level;
 
@@ -53,7 +54,20 @@ pub fn prove(
 
     assert!(env.encloses(term_in));
 
-    let result_set = prove_wc_list(decls, &env, assumptions, goal);
+    struct ProveFailureLabel(String);
+    let label = ProveFailureLabel(format!(
+        "prove {{ goal: {goal:?}, assumptions: {assumptions:?}, env: {env:?}, decls: {decls:?} }}"
+    ));
+    impl std::fmt::Debug for ProveFailureLabel {
+        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+            f.write_str(&self.0)
+        }
+    }
+    let result_set =
+        match prove_wc_list(decls, &env, assumptions, goal).try_into_iter(|| "".to_string()) {
+            Ok(s) => ProvenSet::from_iter(s),
+            Err(e) => ProvenSet::failed_rules(label, set![FailedRule::new(e)]),
+        };
 
     tracing::debug!(?result_set);
 

crates/formality-prove/src/prove/is_local.rs

@@ -48,12 +48,12 @@ judgment_fn! {
     /// Note that per RFC #2451, upstream crates are not permitted to add blanket impls
     /// and so new upstream impls for local types cannot be added.
     pub fn may_be_remote(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: TraitRef,
     ) => Constraints {
-        debug(assumptions, goal, decls, env)
+        debug(assumptions, goal, env)
         assert(env.bias() == Bias::Completeness)
 
         (
@@ -75,12 +75,12 @@ judgment_fn! {
 judgment_fn! {
     /// True if an impl defining this trait-reference could appear in a downstream crate.
     fn may_be_downstream_trait_ref(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: TraitRef,
     ) => Constraints {
-        debug(goal, assumptions, env, decls)
+        debug(goal, assumptions, env)
         assert(env.bias() == Bias::Completeness)
         (
             // There may be a downstream parameter at position i...
@@ -94,12 +94,12 @@ judgment_fn! {
 
 judgment_fn! {
     fn may_be_downstream_parameter(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         parameter: Parameter,
     ) => Constraints {
-        debug(parameter, assumptions, env, decls)
+        debug(parameter, assumptions, env)
         assert(env.bias() == Bias::Completeness)
         (
             // existential variables *could* be inferred to downstream types; depends on the substitution
@@ -179,12 +179,12 @@ fn may_contain_downstream_type(
 
 judgment_fn! {
     fn normalizes_to_not_downstream(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         parameter: Parameter,
     ) => Constraints {
-        debug(parameter, assumptions, env, decls)
+        debug(parameter, assumptions, env)
 
         (
             (prove_normalize(&decls, &env, &assumptions, parameter) => (c1, parameter))
@@ -198,12 +198,12 @@ judgment_fn! {
 
 judgment_fn! {
     pub fn is_local_trait_ref(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: TraitRef,
     ) => Constraints {
-        debug(goal, assumptions, env, decls)
+        debug(goal, assumptions, env)
         assert(env.bias() == Bias::Soundness)
         (
             (if decls.is_local_trait_id(&goal.trait_id))
@@ -235,12 +235,12 @@ judgment_fn! {
     /// with something like `Vec<DownstreamType>`, but that is not considered downstream
     /// as the outermost type (`Vec`) is upstream.
     fn is_not_downstream(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         parameter: Parameter,
     ) => Constraints {
-        debug(parameter, assumptions, env, decls)
+        debug(parameter, assumptions, env)
         assert(env.bias() == Bias::Soundness)
 
         (
@@ -276,12 +276,12 @@ judgment_fn! {
 
 judgment_fn! {
     fn is_local_parameter(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: Parameter,
     ) => Constraints {
-        debug(goal, assumptions, env, decls)
+        debug(goal, assumptions, env)
         assert(env.bias() == Bias::Soundness)
 
         // If we can normalize `goal` to something else, check if that normalized form is local.

crates/formality-prove/src/prove/prove_after.rs

@@ -7,12 +7,12 @@ use super::constraints::Constraints;
 
 judgment_fn! {
     pub fn prove_after(
-        decls: Decls,
+        _decls: Decls,
         constraints: Constraints,
         assumptions: Wcs,
         goal: Wcs,
     ) => Constraints {
-        debug(constraints, goal, assumptions, decls)
+        debug(constraints, goal, assumptions)
 
         (
             (let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal)))

crates/formality-prove/src/prove/prove_eq.rs

@@ -22,13 +22,13 @@ pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> Relation {
 
 judgment_fn! {
     pub fn prove_eq(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         a: Parameter,
         b: Parameter,
     ) => Constraints {
-        debug(a, b, assumptions, env, decls)
+        debug(a, b, assumptions, env)
 
         assert(a.kind() == b.kind())
 
@@ -75,13 +75,13 @@ judgment_fn! {
 
 judgment_fn! {
     pub fn prove_existential_var_eq(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         v: ExistentialVar,
         b: Parameter,
     ) => Constraints {
-        debug(v, b, assumptions, env, decls)
+        debug(v, b, assumptions, env)
 
         (
             (if let None = t.downcast::<Variable>())

crates/formality-prove/src/prove/prove_normalize.rs

@@ -15,12 +15,12 @@ use super::constraints::Constraints;
 
 judgment_fn! {
     pub fn prove_normalize(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         p: Parameter,
     ) => (Constraints, Parameter) {
-        debug(p, assumptions, env, decls)
+        debug(p, assumptions, env)
 
         (
             (&assumptions => a)!
@@ -48,13 +48,13 @@ judgment_fn! {
 
 judgment_fn! {
     fn prove_normalize_via(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         via: Wc,
         goal: Parameter,
     ) => (Constraints, Parameter) {
-        debug(goal, via, assumptions, env, decls)
+        debug(goal, via, assumptions, env)
 
         // The following 2 rules handle normalization of existential variables. We look specifically for
         // the case of a assumption `?X = Y`, which lets us normalize `?X` to `Y`, and ignore
@@ -126,13 +126,13 @@ judgment_fn! {
 
 judgment_fn! {
     fn prove_syntactically_eq(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         a: Parameter,
         b: Parameter,
     ) => Constraints {
-        debug(a, b, assumptions, env, decls)
+        debug(a, b, assumptions, env)
 
         trivial(a == b => Constraints::none(env))
 

crates/formality-prove/src/prove/prove_via.rs

@@ -8,13 +8,13 @@ use crate::{
 
 judgment_fn! {
     pub fn prove_via(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         via: WcData,
         goal: WcData,
     ) => Constraints {
-        debug(goal, via, assumptions, env, decls)
+        debug(goal, via, assumptions, env)
 
         (
             (let (skel_c, parameters_c) = pred_1.debone())

crates/formality-prove/src/prove/prove_wc.rs

@@ -18,12 +18,12 @@ use super::constraints::Constraints;
 
 judgment_fn! {
     pub fn prove_wc(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: Wc,
     ) => Constraints {
-        debug(goal, assumptions, env, decls)
+        debug(goal, assumptions, env)
 
         (
             (let (env, subst) = env.universal_substitution(&binder))

crates/formality-prove/src/prove/prove_wc_list.rs

@@ -10,12 +10,12 @@ use super::{env::Env, prove_wc::prove_wc};
 
 judgment_fn! {
     pub fn prove_wc_list(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: Wcs,
     ) => Constraints {
-        debug(goal, assumptions, env, decls)
+        debug(goal, assumptions, env)
 
         assert(env.encloses((&assumptions, &goal)))
 

crates/formality-prove/src/prove/prove_wf.rs

@@ -12,12 +12,12 @@ use super::{constraints::Constraints, env::Env};
 
 judgment_fn! {
     pub fn prove_wf(
-        decls: Decls,
+        _decls: Decls,
         env: Env,
         assumptions: Wcs,
         goal: Parameter,
     ) => Constraints {
-        debug(goal, assumptions, env, decls)
+        debug(goal, assumptions, env)
 
         assert(env.encloses((&assumptions, &goal)))