1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
|
Index: Changes
===================================================================
--- Changes (revision 13157)
+++ Changes (working copy)
@@ -1,6 +1,11 @@
Next version
------------
+Type system:
+- Propagate type information towards pattern-matching, even in the presence
+ of polymorphic variants (discarding only information about possibly-present
+ constructors)
+
Compilers:
- PR#5861: raise an error when multiple private keywords are used in type declarations
- PR#5634: parsetree rewriter (-ppx flag)
Index: typing/typecore.ml
===================================================================
--- typing/typecore.ml (revision 13157)
+++ typing/typecore.ml (working copy)
@@ -326,7 +326,7 @@
| _ -> assert false
in
begin match row_field tag row with
- | Rabsent -> assert false
+ | Rabsent -> () (* assert false *)
| Reither (true, [], _, e) when not row.row_closed ->
set_row_field e (Rpresent None)
| Reither (false, ty::tl, _, e) when not row.row_closed ->
@@ -1657,6 +1657,28 @@
sexp unpacks
(* Helpers for type_cases *)
+
+let contains_variant_either ty =
+ let rec loop ty =
+ let ty = repr ty in
+ if ty.level >= lowest_level then begin
+ mark_type_node ty;
+ match ty.desc with
+ Tvariant row ->
+ let row = row_repr row in
+ if not row.row_fixed then
+ List.iter
+ (fun (_,f) ->
+ match row_field_repr f with Reither _ -> raise Exit | _ -> ())
+ row.row_fields;
+ iter_row loop row
+ | _ ->
+ iter_type_expr loop ty
+ end
+ in
+ try loop ty; unmark_type ty; false
+ with Exit -> unmark_type ty; true
+
let iter_ppat f p =
match p.ppat_desc with
| Ppat_any | Ppat_var _ | Ppat_constant _
@@ -1690,6 +1712,24 @@
in
try loop p; false with Exit -> true
+let check_absent_variant env =
+ iter_pattern
+ (function {pat_desc = Tpat_variant (s, arg, row)} as pat ->
+ let row = row_repr !row in
+ if List.exists (fun (s',fi) -> s = s' && row_field_repr fi <> Rabsent)
+ row.row_fields
+ then () else
+ let ty_arg =
+ match arg with None -> [] | Some p -> [correct_levels p.pat_type] in
+ let row' = {row_fields = [s, Reither(arg=None,ty_arg,true,ref None)];
+ row_more = newvar (); row_bound = ();
+ row_closed = false; row_fixed = false; row_name = None} in
+ (* Should fail *)
+ unify_pat env {pat with pat_type = newty (Tvariant row')}
+ (correct_levels pat.pat_type)
+ | _ -> ())
+
+
let dummy_expr = {pexp_desc = Pexp_tuple []; pexp_loc = Location.none}
(* Duplicate types of values in the environment *)
@@ -3037,16 +3077,20 @@
and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
(* ty_arg is _fully_ generalized *)
- let dont_propagate, has_gadts =
- let patterns = List.map fst caselist in
- List.exists contains_polymorphic_variant patterns,
- List.exists (contains_gadt env) patterns in
+ let patterns = List.map fst caselist in
+ let erase_either =
+ List.exists contains_polymorphic_variant patterns
+ && contains_variant_either ty_arg
+ and has_gadts = List.exists (contains_gadt env) patterns in
(* prerr_endline ( if has_gadts then "contains gadt" else "no gadt"); *)
- let ty_arg, ty_res, env =
+ let ty_arg =
+ if (has_gadts || erase_either) && not !Clflags.principal
+ then correct_levels ty_arg else ty_arg
+ and ty_res, env =
if has_gadts && not !Clflags.principal then
- correct_levels ty_arg, correct_levels ty_res,
- duplicate_ident_types loc caselist env
- else ty_arg, ty_res, env in
+ correct_levels ty_res, duplicate_ident_types loc caselist env
+ else ty_res, env
+ in
let lev, env =
if has_gadts then begin
(* raise level for existentials *)
@@ -3072,10 +3116,10 @@
let scope = Some (Annot.Idef loc) in
let (pat, ext_env, force, unpacks) =
let partial =
- if !Clflags.principal then Some false else None in
- let ty_arg =
- if dont_propagate then newvar () else instance ?partial env ty_arg
- in type_pattern ~lev env spat scope ty_arg
+ if !Clflags.principal || erase_either
+ then Some false else None in
+ let ty_arg = instance ?partial env ty_arg in
+ type_pattern ~lev env spat scope ty_arg
in
pattern_force := force @ !pattern_force;
let pat =
@@ -3134,7 +3178,11 @@
else
Partial
in
- add_delayed_check (fun () -> Parmatch.check_unused env cases);
+ add_delayed_check
+ (fun () ->
+ List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
+ pat_env_list;
+ Parmatch.check_unused env cases);
if has_gadts then begin
end_def ();
(* Ensure that existential types do not escape *)
Index: typing/ctype.ml
===================================================================
--- typing/ctype.ml (revision 13157)
+++ typing/ctype.ml (working copy)
@@ -981,6 +981,25 @@
if keep then more else newty more.desc
| _ -> assert false
in
+ (* Open row if partial for pattern and contains Reither *)
+ let more', row =
+ match partial with
+ Some (free_univars, false) when row.row_closed
+ && not row.row_fixed && TypeSet.is_empty (free_univars ty) ->
+ let not_reither (_, f) =
+ match row_field_repr f with
+ Reither _ -> false
+ | _ -> true
+ in
+ if List.for_all not_reither row.row_fields
+ then (more', row) else
+ (newty2 (if keep then more.level else !current_level)
+ (Tvar None),
+ {row_fields = List.filter not_reither row.row_fields;
+ row_more = more; row_bound = ();
+ row_closed = false; row_fixed = false; row_name = None})
+ | _ -> (more', row)
+ in
(* Register new type first for recursion *)
more.desc <- Tsubst(newgenty(Ttuple[more';t]));
(* Return a new copy *)
Index: testsuite/tests/typing-gadts/test.ml.reference
===================================================================
--- testsuite/tests/typing-gadts/test.ml.reference (revision 13157)
+++ testsuite/tests/typing-gadts/test.ml.reference (working copy)
@@ -62,11 +62,11 @@
^^^^^^^^
Error: This pattern matches values of type int t
but a pattern was expected which matches values of type s t
-# Characters 224-237:
- | `A, BoolLit _ -> ()
- ^^^^^^^^^^^^^
-Error: This pattern matches values of type ([? `A ] as 'a) * bool t
- but a pattern was expected which matches values of type 'a * int t
+# module Polymorphic_variants :
+ sig
+ type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
+ val eval : [ `A ] * 's t -> unit
+ end
# module Propagation :
sig
type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
Index: testsuite/tests/typing-gadts/test.ml.principal.reference
===================================================================
--- testsuite/tests/typing-gadts/test.ml.principal.reference (revision 13157)
+++ testsuite/tests/typing-gadts/test.ml.principal.reference (working copy)
@@ -62,11 +62,11 @@
^^^^^^^^
Error: This pattern matches values of type int t
but a pattern was expected which matches values of type s t
-# Characters 224-237:
- | `A, BoolLit _ -> ()
- ^^^^^^^^^^^^^
-Error: This pattern matches values of type ([? `A ] as 'a) * bool t
- but a pattern was expected which matches values of type 'a * int t
+# module Polymorphic_variants :
+ sig
+ type _ t = IntLit : int -> int t | BoolLit : bool -> bool t
+ val eval : [ `A ] * 's t -> unit
+ end
# Characters 299-300:
| BoolLit b -> b
^
|
