Coq: be more careful when type variables couldn't be merged

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 =

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