Merge pull request #124 from nikomatsakis/assoc-ty-norm

tests around associated type normalization

Author: nikomatsakis

Cargo.lock

@@ -14,12 +14,14 @@ expect-test = "1.4.0"
 formality-macros = { version = "0.1.0", path = "crates/formality-macros" }
 formality-core = { version = "0.1.0", path = "crates/formality-core" }
 
+
 [dependencies]
 anyhow = "1"
 clap = { version = "4.0.9", features = ["derive"] }
 formality-rust = { version = "0.1.0", path = "crates/formality-rust" }
 formality-types = { version = "0.1.0", path = "crates/formality-types" }
 formality-check = { version = "0.1.0", path = "crates/formality-check" }
+formality-prove = { version = "0.1.0", path = "crates/formality-prove" }
 
 [workspace]
 members = [

Cargo.toml

@@ -1,7 +1,7 @@
 use anyhow::bail;
 use fn_error_context::context;
 use formality_prove::Env;
-use formality_rust::grammar::{Crate, TraitImpl};
+use formality_rust::grammar::{Crate, NegTraitImpl, TraitImpl};
 use formality_types::{
     cast::Downcasted,
     grammar::{Fallible, Wc, Wcs},
@@ -15,11 +15,17 @@ impl Check<'_> {
         let all_crate_impls: Vec<TraitImpl> =
             self.program.items_from_all_crates().downcasted().collect();
         let current_crate_impls: Vec<TraitImpl> = current_crate.items.iter().downcasted().collect();
+        let current_crate_neg_impls: Vec<NegTraitImpl> =
+            current_crate.items.iter().downcasted().collect();
 
         for impl_a in &current_crate_impls {
             self.orphan_check(impl_a)?;
         }
 
+        for impl_a in &current_crate_neg_impls {
+            self.orphan_check_neg(impl_a)?;
+        }
+
         // check for duplicate impls in the current crate
         for (impl_a, i) in current_crate_impls.iter().zip(0..) {
             if current_crate_impls[i + 1..].contains(impl_a) {
@@ -32,6 +38,7 @@ impl Check<'_> {
             .iter()
             .cartesian_product(&all_crate_impls)
             .filter(|(impl_a, impl_b)| impl_a != impl_b)
+            .filter(|(impl_a, impl_b)| impl_a.trait_id() == impl_b.trait_id())
         {
             self.overlap_check(impl_a, impl_b)?;
         }
@@ -53,6 +60,20 @@ impl Check<'_> {
         )
     }
 
+    #[context("orphan_check_neg({impl_a:?})")]
+    fn orphan_check_neg(&self, impl_a: &NegTraitImpl) -> Fallible<()> {
+        let mut env = Env::default();
+
+        let a = env.instantiate_universally(&impl_a.binder);
+        let trait_ref = a.trait_ref();
+
+        self.prove_goal(
+            &env.with_coherence_mode(true),
+            &a.where_clauses,
+            trait_ref.is_local(),
+        )
+    }
+
     #[tracing::instrument(level = "Debug", skip(self))]
     fn overlap_check(&self, impl_a: &TraitImpl, impl_b: &TraitImpl) -> Fallible<()> {
         let mut env = Env::default();
@@ -72,25 +93,28 @@ impl Check<'_> {
         let trait_ref_a = a.trait_ref();
         let trait_ref_b = b.trait_ref();
 
-        // If the parameters from the two impls cannot be equal, then they do not overlap.
-        //
-        // If we can prove `∀P_a, ∀P_b. not (T_a = T_b, Wc_a, Wc_b)`, then they do not overlap.
-        if let Ok(()) = self.prove_not_goal(
-            &env.with_coherence_mode(true),
-            (&a.where_clauses, &b.where_clauses),
-            Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
-        ) {
-            return Ok(());
-        }
+        assert_eq!(trait_ref_a.trait_id, trait_ref_b.trait_id);
 
-        // If we can disprove the where clauses, then they do not overlap.
-        //
-        // If we can prove `∀P_a, ∀P_b. not [(T_a = T_b) => (Wc_a, Wc_b)]`, then they do not overlap.
+        // If we can prove that the parameters cannot be equated *or* the where-clauses don't hold,
+        // in coherence mode, then they do not overlap.
         if let Ok(()) = self.prove_not_goal(
             &env.with_coherence_mode(true),
-            Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
-            (&a.where_clauses, &b.where_clauses),
+            (),
+            (
+                Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                &a.where_clauses,
+                &b.where_clauses,
+            ),
         ) {
+            tracing::debug!(
+                "proved not {:?}",
+                (
+                    Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                    &a.where_clauses,
+                    &b.where_clauses,
+                )
+            );
+
             return Ok(());
         }
 
@@ -106,18 +130,28 @@ impl Check<'_> {
             .chain(&b.where_clauses)
             .flat_map(|wc| wc.invert())
             .collect();
-        if inverted.iter().any(|inverted_wc| {
+        if let Some(inverted_wc) = inverted.iter().find(|inverted_wc| {
             self.prove_goal(
                 &env,
                 (
                     Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
                     &a.where_clauses,
                     &b.where_clauses,
                 ),
-                inverted_wc,
+                &inverted_wc,
             )
             .is_ok()
         }) {
+            tracing::debug!(
+                "proved {:?} assuming {:?}",
+                &inverted_wc,
+                (
+                    Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+                    &a.where_clauses,
+                    &b.where_clauses,
+                )
+            );
+
             return Ok(());
         }
         bail!("impls may overlap: `{impl_a:?}` vs `{impl_b:?}`")

crates/formality-check/src/coherence.rs

@@ -1,20 +1,28 @@
 use formality_prove::Env;
-use formality_rust::grammar::{Fn, FnBoundData, WhereClause};
-use formality_types::{cast::Upcast, grammar::Fallible};
+use formality_rust::{
+    grammar::{Fn, FnBoundData},
+    prove::ToWcs,
+};
+use formality_types::{
+    grammar::{Fallible, Wcs},
+};
 
 use crate::Check;
 
 impl Check<'_> {
-    pub(crate) fn check_free_fn(&self, _f: &Fn) -> Fallible<()> {
-        todo!()
+    pub(crate) fn check_free_fn(&self, f: &Fn) -> Fallible<()> {
+        self.check_fn(&Env::default(), Wcs::t(), f)
     }
 
     pub(crate) fn check_fn(
         &self,
         in_env: &Env,
-        in_assumptions: &[WhereClause],
+        in_assumptions: impl ToWcs,
         f: &Fn,
     ) -> Fallible<()> {
+        let in_assumptions = in_assumptions.to_wcs();
+        assert!(in_env.only_universal_variables() && in_env.encloses((&in_assumptions, f)));
+
         let mut env = in_env.clone();
 
         let Fn { id: _, binder } = f;
@@ -26,15 +34,15 @@ impl Check<'_> {
             body: _,
         } = env.instantiate_universally(binder);
 
-        let assumptions: Vec<WhereClause> = (in_assumptions, &where_clauses).upcast();
+        let fn_assumptions: Wcs = (in_assumptions, &where_clauses).to_wcs();
 
-        self.prove_where_clauses_well_formed(&env, &assumptions, &where_clauses)?;
+        self.prove_where_clauses_well_formed(&env, &fn_assumptions, &where_clauses)?;
 
         for input_ty in &input_tys {
-            self.prove_goal(&env, &assumptions, input_ty.well_formed())?;
+            self.prove_goal(&env, &fn_assumptions, input_ty.well_formed())?;
         }
 
-        self.prove_goal(&env, &assumptions, output_ty.well_formed())?;
+        self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?;
 
         Ok(())
     }

crates/formality-check/src/fns.rs

@@ -1,17 +1,19 @@
 use anyhow::bail;
-use contracts::requires;
+
 use fn_error_context::context;
 use formality_prove::Env;
-use formality_rust::grammar::{
-    AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn,
-    FnBoundData, ImplItem, NegTraitImpl, NegTraitImplBoundData, TraitBoundData, TraitImpl,
-    TraitImplBoundData, TraitItem, WhereClause,
+use formality_rust::{
+    grammar::{
+        AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn,
+        FnBoundData, ImplItem, NegTraitImpl, NegTraitImplBoundData, TraitBoundData, TraitImpl,
+        TraitImplBoundData, TraitItem,
+    },
+    prove::ToWcs,
 };
 use formality_types::{
     cast::Downcasted,
     grammar::{Binder, Fallible, Relation, Substitution, Wcs},
     term::Term,
-    visit::Visit,
 };
 
 impl super::Check<'_> {
@@ -69,16 +71,20 @@ impl super::Check<'_> {
         Ok(())
     }
 
-    #[requires(assumptions.iter().all(|a| a.references_only_placeholder_variables()))]
     fn check_trait_impl_item(
         &self,
         env: &Env,
-        assumptions: &[WhereClause],
+        assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
     ) -> Fallible<()> {
+        let assumptions: Wcs = assumptions.to_wcs();
+        assert!(
+            env.only_universal_variables() && env.encloses((&assumptions, trait_items, impl_item))
+        );
+
         match impl_item {
-            ImplItem::Fn(v) => self.check_fn_in_impl(env, assumptions, trait_items, v),
+            ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v),
             ImplItem::AssociatedTyValue(v) => {
                 self.check_associated_ty_value(env, assumptions, trait_items, v)
             }
@@ -88,12 +94,13 @@ impl super::Check<'_> {
     fn check_fn_in_impl(
         &self,
         env: &Env,
-        impl_assumptions: &[WhereClause],
+        impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         ii_fn: &Fn,
     ) -> Fallible<()> {
+        let impl_assumptions: Wcs = impl_assumptions.to_wcs();
         assert!(
-            env.only_universal_variables() && env.encloses((impl_assumptions, trait_items, ii_fn))
+            env.only_universal_variables() && env.encloses((&impl_assumptions, trait_items, ii_fn))
         );
 
         // Find the corresponding function from the trait:
@@ -108,7 +115,7 @@ impl super::Check<'_> {
 
         tracing::debug!(?ti_fn);
 
-        self.check_fn(env, impl_assumptions, ii_fn)?;
+        self.check_fn(env, &impl_assumptions, ii_fn)?;
 
         let mut env = env.clone();
         let (
@@ -128,7 +135,7 @@ impl super::Check<'_> {
 
         self.prove_goal(
             &env,
-            (impl_assumptions, &ti_where_clauses),
+            (&impl_assumptions, &ti_where_clauses),
             &ii_where_clauses,
         )?;
 
@@ -143,27 +150,35 @@ impl super::Check<'_> {
         for (ii_input_ty, ti_input_ty) in ii_input_tys.iter().zip(&ti_input_tys) {
             self.prove_goal(
                 &env,
-                (impl_assumptions, &ii_where_clauses),
+                (&impl_assumptions, &ii_where_clauses),
                 Relation::sub(ti_input_ty, ii_input_ty),
             )?;
         }
 
         self.prove_goal(
             &env,
-            (impl_assumptions, &ii_where_clauses),
+            (&impl_assumptions, &ii_where_clauses),
             Relation::sub(ii_output_ty, ti_output_ty),
         )?;
 
         Ok(())
     }
 
+    #[context("check_associated_ty_value({impl_value:?})")]
     fn check_associated_ty_value(
         &self,
         impl_env: &Env,
-        impl_assumptions: &[WhereClause],
+        impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_value: &AssociatedTyValue,
     ) -> Fallible<()> {
+        let impl_assumptions: Wcs = impl_assumptions.to_wcs();
+
+        assert!(
+            impl_env.only_universal_variables()
+                && impl_env.encloses((&impl_assumptions, trait_items, impl_value))
+        );
+
         let AssociatedTyValue { id, binder } = impl_value;
 
         let trait_associated_ty = match trait_items
@@ -190,24 +205,24 @@ impl super::Check<'_> {
 
         self.prove_where_clauses_well_formed(
             &env,
-            (impl_assumptions, &ii_where_clauses),
+            (&impl_assumptions, &ii_where_clauses),
             &ii_where_clauses,
         )?;
 
         self.prove_goal(
             &env,
-            (impl_assumptions, &ti_where_clauses),
+            (&impl_assumptions, &ti_where_clauses),
             &ii_where_clauses,
         )?;
 
         self.prove_goal(
             &env,
-            (impl_assumptions, &ii_where_clauses),
+            (&impl_assumptions, &ii_where_clauses),
             ii_ty.well_formed(),
         )?;
 
         let ensures: Wcs = ti_ensures.iter().map(|e| e.to_wc(&ii_ty)).collect();
-        self.prove_goal(&env, (impl_assumptions, &ii_where_clauses), ensures)?;
+        self.prove_goal(&env, (&impl_assumptions, &ii_where_clauses), ensures)?;
 
         Ok(())
     }

crates/formality-check/src/impls.rs

@@ -12,10 +12,9 @@ impl super::Check<'_> {
     pub(crate) fn prove_where_clauses_well_formed(
         &self,
         env: &Env,
-        assumptions: impl Upcast<Vec<WhereClause>>,
+        assumptions: impl ToWcs,
         where_clauses: &[WhereClause],
     ) -> Fallible<()> {
-        let assumptions: Vec<WhereClause> = assumptions.upcast();
         for where_clause in where_clauses {
             self.prove_where_clause_well_formed(env, &assumptions, where_clause)?;
         }
@@ -25,10 +24,9 @@ impl super::Check<'_> {
     fn prove_where_clause_well_formed(
         &self,
         in_env: &Env,
-        assumptions: impl Upcast<Vec<WhereClause>>,
+        assumptions: impl ToWcs,
         where_clause: &WhereClause,
     ) -> Fallible<()> {
-        let assumptions: Vec<WhereClause> = assumptions.upcast();
         match where_clause.data() {
             WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => self
                 .prove_trait_ref_well_formed(

crates/formality-check/src/where_clauses.rs

@@ -6,7 +6,10 @@ mod prove;
 
 pub use decls::*;
 pub use prove::prove;
+pub use prove::Constraints;
 pub use prove::Env;
 
 #[cfg(test)]
 mod test;
+
+pub mod test_util;