Bug: `Rvalue::Aggregate` for a newtype struct ignores `Model::Ty`, causing call-site sort mismatch

[coord-e]

Minimal Repro

struct Counter(i32);

impl thrust_models::Model for Counter {
    type Ty = thrust_models::model::Int;
}

impl Counter {
    fn increment(&mut self) {}

    #[thrust::formula_fn]
    fn _thrust_requires_increment(_s: thrust_models::model::Mut<thrust_models::model::Int>) -> bool {
        true
    }

    #[thrust::formula_fn]
    fn _thrust_ensures_increment(_r: (), _s: thrust_models::model::Mut<thrust_models::model::Int>) -> bool {
        true
    }

    #[thrust::extern_spec_fn]
    #[allow(path_statements)]
    fn _thrust_extern_spec_increment(&mut self) {
        #[thrust::requires_path]
        Self::_thrust_requires_increment;
        #[thrust::ensures_path]
        Self::_thrust_ensures_increment;
        Self::increment(self)
    }
}

fn main() {
    let mut c = Counter(0);
    c.increment();
}

Panic

inconsistent types: got=(own int,), expected=int

(in relate_fn_sub_type / relate_sub_type)

Root Cause

The bug is in rvalue_type in src/analyze/basic_block.rs. When processing Rvalue::Aggregate for a struct, it collects the field types and wraps them in a TupleType — without calling resolve_model_ty:

// basic_block.rs, Rvalue::Aggregate arm, struct branch:
_ => PlaceType::tuple(field_tys),  // Counter(i32) → (own int,)

The TypeBuilder::build and TemplateTypeBuilder::build paths (used for local declarations, function signatures, and def_ty_with_args) both call resolve_model_ty first. They correctly normalize Counter → <Counter as Model>::Ty = Int → rty::Type::int(). But the aggregate path skips this.

Step-by-step trace for let mut c = Counter(0); c.increment()

1. c = Counter(0) is a new binding (analyze_assignment, definition path):

   • rvalue_refined_type(Counter(0)) → rvalue_type(Aggregate(Counter, [0i32])) → collects field 0i32 as own(int) → returns PlaceType with type (own int,).
   • bind_local(c, (own int,)): since c is a mutable local, wraps it → stores c: own (own int,) in the env.

2. Call c.increment():

   • The argument is &mut c. mutable_borrow(c) borrows the value behind c's pointer. The value type is (own int,), so the borrow type is Mut<(own int,)>.
   • def_ty_with_args(Counter::increment) builds the expected type for self: resolve_model_ty(&mut Counter) → <&mut Counter as Model>::Ty = Mut<Int> → expected type Mut<int>.
   • relate_fn_sub_type: got = Mut<(own int,)>, expected = Mut<int>. Sorts (own int,) and int are incompatible → panic.

Why the existing tests don't catch this

The annot_mut_receiver-style tests use struct Counter; (a ZST). A ZST struct has no fields, so its TupleType is () — a singleton sort. Singleton sorts are skipped throughout the refinement logic (e.g., is_singleton() checks). Also, those tests have an empty main, so no call site is ever checked. Both of these together hide the bug.

Fix Direction

In rvalue_type in src/analyze/basic_block.rs, the Rvalue::Aggregate arm for structs should call self.type_builder.build(adt_ty) (which goes through resolve_model_ty) to get the refined type for the struct value, instead of directly constructing a TupleType from its fields. When the struct has a Model impl, the model type should be used — and the field values matched against that model type rather than exposed as a raw tuple.

The same issue likely applies to any place where PlaceType::tuple is used for a user-defined ADT with a Model impl.