From 70a76ef699ffc8d415afd047629c642296f9bcc4 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 28 Mar 2019 17:03:36 +0900 Subject: [PATCH 1/7] Fix #8550: Soundness issue with class generalization --- Changes | 4 ++++ testsuite/tests/typing-poly/poly.ml | 12 ++++++++++++ typing/ctype.ml | 24 +++++++++++++----------- 3 files changed, 29 insertions(+), 11 deletions(-) diff --git a/Changes b/Changes index 662e634e1186..f996c3d67113 100644 --- a/Changes +++ b/Changes @@ -804,6 +804,10 @@ OCaml 4.08.0 - GPR#2231: Env: always freshen persistent signatures before using them (Thomas Refis and Leo White, review by Gabriel Radanne) +- #8550: Soundness issue with class generalization + (Jacques Garrigue, report by Jeremy Yallop) + + OCaml 4.07.1 (4 October 2018) ----------------------------- diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml index c60bdfa8de9f..a972e8f67a0c 100644 --- a/testsuite/tests/typing-poly/poly.ml +++ b/testsuite/tests/typing-poly/poly.ml @@ -1713,3 +1713,15 @@ module M : val i : 'a -> 'a end |}] + +(* #8550 *) +class ['a] r = let r : 'a = ref [] in object method get = r end;; +[%%expect{| +Line 1, characters 0-63: +1 | class ['a] r = let r : 'a = ref [] in object method get = r end;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: The type of this class, + class ['a] r : + object constraint 'a = '_weak2 list ref method get : 'a end, + contains type variables that cannot be generalized +|}] diff --git a/typing/ctype.ml b/typing/ctype.ml index 6ea278e14192..8064cbf6f443 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -869,13 +869,15 @@ let update_level env level ty = (* Generalize and lower levels of contravariant branches simultaneously *) -let rec generalize_expansive env var_level visited ty = +let rec generalize_expansive env var_level visited contra ty = let ty = repr ty in if ty.level = generic_level || ty.level <= var_level then () else - if not (Hashtbl.mem visited ty.id) then begin - Hashtbl.add visited ty.id (); + if try Hashtbl.find visited ty.id < contra with Not_found -> true then begin + Hashtbl.add visited ty.id contra; + let generalize_rec = generalize_expansive env var_level visited in match ty.desc with - Tconstr (path, tyl, abbrev) -> + Tvar _ -> if contra then set_level ty var_level + | Tconstr (path, tyl, abbrev) -> let variance = try (Env.find_type path env).type_variance with Not_found -> @@ -886,21 +888,21 @@ let rec generalize_expansive env var_level visited ty = List.iter2 (fun v t -> if Variance.(mem May_weak v) - then generalize_structure var_level t - else generalize_expansive env var_level visited t) + then generalize_rec true t + else generalize_rec contra t) variance tyl | Tpackage (_, _, tyl) -> - List.iter (generalize_structure var_level) tyl + List.iter (generalize_rec true) tyl | Tarrow (_, t1, t2, _) -> - generalize_structure var_level t1; - generalize_expansive env var_level visited t2 + generalize_rec true t1; + generalize_rec contra t2 | _ -> - iter_type_expr (generalize_expansive env var_level visited) ty + iter_type_expr (generalize_rec contra) ty end let generalize_expansive env ty = simple_abbrevs := Mnil; - generalize_expansive env !nongen_level (Hashtbl.create 7) ty + generalize_expansive env !nongen_level (Hashtbl.create 7) false ty let generalize_structure ty = generalize_structure !current_level ty From 477c3add2fc6ad8cc239b6426948b957d57c4c9b Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 28 Mar 2019 17:13:25 +0900 Subject: [PATCH 2/7] Update comment for generalize_expansive --- typing/ctype.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index 72e5fc8e2f91..b5af7a01dad2 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -878,7 +878,7 @@ let update_level env level ty = update_level env level true ty end -(* Generalize and lower levels of contravariant branches simultaneously *) +(* Lowe level of type variables inside contravariant branches *) let rec generalize_expansive env var_level visited contra ty = let ty = repr ty in From dfa72bfca7ad236a7cfa2d60c4b338d115e2bfcf Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Thu, 28 Mar 2019 17:14:22 +0900 Subject: [PATCH 3/7] typo in comment --- typing/ctype.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index b5af7a01dad2..633abe2408fb 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -878,7 +878,7 @@ let update_level env level ty = update_level env level true ty end -(* Lowe level of type variables inside contravariant branches *) +(* Lower level of type variables inside contravariant branches *) let rec generalize_expansive env var_level visited contra ty = let ty = repr ty in From 527069a6c36f0b1780bbe7abba99d08d797a12c9 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Fri, 29 Mar 2019 07:22:17 +0900 Subject: [PATCH 4/7] make condition more readable --- typing/ctype.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index 633abe2408fb..f19a28836335 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -883,7 +883,11 @@ let update_level env level ty = let rec generalize_expansive env var_level visited contra ty = let ty = repr ty in if ty.level = generic_level || ty.level <= var_level then () else - if try Hashtbl.find visited ty.id < contra with Not_found -> true then begin + let must_visit = + match Hashtbl.find visited ty.id with + | done_contra -> not done_contra && contra + | exception Not_found -> true + in if must_visit then begin Hashtbl.add visited ty.id contra; let generalize_rec = generalize_expansive env var_level visited in match ty.desc with From c05c21a8c8d6bad73b5d9107cd7f8dd1b296820d Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Fri, 29 Mar 2019 08:34:26 +0900 Subject: [PATCH 5/7] generic_level is no longer relevant --- typing/ctype.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index f19a28836335..d7920679d241 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -882,10 +882,10 @@ let update_level env level ty = let rec generalize_expansive env var_level visited contra ty = let ty = repr ty in - if ty.level = generic_level || ty.level <= var_level then () else let must_visit = + ty.level > var_level && match Hashtbl.find visited ty.id with - | done_contra -> not done_contra && contra + | done_contra -> contra && not done_contra | exception Not_found -> true in if must_visit then begin Hashtbl.add visited ty.id contra; From c14273a5add74dcc29827deea556c502b0f81eac Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Tue, 9 Apr 2019 14:04:05 +0900 Subject: [PATCH 6/7] rename generalize_expansive -> lower_contravariant --- typing/ctype.ml | 17 ++++++++--------- typing/ctype.mli | 6 +++--- typing/typecore.ml | 10 +++++----- 3 files changed, 16 insertions(+), 17 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index d7920679d241..93fe75226458 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -721,9 +721,9 @@ let rec generalize_structure var_level ty = end end -let generalize_structure var_level ty = +let generalize_structure ty = simple_abbrevs := Mnil; - generalize_structure var_level ty + generalize_structure !current_level ty (* Generalize the spine of a function, if the level >= !current_level *) @@ -880,16 +880,17 @@ let update_level env level ty = (* Lower level of type variables inside contravariant branches *) -let rec generalize_expansive env var_level visited contra ty = +let rec lower_contravariant env var_level visited contra ty = let ty = repr ty in let must_visit = ty.level > var_level && match Hashtbl.find visited ty.id with | done_contra -> contra && not done_contra | exception Not_found -> true - in if must_visit then begin + in + if must_visit then begin Hashtbl.add visited ty.id contra; - let generalize_rec = generalize_expansive env var_level visited in + let generalize_rec = lower_contravariant env var_level visited in match ty.desc with Tvar _ -> if contra then set_level ty var_level | Tconstr (path, tyl, abbrev) -> @@ -915,11 +916,9 @@ let rec generalize_expansive env var_level visited contra ty = iter_type_expr (generalize_rec contra) ty end -let generalize_expansive env ty = +let lower_contravariant env ty = simple_abbrevs := Mnil; - generalize_expansive env !nongen_level (Hashtbl.create 7) false ty - -let generalize_structure ty = generalize_structure !current_level ty + lower_contravariant env !nongen_level (Hashtbl.create 7) false ty (* Correct the levels of type [ty]. *) let correct_levels ty = diff --git a/typing/ctype.mli b/typing/ctype.mli index 5284ad3f0246..450a5ec22917 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -154,9 +154,9 @@ val filter_row_fields: val generalize: type_expr -> unit (* Generalize in-place the given type *) -val generalize_expansive: Env.t -> type_expr -> unit - (* Generalize the covariant part of a type, making - contravariant branches non-generalizable *) +val lower_contravariant: Env.t -> type_expr -> unit + (* Lower level of type variables inside contravariant branches; + to be used before generalize for expansive expressions *) val generalize_structure: type_expr -> unit (* Same, but variables are only lowered to !current_level *) val generalize_spine: type_expr -> unit diff --git a/typing/typecore.ml b/typing/typecore.ml index c22384a7bc69..d33aaa6edd3b 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -1994,7 +1994,7 @@ let list_labels env ty = (* Check that all univars are safe in a type *) let check_univars env expans kind exp ty_expected vars = if expans && not (is_nonexpansive exp) then - generalize_expansive env exp.exp_type; + lower_contravariant env exp.exp_type; (* need to expand twice? cf. Ctype.unify2 *) let vars = List.map (expand_head env) vars in let vars = List.map (expand_head env) vars in @@ -2489,7 +2489,7 @@ and type_expect_ begin_def (); let arg = type_exp env sarg in end_def (); - if not (is_nonexpansive arg) then generalize_expansive env arg.exp_type; + if not (is_nonexpansive arg) then lower_contravariant env arg.exp_type; generalize arg.exp_type; let cases, partial = type_cases ~exception_allowed:true env arg.exp_type ty_expected true loc @@ -3836,7 +3836,7 @@ and type_label_exp create env loc ty_expected begin_def (); let arg = type_exp env sarg in end_def (); - generalize_expansive env arg.exp_type; + lower_contravariant env arg.exp_type; unify_exp env arg ty_arg; check_univars env false "field value" arg label.lbl_arg vars; arg @@ -4661,7 +4661,7 @@ and type_let List.iter2 (fun pat exp -> if not (is_nonexpansive exp) then - generalize_expansive env pat.pat_type) + lower_contravariant env pat.pat_type) pat_list exp_list; iter_pattern_variables_type generalize pvs; (* We also generalize expressions that are not bound to a variable. @@ -4764,7 +4764,7 @@ let type_expression env sexp = begin_def(); let exp = type_exp env sexp in end_def(); - if not (is_nonexpansive exp) then generalize_expansive env exp.exp_type; + if not (is_nonexpansive exp) then lower_contravariant env exp.exp_type; generalize exp.exp_type; match sexp.pexp_desc with Pexp_ident lid -> From a428bb55c9222f1a44181922e6738a7180917feb Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Tue, 9 Apr 2019 14:05:35 +0900 Subject: [PATCH 7/7] add reviews --- Changes | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Changes b/Changes index 3b5ec6a96a3a..c6e8126153d6 100644 --- a/Changes +++ b/Changes @@ -1001,7 +1001,8 @@ OCaml 4.08.0 report by Daniel Bünzli and Jon Ludlam) - #8550, #8552: Soundness issue with class generalization - (Jacques Garrigue, report by Jeremy Yallop) + (Jacques Garrigue, review by Leo White and Thomas Refis, + report by Jeremy Yallop) OCaml 4.07.1 (4 October 2018) -----------------------------