@@ -737,6 +737,27 @@ module Make (Flow : INPUT) : OUTPUT = struct
737
737
| (_ , ThisTypeAppT (reason_tapp , c , this , ts )) ->
738
738
let reason_op = reason_of_t l in
739
739
instantiate_this_class cx trace ~reason_op ~reason_tapp c ts this (Lower (use_op, l))
740
+ (*
741
+ * When a subtyping question involves a union appearing on the right or an
742
+ * intersection appearing on the left, the simplification rules are
743
+ * imprecise: we split the union / intersection into cases and try to prove
744
+ * that the subtyping question holds for one of the cases, but each of those
745
+ * cases may be unprovable, which might lead to spurious errors. In
746
+ * particular, obvious assertions such as (A | B) & C is a subtype of A | B
747
+ * cannot be proved if we choose to split the union first (discharging
748
+ * unprovable subgoals of (A | B) & C being a subtype of either A or B);
749
+ * dually, obvious assertions such as A & B is a subtype of (A & B) | C
750
+ * cannot be proved if we choose to simplify the intersection first
751
+ * (discharging unprovable subgoals of either A or B being a subtype of (A &
752
+ * B) | C). So instead, we try inclusion rules to handle such cases.
753
+ *
754
+ * An orthogonal benefit is that for large unions or intersections, checking
755
+ * inclusion is significantly faster that splitting for proving simple
756
+ * inequalities (O(n) instead of O(n^2) for n cases).
757
+ *)
758
+ | (IntersectionT (_, rep), u)
759
+ when Base.List. mem ~equal: (Concrete_type_eq. eq cx) (InterRep. members rep) u ->
760
+ ()
740
761
(* If we have a TypeAppT (c, ts) ~> TypeAppT (c, ts) then we want to
741
762
* concretize both cs to PolyTs so that we may referentially compare them.
742
763
* We cannot compare the non-concretized versions since they may have been
@@ -1096,27 +1117,6 @@ module Make (Flow : INPUT) : OUTPUT = struct
1096
1117
| _ -> ()
1097
1118
);
1098
1119
InterRep. members rep |> List. iter (fun t -> rec_flow cx trace (l, UseT (use_op, t)))
1099
- (*
1100
- * When a subtyping question involves a union appearing on the right or an
1101
- * intersection appearing on the left, the simplification rules are
1102
- * imprecise: we split the union / intersection into cases and try to prove
1103
- * that the subtyping question holds for one of the cases, but each of those
1104
- * cases may be unprovable, which might lead to spurious errors. In
1105
- * particular, obvious assertions such as (A | B) & C is a subtype of A | B
1106
- * cannot be proved if we choose to split the union first (discharging
1107
- * unprovable subgoals of (A | B) & C being a subtype of either A or B);
1108
- * dually, obvious assertions such as A & B is a subtype of (A & B) | C
1109
- * cannot be proved if we choose to simplify the intersection first
1110
- * (discharging unprovable subgoals of either A or B being a subtype of (A &
1111
- * B) | C). So instead, we try inclusion rules to handle such cases.
1112
- *
1113
- * An orthogonal benefit is that for large unions or intersections, checking
1114
- * inclusion is significantly faster that splitting for proving simple
1115
- * inequalities (O(n) instead of O(n^2) for n cases).
1116
- *)
1117
- | (IntersectionT (_, rep), u)
1118
- when Base.List. mem ~equal: (Concrete_type_eq. eq cx) (InterRep. members rep) u ->
1119
- ()
1120
1120
(* String enum sets can be handled in logarithmic time by just
1121
1121
* checking for membership in the set.
1122
1122
*)
0 commit comments