Panic `unimplemented!(unrefined_ty: FnDef(..))` when passing a named function (function item) to a higher-order function

[coord-e]

Summary

Passing a named function (a function item, whose type is TyKind::FnDef) as the argument to a generic Fn-bounded parameter makes Thrust panic with not implemented: unrefined_ty: FnDef(..). The crash happens during type-template construction, before any solving, and aborts verification of the whole crate.

TemplateTypeBuilder::build (src/refine/template.rs:206) handles function pointers (TyKind::FnPtr, line 225) and closures (via closure_model, line 197), but has no arm for TyKind::FnDef, so the type of the generic parameter — once it has been instantiated with a concrete function item — falls through to the catch-all unimplemented!() at src/refine/template.rs:261.

This is ordinary, idiomatic Rust (e.g. apply(helper, x), opt.map(my_fn)), and the same shape works for closures and for fn(..) pointers, so the gap is specifically the FnDef → generic Fn path.

Reproduction (minimal, no annotations)

fn id(r: i32) -> i32 { r }
fn apply<F: Fn(i32) -> i32>(f: F, a: i32) -> i32 { f(a) }
fn main() { let _ = apply(id, 5); }

This is valid Rust and runs fine under plain rustc. Thrust panics:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' panicked at src/refine/template.rs:261:21:
not implemented: unrefined_ty: FnDef(DefId(0:3 ~ repro[851a]::id), [])

No requires/ensures/param/ret annotation is involved; main need only construct the call.

What works vs. what panics

case	code	result
direct call	id(5)	ok
bind item to local, call directly	let f = id; f(5)	ok
named fn item → generic Fn param	apply::<_>(id, 5) where F: Fn(i32)->i32	panic
closure literal → generic Fn param	apply(|y| y + 1, 5)	ok (closures handled via closure_model)
named fn item → fn(i32)->i32 pointer param	fn apply(f: fn(i32)->i32, a: i32); apply(id, 5)	ok (handled by the FnPtr arm)

So the trigger is precisely: a FnDef type reaching TemplateTypeBuilder::build as (the instantiation of) a generic function-typed parameter.

Root cause

src/refine/template.rs:206-262, TemplateTypeBuilder::build:

pub fn build(&self, ty: mir_ty::Ty<'tcx>) -> rty::Type<rty::Closed> {
    let ty = self.resolve_model_ty(ty);
    match ty.kind() {
        mir_ty::TyKind::Bool => rty::Type::bool(),
        ...
        mir_ty::TyKind::FnPtr(sig_tys, hdr) => {            // function POINTERS handled
            let sig = sig_tys.with(*hdr).skip_binder();
            let params = sig.inputs().iter()
                .map(|ty| rty::RefinedType::unrefined(self.build(*ty)).vacuous())
                .collect();
            let ret = rty::RefinedType::unrefined(self.build(sig.output()));
            rty::FunctionType::new(params, ret.vacuous()).into()
        }
        mir_ty::TyKind::Adt(def, params) => { ... }        // closures handled via model_adt/closure_model
        kind => unimplemented!("unrefined_ty: {:?}", kind), // <-- FnDef lands here (line 261)
    }
}

When apply is analyzed/instantiated with F = FnDef(id), building the type of the parameter f: F calls build on the FnDef type. There is no TyKind::FnDef arm, so it hits the catch-all and panics.

A FnDef carries the same information needed to build a rty::FunctionType as the existing FnPtr arm: its signature is available via tcx.fn_sig(def_id).instantiate(tcx, args). The FnDef case can be handled analogously to FnPtr (a function item coerces to a function pointer of its signature), or — to track the callee precisely — resolved to that specific function's refined signature.

Suggested direction

Add a TyKind::FnDef(def_id, args) arm to TemplateTypeBuilder::build (and to the sibling builder referenced by the // TODO: consolidate two impls note at template.rs:205) that obtains the instantiated signature and constructs a rty::FunctionType, mirroring the FnPtr arm. At minimum, the unhandled case should produce a graceful "unsupported" diagnostic rather than an ICE-style panic.

Environment

• thrust @ 8a269d8
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 4.16.0, default solver configuration