The unpac monorepo manager self-hosting as a monorepo using unpac
Fix #13495: typechecker crash while typing objects (#13514)
Fix 13495, making out of scope universal variables fatal, except for equality
authored by
Jacques Garrigue
and committed by
GitHub
e026d942
f2bac84c
+78
-11
+4
Changes
+4
Changes
···
789
789
path under Win32.
790
790
(Nicolás Ojeda Bär, review by David Allsopp and Damien Doligez)
791
791
792
+
- #13495, #13514: Fix typechecker crash while typing objects
793
+
(Jacques Garrigue, report by Nicolás Ojeda Bär, review by
794
+
Nicolas Ojeda Bär, Gabriel Scherer, Stephen Dolan, Florian Angeletti)
795
+
792
796
- #13263, #13560: fix printing true and false in toplevel and error
793
797
messages (no more unexpected \#true)
794
798
(Florian Angeletti, report by Samuel Vivien, review by Gabriel Scherer)
+26
testsuite/tests/typing-objects/pr13495.ml
+26
testsuite/tests/typing-objects/pr13495.ml
···
1
+
(* TEST
2
+
expect;
3
+
*)
4
+
5
+
class type gui =
6
+
object
7
+
method sub: 'b. 'b -> 'b
8
+
end
9
+
10
+
class virtual local_sub =
11
+
object
12
+
method virtual sub: 'b. 'b -> 'b option
13
+
end
14
+
[%%expect{|
15
+
class type gui = object method sub : 'b -> 'b end
16
+
class virtual local_sub : object method virtual sub : 'b -> 'b option end
17
+
|}]
18
+
19
+
class virtual ['a] compound_gui =
20
+
object (_: #gui)
21
+
constraint 'a = #local_sub
22
+
end
23
+
[%%expect{|
24
+
class virtual ['a] compound_gui :
25
+
object constraint 'a = #local_sub method virtual sub : 'b -> 'b end
26
+
|}]
+17
testsuite/tests/typing-recmod/pr13514.ml
+17
testsuite/tests/typing-recmod/pr13514.ml
···
1
+
(* TEST
2
+
expect;
3
+
*)
4
+
5
+
module rec M: sig
6
+
type t = { r: 'a 'b. 'a -> ' b -> 'a }
7
+
val f: t -> t
8
+
end = struct
9
+
type t = { r : 'a. 'a -> 'a -> 'a }
10
+
let f: t -> M.t = fun x -> x
11
+
end
12
+
[%%expect{|
13
+
Line 6, characters 29-30:
14
+
6 | let f: t -> M.t = fun x -> x
15
+
^
16
+
Error: The value "x" has type "t" but an expression was expected of type "M.t"
17
+
|}]
+31
-11
typing/ctype.ml
+31
-11
typing/ctype.ml
···
134
134
135
135
exception Cannot_unify_universal_variables
136
136
137
+
exception Out_of_scope_universal_variable
138
+
137
139
exception Matches_failure of Env.t * unification_error
138
140
139
141
exception Incompatible
···
1969
1971
raise Cannot_unify_universal_variables
1970
1972
end
1971
1973
| [] ->
1972
-
Misc.fatal_error "Ctype.unify_univar: univar not in scope"
1974
+
raise Out_of_scope_universal_variable
1973
1975
1974
1976
(* The same as [unify_univar], but raises the appropriate exception instead of
1975
1977
[Cannot_unify_universal_variables] *)
1976
-
let unify_univar_for tr_exn t1 t2 univar_pairs =
1977
-
try unify_univar t1 t2 univar_pairs
1978
-
with Cannot_unify_universal_variables -> raise_unexplained_for tr_exn
1978
+
let unify_univar_for (type a) (tr_exn : a trace_exn) t1 t2 univar_pairs =
1979
+
try unify_univar t1 t2 univar_pairs with
1980
+
| Cannot_unify_universal_variables -> raise_unexplained_for tr_exn
1981
+
| Out_of_scope_universal_variable ->
1982
+
(* Allow unscoped univars when checking for equality, since one
1983
+
might want to compare arbitrary subparts of types, ignoring scopes;
1984
+
see Typedecl_variance (#13514) for instance *)
1985
+
match tr_exn with
1986
+
| Equality -> raise_unexplained_for tr_exn
1987
+
| _ -> fatal_error "Ctype.unify_univar_for: univar not in scope"
1979
1988
1980
1989
(* Test the occurrence of free univars in a type *)
1981
1990
(* That's way too expensive. Must do some kind of caching *)
···
2321
2330
end
2322
2331
| _ -> false
2323
2332
2324
-
(* [mcomp] tests if two types are "compatible" -- i.e., if they could ever
2325
-
unify. (This is distinct from [eqtype], which checks if two types *are*
2326
-
exactly the same.) This is used to decide whether GADT cases are
2327
-
unreachable. It is broadly part of unification. *)
2333
+
(* [mcomp] tests if two types are "compatible" -- i.e., if there could
2334
+
exist a witness of their equality. This is distinct from [eqtype],
2335
+
which checks if two types *are* exactly the same.
2336
+
[mcomp] is used to decide whether GADT cases are unreachable.
2337
+
The existence of a witness is necessarily an incomplete property,
2338
+
i.e. there exists types for which we cannot tell if an equality
2339
+
witness could exist or not. Typically, this is the case for
2340
+
abstract types, which could be equal to anything, depending on
2341
+
their actual definition. As a result [mcomp] overapproximates
2342
+
compatibilty, i.e. when it says that two types are incompatible, we
2343
+
are sure that there exists no equality witness, but if it does not
2344
+
say so, there is no guarantee that such a witness could exist.
2345
+
*)
2328
2346
2329
-
(* mcomp type_pairs subst env t1 t2 does not raise an
2347
+
(* [mcomp type_pairs subst env t1 t2] should not raise an
2330
2348
exception if it is possible that t1 and t2 are actually
2331
2349
equal, assuming the types in type_pairs are equal and
2332
2350
that the mapping subst holds.
···
2393
2411
t1 tl1 t2 tl2 (mcomp type_pairs env)
2394
2412
with Escape _ -> raise Incompatible)
2395
2413
| (Tunivar _, Tunivar _) ->
2396
-
(try unify_univar t1' t2' !univar_pairs
2397
-
with Cannot_unify_universal_variables -> raise Incompatible)
2414
+
begin try unify_univar t1' t2' !univar_pairs with
2415
+
| Cannot_unify_universal_variables -> raise Incompatible
2416
+
| Out_of_scope_universal_variable -> ()
2417
+
end
2398
2418
| (_, _) ->
2399
2419
raise Incompatible
2400
2420
end