Skip to content

Removed warning for levelled GADTs #28

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

Merged
merged 6 commits into from
Oct 13, 2025
Merged

Removed warning for levelled GADTs #28

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
df27f83
Removed warning for levelled GADTs
michaelleejl Oct 6, 2025
bfc4b0b
Add guard
michaelleejl Oct 7, 2025
5aa8168
Make alldepend
michaelleejl Oct 7, 2025
ac09fea
Update typing/ctype.ml
michaelleejl Oct 10, 2025
1ac6272
Revert "Make alldepend"
yallop Oct 13, 2025
1db20b3
.depend: remove Ctype dependency on the Warnings module
yallop Oct 13, 2025
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
2 changes: 0 additions & 2 deletions .depend
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -619,7 +619,6 @@ typing/cmt2annot.cmi : \
parsing/location.cmi \
file_formats/cmt_format.cmi
typing/ctype.cmo : \
utils/warnings.cmi \
typing/types.cmi \
typing/type_immediacy.cmi \
typing/subst.cmi \
Expand All @@ -638,7 +637,6 @@ typing/ctype.cmo : \
parsing/asttypes.cmi \
typing/ctype.cmi
typing/ctype.cmx : \
utils/warnings.cmx \
typing/types.cmx \
typing/type_immediacy.cmx \
typing/subst.cmx \
Expand Down
11 changes: 1 addition & 10 deletions testsuite/tests/macros/gadts.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,38 +8,29 @@ macro m : type a. (a, int) Type.eq expr -> a -> unit expr =
;;

[%%expect{|
File "_none_", line 1:
Warning 75 [maco-dev]: maco: avoided gadt constraint at level 0

Line 3, characters 47-48:
3 | << match $p with Type.Equal -> $(let _ = 1 + x in << () >>) >>
^
Error: The value "x" has type "a" but an expression was expected of type "int"
|}]

(* TODO: we don't need a warning here *)
macro m : type a. (a, int) Type.eq expr -> unit expr =
fun p ->
<< match $p with Type.Equal -> () >>
;;

[%%expect{|
File "_none_", line 1:
Warning 75 [maco-dev]: maco: avoided gadt constraint at level 0

macro m : ('a, int) Type.eq expr -> unit expr = <fun>
|}]


(* TODO: we should eventually allow this *)
macro m : type a. (a, int) Type.eq expr -> a expr -> int expr =
fun p x ->
<< match $p with Type.Equal -> $x >>
;;

[%%expect{|
File "_none_", line 1:
Warning 75 [maco-dev]: maco: avoided gadt constraint at level 0

Line 3, characters 34-35:
3 | << match $p with Type.Equal -> $x >>
^
Expand Down
9 changes: 3 additions & 6 deletions typing/ctype.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2584,14 +2584,11 @@ let add_gadt_equation uenv source destination =
expressive)? as that lets us do anything inside an (unquoted) macro body *)

let env = get_env uenv in

let staging_level = Env.get_env_level env in

let staging_mode = Env.get_env_mode env in

if (* staging_level <> 0 ||*) staging_mode <> M_C then
Location.prerr_warning Location.none (Warnings.Maco_dev
("avoided gadt constraint at level "^(string_of_int staging_level)))
else begin
if (* staging_level <> 0 ||*) staging_mode = M_C then
begin
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this removes too much: we don't need the warning, but we probably do still need the check staging_mode <> M_C that guards the else branch.

if has_free_univars env destination then
occur_univar ~inj_only:true env destination
else if local_non_recursive_abbrev uenv source destination then begin
Expand Down
Loading