Infer implied outlives from fn signature

crates/formality-rust/src/check/fns.rs

@@ -1,6 +1,7 @@
 use crate::check::borrow_check::env::TypeckEnv;
 use crate::check::borrow_check::flow_state::FlowState;
 use crate::check::borrow_check::nll::borrow_check;
+use crate::check::implied_bounds::implied_bounds_from_fn;
 use crate::check::prove_goal;
 use crate::check::where_clauses::prove_where_clauses_well_formed;
 use crate::grammar::{CrateId, FnBody, MaybeFnBody, Relation, Wcs};
@@ -47,7 +48,8 @@ judgment_fn! {
         (
             (let (env, bound_data) = env.instantiate_universally(&f.binder))
             (let FnBoundData { input_args, output_ty, where_clauses, body } = bound_data)
-            (let assumptions: Wcs = (assumptions, where_clauses).to_wcs())
+            (implied_bounds_from_fn(input_args, output_ty) => implied_bounds)
+            (let assumptions: Wcs = (assumptions, where_clauses, implied_bounds).to_wcs())
             (prove_where_clauses_well_formed(program, env, assumptions, where_clauses) => ())
             (for_all(input_arg in input_args)
                 (prove_goal(program, env, assumptions, Relation::well_formed(&input_arg.ty)) => ()))

crates/formality-rust/src/check/implied_bounds.rs

@@ -0,0 +1,94 @@
+use crate::grammar::{InputArg, Parameter, RigidName, RigidTy, Ty, Wcs, WhereClause};
+use formality_core::{judgment_fn, Cons};
+
+judgment_fn! {
+    pub fn implied_bounds_from_fn(
+        args: Vec<InputArg>,
+        output: Ty,
+    ) => Wcs {
+        debug(args, output)
+
+        (
+            (implied_bounds_from_args(args) => args_wcs)
+            (implied_bounds_from_ty(output) => output_wcs)
+            ------------------------------------------------------------ ("bounds")
+            (implied_bounds_from_fn(args, output) => (args_wcs, output_wcs))
+        )
+    }
+
+}
+
+judgment_fn! {
+    fn implied_bounds_from_args(
+        tys: Vec<InputArg>
+    ) => Wcs {
+        debug(tys)
+
+        (
+            ((implied_bounds_from_ty(&arg.ty)) => head_wcs)
+            (implied_bounds_from_args(tail) => tail_wcs)
+            ------------------------------------------------------------ ("recurse args")
+            (implied_bounds_from_args(Cons(arg, tail)) => (head_wcs, tail_wcs))
+        )
+
+        (
+            ------------------------------------------------------------ ("nil")
+            (implied_bounds_from_args(()) => ())
+        )
+    }
+
+}
+
+judgment_fn! {
+    fn implied_bounds_from_ty(
+        ty: Ty,
+    ) => Wcs {
+        debug(ty)
+
+        (
+            (if let [Parameter::Lt(lt), inner] = &parameters[..])
+            (let wc = vec![WhereClause::outlives(inner, lt)])
+            (implied_bounds_from_params(vec![inner]) => inner_wcs)
+            ------------------------------------------------------------ ("inner ref")
+            (implied_bounds_from_ty(RigidTy { name: RigidName::Ref(_), parameters }, ) => (inner_wcs, wc))
+        )
+
+        (
+            (implied_bounds_from_params(parameters) => wcs)
+            ------------------------------------------------------------ ("inner T")
+            (implied_bounds_from_ty(RigidTy { name: _, parameters }) => wcs)
+        )
+
+        (
+            ------------------------------------------------------------ ("no bounds")
+            (implied_bounds_from_ty(ty) => ())
+        )
+    }
+
+}
+
+judgment_fn! {
+    fn implied_bounds_from_params(
+        param: Vec<Parameter>
+    ) => Wcs {
+        debug(param)
+
+        (
+            (implied_bounds_from_ty(ty) => head_wcs)
+            (implied_bounds_from_params(tail) => tail_wcs)
+            ------------------------------------------------------------ ("recurse ty param")
+            (implied_bounds_from_params(Cons(Parameter::Ty(ty), tail)) => (head_wcs, tail_wcs))
+        )
+
+        (
+            (implied_bounds_from_params(tail) => tail_wcs)
+            ------------------------------------------------------------ ("param not ty")
+            (implied_bounds_from_params(Cons(_, tail)) => tail_wcs)
+        )
+
+        (
+            ------------------------------------------------------------ ("nil")
+            (implied_bounds_from_params(_x) => ())
+        )
+    }
+}

crates/formality-rust/src/check/mod.rs

@@ -25,6 +25,7 @@ mod adts;
 mod coherence;
 mod core_crate;
 mod fns;
+mod implied_bounds;
 mod impls;
 mod traits;
 mod where_clauses;