WIP: const effect

crates/formality-check/src/fns.rs

@@ -1,9 +1,9 @@
 use formality_prove::Env;
 use formality_rust::{
-    grammar::{Fn, FnBoundData},
+    grammar::{Fn, FnBody, FnBoundData, MaybeFnBody},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Wcs};
+use formality_types::grammar::{Fallible, Relation, Wcs};
 
 use crate::Check;
 
@@ -29,7 +29,8 @@ impl Check<'_> {
             input_tys,
             output_ty,
             where_clauses,
-            body: _,
+            effect: declared_effect,
+            body,
         } = env.instantiate_universally(binder);
 
         let fn_assumptions: Wcs = (in_assumptions, &where_clauses).to_wcs();
@@ -42,6 +43,35 @@ impl Check<'_> {
 
         self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?;
 
+        // prove that the body type checks (if present)
+        match body {
+            MaybeFnBody::NoFnBody => {
+                // No fn body: this occurs e.g. for the fn `bar`
+                // in `trait Foo { fn bar(); }`. No check required.
+            }
+            MaybeFnBody::FnBody(fn_body) => match fn_body {
+                FnBody::TrustedFnBody => {
+                    // Trusted: just assume it's ok, useful for tests
+                    // to indicate things we don't want to think about.
+                }
+                FnBody::MirFnBody(_mir_fn_body) => {
+                    // TODO: this nikomatsakis is theoretically working on removing
+                    // though he has not made much time for it.
+                    unimplemented!()
+                }
+                FnBody::FnBodyWithEffect(body_effect) => {
+                    // Useful for tests: declares "some body" with the
+                    // given effect. So we need to check that the effect
+                    // is in bounds of the declaration.
+                    self.prove_goal(
+                        &env,
+                        &fn_assumptions,
+                        Relation::EffectSubset(body_effect, declared_effect)
+                    )?;
+                }
+            }
+        }
+
         Ok(())
     }
 }

crates/formality-check/src/impls.rs

@@ -11,8 +11,9 @@ use formality_rust::{
     },
     prove::ToWcs,
 };
+use formality_types::grammar::AtomicEffect::Runtime;
 use formality_types::{
-    grammar::{Binder, Fallible, Relation, Substitution, Wcs},
+    grammar::{Binder, Effect, Fallible, Relation, Substitution, Wcs},
     rust::Term,
 };
 
@@ -24,14 +25,15 @@ impl super::Check<'_> {
         let mut env = Env::default();
 
         let TraitImplBoundData {
+            effect,
             trait_id,
             self_ty,
             trait_parameters,
             where_clauses,
             impl_items,
         } = env.instantiate_universally(binder);
 
-        let trait_ref = trait_id.with(self_ty, trait_parameters);
+        let trait_ref = trait_id.with(&effect, self_ty, trait_parameters);
 
         self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
 
@@ -43,6 +45,7 @@ impl super::Check<'_> {
         let TraitBoundData {
             where_clauses: _,
             trait_items,
+            effect_items: _,
         } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?;
 
         self.check_safety_matches(trait_decl, trait_impl)?;
@@ -67,7 +70,7 @@ impl super::Check<'_> {
             where_clauses,
         } = env.instantiate_universally(binder);
 
-        let trait_ref = trait_id.with(self_ty, trait_parameters);
+        let trait_ref = trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters);
 
         // Negative impls are always safe (rustc E0198) regardless of the trait's safety.
         if *safety == Safety::Unsafe {
@@ -115,6 +118,44 @@ impl super::Check<'_> {
         }
     }
 
+    /// Check that function `ii_fn` that appears in an impl is valid.
+    /// This includes the core check from [`Self::check_fn`][],
+    /// but also additional checks to ensure that the signature in the impl
+    /// matches what is declared in the trait.
+    ///
+    /// # Example
+    ///
+    /// Suppose we are checking `<Cup<L> as Potable>::drink` in this example...
+    ///
+    /// ```rust,ignore
+    /// trait Potable {
+    ///     fn drink(&self); // `trait_items` includes these fns
+    ///     fn smell(&self); //
+    /// }
+    ///
+    /// struct Water;
+    /// impl Potable for Water {
+    ///     fn drink(&self) {}
+    ///     fn smell(&self) {}
+    /// }
+    ///
+    /// struct Cup<L>;
+    /// impl<L> Potable for Cup<L> // <-- env has `L` in scope
+    /// where
+    ///     L: Potable, // <-- `impl_assumptions`
+    /// {
+    ///     fn drink(&self) {} // <-- `ii_fn`
+    ///     fn smell(&self) {} // not currently being checked
+    /// }
+    /// ```
+    ///
+    /// # Parameters
+    ///
+    /// * `env`, the environment from the impl header
+    /// * `impl_assumptions`, where-clauses declared on the impl
+    /// * `trait_items`, items declared in the trait that is being implemented
+    ///   (we search this to find the corresponding declaration of the method)
+    /// * `ii_fn`, the fn as declared in the impl
     fn check_fn_in_impl(
         &self,
         env: &Env,
@@ -143,16 +184,21 @@ impl super::Check<'_> {
 
         let mut env = env.clone();
         let (
+            // ii_: the signature of the function as found in the impl item (ii)
             FnBoundData {
                 input_tys: ii_input_tys,
                 output_ty: ii_output_ty,
                 where_clauses: ii_where_clauses,
+                effect: ii_effect,
                 body: _,
             },
+
+            // ti_: the signature of the function as found in the trait item (ti)
             FnBoundData {
                 input_tys: ti_input_tys,
                 output_ty: ti_output_ty,
                 where_clauses: ti_where_clauses,
+                effect: ti_effect,
                 body: _,
             },
         ) = env.instantiate_universally(&self.merge_binders(&ii_fn.binder, &ti_fn.binder)?);
@@ -163,6 +209,7 @@ impl super::Check<'_> {
             &ii_where_clauses,
         )?;
 
+        // Must have same number of arguments as declared in the trait
         if ii_input_tys.len() != ti_input_tys.len() {
             bail!(
                 "impl has {} function arguments but trait has {} function arguments",
@@ -171,6 +218,16 @@ impl super::Check<'_> {
             )
         }
 
+        // The type `ii_input_ty` of argument `i` in the impl
+        // must be a supertype of the correspond type `ti_input_ty` from the trait.
+        //
+        // e.g. if you have `fn foo(arg: for<'a> fn(&u8))` in the trait
+        // you can have `fn foo(arg: fn(&'static u8))` in the impl.
+        //
+        // Why? Trait guarantees you are receiving a fn that can take
+        // an `&u8` in any lifetime. Impl is saying "I only need a fn that can
+        // take `&u8` in static lifetime", which is more narrow, and that's ok,
+        // because a functon that can handle any lifetime can also handle static.
         for (ii_input_ty, ti_input_ty) in ii_input_tys.iter().zip(&ti_input_tys) {
             self.prove_goal(
                 &env,
@@ -179,12 +236,20 @@ impl super::Check<'_> {
             )?;
         }
 
+        // Impl must return a subtype of the return type from the trait.
         self.prove_goal(
             &env,
             (&impl_assumptions, &ii_where_clauses),
             Relation::sub(ii_output_ty, ti_output_ty),
         )?;
 
+        // Impl must not have more effects than what are declared in the trait.
+        self.prove_goal(
+            &env,
+            (&impl_assumptions, &ii_where_clauses),
+            Relation::EffectSubset(ii_effect, ti_effect),
+        )?;
+
         Ok(())
     }
 

crates/formality-check/src/traits.rs

@@ -14,12 +14,14 @@ impl super::Check<'_> {
             safety: _,
             id: _,
             binder,
+            effect: _,
         } = t;
         let mut env = Env::default();
 
         let TraitBoundData {
             where_clauses,
             trait_items,
+            effect_items: _,
         } = env.instantiate_universally(&binder.explicit_binder);
 
         self.check_trait_items_have_unique_names(&trait_items)?;

crates/formality-prove/src/decls.rs

@@ -1,8 +1,9 @@
 use formality_core::{set, Set, Upcast};
 use formality_macros::term;
+use formality_types::grammar::Effect;
 use formality_types::grammar::{
-    AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc,
-    Wcs,
+    AdtId, AliasName, AliasTy, AtomicEffect, Binder, Parameter, Predicate, Relation, TraitId,
+    TraitRef, Ty, Wc, Wcs,
 };
 
 #[term]
@@ -153,8 +154,9 @@ pub enum Safety {
 /// It doesn't capture the trait items, which will be transformed into other sorts of rules.
 ///
 /// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`.
-#[term($?safety trait $id $binder)]
+#[term($?effect $?safety trait $id $binder)]
 pub struct TraitDecl {
+    pub effect: Effect,
     /// The name of the trait
     pub id: TraitId,
 
@@ -187,6 +189,7 @@ impl TraitDecl {
                     is_supertrait(self_var, binder.peek())
                 }
                 formality_types::grammar::WcData::Implies(_, c) => is_supertrait(self_var, c),
+                formality_types::grammar::WcData::EffectSubset(_, _) => todo!(),
             }
         }
 
@@ -197,7 +200,7 @@ impl TraitDecl {
                 binder: Binder::new(
                     &variables,
                     TraitInvariantBoundData {
-                        trait_ref: TraitRef::new(&self.id, &variables),
+                        trait_ref: TraitRef::new(AtomicEffect::Runtime, &self.id, &variables),
                         where_clause,
                     },
                 ),

crates/formality-prove/src/prove.rs

@@ -5,6 +5,7 @@ mod is_local;
 mod minimize;
 mod negation;
 mod prove_after;
+mod prove_effect_subset;
 mod prove_eq;
 mod prove_normalize;
 mod prove_via;