Incompleteness: `Box<T>` (`Own`) is related invariantly in subtyping, wrongly rejecting valid refinement weakening through a box

[coord-e]

Summary

In relate_sub_type, an owned pointer (Box<T>, PointerKind::Own) is grouped together with &mut T and related invariantly, whereas a shared reference &T (PointerKind::Ref(RefKind::Immut)) is related covariantly. Because a Box<T> is alias-free and — in this codebase — has an encoding identical to &T (a current-value-only "box", with no prophecy/final component), covariant refinement subtyping is sound for it, exactly as for &T. Forcing invariance additionally emits the reverse subtyping obligation, which wrongly rejects valid programs that weaken a refinement through a Box.

This is an incompleteness (false-rejection) bug, not an unsoundness. It is also internally inconsistent: Own is treated the same as Ref(Immut) everywhere else in the type machinery, and only diverges here.

Location

src/rty/subtyping.rs:91-101:

(Type::Pointer(got), Type::Pointer(expected)) if got.kind == expected.kind => {
    match got.kind {
        PointerKind::Ref(RefKind::Immut) => {
            let cs = self.relate_sub_refined_type(&got.elem, &expected.elem);   // covariant
            clauses.extend(cs);
        }
        PointerKind::Own | PointerKind::Ref(RefKind::Mut) => {
            let cs = self.relate_equal_refined_type(&got.elem, &expected.elem); // INVARIANT
            clauses.extend(cs);
        }
    }
}

relate_equal_refined_type (src/rty/subtyping.rs:157-171) emits subtyping in both directions:

let mut clauses = self.relate_sub_refined_type(got, expected);
clauses.extend(self.relate_sub_refined_type(expected, got)); // the spurious obligation

Why this is wrong

Own and Ref(Immut) have an identical CHC representation and dereference semantics; only Ref(Mut) differs:

• Type::to_sort — src/rty.rs:1116: PointerKind::Ref(RefKind::Immut) | PointerKind::Own => chc::Sort::box_(elem_sort), while Ref(Mut) => chc::Sort::mut_(elem_sort).
• PointerKind::deref_term — src/rty.rs:458: PointerKind::Own | PointerKind::Ref(RefKind::Immut) => term.box_current(), while Ref(Mut) => term.mut_current().
• Binding — Env::bind_own (src/refine/env.rs:624-651) installs FlowBinding::Box(current), which carries only a current value. By contrast bind_mut (src/refine/env.rs:653-689) installs FlowBinding::Mut(current, final_) with a separate prophecy/final value.

The reason &mut T must be invariant is precisely its prophecy/final component (the mut_ sort) and the fact that the borrow and its origin coexist. A Box<T> has neither: it is owned, unique (no aliasing), and has no final value. Ownership transfers on coercion, so the source's stronger refinement is consumed and cannot be relied upon afterward. Weakening (covariance) is therefore sound — the same justification that already makes &T covariant one arm above.

So the variance of Own is inconsistent with how Own is treated in every other part of the type system, and the inconsistency is what produces the false rejections.

Concrete trigger

A safe program that should verify but is rejected because the invariant path additionally demands the (false) reverse implication:

#[thrust_macros::requires(*x > 0)]
fn consume(x: Box<i64>) {}

#[thrust::callable]
fn caller() {
    let b: Box<i64> = Box::new(5); // b : Box<{ v: i64 | v == 5 }>
    consume(b);                    // requires Box<{v == 5}> <: Box<{v > 0}>
}

Passing b to consume requires Box<{v == 5}> <: Box<{v > 0}>.

• Covariant (correct): generates only {v == 5} ⟹ {v > 0} — holds.
• Invariant (current behavior): also generates {v > 0} ⟹ {v == 5} — false — so the obligation is Unsat and Thrust rejects a clearly safe program.

The analogous shared-reference version (fn consume(x: &i64) with *x > 0, passing &5) verifies, demonstrating the inconsistency directly.

Suggested fix

Move Own into the covariant arm alongside Ref(RefKind::Immut):

match got.kind {
    PointerKind::Ref(RefKind::Immut) | PointerKind::Own => {
        let cs = self.relate_sub_refined_type(&got.elem, &expected.elem); // covariant
        clauses.extend(cs);
    }
    PointerKind::Ref(RefKind::Mut) => {
        let cs = self.relate_equal_refined_type(&got.elem, &expected.elem); // invariant
        clauses.extend(cs);
    }
}

This restores consistency with to_sort / deref_term / bind_own, all of which already treat Own like Ref(Immut).

Notes

• Found by static analysis / code reading; I was not able to run the UI tests in this environment (Z3 not installed), so the concrete trigger above is reasoned rather than executed. A tests/ui/pass case mirroring the snippet would confirm the fix.
• If the invariance was an intentional conservative choice, it would still be worth documenting why Box cannot be covariant despite sharing &T's representation, since the current grouping reads as an oversight.