From 419d3748a058ba542f74be9af86bcf301675febd Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Wed, 11 Feb 2026 17:08:47 -0800
Subject: [PATCH] Fixes #1576

---
 CHANGES.md                         |  3 +++
 src/Cryptol/Symbolic.hs            |  2 +-
 tests/issues/issue1576.cry         | 16 ++++++++++++++++
 tests/issues/issue1576.icry        |  2 ++
 tests/issues/issue1576.icry.stdout |  4 ++++
 5 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 tests/issues/issue1576.cry
 create mode 100644 tests/issues/issue1576.icry
 create mode 100644 tests/issues/issue1576.icry.stdout

diff --git a/CHANGES.md b/CHANGES.md
index 7243db505..2ba8c4b62 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -10,6 +10,9 @@
 * Fix incorrect module context computation for nested functors.
   ([#1872](https://github.com/GaloisInc/cryptol/issues/1872))
   ([#1898](https://github.com/GaloisInc/cryptol/issues/1898))
+
+* Don't consider schemas with trivial `True` constraints to be polymorphic.
+  ([#1576](https://github.com/GaloisInc/cryptol/issues/1576))
   
 
 # 3.5.0 -- 2026-01-27
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index bd2f3293f..4e6d6d0e2 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -127,7 +127,7 @@ data ProverResult = AllSatResult [SatResult] -- LAZY
 
 predArgTypes :: QueryType -> Schema -> Either Doc [FinType]
 predArgTypes qtype schema@(Forall ts ps ty)
-  | null ts && null ps =
+  | null ts && all pIsTrue ps = -- We could have `True` constraints due to module instantiations (see #1576)
     case evalType mempty ty of
       Left _ -> Left "Predicate needs to be of kind *"
       Right tval ->
diff --git a/tests/issues/issue1576.cry b/tests/issues/issue1576.cry
new file mode 100644
index 000000000..047651c4f
--- /dev/null
+++ b/tests/issues/issue1576.cry
@@ -0,0 +1,16 @@
+module issue1576 where
+  interface submodule I where
+    type Value : *
+    value: Value
+
+  submodule F where
+    import interface submodule I
+
+    eq_self : Eq Value => Bool
+    property eq_self = value == value
+
+  submodule P where
+    type Value = [16]
+    value = 0xe641
+
+  import submodule F { submodule P } as FP
\ No newline at end of file
diff --git a/tests/issues/issue1576.icry b/tests/issues/issue1576.icry
new file mode 100644
index 000000000..e4daf23ed
--- /dev/null
+++ b/tests/issues/issue1576.icry
@@ -0,0 +1,2 @@
+:load issue1576.cry
+:prove FP::eq_self
\ No newline at end of file
diff --git a/tests/issues/issue1576.icry.stdout b/tests/issues/issue1576.icry.stdout
new file mode 100644
index 000000000..96098f2b2
--- /dev/null
+++ b/tests/issues/issue1576.icry.stdout
@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module issue1576
+Q.E.D.