From 8911a751e2bb78a8032c3eadb8d1219a40f470d2 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Thu, 14 Mar 2024 09:51:07 -0700
Subject: [PATCH] Allow polymorphic kvars and qualifiers

---
 crates/flux-fixpoint/src/lib.rs                      |  3 +++
 crates/flux-middle/src/rty/expr.rs                   |  2 +-
 crates/flux-refineck/src/fixpoint_encoding.rs        |  2 +-
 .../src/ghost_statements/fold_unfold.rs              |  2 +-
 .../tests/pos/surface/polymorphic_qualifier          | 12 ++++++++++++
 5 files changed, 18 insertions(+), 3 deletions(-)
 create mode 100644 crates/flux-tests/tests/pos/surface/polymorphic_qualifier

diff --git a/crates/flux-fixpoint/src/lib.rs b/crates/flux-fixpoint/src/lib.rs
index 38936eec17..43b416c3b7 100644
--- a/crates/flux-fixpoint/src/lib.rs
+++ b/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())
diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs
index 8d880d25b3..15cbd199d2 100644
--- a/crates/flux-middle/src/rty/expr.rs
+++ b/crates/flux-middle/src/rty/expr.rs
@@ -959,7 +959,7 @@ mod pretty {
                     }
                 }
                 ExprKind::App(func, args) => {
-                    w!("{:?}({})",
+                    w!("({:?})({})",
                         func,
                         ^args
                             .iter()
diff --git a/crates/flux-refineck/src/fixpoint_encoding.rs b/crates/flux-refineck/src/fixpoint_encoding.rs
index c1066f401d..6565a93c41 100644
--- a/crates/flux-refineck/src/fixpoint_encoding.rs
+++ b/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));
diff --git a/crates/flux-refineck/src/ghost_statements/fold_unfold.rs b/crates/flux-refineck/src/ghost_statements/fold_unfold.rs
index 11eb208d5b..2ef3d534a7 100644
--- a/crates/flux-refineck/src/ghost_statements/fold_unfold.rs
+++ b/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;
diff --git a/crates/flux-tests/tests/pos/surface/polymorphic_qualifier b/crates/flux-tests/tests/pos/surface/polymorphic_qualifier
new file mode 100644
index 0000000000..e0d6d54131
--- /dev/null
+++ b/crates/flux-tests/tests/pos/surface/polymorphic_qualifier
@@ -0,0 +1,12 @@
+#![flux::cfg(scrape_quals = true)]
+
+#[flux::sig(fn<T as base, refine p: T -> bool>(vec: Vec<T{v: p(v)}>, init: T{ p(init) }) -> T{v: p(v)})]
+fn maximum<T: Ord>(vec: Vec<T>, init: T) -> T {
+    let mut max = init;
+    for v in vec {
+        if let std::cmp::Ordering::Greater = max.cmp(&v) {
+            max = v;
+        }
+    }
+    max
+}