The unpac monorepo manager self-hosting as a monorepo using unpac
Allow to name new abstract types in constructor type annotations (#12507)
authored by
Jacques Garrigue
and committed by
GitHub
c7ad1a17
42ece636
+244
-21
+4
Changes
+4
Changes
···
121
121
is given. This allows to work around problems with GADTs in as-patterns.
122
122
(Jacques Garrigue, report by Leo White, review by Gabriel Scherer)
123
123
124
+
- #11891, #12507: Allow to name new locally abstract types in constructor type
125
+
annotations.
126
+
(Jacques Garrigue, report and review by Gabriel Scherer and Florian Angeletti)
127
+
124
128
### Runtime system:
125
129
126
130
- #12193: Re-introduce GC compaction for shared pools
+15
-2
manual/src/tutorials/gadtexamples.etex
+15
-2
manual/src/tutorials/gadtexamples.etex
···
249
249
type ('arg,'result,'aux) fn =
250
250
| Fun: ('a ->'b) -> ('a,'b,unit) fn
251
251
| Mem1: ('a ->'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
252
-
let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
252
+
let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
253
253
match f with
254
254
| Fun f -> f x
255
255
| Mem1 (f,y,fy) -> if x = y then fy else f x
···
272
272
type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
273
273
let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)
274
274
\end{caml_example*}
275
-
All existential type variables of the constructor must by introduced by
275
+
All existential type variables of the constructor must be introduced by
276
276
the ("type" ...) construct and bound by a type annotation on the
277
277
outside of the constructor argument.
278
+
279
+
One can additionally bind existentials that were freshly introduced
280
+
by the refinement of another existential type, if they appear in the
281
+
type of the arguments.
282
+
\begin{caml_example*}{verbatim}
283
+
type _ ty =
284
+
| Int : int ty
285
+
| Pair : 'b ty * 'c ty -> ('b * 'c) ty
286
+
let rec default : type a. a ty -> a = function
287
+
| Int -> 0
288
+
| Pair (type b c) (b, c : b ty * c ty) ->
289
+
(default b : b), (default c : c)
290
+
\end{caml_example*}
278
291
279
292
\section{s:gadt-equation-nonlocal-abstract}{Equations on non-local abstract types}
280
293
+130
-4
testsuite/tests/typing-gadts/name_existentials.ml
+130
-4
testsuite/tests/typing-gadts/name_existentials.ml
···
37
37
Line 1, characters 42-50:
38
38
1 | let ko2 = function Dyn (type a b) (a, x : a ty * b) -> ignore (x : b)
39
39
^^^^^^^^
40
-
Error: This pattern matches values of type "a ty * b"
41
-
but a pattern was expected which matches values of type "a ty * a"
42
-
Type "b" is not compatible with type "a"
40
+
Error: The local name "b" can only be given to an existential variable
41
+
introduced by this GADT constructor.
42
+
The type annotation tries to bind it to the name "a"
43
+
that is already bound.
43
44
|}]
44
45
45
46
type u = C : 'a * ('a -> 'b list) -> u
···
84
85
Line 2, characters 22-23:
85
86
2 | | Int (type b) (n : a) -> n
86
87
^
87
-
Error: This type does not bind all existentials in the constructor: "type b. a"
88
+
Error: The local name "b" can only be given to an existential variable
89
+
introduced by this GADT constructor.
90
+
The type annotation tries to bind it to the type "'a"
91
+
that is not a locally abstract type.
88
92
|}]
89
93
90
94
(* Strange wildcard *)
···
117
121
type ('a, 'b) pair = Pair of 'a * 'b
118
122
val f : (int, int) pair -> int = <fun>
119
123
|}]
124
+
125
+
126
+
(* #11891: allow naming more types *)
127
+
(* We stillonly allow to name freshly introduced existentials *)
128
+
129
+
type _ ty =
130
+
| Int : int ty
131
+
| Pair : 'b ty * 'c ty -> ('b * 'c) ty
132
+
let rec example : type a . a ty -> a = function
133
+
| Int -> 0
134
+
| Pair (x, y) -> (example x, example y)
135
+
let rec example : type a . a ty -> a = function
136
+
| Int -> 0
137
+
| Pair (type b c) (x, y : b ty * c ty) -> (example x, example y)
138
+
[%%expect{|
139
+
type _ ty = Int : int ty | Pair : 'b ty * 'c ty -> ('b * 'c) ty
140
+
val example : 'a ty -> 'a = <fun>
141
+
val example : 'a ty -> 'a = <fun>
142
+
|}]
143
+
144
+
let rec example : type a . a ty -> a = function
145
+
| Int -> 0
146
+
| Pair (type b c) (x, y : b ty * c ty) -> (example x, example (*error*)x)
147
+
[%%expect{|
148
+
Line 3, characters 54-72:
149
+
3 | | Pair (type b c) (x, y : b ty * c ty) -> (example x, example (*error*)x)
150
+
^^^^^^^^^^^^^^^^^^
151
+
Error: This expression has type "b" = "$0" but an expression was expected of type
152
+
"$1"
153
+
|}]
154
+
155
+
type _ th =
156
+
| Thunk : 'a * ('a -> 'b) -> 'b th
157
+
let f1 (type a) : a th -> a = function
158
+
| Thunk (type b) (x, f : b * (b -> _)) -> f x
159
+
let f2 (type a) : a th -> a = function
160
+
| Thunk (type b c) (x, f : b * (b -> c)) -> f x
161
+
[%%expect{|
162
+
type _ th = Thunk : 'a * ('a -> 'b) -> 'b th
163
+
val f1 : 'a th -> 'a = <fun>
164
+
Line 6, characters 29-41:
165
+
6 | | Thunk (type b c) (x, f : b * (b -> c)) -> f x
166
+
^^^^^^^^^^^^
167
+
Error: The local name "c" can only be given to an existential variable
168
+
introduced by this GADT constructor.
169
+
The type annotation tries to bind it to the name "a"
170
+
that was defined before.
171
+
|}]
172
+
(* Do not allow to deduce extra assumptions *)
173
+
let ko1 (type a) : a th -> a = function
174
+
| Thunk (type b c) (x, f : b * (b -> c option)) -> f x
175
+
[%%expect{|
176
+
Line 2, characters 29-48:
177
+
2 | | Thunk (type b c) (x, f : b * (b -> c option)) -> f x
178
+
^^^^^^^^^^^^^^^^^^^
179
+
Error: This pattern matches values of type "b * (b -> c option)"
180
+
but a pattern was expected which matches values of type "b * (b -> a)"
181
+
Type "c option" is not compatible with type "a"
182
+
|}]
183
+
(* Can only name fresh existentials *)
184
+
let ko2 = function
185
+
| Thunk (type b c) (x, f : b * (b -> c)) -> f x
186
+
[%%expect{|
187
+
Line 2, characters 29-41:
188
+
2 | | Thunk (type b c) (x, f : b * (b -> c)) -> f x
189
+
^^^^^^^^^^^^
190
+
Error: The local name "c" can only be given to an existential variable
191
+
introduced by this GADT constructor.
192
+
The type annotation tries to bind it to the type "'a"
193
+
that is not a locally abstract type.
194
+
|}]
195
+
let ko3 () =
196
+
match [] with
197
+
| [Thunk (type b c) (x, f : b * (b -> c))] -> f x
198
+
| _ -> assert false
199
+
[%%expect{|
200
+
Line 3, characters 30-42:
201
+
3 | | [Thunk (type b c) (x, f : b * (b -> c))] -> f x
202
+
^^^^^^^^^^^^
203
+
Error: The local name "c" can only be given to an existential variable
204
+
introduced by this GADT constructor.
205
+
The type annotation tries to bind it to the type "'a"
206
+
that is not a locally abstract type.
207
+
|}]
208
+
209
+
type _ tho =
210
+
| Thunk_opt : 'b * ('b -> 'c option) -> 'c option tho
211
+
let f3 (type a) : a tho -> a = function
212
+
| Thunk_opt (type b c) (x, f : b * (b -> c option)) -> f x
213
+
[%%expect{|
214
+
type _ tho = Thunk_opt : 'b * ('b -> 'c option) -> 'c option tho
215
+
val f3 : 'a tho -> 'a = <fun>
216
+
|}]
217
+
218
+
219
+
(* check locality *)
220
+
type 'a wrap = Wrap of 'a
221
+
type _ ty = Int : int ty | Pair : ('b ty * 'c ty) wrap -> ('b * 'c) ty
222
+
(* ok *)
223
+
let rec default : type a. a ty -> a = function
224
+
| Int -> 0
225
+
| Pair (type b c) (Wrap (b, c) : (b ty * c ty) wrap) ->
226
+
(default b : b), (default c : c)
227
+
[%%expect{|
228
+
type 'a wrap = Wrap of 'a
229
+
type _ ty = Int : int ty | Pair : ('b ty * 'c ty) wrap -> ('b * 'c) ty
230
+
val default : 'a ty -> 'a = <fun>
231
+
|}]
232
+
(* ko *)
233
+
let rec default : type a. a ty -> a = function
234
+
| Int -> 0
235
+
| Pair (Wrap (type b c) (b, c : b ty * c ty)) ->
236
+
(default b : b), (default c : c)
237
+
[%%expect{|
238
+
Line 3, characters 34-45:
239
+
3 | | Pair (Wrap (type b c) (b, c : b ty * c ty)) ->
240
+
^^^^^^^^^^^
241
+
Error: The local name "b" can only be given to an existential variable
242
+
introduced by this GADT constructor.
243
+
The type annotation tries to bind it to the name "$0"
244
+
that was defined before.
245
+
|}]
+3
typing/ident.ml
+3
typing/ident.ml
+4
typing/ident.mli
+4
typing/ident.mli
···
50
50
[create_*], or if they are both persistent and have the same
51
51
name. *)
52
52
53
+
val compare_stamp: t -> t -> int
54
+
(** Compare only the internal stamps, 0 if absent *)
55
+
53
56
val compare: t -> t -> int
57
+
(** Compare identifiers structurally, including the name *)
54
58
55
59
val global: t -> bool
56
60
val is_predef: t -> bool
+82
-15
typing/typecore.ml
+82
-15
typing/typecore.ml
···
96
96
| In_class_def (** or in [class c = let ... in ...] *)
97
97
| In_self_pattern (** or in self pattern *)
98
98
99
+
type existential_binding =
100
+
| Bind_already_bound
101
+
| Bind_not_in_scope
102
+
| Bind_non_locally_abstract
103
+
99
104
type error =
100
105
| Constructor_arity_mismatch of Longident.t * int * int
101
106
| Label_mismatch of Longident.t * Errortrace.unification_error
···
189
194
| Andop_type_clash of string * Errortrace.unification_error
190
195
| Bindings_type_clash of Errortrace.unification_error
191
196
| Unbound_existential of Ident.t list * type_expr
197
+
| Bind_existential of existential_binding * Ident.t * type_expr
192
198
| Missing_type_constraint
193
199
| Wrong_expected_kind of wrong_kind_sort * wrong_kind_context * type_expr
194
200
| Expr_not_a_record_type of type_expr
···
747
753
vars
748
754
749
755
let solve_constructor_annotation
750
-
tps (penv : Pattern_env.t) name_list sty ty_args ty_ex =
756
+
tps (penv : Pattern_env.t) name_list sty ty_args ty_ex unify_res =
751
757
let expansion_scope = penv.equations_scope in
752
-
let ids =
758
+
(* Introduce fresh type names that expand to type variables.
759
+
They should eventually be bound to ground types. *)
760
+
let ids_decls =
753
761
List.map
754
762
(fun name ->
755
-
let decl = new_local_type ~loc:name.loc Definition in
763
+
let tv = newvar () in
764
+
let decl =
765
+
new_local_type ~loc:name.loc Definition
766
+
~manifest_and_scope:(tv, Ident.lowest_scope) in
756
767
let (id, new_env) =
757
768
Env.enter_type ~scope:expansion_scope name.txt decl !!penv in
758
769
Pattern_env.set_env penv new_env;
759
-
{name with txt = id})
770
+
({name with txt = id}, (decl, tv)))
760
771
name_list
761
772
in
773
+
(* Translate the type annotation using these type names. *)
762
774
let cty, ty, force =
763
775
with_local_level ~post:(fun (_,ty,_) -> generalize_structure ty)
764
776
(fun () -> Typetexp.transl_simple_type_delayed !!penv sty)
765
777
in
766
778
tps.tps_pattern_force <- force :: tps.tps_pattern_force;
779
+
(* Only unify the return type after generating the ids *)
780
+
unify_res ();
767
781
let ty_args =
768
782
let ty1 = instance ty and ty2 = instance ty in
769
783
match ty_args with
···
777
791
Ttuple tyl -> tyl
778
792
| _ -> assert false
779
793
in
780
-
if ids <> [] then ignore begin
781
-
let ids = List.map (fun x -> x.txt) ids in
794
+
if ids_decls <> [] then begin
795
+
let ids_decls = List.map (fun (x,dm) -> (x.txt,dm)) ids_decls in
796
+
let ids = List.map fst ids_decls in
782
797
let rem =
798
+
(* First process the existentials introduced by this constructor.
799
+
Just need to make their definitions abstract. *)
783
800
List.fold_left
784
801
(fun rem tv ->
785
802
match get_desc tv with
786
-
Tconstr(Path.Pident id, [], _) when List.mem id rem ->
787
-
list_remove id rem
803
+
Tconstr(Path.Pident id, [], _) when List.mem_assoc id rem ->
804
+
let decl, tv' = List.assoc id ids_decls in
805
+
let env =
806
+
Env.add_type ~check:false id
807
+
{decl with type_manifest = None} !!penv
808
+
in
809
+
Pattern_env.set_env penv env;
810
+
(* We have changed the definition, so clean up *)
811
+
Btype.cleanup_abbrev ();
812
+
(* Since id is now abstract, this does not create a cycle *)
813
+
unify_pat_types cty.ctyp_loc env tv tv';
814
+
List.remove_assoc id rem
788
815
| _ ->
789
816
raise (Error (cty.ctyp_loc, !!penv,
790
817
Unbound_existential (ids, ty))))
791
-
ids ty_ex
818
+
ids_decls ty_ex
792
819
in
793
-
if rem <> [] then
794
-
raise (Error (cty.ctyp_loc, !!penv,
795
-
Unbound_existential (ids, ty)))
820
+
(* The other type names should be bound to newly introduced existentials. *)
821
+
let bound_ids = ref ids in
822
+
List.iter
823
+
(fun (id, (decl, tv')) ->
824
+
let tv' = expand_head !!penv tv' in
825
+
begin match get_desc tv' with
826
+
| Tconstr (Path.Pident id', [], _) ->
827
+
if List.exists (Ident.same id') !bound_ids then
828
+
raise (Error (cty.ctyp_loc, !!penv,
829
+
Bind_existential (Bind_already_bound, id, tv')));
830
+
(* Both id and id' are Scoped identifiers, so their stamps grow *)
831
+
if Ident.scope id' <> penv.equations_scope
832
+
|| Ident.compare_stamp id id' > 0 then
833
+
raise (Error (cty.ctyp_loc, !!penv,
834
+
Bind_existential (Bind_not_in_scope, id, tv')));
835
+
bound_ids := id' :: !bound_ids
836
+
| _ ->
837
+
raise (Error (cty.ctyp_loc, !!penv,
838
+
Bind_existential
839
+
(Bind_non_locally_abstract, id, tv')));
840
+
end;
841
+
let env =
842
+
Env.add_type ~check:false id
843
+
{decl with type_manifest = Some (correct_levels tv')} !!penv
844
+
in
845
+
Pattern_env.set_env penv env)
846
+
rem;
847
+
if rem <> [] then Btype.cleanup_abbrev ();
796
848
end;
797
-
ty_args, Some (ids, cty)
849
+
ty_args, Some (List.map fst ids_decls, cty)
798
850
799
851
let solve_Ppat_construct ~refine tps penv loc constr no_existentials
800
852
existential_styp expected_ty =
···
832
884
let ty_args, ty_res, ty_ex =
833
885
instance_constructor existential_treatment constr
834
886
in
835
-
let equated_types = unify_res ty_res expected_ty in
887
+
let equated_types = lazy (unify_res ty_res expected_ty) in
836
888
let ty_args, existential_ctyp =
837
889
solve_constructor_annotation tps penv name_list sty ty_args ty_ex
890
+
(fun () -> ignore (Lazy.force equated_types))
838
891
in
839
-
ty_args, ty_res, equated_types, existential_ctyp
892
+
ty_args, ty_res, Lazy.force equated_types, existential_ctyp
840
893
in
841
894
if constr.cstr_existentials <> [] then
842
895
lower_variables_only !!penv penv.Pattern_env.equations_scope ty_res;
···
6864
6917
"@[<2>%s:@ %a@]"
6865
6918
"This type does not bind all existentials in the constructor"
6866
6919
(Style.as_inline_code pp_type) (ids, ty)
6920
+
| Bind_existential (reason, id, ty) ->
6921
+
let reason1, reason2 = match reason with
6922
+
| Bind_already_bound -> "the name", "that is already bound"
6923
+
| Bind_not_in_scope -> "the name", "that was defined before"
6924
+
| Bind_non_locally_abstract -> "the type",
6925
+
"that is not a locally abstract type"
6926
+
in
6927
+
Location.errorf ~loc
6928
+
"@[<hov0>The local name@ %a@ %s@ %s.@ %s@ %s@ %a@ %s.@]"
6929
+
(Style.as_inline_code Printtyp.ident) id
6930
+
"can only be given to an existential variable"
6931
+
"introduced by this GADT constructor"
6932
+
"The type annotation tries to bind it to"
6933
+
reason1 (Style.as_inline_code Printtyp.type_expr) ty reason2
6867
6934
| Missing_type_constraint ->
6868
6935
Location.errorf ~loc
6869
6936
"@[%s@ %s@]"
+6
typing/typecore.mli
+6
typing/typecore.mli
···
142
142
143
143
val self_coercion : (Path.t * Location.t list ref) list ref
144
144
145
+
type existential_binding =
146
+
| Bind_already_bound
147
+
| Bind_not_in_scope
148
+
| Bind_non_locally_abstract
149
+
145
150
type error =
146
151
| Constructor_arity_mismatch of Longident.t * int * int
147
152
| Label_mismatch of Longident.t * Errortrace.unification_error
···
223
228
| Andop_type_clash of string * Errortrace.unification_error
224
229
| Bindings_type_clash of Errortrace.unification_error
225
230
| Unbound_existential of Ident.t list * type_expr
231
+
| Bind_existential of existential_binding * Ident.t * type_expr
226
232
| Missing_type_constraint
227
233
| Wrong_expected_kind of wrong_kind_sort * wrong_kind_context * type_expr
228
234
| Expr_not_a_record_type of type_expr