diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml
index 85151f1cf..48ddc2e18 100644
--- a/src/sail_coq_backend/pretty_print_coq.ml
+++ b/src/sail_coq_backend/pretty_print_coq.ml
@@ -1881,6 +1881,10 @@ let doc_exp, doc_let =
                         );
                     underscore
                 | Some (Nexp_aux (Nexp_var _, _)), Some (Nexp_aux (Nexp_constant c, _)) -> string (Big_int.to_string c)
+                (* If an integer argument is the same as a type variable, but we couldn't merge them, then use the type variable to ensure that the result type won't be the wrong one. *)
+                | Some (Nexp_aux (Nexp_var v, _)), _
+                  when KidSet.mem v ctxt.bound_nvars && not (KBindings.mem v ctxt.kid_id_renames) ->
+                    doc_var ctxt v
                 | _ -> construct_dep_pairs ctxt inst_env want_parens arg typ_from_fn
               in
               let epp =
diff --git a/test/coq/pass/unmergeablefn.sail b/test/coq/pass/unmergeablefn.sail
new file mode 100644
index 000000000..21a7711e1
--- /dev/null
+++ b/test/coq/pass/unmergeablefn.sail
@@ -0,0 +1,10 @@
+default Order dec
+$include <prelude.sail>
+
+/* Putting the integer for 'n inside a pair prevents the Coq backend from
+   merging the type variable and the argument, so it has to be careful about
+   the value passed to sail_zeros. */
+
+val f : forall 'n, 'n > 0. (bool, (int('n), bool)) -> bits('n)
+
+function f(b, p) = match p { (n, b2) => sail_zeros(n) }