Extend well-formedness check of ADTs to include where-clauses

crates/formality-prove/src/decls.rs

@@ -15,6 +15,7 @@ pub struct Decls {
     pub neg_impl_decls: Vec<NegImplDecl>,
     pub alias_eq_decls: Vec<AliasEqDecl>,
     pub alias_bound_decls: Vec<AliasBoundDecl>,
+    pub adt_decls: Vec<AdtDecl>,
     pub local_trait_ids: Set<TraitId>,
     pub local_adt_ids: Set<AdtId>,
 }
@@ -70,6 +71,13 @@ impl Decls {
         &self.alias_bound_decls
     }
 
+    pub fn adt_decl(&self, adt_id: &AdtId) -> &AdtDecl {
+        let mut v: Vec<_> = self.adt_decls.iter().filter(|t| t.id == *adt_id).collect();
+        assert!(!v.is_empty(), "no ADT named `{adt_id:?}`");
+        assert!(v.len() <= 1, "multiple ADTs named `{adt_id:?}`");
+        v.pop().unwrap()
+    }
+
     /// Return the set of "trait invariants" for all traits.
     /// See [`TraitDecl::trait_invariants`].
     pub fn trait_invariants(&self) -> Set<TraitInvariant> {
@@ -87,6 +95,7 @@ impl Decls {
             neg_impl_decls: vec![],
             alias_eq_decls: vec![],
             alias_bound_decls: vec![],
+            adt_decls: vec![],
             local_trait_ids: set![],
             local_adt_ids: set![],
         }
@@ -257,3 +266,23 @@ pub struct AliasBoundDeclBoundData {
     pub ensures: Binder<Wc>,
     pub where_clause: Wcs,
 }
+
+/// An "ADT declaration" declares an ADT name, its generics, and its where-clauses.
+/// It doesn't capture the ADT fields, yet.
+///
+/// In Rust syntax, it covers the `struct Foo<X> where X: Bar` part of the declaration, but not what appears in the `{...}`.
+#[term(adt $id $binder)]
+pub struct AdtDecl {
+    /// The name of the ADT.
+    pub id: AdtId,
+
+    /// The binder here captures the generics of the ADT.
+    pub binder: Binder<AdtDeclBoundData>,
+}
+
+/// The "bound data" for a [`AdtDecl`][].
+#[term(where $where_clause)]
+pub struct AdtDeclBoundData {
+    /// The where-clauses declared on the ADT,
+    pub where_clause: Wcs,
+}

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

@@ -3,7 +3,10 @@ use formality_types::grammar::{
     AliasName, AliasTy, ConstData, Parameter, Parameters, RigidName, RigidTy, UniversalVar, Wcs,
 };
 
-use crate::{decls::Decls, prove::combinators::for_all};
+use crate::{
+    decls::Decls,
+    prove::{combinators::for_all, prove_after::prove_after},
+};
 
 use super::{constraints::Constraints, env::Env};
 
@@ -41,8 +44,11 @@ judgment_fn! {
 
         (
             (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            (let t = decls.adt_decl(&adt_id))
+            (let t = t.binder.instantiate_with(&parameters).unwrap())
+            (prove_after(&decls, c, &assumptions, t.where_clause) => c)
             --- ("ADT")
-            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(_), parameters }) => c)
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c)
         )
 
         (

crates/formality-prove/src/test.rs

@@ -1,3 +1,4 @@
+mod adt_wf;
 mod eq_assumptions;
 mod eq_partial_eq;
 mod exists_constraints;

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

@@ -0,0 +1,48 @@
+use expect_test::expect;
+use formality_core::test;
+use formality_types::{
+    grammar::{Parameter, Relation, Wcs},
+    rust::term,
+};
+
+use crate::{decls::Decls, prove::prove};
+
+fn decls() -> Decls {
+    Decls {
+        trait_decls: vec![term("trait Foo<ty Self> where {}")],
+        impl_decls: vec![term("impl<> Foo(u32) where {}")],
+        adt_decls: vec![term("adt X<ty T> where {Foo(T)}")],
+        ..Decls::empty()
+    }
+}
+
+#[test]
+fn well_formed_adt() {
+    let assumptions: Wcs = Wcs::t();
+    let goal: Parameter = term("X<u32>");
+    let constraints = prove(decls(), (), assumptions, Relation::WellFormed(goal));
+    expect![[r#"
+        {
+            Constraints {
+                env: Env {
+                    variables: [],
+                    coherence_mode: false,
+                },
+                known_true: true,
+                substitution: {},
+            },
+        }
+    "#]]
+    .assert_debug_eq(&constraints);
+}
+
+#[test]
+fn not_well_formed_adt() {
+    let assumptions: Wcs = Wcs::t();
+    let goal: Parameter = term("X<u64>");
+    let constraints = prove(decls(), (), assumptions, Relation::WellFormed(goal));
+    expect![[r#"
+        {}
+    "#]]
+    .assert_debug_eq(&constraints);
+}

crates/formality-rust/src/prove.rs

@@ -1,8 +1,8 @@
 use crate::grammar::{
-    AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Crate,
-    CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData, Program, Trait, TraitBoundData,
-    TraitImpl, TraitImplBoundData, TraitItem, WhereBound, WhereBoundData, WhereClause,
-    WhereClauseData,
+    Adt, AdtBoundData, AssociatedTy, AssociatedTyBoundData, AssociatedTyValue,
+    AssociatedTyValueBoundData, Crate, CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData,
+    Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem, WhereBound,
+    WhereBoundData, WhereClause, WhereClauseData,
 };
 use formality_core::{seq, Set, To, Upcast, Upcasted};
 use formality_prove as prove;
@@ -22,6 +22,7 @@ impl Program {
             neg_impl_decls: self.neg_impl_decls(),
             alias_eq_decls: self.alias_eq_decls(),
             alias_bound_decls: self.alias_bound_decls(),
+            adt_decls: self.adt_decls(),
             local_trait_ids: self.local_trait_ids(),
             local_adt_ids: self.local_adt_ids(),
         }
@@ -56,6 +57,10 @@ impl Program {
             .collect()
     }
 
+    fn adt_decls(&self) -> Vec<prove::AdtDecl> {
+        self.crates.iter().flat_map(|c| c.adt_decls()).collect()
+    }
+
     fn local_trait_ids(&self) -> Set<TraitId> {
         self.crates
             .last()
@@ -279,6 +284,35 @@ impl Crate {
             .collect()
     }
 
+    fn adt_decls(&self) -> Vec<prove::AdtDecl> {
+        self.items
+            .iter()
+            .flat_map(|item| match item {
+                CrateItem::Struct(s) => Some(s.to_adt()),
+                CrateItem::Enum(e) => Some(e.to_adt()),
+                _ => None,
+            })
+            .map(|Adt { id, binder }| {
+                let (
+                    vars,
+                    AdtBoundData {
+                        where_clauses,
+                        variants: _,
+                    },
+                ) = binder.open();
+                prove::AdtDecl {
+                    id: id.clone(),
+                    binder: Binder::new(
+                        vars,
+                        prove::AdtDeclBoundData {
+                            where_clause: where_clauses.iter().flat_map(|wc| wc.to_wcs()).collect(),
+                        },
+                    ),
+                }
+            })
+            .collect()
+    }
+
     fn adt_ids(&self) -> Set<AdtId> {
         self.items
             .iter()