Skip to content

Prevent type parameters in subtypes #1012

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
oskgo wants to merge 1 commit into
base: main
Choose a base branch
from
+16 −1
Open

Prevent type parameters in subtypes #1012

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/ecScope.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
11 changes: 11 additions & 0 deletions tests/subtype-clone-sugar.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<:_> }.
Loading