Fn output fix (#2477)

Author: parno

source/rust_verify_test/tests/fndef_types.rs

@@ -2006,5 +2006,34 @@ test_verify_one_file_with_options! {
             y.touch();
             assert(y.index() == y.seq().len());
         }
+
+
+        // Module `a` defines a struct with restricted visibility and a
+        // function whose signature mentions it. The function is used as an
+        // FnDef value, so Verus emits an auto-generated
+        // `<FnDef(takes_hidden) as FnOnce<(Hidden,)>>::Output = Hidden`
+        // AssocTypeImpl referencing `Hidden`.
+        mod a {
+            mod inner {
+                pub(super) struct Hidden { pub x: u32 }
+            }
+
+            fn takes_hidden(h: inner::Hidden) -> inner::Hidden { h }
+
+            fn use_as_fndef() {
+                let _f = takes_hidden;
+            }
+        }
+
+        // Module `b` cannot see `Hidden`.
+        // `b`'s code reaches the `FnOnce::Output` associated-type decl via
+        // the `F::Output` projection inside the `HasItem for Ad<F>` impl.
+        mod b {
+            fn foo(x: u32) -> u32 { x }
+
+            fn use_fn() {
+                let _y = crate::W { i: crate::Ad(foo) };
+            }
+        }
     } => Ok(())
 }

source/vir/src/ast_simplify.rs

@@ -1044,11 +1044,9 @@ fn add_fndef_axioms_to_function(
     let (trait_impls_out, assoc_type_impl) = if fn_once_trait_in_scope {
         let self_typ = Arc::new(TypX::FnDef(fun.clone(), typ_args.clone(), None));
         let arg_typs: Vec<Typ> = params.iter().map(|p| p.a.clone()).collect();
-        let args_tuple_typ = Arc::new(TypX::Datatype(
-            Dt::Tuple(arg_typs.len()),
-            Arc::new(arg_typs),
-            Arc::new(vec![]),
-        ));
+        let tuple_dt = state.tuple_type_name(arg_typs.len());
+        let args_tuple_typ =
+            Arc::new(TypX::Datatype(tuple_dt, Arc::new(arg_typs), Arc::new(vec![])));
         let trait_typ_args = Arc::new(vec![self_typ, args_tuple_typ]);
 
         let mk_impl_path = |kind: ClosureKind| {

source/vir/src/prune.rs

@@ -35,6 +35,7 @@ enum ReachedType {
     Float(u32),
     SpecFn(usize),
     Datatype(Dt),
+    FnDef(Fun, Vec<ReachedType>),
     StrSlice,
     Array,
     Primitive,
@@ -131,7 +132,9 @@ fn typ_to_reached_type(typ: &Typ) -> ReachedType {
         TypX::AnonymousClosure(..) => ReachedType::None,
         TypX::Datatype(dt, _, _) => ReachedType::Datatype(dt.clone()),
         TypX::Dyn(..) => ReachedType::None,
-        TypX::FnDef(..) => ReachedType::None,
+        TypX::FnDef(fun, typs, _) => {
+            ReachedType::FnDef(fun.clone(), typs.iter().map(typ_to_reached_type).collect())
+        }
         TypX::Decorate(_, _, t) => typ_to_reached_type(t),
         TypX::Boxed(t) => typ_to_reached_type(t),
         TypX::TypParam(_) => ReachedType::None,
@@ -309,9 +312,11 @@ fn reach_typ(ctxt: &Ctxt, state: &mut State, typ: &Typ) {
             reach_assoc_type_decl(ctxt, state, &(trait_path.clone(), name.clone()));
             // let visitor handle self_typ, trait_typ_args
         }
-        TypX::FnDef(fun, _typs, res_fun_opt) => {
+        TypX::FnDef(fun, typs, res_fun_opt) => {
             state.fndef_types.insert(fun.clone());
             reach_function(ctxt, state, fun);
+            let typ_args: Vec<ReachedType> = typs.iter().map(typ_to_reached_type).collect();
+            reach_type(ctxt, state, &ReachedType::FnDef(fun.clone(), typ_args));
 
             if let Some(res_fun) = res_fun_opt {
                 state.fndef_types.insert(res_fun.clone());