prove_wc WellFormedTraitRef rule: require the parameters to be well-formed

Author: mattheww

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

@@ -4,6 +4,7 @@ use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs};
 use crate::{
     decls::Decls,
     prove::{
+        combinators::for_all,
         env::{Bias, Env},
         is_local::{is_local_trait_ref, may_be_remote},
         prove,
@@ -105,9 +106,10 @@ judgment_fn! {
         )
 
         (
-            (let t = decls.trait_decl(&trait_ref.trait_id))
+            (for_all(&decls, &env, &assumptions, &trait_ref.parameters, &prove_wf) => c)
+            (let t = &decls.trait_decl(&trait_ref.trait_id))
             (let t = t.binder.instantiate_with(&trait_ref.parameters).unwrap())
-            (prove(decls, env, assumptions, t.where_clause) => c)
+            (prove_after(&decls, c, &assumptions, t.where_clause) => c)
             ----------------------------- ("trait well formed")
             (prove_wc(decls, env, assumptions, Predicate::WellFormedTraitRef(trait_ref)) => c)
         )