Use the singleton value in place of a singleton-sorted variable

[coord-e]

Fixes #217.

Problem

Env::dependencies withholds a clause variable from a local whose sort is singleton — such a value carries no logical content, and the rest of the codebase assumes the same (Template::build, with_value_var, and From<PlaceType> for RefinedType all skip singleton sorts the same way).

Env::var_type, however, 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 survived into clause construction and aborted there, at either of two consumers:

• ClauseBuilder::mapped_var — unbound var _2
• PrecondCapture::finish — no entry found for key

Both Type::Function and Type::String lower to chc::Sort::Null, so a fn(..) pointer and a &str reproduce it alike; it is the mixture of a null-sorted field with a non-singleton one that triggers it, not the function pointer, the call, or the aggregate kind.

Fix

A singleton sort has exactly one value, so var_type names that value (chc::Term::default_for) instead of the variable. Nothing dangling reaches clause construction.

Test

One pass/fail pair, fn_ptr_tuple_field: a (fn(i64) -> i64, i64) tuple whose fn field is called.

This single program covers both panic sites. Verified on the base commit cd33fbf by suppressing the mapped_var panic — the same program then aborts in PrecondCapture::finish, so the call path and the block-boundary path are both exercised. A no-call variant, and a &str-instead-of-fn variant, were both tried and dropped: each reaches only PrecondCapture::finish, a strict subset, and neither can fail independently of this pair.

Verification

• Every row of the issue's behavior matrix checks safe, including all six previously-panicking rows. Breaking the asserted property in each still yields Unsat, so the fix does not paper over the check.
• Full UI suite green, locally and on CI. fmt, clippy, and test all pass.

tests/ui/fail/option_map.rs could not be run locally — it reports verification error: Timeout(30s) identically at the base commit cd33fbf and on this branch, because its pcsat solver runs under Docker in the dev container and cannot find the counterexample within the 30s solver timeout. CI has more headroom and runs it green, confirming it is unrelated to this change.

Out of scope

• dependencies filters singleton locals but not singleton temps; temps are always registered, which is why that path never hit this asymmetry.
• Type::Never also lowers to Sort::Null and is presumably covered by the same change, but no case was constructed to confirm it.

[Copilot]

Pull request overview

Fixes dangling references to singleton-sorted locals during CHC construction by substituting their canonical singleton value.

Changes:

• Use Term::default_for for singleton sorts in Env::var_type.
• Add paired UI tests covering successful and failing tuple verification.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/refine/env.rs	Replaces unregistered singleton variables with canonical values.
tests/ui/pass/fn_ptr_tuple_field.rs	Verifies the valid function-pointer tuple case.
tests/ui/fail/fn_ptr_tuple_field.rs	Confirms an invalid assertion remains unsatisfiable.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.