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