Panic (`deref unbound var` / `borrowing unbound var`): `THRUST_ENUM_EXPANSION_DEPTH_LIMIT` truncates every binding form, not just enum unfolding, so a `&mut` two `enum` layers deep (`Result<Option<&mut T>, E>`) gets no flow binding and any use of it aborts the compiler

[coord-e]

Summary

Env::bind_impl (src/refine/env.rs:847) applies the THRUST_ENUM_EXPANSION_DEPTH_LIMIT cutoff to every binding form, while the depth counter is only ever incremented by bind_enum:

fn bind_impl(&mut self, var: Var, rty: rty::RefinedType<Var>, depth: usize) {
    if depth >= self.enum_expansion_depth_limit {
        self.bind_var(var, rty);          // <- no FlowBinding is recorded
        return;
    }
    match rty.ty {
        rty::Type::Pointer(ty) if ty.is_own() => self.bind_own(var, ty, rty.refinement, depth),
        rty::Type::Pointer(ty) if ty.is_mut() => self.bind_mut(var, ty, rty.refinement, depth),
        rty::Type::Tuple(ty) if !ty.is_unit() => self.bind_tuple(var, ty, rty.refinement, depth),
        rty::Type::Enum(ty) => self.bind_enum(var, ty, rty.refinement, depth + 1),
        _ => self.bind_var(var, rty),
    }
}

bind_var records the value as a single logical variable and installs no FlowBinding, so a &mut (or a Box, or a tuple/struct) that happens to sit at the cutoff depth loses the current/prophecy pair that Env::locate_place and Env::borrow_var navigate. The knob is documented as bounding the expansion of recursively defined enums, but because the cutoff gates bind_mut/bind_own/bind_tuple as well, its real effect is a cap on how many enum layers may sit above a &mut: with the default value 2 that cap is one.

Option<&mut T> therefore works and Result<Option<&mut T>, E> does not. Any use of the inner reference — writing through it, reading it, or merely binding it in a nested pattern — makes ReborrowVisitor::visit_operand insert a reborrow for the &mut-typed operand, and the ensuing lookup aborts the compiler at

• src/refine/env.rs:1037 — .expect("deref unbound var") in locate_place, or
• src/refine/env.rs:1014 — .expect("borrowing unbound var") in borrow_var (tuple/struct payloads).

The types involved are ordinary and not recursive, the programs are valid Rust that run correctly under rustc, and every one of them verifies — with the right answer in both directions — under THRUST_ENUM_EXPANSION_DEPTH_LIMIT=3. This is a mis-scoped depth cutoff, not an unsupported construct.

Minimal reproduction

No annotations, no closures, no recursion:

fn go(r: Result<Option<&mut i64>, i64>) {
    match r {
        Ok(Some(m)) => *m = 5,
        Ok(None) => {}
        Err(_) => {}
    }
}

fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false --edition 2021 min.rs
thread 'rustc' panicked at src/refine/env.rs:1037:55:
deref unbound var
...
   4: thrust::refine::env::Env<T>::locate_place
   5: thrust::refine::env::Env<T>::borrow_place
   6: thrust::analyze::basic_block::Analyzer::borrow_place_
   7: thrust::analyze::basic_block::visitor::reborrow::ReborrowVisitor::insert_reborrow
  15: thrust::analyze::basic_block::visitor::reborrow::ReborrowVisitor::visit_statement
  16: thrust::analyze::basic_block::Analyzer::analyze_statements

$ THRUST_ENUM_EXPANSION_DEPTH_LIMIT=3 \
    cargo run -q -- -Adead_code -C debug-assertions=false --edition 2021 min.rs && echo safe
safe

A whole program built on the same shape — an "entry"-style API handing out an optional mutable slot — behaves the same way:

struct Store { slot: i64 }
impl thrust_models::Model for Store { type Ty = Self; }

fn apply(r: Result<Option<&mut i64>, i64>, v: i64) -> bool {
    match r {
        Ok(Some(m)) => { *m = v; true }
        Ok(None) => false,
        Err(_) => false,
    }
}

fn main() {
    let mut s = Store { slot: 0 };
    let ok = apply(Ok(Some(&mut s.slot)), 7);
    assert!(ok);
    assert!(s.slot == 7);      // holds at run time
}

ICEs with deref unbound var at the default configuration; safe at THRUST_ENUM_EXPANSION_DEPTH_LIMIT=3, and Unsat there once s.slot == 7 is changed to s.slot == 8, so the verdict at the raised limit is a real one and not vacuity.

Every shape that puts a &mut two enum layers deep reproduces it

All of these ICE at the default limit and verify at 3:

// R1 — a local rather than a parameter
fn main() {
    let mut x = 0i64;
    {
        let r: Result<Option<&mut i64>, i64> = Ok(Some(&mut x));
        match r { Ok(Some(m)) => *m = 5, Ok(None) => {}, Err(_) => {} }
    }
    assert!(x == 5);
}

// R3 — Option<Option<&mut T>>
fn go(o: Option<Option<&mut i64>>) {
    match o { Some(Some(m)) => *m = 5, Some(None) => {}, None => {} }
}

// R4 — a user enum carrying an Option<&mut T>
enum Slot<'a> { Filled(Option<&'a mut i64>), Empty }
fn go(s: Slot) {
    match s { Slot::Filled(Some(m)) => *m = 5, Slot::Filled(None) => {}, Slot::Empty => {} }
}

// R5 — a struct in between (structs do not increment the counter)
struct W<'a> { o: Option<&'a mut i64> }
fn go(w: Option<W>) {
    match w { Some(W { o: Some(m) }) => *m = 5, Some(W { o: None }) => {}, None => {} }
}

// R10 — the reference is only *read*, never written
fn go(r: Result<Option<&mut i64>, i64>) {
    match r { Ok(Some(m)) => { let _v = *m; }, Ok(None) => {}, Err(_) => {} }
}

// R12 — a tuple payload, reached through `&mut`; panics with "borrowing unbound var"
fn go(o: &mut Option<Option<(i64, i64)>>) {
    if let Some(Some(t)) = o { t.0 = 5; }
}

Behaviour matrix

All with -Adead_code -C debug-assertions=false --edition 2021, varying only THRUST_ENUM_EXPANSION_DEPTH_LIMIT (default 2):

program	1	2 (default)	3	4
Option<&mut T>, one enum layer	ICE	safe ✔	safe ✔	safe ✔
Result<Option<&mut T>, E>, two layers	ICE	ICE	safe ✔	safe ✔
Option<Option<Option<&mut T>>>, three layers	ICE	ICE	ICE	safe ✔
&mut Option<(i64, i64)>, one layer	ICE	safe ✔	safe ✔	safe ✔
&mut Option<Option<(i64, i64)>>, two layers	ICE	ICE	safe ✔	safe ✔

The rule is exactly limit > (number of enum layers above the reference). Nothing else about the programs changes.

The failure does not depend on the optimization level — deref unbound var at every one of 0, 1, 2, 3, s, z — and the same shape without a &mut in it (Result<Option<i64>, E>, Option<Option<Option<i64>>>, Option<Option<Box<i64>>>) is analyzed correctly at the default limit, so plain data is not affected.

Root cause

For fn go(r: Result<Option<&mut i64>, i64>) the parameter is bound as own Result<Option<&mut int>, int>, and bind_impl descends:

step	call	depth
parameter	bind_own(_1, …)	0
Result<…>	bind_enum(c, …)	0 → 1
Ok's field, Box<Option<&mut i64>>	bind_own(x, …)	1
Option<&mut i64>	bind_enum(y, …)	1 → 2
Some's field, Box<&mut i64>	bind_impl(z, …, 2) → 2 >= 2, so bind_var	2

RUST_LOG=thrust=debug shows the inner enum still being expanded (matcher_pred<std.option.Option<mut int>> t5 e0 ∧ t4 = discriminant(e0)) while its field t5 gets no FlowBinding.

The MIR of the match arm is a single statement:

_4 = move ((((_1 as Ok).0: std::option::Option<&mut i64>) as Some).0: &mut i64);
(*_4) = const 5_i64;

ReborrowVisitor::visit_operand fires on the &mut i64-typed operand and calls insert_reborrow on its dereference, which reaches Env::locate_place. Walking the elaborated place, the Deref step that unboxes Some's field looks up flow_binding(t5), finds None, and

var = match (elem, self.flow_binding(var).expect("deref unbound var")) {

aborts the compiler. When the payload is a tuple/struct instead of a bare reference the same missing binding surfaces one frame later, in borrow_var's .expect("borrowing unbound var").

Since bind_own/bind_mut/bind_tuple recurse with an unchanged depth, only enum nesting can drive depth up — so the cutoff can never be needed to break a Box/&mut/tuple chain, and gating those three on it only truncates finite structure.

Confirmed by experiment

Restricting the cutoff to the arm whose recursion actually increments it:

     fn bind_impl(&mut self, var: Var, rty: rty::RefinedType<Var>, depth: usize) {
-        if depth >= self.enum_expansion_depth_limit {
-            self.bind_var(var, rty);
-            return;
-        }
         match rty.ty {
             rty::Type::Pointer(ty) if ty.is_own() => self.bind_own(var, ty, rty.refinement, depth),
             rty::Type::Pointer(ty) if ty.is_mut() => self.bind_mut(var, ty, rty.refinement, depth),
             rty::Type::Tuple(ty) if !ty.is_unit() => {
                 self.bind_tuple(var, ty, rty.refinement, depth)
             }
-            rty::Type::Enum(ty) => self.bind_enum(var, ty, rty.refinement, depth + 1),
-            _ => self.bind_var(var, rty),
+            rty::Type::Enum(ty) if depth < self.enum_expansion_depth_limit => {
+                self.bind_enum(var, ty, rty.refinement, depth + 1)
+            }
+            ty => self.bind_var(var, rty::RefinedType::new(ty, rty.refinement)),
         }
     }

makes every two-layer reproducer above verify at the default limit, with the negated assertions still Unsat, and leaves the UI suite byte-identical: running all 152 tests/ui/pass and 148 tests/ui/fail files that do not need the pcsat wrapper gives exactly the same 152 safe / 148 Unsat before and after.

This is offered as evidence for the diagnosis rather than as a proposed patch. It does not make the knob harmless — with three enum layers the innermost enum is itself left unexpanded, and projecting into it panics the same way (row 3 of the matrix stays ICE). Reaching the limit currently produces an environment that cannot answer questions later asked of it; a real fix probably wants the limit to be driven by actual type recursion (or to report a diagnostic when a still-needed projection has been truncated) rather than by a global nesting counter.

Raising the default is also not obviously disruptive: sweeping all of tests/ui/pass and tests/ui/fail at THRUST_ENUM_EXPANSION_DEPTH_LIMIT=2 and =4 produces identical verdicts for every test, so no existing test exercises the knob at all.

Workaround

Peeling the layers one at a time rebinds the intermediate value into a fresh local, which is bound at depth 0 again, so this is accepted at the default limit:

fn go(r: Result<Option<&mut i64>, i64>) {
    if let Ok(o) = r {              // `o` is a fresh local, re-bound at depth 0
        if let Some(m) = o { *m = 5; }
    }
}

The nested-pattern spelling (if let Ok(Some(m)) = r) is the one that fails, which makes the failure look arbitrary from the outside.

Distinct from existing issues

• Panic: "borrowing unbound var" when writing through a reassigned &mut local #176 (borrowing unbound var when writing through a reassigned &mut local) shares one of the two panic messages but not the cause: its reproducer has no enums and is completely insensitive to THRUST_ENUM_EXPANSION_DEPTH_LIMIT (still borrowing unbound var at 2, 4 and 8), while every reproducer here disappears at 3.
• Stack overflow (non-termination) in TypeBuilder::build: a struct is always expanded structurally with no cycle cut, so any struct that reaches itself (struct Node { next: Option<Box<Node>> }, struct Tree { kids: Vec<Tree> }) aborts the compiler #249 / Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 are non-termination on recursive ADTs; nothing here is recursive, and these abort with a panic in Env, not a stack overflow.
• 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 #235 (a generic-enum parameter that is not the last one) is fixed on main; these reproducers fail with a single parameter, and in main with no parameters at all.
• Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121 / Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122 / Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177 / Unsound: moving a &mut-capturing closure out of any aggregate (incl. enum/Option), with no higher-order call, drops its prophecy and verifies panicking programs as safe (generalizes #177) #207 are about a &mut whose prophecy is resolved twice after a move out of an aggregate; they produce a wrong safe, not a panic, and are unaffected by the knob.
• Incompleteness: a &mut stored in a Vec (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as Unsat #202 (a &mut stored in a Vec) and Incompleteness: dropping a recursively-defined ADT does not resolve &mut prophecies stored in its recursive-position field, so safe programs are wrongly rejected #173 (a &mut in a recursive ADT's recursive field) concern containers that are never expanded at all; here the container is an ordinary two-level enum that is expanded one level too few.
• Incompleteness: a refinement on a generic type argument in #[param] position is dropped for multi-variant enums, so the payload refinement is never assumed in the callee #193 and Implicit derefs (rustc adjustments) are dropped in annotation translation, so any v.len()/v.length/s.0 on a &mut parameter builds an ill-sorted term and ICEs — only the explicit (*v) spelling works #239 are annotation-translation issues; these programs carry no annotations.
• Not a numeric-range/overflow issue: the only values are 0, 5 and 7.

Environment

• main @ 35eea46
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (the version pinned by .github/actions/setup-z3), default solver configuration