Fix unsoundness when expanding variant of polymorphic enum

[coord-e]

unsoundness found in #17:

enum X<T> {
    None1,
    None2,
    Some(T),
}

fn main() {
    let mut opt: X<i32> = X::None1;
    opt = X::None2;
    assert!(matches!(opt, X::None1));
}

When typing opt = X::None1, Thrust allocates new predicate variable (call it p_1 here) for X<{ i32 | p_1 v }>. During the expansion of X::None1: X<{ i32 | p_1 v }>, we have an i32 implicit variable (call it t_1) for Some variant to be an argument of matcher_pred. The problem here is that t_1: { i32 | p_1 v } is bound to the environment without any constraint, enabling p_1 to be inferred to false to satisfy the entire clauses. This PR introduces a guard to t_1 refinement, making t_1: { i32 | t_d == discr(Some) => p_1 v } (t_d is an implicit variable for the discriminant) to prevent p_1 to be available regardless of the current variant.

[Copilot]

Pull request overview

This PR fixes an unsoundness issue in the refinement type checker when expanding variants of polymorphic enums. The bug allowed incorrect assertions to pass when assigning one variant and checking for another variant of the same enum.

Key Changes:

• Introduced guard support to CHC atoms to conditionally apply predicates
• Modified enum variant expansion to guard field type refinements with discriminant checks
• Added comprehensive test cases to verify the fix

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/ui/pass/adt_variant_without_params.rs	Test case verifying that correct variant matching passes
tests/ui/fail/adt_variant_without_params.rs	Test case verifying that incorrect variant matching fails (regression test for the bug)
src/rty.rs	Added guarded methods to Formula and RefinedType for conditional refinements
src/refine/env.rs	Core fix: guards enum field types with discriminant checks to prevent unsound predicate inference
src/chc.rs	Extended Atom structure with optional guard field and implemented guard composition logic
src/chc/unbox.rs	Updated unboxing transformation to preserve guards
src/chc/smtlib2.rs	Updated SMT-LIB2 formatting to emit implication for guarded atoms

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.