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

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)
  }
  }
  }

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);
+}

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);
+}