Skip to content

Fix check_and_update_generalized_ty_jkind #2615

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
68 changes: 9 additions & 59 deletions ocaml/testsuite/tests/typing-layouts/erasable_annot.ml
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,6 @@ can't be erased for compatibility with upstream OCaml.
module type S = sig type _ g = MkG : ('a : immediate). 'a g end
|}];;

(* CR layouts: only show the warning once; same for tests below *)
let f (type a : immediate): a -> a = fun x -> x
[%%expect {|
Line 1, characters 4-5:
Expand All @@ -76,12 +75,6 @@ Line 1, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 1, characters 6-47:
1 | let f (type a : immediate): a -> a = fun x -> x
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate). 'a -> 'a = <fun>
|}];;

Expand All @@ -93,12 +86,6 @@ Line 1, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 1, characters 6-31:
1 | let f x = (x : (_ : immediate))
^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate). 'a -> 'a = <fun>
|}];;

Expand All @@ -110,12 +97,6 @@ Line 1, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 1, characters 6-63:
1 | let f v: ((_ : immediate)[@error_message "Custom message"]) = v
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate). 'a -> 'a = <fun>
|}];;

Expand Down Expand Up @@ -182,12 +163,6 @@ Line 1, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 1, characters 6-49:
1 | let f (type a : immediate64): a -> a = fun x -> x
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate64). 'a -> 'a = <fun>
|}];;

Expand All @@ -199,12 +174,6 @@ Line 1, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 1, characters 6-33:
1 | let f x = (x : (_ : immediate64))
^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate64). 'a -> 'a = <fun>
|}];;

Expand All @@ -216,12 +185,6 @@ Line 1, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 1, characters 6-65:
1 | let f v: ((_ : immediate64)[@error_message "Custom message"]) = v
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate64). 'a -> 'a = <fun>
|}];;

Expand Down Expand Up @@ -289,15 +252,13 @@ Line 5, characters 4-5:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

Line 5, characters 6-50:
5 | let f (module _ : S with type t = 'a) (x : 'a) = x
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
can't be erased for compatibility with upstream OCaml.

val f : ('a : immediate). (module S with type t = 'a) -> 'a -> 'a = <fun>
|}]

(* CR layouts: this example should raise a warning, but it does not.
It's quite complicated, and missing it only means that this error
will be caught by the upstream compiler later. We have decided that
fixing this is not worth the effort. *)
module type S = sig
type t [@@immediate]
end
Expand All @@ -312,7 +273,10 @@ module type S = sig type t : immediate end
val x : int = 15
|}]

(* CR layouts: this should raise a warning *)
(* CR layouts: this example should raise a warning, but it does not.
It's quite complicated, and missing it only means that this error
will be caught by the upstream compiler later. We have decided that
fixing this is not worth the effort. *)
let y =
ignore (fun (type a : immediate) (x : a) ->
let module _ : S = struct
Expand Down Expand Up @@ -580,12 +544,6 @@ Line 1, characters 21-26:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in fails
can't be erased for compatibility with upstream OCaml.

Line 1, characters 27-68:
1 | let[@warning "-187"] fails (type a : immediate): a -> a = fun x -> x
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in fails
can't be erased for compatibility with upstream OCaml.

val fails : ('a : immediate). 'a -> 'a = <fun>
|}]

Expand All @@ -603,9 +561,7 @@ can't be erased for compatibility with upstream OCaml.
module type S1 = sig type ('a : immediate) fails = int end
|}]

(* Disabling the warning just in the signature isn't sufficient.

The check here is also ran twice for some reason. *)
(* Disabling the warning just in the signature isn't sufficient. *)
module M6 : sig
[@@@warning "-187"]
type ('a : immediate) t = 'a * 'a
Expand All @@ -619,12 +575,6 @@ Line 5, characters 2-35:
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in t
can't be erased for compatibility with upstream OCaml.

Line 5, characters 2-35:
5 | type ('a : immediate) t = 'a * 'a
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in t
can't be erased for compatibility with upstream OCaml.

module M6 : sig type ('a : immediate) t = 'a * 'a end
|}]

Expand Down
26 changes: 14 additions & 12 deletions ocaml/typing/ctype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2314,32 +2314,34 @@ let check_and_update_generalized_ty_jkind ?name ~loc ty =
| _ -> false)
in
if Language_extension.erasable_extensions_only ()
&& is_immediate jkind
&& is_immediate jkind && not (Jkind.has_warned jkind)
then
let id =
match name with
| Some id -> Ident.name id
| None -> "<unknown>"
in
Location.prerr_warning loc (Warnings.Incompatible_with_upstream
(Warnings.Immediate_erasure id))
else ()
(Warnings.Immediate_erasure id));
Jkind.with_warning jkind
else jkind
in
let generalization_check level jkind =
if level = generic_level then
Jkind.(update_reason jkind (Generalized (name, loc)))
else jkind
in
let rec inner ty =
let level = get_level ty in
if level = generic_level && try_mark_node ty then begin
if try_mark_node ty then begin
begin match get_desc ty with
| Tvar ({ jkind; _ } as r) ->
immediacy_check jkind;
let new_jkind =
Jkind.(update_reason jkind (Generalized (name, loc)))
in
let new_jkind = immediacy_check jkind in
let new_jkind = generalization_check level new_jkind in
set_type_desc ty (Tvar {r with jkind = new_jkind})
| Tunivar ({ jkind; _ } as r) ->
immediacy_check jkind;
let new_jkind =
Jkind.(update_reason jkind (Generalized (name, loc)))
in
let new_jkind = immediacy_check jkind in
let new_jkind = generalization_check level new_jkind in
set_type_desc ty (Tunivar {r with jkind = new_jkind})
| _ -> ()
end;
Expand Down
29 changes: 22 additions & 7 deletions ocaml/typing/jkind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -526,17 +526,22 @@ include Jkind_intf.History

type t = type_expr Jkind_types.t

let fresh_jkind jkind ~why = { jkind; history = Creation why }
let fresh_jkind jkind ~why =
{ jkind; history = Creation why; has_warned = false }

(******************************)
(* constants *)

let any_dummy_jkind =
{ jkind = Jkind_desc.max; history = Creation (Any_creation Dummy_jkind) }
{ jkind = Jkind_desc.max;
history = Creation (Any_creation Dummy_jkind);
has_warned = false
}

let value_v1_safety_check =
{ jkind = Jkind_desc.value;
history = Creation (Value_creation V1_safety_check)
history = Creation (Value_creation V1_safety_check);
has_warned = false
}

(* CR layouts: Should we be doing more memoization here? *)
Expand Down Expand Up @@ -761,6 +766,10 @@ let has_imported_history t =

let update_reason t reason = { t with history = Creation reason }

let with_warning t = { t with has_warned = true }

let has_warned t = t.has_warned

let printtyp_path = ref (fun _ _ -> assert false)

let set_printtyp_path f = printtyp_path := f
Expand Down Expand Up @@ -1225,8 +1234,9 @@ end
(******************************)
(* relations *)

let equate_or_equal ~allow_mutation { jkind = jkind1; history = _ }
{ jkind = jkind2; history = _ } =
let equate_or_equal ~allow_mutation
{ jkind = jkind1; history = _; has_warned = _ }
{ jkind = jkind2; history = _; has_warned = _ } =
Jkind_desc.equate_or_equal ~allow_mutation jkind1 jkind2

(* CR layouts v2.8: Switch this back to ~allow_mutation:false *)
Expand Down Expand Up @@ -1272,7 +1282,12 @@ let combine_histories reason lhs rhs =
let intersection ~reason t1 t2 =
match Jkind_desc.intersection t1.jkind t2.jkind with
| None -> Error (Violation.of_ (No_intersection (t1, t2)))
| Some jkind -> Ok { jkind; history = combine_histories reason t1 t2 }
| Some jkind ->
Ok
{ jkind;
history = combine_histories reason t1 t2;
has_warned = t1.has_warned || t2.has_warned
}

(* this is hammered on; it must be fast! *)
let check_sub sub super = Jkind_desc.sub sub.jkind super.jkind
Expand Down Expand Up @@ -1470,7 +1485,7 @@ module Debug_printers = struct
lhs_history Jkind_desc.Debug_printers.t rhs_jkind history rhs_history
| Creation c -> fprintf ppf "Creation (%a)" creation_reason c

let t ppf ({ jkind; history = h } : t) : unit =
let t ppf ({ jkind; history = h; has_warned = _ } : t) : unit =
fprintf ppf "@[<v 2>{ jkind = %a@,; history = %a }@]"
Jkind_desc.Debug_printers.t jkind history h
end
Expand Down
6 changes: 6 additions & 0 deletions ocaml/typing/jkind.mli
Original file line number Diff line number Diff line change
Expand Up @@ -304,6 +304,12 @@ val has_imported_history : t -> bool

val update_reason : t -> creation_reason -> t

(* Mark the jkind as having produced a compiler warning. *)
val with_warning : t -> t

(* Whether this jkind has produced a compiler warning. *)
val has_warned : t -> bool

(******************************)
(* relations *)

Expand Down
3 changes: 2 additions & 1 deletion ocaml/typing/jkind_types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,8 @@ type 'type_expr history =

type 'type_expr t =
{ jkind : 'type_expr Jkind_desc.t;
history : 'type_expr history
history : 'type_expr history;
has_warned : bool
}

type const =
Expand Down
3 changes: 2 additions & 1 deletion ocaml/typing/jkind_types.mli
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,8 @@ type 'type_expr history =

type 'type_expr t =
{ jkind : 'type_expr Jkind_desc.t;
history : 'type_expr history
history : 'type_expr history;
has_warned : bool
}

type annotation = const * Jane_syntax.Jkind.annotation
Loading