177 lines
5.7 KiB
Diff
177 lines
5.7 KiB
Diff
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
|
|
|