ICE: `elaborate_unused_args` panics when ZST local appears in START block liveness

[coord-e]

Summary

elaborate_unused_args in src/analyze/local_def.rs (around line 821–824) copies the refinement from a basic-block param whose type is non-unit (e.g. own int for a mutable ZST local) into a freshly-created unit()-typed placeholder param. The refinement contains Value (ν), but unit() is a singleton sort, so with_value_var sets value_var = None. When head(refinement_with_Value) is subsequently called, Instantiator::instantiate() hits value_var.clone().unwrap() and panics.

Root Cause

In elaborate_unused_args, when the current param is both the last param and corresponds to a non-argument local, the code does:

// src/analyze/local_def.rs ~821
params.push(rty::RefinedType::new(
    rty::Type::unit(),
    param_ty.refinement.clone(),  // ← refinement may contain Value (ν)
));

The refinement is taken verbatim from param_ty (which may have sort own int for a mutable ZST), then paired with Type::unit(). Later, with_value_var is called:

// src/rty/clause_builder.rs:27
let value_var = (!ty_sort.is_singleton()).then(|| self.add_var(ty_sort));

Because unit() is a singleton, value_var is None. When Instantiator::instantiate() maps RefinedTypeVar::Value, it calls value_var.clone().unwrap() and panics.

Trigger Condition

This is specific to ZST locals (e.g. struct Counter;) that appear in MaybeLiveLocals at START_BLOCK before any definition. ZST assignments are no-ops in MIR and do not kill liveness, so ZST variables remain live from block start. Non-ZST locals do not have this problem because their definition appears as a real MIR statement that kills liveness.

Reproducer

//@check-pass
//@compile-flags: -C debug-assertions=off

struct Counter;  // ZST

fn use_counter(c: Counter) -> Counter {
    let _x: Counter = c;
    _x
}

fn main() {
    let c = Counter;
    let _ = use_counter(c);
}

Or a variant that more directly triggers the mutable ZST path:

//@check-pass
//@compile-flags: -C debug-assertions=off

struct Token;  // ZST

fn take_token(mut t: Token) -> Token {
    t = Token;
    t
}

fn main() {
    let _ = take_token(Token);
}

Expected: analysis completes without panic.
Actual: ICE with called Option::unwrap() on a None value inside Instantiator::instantiate (src/rty.rs:1398), triggered from elaborate_unused_args → assert_entry → the subtyping/clause-building path.

Relevant Code

• src/analyze/local_def.rs:801 — elaborate_unused_args
• src/rty.rs:1388 — Instantiator::instantiate (the unwrap() site)
• src/rty/clause_builder.rs:25 — with_value_var (sets value_var = None for singletons)
• src/analyze/local_def.rs:693 — refine_basic_blocks / MaybeLiveLocals usage that produces the live-at-start ZST locals

Notes

There is already a // TODO: remove this comment on elaborate_unused_args, suggesting the function is known to be fragile. A short-term fix would be to not copy the refinement verbatim when constructing the unit() placeholder—using Refinement::top() (or otherwise stripping Value from the refinement) when the target type is a singleton sort. The deeper fix is to eliminate elaborate_unused_args entirely.