check wf'd ness of placeholders

Author: nikomatsakis

crates/formality-prove/src/prove.rs

@@ -8,6 +8,7 @@ mod prove_normalize;
 mod prove_via;
 mod prove_wc;
 mod prove_wc_list;
+mod prove_wf;
 mod combinators;
 
 pub use constraints::Constraints;

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

@@ -12,6 +12,7 @@ use crate::{
         prove_after::prove_after,
         prove_eq::prove_eq,
         prove_via::prove_via,
+        prove_wf::prove_wf,
     },
 };
 
@@ -106,5 +107,12 @@ judgment_fn! {
             ----------------------------- ("trait ref is local")
             (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c)
         )
+
+
+        (
+            (prove_wf(decls, env, assumptions, p) => c)
+            ----------------------------- ("trait ref is local")
+            (prove_wc(decls, env, assumptions, Relation::WellFormed(p)) => c)
+        )
     }
 }

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

@@ -0,0 +1,30 @@
+use formality_types::{
+    grammar::{Parameter, PlaceholderVar, Wcs},
+    judgment_fn,
+};
+
+use crate::decls::Decls;
+
+use super::{constraints::Constraints, env::Env};
+
+judgment_fn! {
+    pub fn prove_wf(
+        decls: Decls,
+        env: Env,
+        assumptions: Wcs,
+        goal: Parameter,
+    ) => Constraints {
+        debug(goal, assumptions, env, decls)
+
+        assert(env.encloses((&assumptions, &goal)))
+
+        (
+            // Always assume that universal variables are WF. This is debatable, it implies
+            // that we ensure by construction that the values we infer for existential variables
+            // are WF. An alternative would be to add explicit assumptions into the environment
+            // for every universal variable. That just seems tedious.
+            --- ("universal variables")
+            (prove_wf(_decls, env, _assumptions, PlaceholderVar { .. }) => Constraints::none(env))
+        )
+    }
+}

tests/associated_type_normalization.rs

@@ -6,12 +6,31 @@ fn test_mirror_normalizes_u32_to_u32() {
     // where there is a negative impl, so it is accepted.
 
     expect_test::expect![[r#"
-        Err(
-            Error {
-                context: "check_trait_impl(impl <ty> Mirror < > for ^ty0_0 where [] { type Assoc <> = ^ty1_0 where [] ; })",
-                source: Error {
-                    context: "check_associated_ty_value(type Assoc <> = !ty_1 where [] ;)",
-                    source: "failed to prove {@ wf(!ty_1)} given {}, got {}",
+        Ok(
+            {
+                Constraints {
+                    env: Env {
+                        variables: [
+                            ?ty_1,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_1 => (rigid (scalar u32)),
+                    },
+                },
+                Constraints {
+                    env: Env {
+                        variables: [
+                            ?ty_1,
+                        ],
+                        coherence_mode: false,
+                    },
+                    known_true: true,
+                    substitution: {
+                        ?ty_1 => (alias (Mirror :: Assoc) (rigid (scalar u32))),
+                    },
                 },
             },
         )