Show which where clause failed in diagnostics

Author: oli-obk

crates/formality-check/src/lib.rs

@@ -1,6 +1,6 @@
 #![allow(dead_code)]
 
-use std::collections::VecDeque;
+use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
 use formality_prove::{Decls, Env};
@@ -86,7 +86,12 @@ impl Check<'_> {
         }
     }
 
-    fn prove_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
+    fn prove_goal(
+        &self,
+        env: &Env,
+        assumptions: impl ToWcs,
+        goal: impl ToWcs + Debug,
+    ) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 
@@ -101,7 +106,12 @@ impl Check<'_> {
         bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
 
-    fn prove_not_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
+    fn prove_not_goal(
+        &self,
+        env: &Env,
+        assumptions: impl ToWcs,
+        goal: impl ToWcs + Debug,
+    ) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 

crates/formality-check/src/where_clauses.rs

@@ -1,3 +1,4 @@
+use fn_error_context::context;
 use formality_prove::Env;
 use formality_rust::{
     grammar::{WhereClause, WhereClauseData},
@@ -21,6 +22,7 @@ impl super::Check<'_> {
         Ok(())
     }
 
+    #[context("prove_where_clauses_well_formed({where_clause:?})")]
     fn prove_where_clause_well_formed(
         &self,
         in_env: &Env,

tests/hello_world.rs

@@ -6,7 +6,10 @@ fn test_broken() {
         Err(
             Error {
                 context: "check_trait(Foo)",
-                source: "failed to prove {@ WellFormedTraitRef(Bar(!ty_2, !ty_1))} given {Bar(!ty_2, !ty_1)}, got {}",
+                source: Error {
+                    context: "prove_where_clause_well_formed(!ty_2 : Bar < !ty_1 >)",
+                    source: "failed to prove {@ WellFormedTraitRef(Bar(!ty_2, !ty_1))} given {Bar(!ty_2, !ty_1)}, got {}",
+                },
             },
         )
     "#]].assert_debug_eq(&test_program_ok(