From b76f7fa82c3e433c0fe146b5771e58e79a6c369b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 02:44:23 +0000 Subject: [PATCH] Use the singleton value in place of a singleton-sorted variable `Env::dependencies` withholds a clause variable from a local whose sort is singleton, but `Env::var_type` still referred to such a local by name. Storing the local into an aggregate that also has a non-singleton field carried that name into the aggregate's term, and the aggregate does get a clause variable, so the reference reached clause construction and aborted there: `unbound var` in `ClauseBuilder::mapped_var` when the aggregate's `fn` field is called, or a missing substitution in `PrecondCapture::finish` when the aggregate is merely held across a basic-block boundary. A singleton sort has exactly one value, so name the value itself instead. The two test pairs differ in whether the `fn` field is called, which is what selects between the two consumers. The type of the null-sorted field does not: a `&str` field reaches the same `PrecondCapture` abort as an uncalled `fn` one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MyiZkfhBzL1EAqmDMLLN6Q --- src/refine/env.rs | 11 ++++++++++- tests/ui/fail/fn_ptr_tuple_field.rs | 12 ++++++++++++ tests/ui/pass/fn_ptr_tuple_field.rs | 12 ++++++++++++ 3 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/fn_ptr_tuple_field.rs create mode 100644 tests/ui/pass/fn_ptr_tuple_field.rs diff --git a/src/refine/env.rs b/src/refine/env.rs index f54ca15c..88397fa6 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -992,7 +992,16 @@ where } None => { let rty = self.var(var).expect("unbound var"); - PlaceType::with_ty_and_term(rty.ty.clone(), chc::Term::var(var)) + let sort = rty.ty.to_sort(); + // A variable of a singleton sort is not registered as a clause variable (see + // `dependencies`), so it must not be referred to by name. Such a sort has exactly + // one value, and that value stands for the variable instead. + let term = if sort.is_singleton() { + chc::Term::default_for(&sort) + } else { + chc::Term::var(var) + }; + PlaceType::with_ty_and_term(rty.ty.clone(), term) } } } diff --git a/tests/ui/fail/fn_ptr_tuple_field.rs b/tests/ui/fail/fn_ptr_tuple_field.rs new file mode 100644 index 00000000..1973dc1d --- /dev/null +++ b/tests/ui/fail/fn_ptr_tuple_field.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn add1(x: i64) -> i64 { + x + 1 +} + +fn main() { + let p: (fn(i64) -> i64, i64) = (add1, 3); + let a = (p.0)(p.1); + assert!(a == 3); +} diff --git a/tests/ui/pass/fn_ptr_tuple_field.rs b/tests/ui/pass/fn_ptr_tuple_field.rs new file mode 100644 index 00000000..0270f98e --- /dev/null +++ b/tests/ui/pass/fn_ptr_tuple_field.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn add1(x: i64) -> i64 { + x + 1 +} + +fn main() { + let p: (fn(i64) -> i64, i64) = (add1, 3); + let a = (p.0)(p.1); + assert!(a == 4); +}