Fixes #1576

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

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

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

tests/issues/issue1576.icry

@@ -0,0 +1,2 @@
+:load issue1576.cry
+:prove FP::eq_self

tests/issues/issue1576.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module issue1576
+Q.E.D.