Skip to content

Commit 27ea321

Browse files
panagosg7facebook-github-bot
authored andcommitted
Fix sharing of upper bound edges under speculation
Summary: ## The problem Short-circuiting constraints that have been seen before in different speculation branches can be unsound. Consider for example the following ``` type X = (x: $ElementType<{name: string}, 'name'>) => void; declare var foo: X & X; foo(1); ``` Here the following sequence happens leading to an unsound result: ``` Speculation begins Branch A: A1. new tvar v for EvalT [...] A2. v ~> ReposUseT A3. ReposUseT is added to v.upper [...] A4. Speculative Error recorded Branch B: B1. reuse cached v for EvalT [...] (same as in case A) B2. v ~> ReposUseT B3. immediate success, because ReposUseT is already in v.upper ``` The problem with the above is that constraint `v ~> ReposUseT` was reused across speculation branches. ## The fix This diff ensures that we only short-circuit upper-bounds, when the previous edge was discovered on the same speculation path (same or ancestor branch). To do this, it adds an optional (speculation id, case id) pair as part of the key to the map that stores upper bounds of type variables. This way, in the example above, the edge created in A2, will not be reused in B3, since the speculation cases differ. Reviewed By: mvitousek Differential Revision: D24848916 fbshipit-source-id: 8c800e7ef6ad691dbf18aa1766c746dbf1a0fd5c
1 parent 190fa42 commit 27ea321

File tree

12 files changed

+104
-109
lines changed

12 files changed

+104
-109
lines changed

src/typing/constraint.ml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,20 @@ open Type
99

1010
type ident = int
1111

12+
module UseTypeKey = struct
13+
type speculation_id = int
14+
15+
type case_id = int
16+
17+
type key = TypeTerm.use_t * (speculation_id * case_id) option
18+
19+
type t = key
20+
21+
let compare = Stdlib.compare
22+
end
23+
24+
module UseTypeMap = WrappedMap.Make (UseTypeKey)
25+
1226
(** Type variables are unknowns, and we are ultimately interested in constraints
1327
on their solutions for type inference.
1428

src/typing/constraint.mli

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,22 @@
77

88
type ident = int
99

10+
module UseTypeKey : sig
11+
type speculation_id = int
12+
13+
type case_id = int
14+
15+
type key = Type.use_t * (speculation_id * case_id) option
16+
17+
type t = key
18+
19+
val compare : key -> key -> int
20+
end
21+
22+
module UseTypeMap : sig
23+
include module type of WrappedMap.Make (UseTypeKey)
24+
end
25+
1026
(***************************************)
1127

1228
type node =
@@ -25,7 +41,7 @@ and constraints =
2541

2642
and bounds = {
2743
mutable lower: (Trace.t * Type.use_op) Type.TypeMap.t;
28-
mutable upper: Trace.t Type.UseTypeMap.t;
44+
mutable upper: Trace.t UseTypeMap.t;
2945
mutable lowertvars: (Trace.t * Type.use_op) IMap.t;
3046
mutable uppertvars: (Trace.t * Type.use_op) IMap.t;
3147
}

src/typing/context.ml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -891,3 +891,9 @@ let fix_cache cx = cx.ccx.fix_cache
891891
let spread_cache cx = cx.ccx.spread_cache
892892

893893
let speculation_state cx = cx.ccx.speculation_state
894+
895+
let speculation_id cx =
896+
let open Speculation_state in
897+
match !(speculation_state cx) with
898+
| [] -> None
899+
| { speculation_id; case = { case_id; _ }; _ } :: _ -> Some (speculation_id, case_id)

src/typing/context.mli

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -463,3 +463,5 @@ val fix_cache : t -> (Reason.t * Type.t, Type.t) Hashtbl.t
463463
val spread_cache : t -> Spread_cache.t
464464

465465
val speculation_state : t -> Speculation_state.t
466+
467+
val speculation_id : t -> (int * int) option

src/typing/debug_js.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -914,7 +914,7 @@ and dump_tvar_ (depth, tvars) cx id =
914914
"; "
915915
(List.rev
916916
(UseTypeMap.fold
917-
(fun use_t _ acc -> dump_use_t_ (depth - 1, stack) cx use_t :: acc)
917+
(fun (use_t, _) _ acc -> dump_use_t_ (depth - 1, stack) cx use_t :: acc)
918918
upper
919919
[])))
920920
with Context.Tvar_not_found _ -> spf "Not Found: %d" id)

src/typing/flow_js.ml

Lines changed: 30 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,7 @@ let possible_types_of_type cx = function
172172

173173
let uses_of constraints =
174174
match constraints with
175-
| Unresolved { upper; _ } -> UseTypeMap.keys upper
175+
| Unresolved { upper; _ } -> Base.List.map ~f:fst (UseTypeMap.keys upper)
176176
| Resolved (use_op, t)
177177
| FullyResolved (use_op, t) ->
178178
[UseT (use_op, t)]
@@ -11033,7 +11033,7 @@ struct
1103311033
(* for each u in us: l => u *)
1103411034
and flows_from_t cx trace ~new_use_op l us =
1103511035
us
11036-
|> UseTypeMap.iter (fun u trace_u ->
11036+
|> UseTypeMap.iter (fun (u, _) trace_u ->
1103711037
let u = flow_use_op cx new_use_op u in
1103811038
join_flow cx [trace; trace_u] (l, u))
1103911039

@@ -11042,12 +11042,13 @@ struct
1104211042
ls
1104311043
|> TypeMap.iter (fun l (trace_l, use_op') ->
1104411044
us
11045-
|> UseTypeMap.iter (fun u trace_u ->
11045+
|> UseTypeMap.iter (fun (u, _) trace_u ->
1104611046
let u = flow_use_op cx use_op' (flow_use_op cx use_op u) in
1104711047
join_flow cx [trace_l; trace; trace_u] (l, u)))
1104811048

1104911049
(* bounds.upper += u *)
11050-
and add_upper u trace bounds = bounds.upper <- UseTypeMap.add u trace bounds.upper
11050+
and add_upper cx u trace bounds =
11051+
bounds.upper <- UseTypeMap.add (u, Context.speculation_id cx) trace bounds.upper
1105111052

1105211053
(* bounds.lower += l *)
1105311054
and add_lower l (trace, use_op) bounds =
@@ -11076,10 +11077,10 @@ struct
1107611077
goto node (so that updating its bounds is unnecessary). **)
1107711078
and edges_to_t cx trace ?(opt = false) (id1, bounds1) t2 =
1107811079
let max = Context.max_trace_depth cx in
11079-
if not opt then add_upper t2 trace bounds1;
11080+
if not opt then add_upper cx t2 trace bounds1;
1108011081
iter_with_filter cx bounds1.lowertvars id1 (fun (_, bounds) (trace_l, use_op) ->
1108111082
let t2 = flow_use_op cx use_op t2 in
11082-
add_upper t2 (Trace.concat_trace ~max [trace_l; trace]) bounds)
11083+
add_upper cx t2 (Trace.concat_trace ~max [trace_l; trace]) bounds)
1108311084
(* for each id in id2 + bounds2.uppertvars:
1108411085
id.bounds.lower += t1
1108511086
*)
@@ -11095,17 +11096,17 @@ struct
1109511096
add_lower t1 (Trace.concat_trace ~max [trace; trace_u], use_op) bounds)
1109611097

1109711098
(* for each id' in id + bounds.lowertvars:
11098-
id'.bounds.upper += us
11099+
id'.bounds.upper += us
1109911100
*)
1110011101
and edges_to_ts ~new_use_op cx trace ?(opt = false) (id, bounds) us =
1110111102
let max = Context.max_trace_depth cx in
1110211103
us
11103-
|> UseTypeMap.iter (fun u trace_u ->
11104+
|> UseTypeMap.iter (fun (u, _) trace_u ->
1110411105
let u = flow_use_op cx new_use_op u in
1110511106
edges_to_t cx (Trace.concat_trace ~max [trace; trace_u]) ~opt (id, bounds) u)
1110611107

1110711108
(* for each id' in id + bounds.uppertvars:
11108-
id'.bounds.lower += ls
11109+
id'.bounds.lower += ls
1110911110
*)
1111011111
and edges_from_ts cx trace ~new_use_op ?(opt = false) ls (id, bounds) =
1111111112
let max = Context.max_trace_depth cx in
@@ -11114,20 +11115,29 @@ struct
1111411115
let new_use_op = pick_use_op cx use_op new_use_op in
1111511116
edges_from_t cx (Trace.concat_trace ~max [trace_l; trace]) ~new_use_op ~opt l (id, bounds))
1111611117
(* for each id in id1 + bounds1.lowertvars:
11117-
id.bounds.upper += t2
11118-
for each l in bounds1.lower: l => t2
11118+
id.bounds.upper += t2
11119+
for each l in bounds1.lower: l => t2
1111911120
*)
1112011121

1112111122
(** As an invariant, bounds1.lower should already contain id.bounds.lower for
1112211123
each id in bounds1.lowertvars. **)
1112311124
and edges_and_flows_to_t cx trace ?(opt = false) (id1, bounds1) t2 =
11124-
if not (UseTypeMap.mem t2 bounds1.upper) then (
11125+
(* Skip iff edge exists as part of the speculation path to the current branch *)
11126+
let skip =
11127+
List.exists
11128+
(fun branch ->
11129+
let Speculation_state.{ speculation_id; case = { case_id; _ }; _ } = branch in
11130+
UseTypeMap.mem (t2, Some (speculation_id, case_id)) bounds1.upper)
11131+
!(Context.speculation_state cx)
11132+
|| UseTypeMap.mem (t2, None) bounds1.upper
11133+
in
11134+
if not skip then (
1112511135
edges_to_t cx trace ~opt (id1, bounds1) t2;
1112611136
flows_to_t cx trace bounds1.lower t2
1112711137
)
1112811138
(* for each id in id2 + bounds2.uppertvars:
11129-
id.bounds.lower += t1
11130-
for each u in bounds2.upper: t1 => u
11139+
id.bounds.lower += t1
11140+
for each u in bounds2.upper: t1 => u
1113111141
*)
1113211142

1113311143
(** As an invariant, bounds2.upper should already contain id.bounds.upper for
@@ -11173,9 +11183,9 @@ struct
1117311183
add_lowertvar id1 (Trace.concat_trace ~max [trace; trace_u]) use_op bounds)
1117411184

1117511185
(* for each id in id1 + bounds1.lowertvars:
11176-
id.bounds.upper += bounds2.upper
11177-
id.bounds.uppertvars += id2
11178-
id.bounds.uppertvars += bounds2.uppertvars
11186+
id.bounds.upper += bounds2.upper
11187+
id.bounds.uppertvars += id2
11188+
id.bounds.uppertvars += bounds2.uppertvars
1117911189
*)
1118011190
and add_upper_edges ~new_use_op cx trace ?(opt = false) (id1, bounds1) (id2, bounds2) =
1118111191
let max = Context.max_trace_depth cx in
@@ -11187,9 +11197,9 @@ struct
1118711197
edges_to_tvar cx trace ~new_use_op ~opt (id1, bounds1) tvar)
1118811198

1118911199
(* for each id in id2 + bounds2.uppertvars:
11190-
id.bounds.lower += bounds1.lower
11191-
id.bounds.lowertvars += id1
11192-
id.bounds.lowertvars += bounds1.lowertvars
11200+
id.bounds.lower += bounds1.lower
11201+
id.bounds.lowertvars += id1
11202+
id.bounds.lowertvars += bounds1.lowertvars
1119311203
*)
1119411204
and add_lower_edges cx trace ~new_use_op ?(opt = false) (id1, bounds1) (id2, bounds2) =
1119511205
let max = Context.max_trace_depth cx in

src/typing/ty_normalizer.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -953,7 +953,7 @@ end = struct
953953
>>| Base.List.dedup_and_sort ~compare:Stdlib.compare
954954

955955
and empty_with_upper_bounds ~env bounds =
956-
let uses = T.UseTypeMap.keys bounds.Constraint.upper in
956+
let uses = Base.List.map ~f:fst (Constraint.UseTypeMap.keys bounds.Constraint.upper) in
957957
let%map use_kind = uses_t ~env uses in
958958
Ty.Bot (Ty.NoLowerWithUpper use_kind)
959959

src/typing/type.ml

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2308,14 +2308,6 @@ and UseTypeSet : (Set.S with type elt = TypeTerm.use_t) = Set.Make (struct
23082308
let compare = Stdlib.compare
23092309
end)
23102310

2311-
and UseTypeMap : (WrappedMap.S with type key = TypeTerm.use_t) = WrappedMap.Make (struct
2312-
type key = TypeTerm.use_t
2313-
2314-
type t = key
2315-
2316-
let compare = Stdlib.compare
2317-
end)
2318-
23192311
and Object : sig
23202312
type resolve_tool =
23212313
(* Each part of a spread must be resolved in order to compute the result *)

src/typing/type_mapper.ml

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -701,7 +701,17 @@ class virtual ['a] t =
701701
Constraint.(
702702
let lower' = TypeMap.ident_map_key (self#type_ cx map_cx) t.lower in
703703
if lower' != t.lower then t.lower <- lower';
704-
let upper' = UseTypeMap.ident_map_key (self#use_type cx map_cx) t.upper in
704+
let upper' =
705+
UseTypeMap.ident_map_key
706+
(fun u ->
707+
let (t, speculation) = u in
708+
let t' = self#use_type cx map_cx t in
709+
if t == t' then
710+
u
711+
else
712+
(t', speculation))
713+
t.upper
714+
in
705715
if upper' != t.upper then t.upper <- upper';
706716
t)
707717

Lines changed: 1 addition & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -1,75 +1,3 @@
1-
Error ----------------------------------------------------------------------------------------------- positining.js:28:2
2-
3-
Cannot cast `x` to `$RelayProps` because property `$fragmentRefs` is missing in object type [1] but exists in
4-
`$FragmentRef` [2] in property `selectedValue`. [prop-missing]
5-
6-
positining.js:28:2
7-
28| (x: $RelayProps<Props>);
8-
^
9-
10-
References:
11-
positining.js:23:18
12-
23| selectedValue: X,
13-
^ [1]
14-
positining.js:19:49
15-
19| (<TRef: 3, T: {+$refType: TRef, ...}>(T) => $FragmentRef<T>),
16-
^^^^^^^^^^^^^^^ [2]
17-
18-
19-
Error ----------------------------------------------------------------------------------------------- positining.js:28:2
20-
21-
Cannot cast `x` to `$RelayProps` because property `$refType` is missing in `$FragmentRef` [1] but exists in object
22-
type [2] in property `selectedValue`. [prop-missing]
23-
24-
positining.js:28:2
25-
28| (x: $RelayProps<Props>);
26-
^
27-
28-
References:
29-
positining.js:19:49
30-
19| (<TRef: 3, T: {+$refType: TRef, ...}>(T) => $FragmentRef<T>),
31-
^^^^^^^^^^^^^^^ [1]
32-
positining.js:23:18
33-
23| selectedValue: X,
34-
^ [2]
35-
36-
37-
Error ----------------------------------------------------------------------------------------------- positining.js:28:2
38-
39-
Cannot cast `x` to `$RelayProps` because number literal `3` [1] is incompatible with empty [2] in the first argument.
40-
[incompatible-type]
41-
42-
positining.js:28:2
43-
28| (x: $RelayProps<Props>);
44-
^
45-
46-
References:
47-
positining.js:12:14
48-
12| +$refType: 3,
49-
^ [1]
50-
positining.js:17:20
51-
17| (<T: {+$refType: empty, ...}>(T) => T) &
52-
^^^^^ [2]
53-
54-
55-
Error ----------------------------------------------------------------------------------------------- positining.js:28:2
56-
57-
Cannot cast `x` to `$RelayProps` because number literal `3` [1] is incompatible with empty [2] in type argument `T` of
58-
the first argument. [incompatible-type]
59-
60-
positining.js:28:2
61-
28| (x: $RelayProps<Props>);
62-
^
63-
64-
References:
65-
positining.js:12:14
66-
12| +$refType: 3,
67-
^ [1]
68-
positining.js:18:22
69-
18| (<T: {+$refType: empty, ...}>(?T) => ?T) &
70-
^^^^^ [2]
71-
72-
731
Error ----------------------------------------------------------------------------------------------------- test.js:18:6
742

753
Cannot create `Foo` element because number [1] is incompatible with boolean [2] in property `a`. [incompatible-type]
@@ -85,7 +13,4 @@ References:
8513

8614

8715

88-
Found 5 errors
89-
90-
Only showing the most relevant union/intersection branches.
91-
To see all branches, re-run Flow with --show-all-branches
16+
Found 1 error

0 commit comments

Comments
 (0)