From 4c03e721b4c53240a9091790acb401b27e72dce0 Mon Sep 17 00:00:00 2001 From: Florian Angeletti Date: Wed, 4 Oct 2023 10:05:44 +0200 Subject: [PATCH 1/5] Fix variance composition (#12623) Possible positive occurrence under possible negative occurrence were forgotten, making the typechecker accepts the absurd statement type -'a n type +'a p type +'a ko = 'a p n (cherry picked from commit 1a9c45317b2c6c9ca9b4cb95fe4891f9f1a2820e) --- Changes | 8 +++ boot/ocamlc | Bin 3051798 -> 3051796 bytes boot/ocamllex | Bin 391863 -> 391861 bytes testsuite/tests/typing-misc/variance.ml | 87 ++++++++++++++++++++++++ typing/types.ml | 2 +- 5 files changed, 96 insertions(+), 1 deletion(-) diff --git a/Changes b/Changes index 20b7b8ee22..dccdc9baba 100644 --- a/Changes +++ b/Changes @@ -1,3 +1,11 @@ +OCaml 5.1.1 +----------- + +### Bug fixes: + +- #12623, fix the computation of variance composition + (Florian Angeletti, report by Vesa Karvonen, review by Gabriel Scherer) + OCaml 5.1.0 (14 September 2023) ------------------------------- diff --git a/boot/ocamlc b/boot/ocamlc index f3b2cba8df84a5f1326c7fe7bdf12b85159f65b3..4db4d848dbc3c2411a9e6160e9d932dd7ba35a34 100755 GIT binary patch delta 244 zcmZ9=y)pw)7zW@yD_A75h=~7x4sq6QNTHKLLz5Y;l1i^m@y)Byq%e*dP4>M3jS*A| zH=r=XOm0DACarO5#nU`Dd{Ng71+*IApk>g1RMp&zydf97QqRy1Wtle;50Y`&VqB`Jh%WZf=l2sxB{+% zYvB4LHS4)A&pSWz{Q8@xo}b$HKl;!&)oPSPN%{2bA~uz{vSZ>slkC18)N0Mv{`SAV Z)LrdtIGaw{*=p;q`M6Wx_O}_8{s6iiTe|=N delta 266 zcmbQTXcyx&AZ}=3Y+-6)ZeeL*ZDDI+Z{cX+Y~gC*ZsBR+ZQ*O--y(2h;q(<<0zA`W z77B1oUvN>3W%_}I0zB=17775dAP@@yu`m#e0I?_#ivh7X5K92DBoIphu{03N0I@6( z%K@=G5Gw$&A`mM9u`&>=0I@0%s{yh4_CE_XmId(MW?;znW?%|9%D}jD=l1oVG`yJf z%}n(S^$fIAQp*fYb&U*+jCBnxbq!1pxH>vaSm0oQF5a&8RRf4MfmjQOwSib?yV_UX OtFsy3PyaJPPXYiZJ96a! diff --git a/boot/ocamllex b/boot/ocamllex index cfdfbe8b4541516ef49c895ea691ea534706de67..b2b5404e69f35a1eb7d0a74fe687a4f4508a7149 100755 GIT binary patch delta 98 zcmdn~RebAL@rD-07N!>F7M3lnT~@qO3=Hgl7#JKo7#Or4Zl7+&>cymMYN}_bXQ-W$ qT4tbYWME{hYhbBsXmY^S(Q(282Yoc*?EF7M3lnT~@p@3=Hgl7#JKo85p!5ZJ%z%>cymQW~yhXXP}*u rT4rdfYh++#tZQJYYhZf7)zM+X0tW+h@$G!JtbKbK4W`fi#VP>+{6`&d diff --git a/testsuite/tests/typing-misc/variance.ml b/testsuite/tests/typing-misc/variance.ml index d0f754f716..419e348f48 100644 --- a/testsuite/tests/typing-misc/variance.ml +++ b/testsuite/tests/typing-misc/variance.ml @@ -36,3 +36,90 @@ type !'a t = (module s with type t = 'a);; module type s = sig type t end type 'a t = (module s with type t = 'a) |}] + +(* Composition *) +type -'a n +type +'a p +type !'a i + +type +'a error_np = 'a n p;; +[%%expect{| +type -'a n +type +'a p +type !'a i +Line 5, characters 0-26: +5 | type +'a error_np = 'a n p;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be covariant, + but it is contravariant. +|}] + + +type +'a error_pn = 'a p n;; +[%%expect{| +Line 1, characters 0-26: +1 | type +'a error_pn = 'a p n;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be covariant, + but it is contravariant. +|}] + +type -'a error_pp = 'a p p;; +[%%expect{| +Line 1, characters 0-26: +1 | type -'a error_pp = 'a p p;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be contravariant, + but it is covariant. +|}] + +type -'a error_nn = 'a n n;; +[%%expect{| +Line 1, characters 0-26: +1 | type -'a error_nn = 'a n n;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be contravariant, + but it is covariant. +|}] + +type !'a inj_in = 'a i n +[%%expect{| +Line 1, characters 0-24: +1 | type !'a inj_in = 'a i n + ^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be injective invariant, + but it is invariant. +|}] + +type !'a inj_in = 'a n i +[%%expect{| +Line 1, characters 0-24: +1 | type !'a inj_in = 'a n i + ^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be injective invariant, + but it is invariant. +|}] + +module Make_covariant(M: sig type 'a t end): sig + type 'a i = 'a + type +'a t = 'a i M.t +end = struct + type 'a i = 'a + type +'a t = 'a i M.t +end + +module Positive_ref = Make_covariant(struct type 'a t = 'a ref end) +[%%expect {| +Line 6, characters 2-23: +6 | type +'a t = 'a i M.t + ^^^^^^^^^^^^^^^^^^^^^ +Error: In this definition, expected parameter variances are not satisfied. + The 1st type parameter was expected to be covariant, + but it is invariant. +|}] diff --git a/typing/types.ml b/typing/types.ml index 45a4f896d6..c1dbdb6895 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -186,7 +186,7 @@ module Variance = struct let mp = mem May_pos v1 && mem May_pos v2 || mem May_neg v1 && mem May_neg v2 and mn = - mem May_pos v1 && mem May_neg v2 || mem May_pos v1 && mem May_neg v2 + mem May_pos v1 && mem May_neg v2 || mem May_neg v1 && mem May_pos v2 and mw = mem May_weak v1 && v2 <> null || v1 <> null && mem May_weak v2 and inj = mem Inj v1 && mem Inj v2 and pos = mem Pos v1 && mem Pos v2 || mem Neg v1 && mem Neg v2 -- 2.41.0