add some wf checks for fn types

crates/formality-prove/src/decls.rs

@@ -1,8 +1,8 @@
 use formality_core::{set, Set, Upcast};
 use formality_macros::term;
 use formality_types::grammar::{
-    AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc,
-    Wcs,
+    AdtId, AliasName, AliasTy, Binder, FnId, Parameter, Predicate, Relation, TraitId, TraitRef, Ty,
+    Wc, Wcs,
 };
 
 #[term]
@@ -16,6 +16,7 @@ pub struct Decls {
     pub alias_eq_decls: Vec<AliasEqDecl>,
     pub alias_bound_decls: Vec<AliasBoundDecl>,
     pub adt_decls: Vec<AdtDecl>,
+    pub fn_decls: Vec<FnDecl>,
     pub local_trait_ids: Set<TraitId>,
     pub local_adt_ids: Set<AdtId>,
 }
@@ -78,6 +79,13 @@ impl Decls {
         v.pop().unwrap()
     }
 
+    pub fn fn_decl(&self, fn_id: &FnId) -> &FnDecl {
+        let mut v: Vec<_> = self.fn_decls.iter().filter(|t| t.id == *fn_id).collect();
+        assert!(!v.is_empty(), "no fn named `{fn_id:?}`");
+        assert!(v.len() <= 1, "multiple fns named `{fn_id:?}`");
+        v.pop().unwrap()
+    }
+
     /// Return the set of "trait invariants" for all traits.
     /// See [`TraitDecl::trait_invariants`].
     pub fn trait_invariants(&self) -> Set<TraitInvariant> {
@@ -96,6 +104,7 @@ impl Decls {
             alias_eq_decls: vec![],
             alias_bound_decls: vec![],
             adt_decls: vec![],
+            fn_decls: vec![],
             local_trait_ids: set![],
             local_adt_ids: set![],
         }
@@ -304,3 +313,21 @@ pub struct AdtDeclBoundData {
     /// The where-clauses declared on the ADT,
     pub where_clause: Wcs,
 }
+
+/// A "function declaration" declares a function name, its generics, its input and ouput types, and its where-clauses.
+/// It doesn't currently capture the function body, or input argument names.
+///
+/// In Rust syntax, it covers the `fn foo<T, U>(_: T) -> U where T: Bar`
+#[term(fn $id $binder)]
+pub struct FnDecl {
+    pub id: FnId,
+    pub binder: Binder<FnDeclBoundData>,
+}
+
+/// The "bound data" for a [`FnDecl`][].
+#[term(($input_tys) -> $output_ty $:where $where_clause)]
+pub struct FnDeclBoundData {
+    pub input_tys: Vec<Ty>,
+    pub output_ty: Ty,
+    pub where_clause: Wcs,
+}

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

@@ -42,6 +42,13 @@ judgment_fn! {
             (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c)
         )
 
+        (
+            // only checks that type is well-formed, does not do any lifetime or borrow check
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            --- ("ref")
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Ref(_), parameters }) => c)
+        )
+
         (
             (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
             (let t = decls.adt_decl(&adt_id))
@@ -51,6 +58,21 @@ judgment_fn! {
             (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c)
         )
 
+        (
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            (let t = decls.fn_decl(&fn_id))
+            (let t = t.binder.instantiate_with(&parameters).unwrap())
+            (prove_after(&decls, c, &assumptions, t.where_clause) => c)
+            --- ("fn-defs")
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::FnDef(fn_id), parameters }) => c)
+        )
+
+        (
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            --- ("fn-ptr")
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::FnPtr(_), parameters }) => c)
+        )
+
         (
             (prove_wf(&decls, &env, &assumptions, ty) => c)
             --- ("rigid constants")

crates/formality-prove/src/test/adt_wf.rs

@@ -51,17 +51,17 @@ fn not_well_formed_adt() {
         assumptions,
         Relation::WellFormed(goal),
     ).assert_err(expect![[r#"
-        judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+        judgment `prove_wc_list { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+            judgment `prove_wc { goal: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+                judgment `prove_wf { goal: X<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {}, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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 <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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 <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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 <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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()`"#]]);
 }