Panic `assert_closed`: "unexpected variable" — a generic-enum parameter (`Option<T>`/`Result<T, E>`, or an aggregate containing one) that is not the last parameter makes any branching body ICE

[coord-e]

Summary

Any function that (a) takes a parameter whose model type contains a generic enum (Option<T>, Result<T, E>, a user enum Foo<T>, or a struct/Vec with such a field), (b) has at least one parameter after it, and (c) whose body branches (if, match, while — anything that produces a basic block with in-degree ≥ 2), aborts the compiler with

thread 'rustc' panicked at src/rty.rs:1188:27:
unexpected variable

This is not an unimplemented! on an unsupported construct: every ingredient is supported on its own, and simply reordering the parameters so the generic enum comes last makes the same program verify. The panic is an internal invariant violation — rty::Type::assert_closed is called on a BasicBlockType parameter type that the template builder deliberately left open.

The pattern is about as common as Rust code gets: fn get_or(o: Option<i64>, d: i64), fn handle(r: Result<T, E>, ctx: &Ctx), and every &self method on a struct that has an Option/Result field (self is a parameter and is never last when the method takes any argument).

Minimal reproduction

repro.rs — the Option is not even used; only its position in the signature and the presence of a branch matter:

fn f(o: Option<i64>, d: i64) -> i64 {
 if d > 0 { 1 } else { 2 }
}

fn main() {
 assert!(f(Some(1), 2) == 1);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs

thread 'rustc' (10399) panicked at src/rty.rs:1188:27:
unexpected variable
stack backtrace:
 2: thrust::rty::Type<T>::assert_closed::{{closure}}
 at ./src/rty.rs:1188:27
 ...
 38: thrust::rty::RefinedType<FV>::map_var
 39: thrust::rty::EnumType<T>::map_var::{{closure}}
 50: thrust::rty::EnumType<T>::map_var
 51: thrust::rty::Type<T>::map_var
 52: thrust::rty::Type<T>::assert_closed
 53: thrust::analyze::basic_block::Analyzer::type_goto::{{closure}}
 69: thrust::analyze::basic_block::Analyzer::type_goto
 70: thrust::analyze::basic_block::Analyzer::analyze_terminator_goto
 71: thrust::analyze::basic_block::Analyzer::run

The program is ordinary Rust and runs cleanly under plain rustc:

$ rustc -Adead_code --edition 2021 -o repro repro.rs && ./repro ; echo "exit=$?"
exit=0

A realistic version of the same thing — a hand-written unwrap_or — is equally fatal:

fn get_or(o: Option<i64>, d: i64) -> i64 {
 match o { Some(x) => x, None => d }
}

fn main() { assert!(get_or(Some(1), 9) == 1); }

Isolation

Every row is the same shape (fn f(<first param>, d: i64) -> i64 { if d > 0 { 1 } else { 2 } }) unless noted, so only the marked ingredient varies.

#	First parameter / variation	Verdict
1	o: Option<i64>	ICE	❌ bug
2	parameters swapped: fn f(d: i64, o: Option<i64>)	safe	✅ (enum is last)
3	only parameter: fn f(o: Option<i64>) -> i64 { if o.is_some() { 1 } else { 2 } }	safe	✅ (enum is last)
4	o: Option<i64> but no branch: fn f(o: Option<i64>, d: i64) -> i64 { d }	safe	✅
5	non-generic enum first: enum E { A(i64), B }, e: E	safe	✅
6	plain struct first: struct S { a: i64, b: i64 }, s: S	safe	✅
7	v: Vec<i64>	safe	✅
8	h: &H where struct H { o: Option<i64> }	ICE	❌ bug
9	r: Result<i64, i64>	ICE	❌ bug
10	fn get_or(o: Option<i64>, d: i64) + match (above)	ICE	❌ bug
11	v: Vec<Option<i64>>	ICE	❌ bug
12	o: Option<i64>, branch is a while loop instead of if	ICE	❌ bug
13	user generic enum: enum My<T> { Yes(T), No }, m: My<i64>	ICE	❌ bug

So the trigger is exactly: a non-last parameter whose rty::Type contains an EnumType with type arguments, in a body that has a basic block needing its own precondition. Rows 5–7 show it is specific to generic enums (a non-generic enum has no type arguments, and Tuple/Array/Pointer never carry a template refinement), and rows 2–3 show the fix is only ever "put it last", which is not available for &self methods.

Root cause

TemplateTypeBuilder::build (src/refine/template.rs:417-421) is the only branch that installs a refinement inside the type it returns — enum type arguments are built with build_refined, which registers a template predicate over the builder's current scope:

if def.is_enum() {
 let sym = refine::datatype_symbol(self.inner.tcx, def.did());
 let args: IndexVec<_, _> =
 params.types().map(|ty| self.build_refined(ty)).collect(); // <- scoped template
 rty::EnumType::new(sym, args).into()
} else if def.is_struct() {
 ... rty::PointerType::own(self.build(ty)).into() ... // <- no refinement
}

So build(ty) returns a Type<Var> that is open (mentions the scope's FunctionParamIdxs) exactly when ty contains a generic enum and the scope is non-empty.

FunctionTemplateTypeBuilder::build (src/refine/template.rs:606-632) then builds a non-last parameter as:

} else if self.param_refinement.is_some() {
 rty::RefinedType::unrefined(self.inner.build(param_ty.ty).vacuous()) // closed
} else {
 rty::RefinedType::unrefined(
 self.inner
 .for_template(self.registry)
 .with_scope(&builder) // <- scope leaks into the enum's type arguments
 .build(param_ty.ty),
 )
}

The two arms are inconsistent: on the user-invariant path (param_refinement.is_some()) the non-last parameter type is closed, but on the inference path it is scoped and therefore open. The last parameter is unaffected because it goes through build_refined, which internally builds the type with for_template(self.registry) and no with_scope before .vacuous().

BasicBlockType::params is live_locals ++ body.args (build_basic_block_with_precondition, src/refine/template.rs:451-495), so every function argument except the last one takes the open branch. analyze::basic_block::Analyzer::type_goto then does

BasicBlockTypeParamKind::OuterFnParam(outer_idx) => {
 let pty = PlaceType::with_ty_and_term(
 rty.ty.clone().assert_closed().vacuous(), // src/analyze/basic_block.rs:774
 chc::Term::var(outer_fn_param_var),
 );

and assert_closed (src/rty.rs:1187-1189) is map_var(|_v| panic!("unexpected variable")). Reaching type_goto's OuterFnParam arm requires a target block that needs_own_precondition, which is why a branch is needed — a straight-line body (row 4) never gets there. install_inherited_bb_ty (src/analyze/basic_block.rs:809) has the same assert_closed call and the same exposure.

Candidate fix (verified locally)

Making the inference arm build the non-last parameter's type the way build_refined does — without leaking the scope into nested type arguments — removes the ICE:

 } else {
 rty::RefinedType::unrefined(
 self.inner
 .for_template(self.registry)
- .with_scope(&builder)
- .build(param_ty.ty),
+ .build(param_ty.ty)
+ .vacuous(),
 )
 }

With that one-line change all 13 rows above verify as safe, and the checking is still sound on this shape:

assert!(get_or(Some(1), 9) == 9) -> Unsat (correctly rejected)
assert!(get_or(None, 9) == 1) -> Unsat (correctly rejected)
assert!(f(Some(1), 2) == 2) -> Unsat (correctly rejected)

Spot-checked tests/ui/pass/{adt_mut,option_mut,option_loop,result_mut,gcd,take_max,loop_invariant,vec_2,annot_enum_simple,fn_poly_annot,closure_mut}.rs still pass and tests/ui/fail/{adt_mut,option_mut,gcd}.rs are still rejected. This is offered only as evidence for the diagnosis — whether the right repair is to drop the scope here, or instead to stop calling assert_closed in type_goto/install_inherited_bb_ty and carry the enum-argument templates through the basic-block parameter properly, is a design call: dropping the scope also removes any dependency of an Option payload's refinement on earlier parameters.

Relation to existing issues

Distinct from every open panic report: #176 is "borrowing unbound var" on a reassigned &mut; #140 is unimplemented!(unrefined_ty: FnDef(..)); #178 is a stack overflow on recursive ADTs; #116/#113 are unwraps on constants and solver env vars. It is also unrelated to the enum-modelling issues #126/#193 (both need annotations or explicit discriminants) — this one fires on a completely unannotated program and does not depend on the enum's contents at all.

Environment

• thrust @ 2ab5271
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration