Allow polymorphic kvars and qualifiers

crates/flux-fixpoint/src/lib.rs

@@ -164,6 +164,9 @@ impl<T: Types> Task<T> {
             .arg("-q")
             .arg("--stdin")
             .arg("--json")
+            .arg("--nosmthorn")
+            .arg("--allowho")
+            .arg("--allowhoqs")
             .stdin(Stdio::piped())
             .stdout(Stdio::piped())
             .stderr(Stdio::null())

crates/flux-middle/src/rty/expr.rs

@@ -959,7 +959,7 @@ mod pretty {
                     }
                 }
                 ExprKind::App(func, args) => {
-                    w!("{:?}({})",
+                    w!("({:?})({})",
                         func,
                         ^args
                             .iter()

crates/flux-refineck/src/fixpoint_encoding.rs

@@ -699,7 +699,7 @@ impl KVarStore {
             let is_self_arg = i < self_args;
             let var = var.to_expr();
             sort.walk(|sort, proj| {
-                if !matches!(sort, rty::Sort::Loc | rty::Sort::Func(..)) {
+                if !matches!(sort, rty::Sort::Loc) {
                     flattened_self_args += is_self_arg as usize;
                     sorts.push(sort.clone());
                     exprs.push(rty::Expr::field_projs(&var, proj));

crates/flux-refineck/src/ghost_statements/fold_unfold.rs

@@ -17,7 +17,7 @@ use flux_middle::{
 };
 use itertools::Itertools;
 use rustc_data_structures::unord::UnordMap;
-use rustc_hash::{FxHashMap, FxHashSet};
+use rustc_hash::FxHashMap;
 use rustc_hir::def_id::DefId;
 use rustc_index::{bit_set::BitSet, Idx, IndexVec};
 use rustc_middle::mir::START_BLOCK;