From 4c03e721b4c53240a9091790acb401b27e72dce0 Mon Sep 17 00:00:00 2001
From: Florian Angeletti <florian.angeletti@inria.fr>
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{Ng<LzMW^BN^$HKIxZ024ql%Br7=?mi$BbncCYl%-WMQ
z3~cMYn6aH>71+*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*?E<!}eR~=8rqBPyDggk+ryT$Q
delta 100
zcmdn`Rebwb@rD-07N!>F7M3lnT~@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