thread impl ToWcs and not &[WhereClause]

nikomatsakis · nikomatsakis · commit 2099cb1d51db · 2023-03-20T05:53:28.000-04:00
this will let us add other things that are not syntactically valid
where clauses
diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.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(())
     }
diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.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,14 +150,14 @@ 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),
         )?;
 
@@ -161,10 +168,17 @@ impl super::Check<'_> {
     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
@@ -191,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(())
     }
diff --git a/crates/formality-check/src/where_clauses.rs b/crates/formality-check/src/where_clauses.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(
