From fa3765590012892b0858534ce421f26ff36bd7f1 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Wed, 20 May 2026 16:18:32 +0200
Subject: [PATCH] prevent type parameters in subtypes

Co-authored-by: Copilot <copilot@github.com>
---
 src/ecScope.ml               |  6 +++++-
 tests/subtype-clone-sugar.ec | 11 +++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/ecScope.ml b/src/ecScope.ml
index 1b1a3a97e9..c7cc2fbe6b 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -2306,7 +2306,7 @@ module Ty = struct
 
     let carrier =
       let ue = EcUnify.UniEnv.create None in
-      transty tp_tydecl env ue subtype.pst_carrier in
+      transty tp_nothing env ue subtype.pst_carrier in
 
     let pred =
       let x = EcIdent.create (fst subtype.pst_pred).pl_desc in
@@ -2316,6 +2316,10 @@ module Ty = struct
       if not (EcUnify.UniEnv.closed ue) then
         hierror ~loc:(snd subtype.pst_pred).pl_loc
           "the predicate contains free type variables";
+      if EcUnify.UniEnv.tparams ue <> [] then
+        hierror ~loc:(snd subtype.pst_pred).pl_loc
+          "Polymorphic predicates are not allowed. \
+           Use clones if you want to make a polymorphic subtype.";
       let uidmap = EcUnify.UniEnv.close ue in
       let fs = Tuni.subst uidmap in
       f_lambda [(x, GTty carrier)] (Fsubst.f_subst fs pred) in
diff --git a/tests/subtype-clone-sugar.ec b/tests/subtype-clone-sugar.ec
index 94bc894913..38239c4feb 100644
--- a/tests/subtype-clone-sugar.ec
+++ b/tests/subtype-clone-sugar.ec
@@ -5,3 +5,14 @@ subtype zmod3 =
   { x : int | 0 <= x < 3 }.
 
 realize inhabited. by exists 0. qed.
+
+op a: 'a.
+subtype uses_thole as ST1 =
+  { x : int | a<:bool> = a<:_> }.
+realize inhabited by done.
+
+fail subtype tvar_carrier as ST2 =
+  { x : 'a | true }.
+
+fail subtype tvar_prop as ST3 =
+  { x : int | a<:'a> = a<:_> }.