| blob | 9eccf5727d5a8e13ad6b64583f14d54f46a20456 |
1 // Copyright (c) Meta Platforms, Inc. and affiliates.
2 //
3 // This source code is licensed under the MIT license found in the
4 // LICENSE file in the "hack" directory of this source tree.
6 use super::{config::Config, env::Env, solve, visited_goals::GoalResult};
7 use crate::typing::typing_error::Result;
8 use im::HashSet;
9 use itertools::{izip, Itertools};
10 use oxidized::ast_defs::Variance;
11 use pos::{Positioned, Symbol, TypeName};
12 use std::ops::Deref;
13 use ty::{
14 local::{Exact, FunType, Prim, Ty, Ty_, Tyvar},
15 local_error::{Primary, TypingError},
16 prop::Prop,
17 reason::Reason,
18 };
20 /// Normalize the proposition `T <: U`
21 pub fn simp_ty<R: Reason>(
22 cfg: &Config,
23 env: &mut Env<R>,
24 ty_sub: &Ty<R>,
25 ty_sup: &Ty<R>,
26 ) -> Result<Prop<R>> {
27 use Ty_::*;
28 let r_sub = ty_sub.reason();
29 let ety_sup = env.inf_env.resolve_ty(ty_sup);
30 let ety_sub = env.inf_env.resolve_ty(ty_sub);
31 match ety_sup.deref() {
32 // -- Super is var -----------------------------------------------------
33 Tvar(tv_sup) => {
34 match ety_sub.deref() {
35 Tunion(_) => simp_ty_common(cfg, env, &ety_sub, &ety_sup),
36 Toption(ty_sub_inner) => {
37 let ty_sub_inner = env.inf_env.resolve_ty(ty_sub_inner);
38 // We special case on `mixed <: Tvar _`, adding the entire `mixed` type
39 // as a lower bound. This enables clearer error messages when upper bounds
40 // are added to the type variable: transitive closure picks up the
41 // entire `mixed` type, and not separately consider `null` and `nonnull`
42 if ty_sub_inner.is_nonnull() {
43 Ok(Prop::subtype_ty(ety_sub, ety_sup))
44 } else {
45 let ty_null = Ty::null(r_sub.clone());
46 simp_conj_sub(cfg, env, &ty_sub_inner, &ty_null, &ety_sup)
47 }
48 }
49 Tvar(tv_sub) if tv_sub == tv_sup => Ok(Prop::valid()),
50 _ => Ok(Prop::subtype_ty(ety_sub, ety_sup)),
51 }
52 }
54 // -- Super is union ---------------------------------------------------
55 Tunion(ty_sups) => {
56 // TOOD[mjt] we don't have negation yet so we're dropping special
57 // case code for t <: (#1 | arraykey) here
58 match ety_sub.deref() {
59 Tunion(_) | Tvar(_) => simp_ty_common(cfg, env, &ety_sub, &ety_sup),
60 Tgeneric(_, _) if cfg.ignore_generic_params => {
61 simp_ty_common(cfg, env, &ety_sub, &ety_sup)
62 }
63 Tprim(p) if matches!(p, Prim::Tnum) => {
64 let r = ety_sub.reason();
65 let ty_float = Ty::float(r.clone());
66 let ty_int = Ty::int(r.clone());
67 simp_conj_sub(cfg, env, &ty_float, &ty_int, ty_sup)
68 }
69 Toption(ty_sub_inner) => {
70 let r = ety_sub.reason();
71 let ty_null = Ty::null(r.clone());
72 let p = simp_conj_sub(cfg, env, ty_sub_inner, &ty_null, ty_sup)?;
73 if p.is_unsat() {
74 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
75 } else {
76 Ok(p)
77 }
78 }
79 _ => {
80 // TODO[mjt] this omits all the like-type pushing for
81 // sound dynamic
82 let p1 = simp_disjs_sup(cfg, env, &ety_sub, ty_sups.iter())?;
83 let p2 = match ety_sub.deref() {
84 // TODO[mjt] It's this kind of thing which makes
85 // understanding subtyping unnecessarily difficult; here
86 // we are matching on the subtype 3 times(!) - twice
87 // here and once in `simp_ty_common` when we really
88 // should pull the generic subtyping logic out instead
89 // and leave this match one level up.
90 // We should go through this and simplify the nested
91 // matches
92 Tgeneric(_, _) => simp_ty_common(cfg, env, &ety_sub, ty_sup)?,
93 _ => Prop::invalid(TypingError::Primary(Primary::Subtype)),
94 };
95 Ok(p1.disj(p2, TypingError::Primary(Primary::Subtype)))
96 }
97 }
98 }
100 // -- Super is option --------------------------------------------------
101 Toption(ty_sup_inner) => {
102 let ety_sup_inner = env.inf_env.resolve_ty(ty_sup_inner);
103 // ?nonnull === mixed
104 // TODO[mjt] why do we use this encoding?
105 if ety_sup_inner.is_nonnull() {
106 Ok(Prop::valid())
107 } else {
108 match ety_sub.deref() {
109 Tprim(p_sub) => match p_sub {
110 Prim::Tnull => Ok(Prop::valid()),
111 Prim::Tvoid => {
112 let p1 = simp_ty(cfg, env, &ety_sub, &ety_sup_inner)?;
113 if p1.is_valid() {
114 Ok(p1)
115 } else {
116 // TODO[mjt]: check on this rule! Here `simp_ty_common`
117 // is `?nonnull == mixed <: ety_sup` (as an implicit upper bound ?)
118 // but we already know that ty_sup is _not_ top, don't we?
119 let p2 = simp_ty_common(cfg, env, &ety_sub, &ety_sup)?;
120 Ok(p1.disj(p2, TypingError::Primary(Primary::Subtype)))
121 }
122 }
123 _ => simp_ty(cfg, env, &ety_sub, &ety_sup_inner),
124 },
125 // ?t <: ?u iff t < ?u
126 // Why?
127 // Since t <: ?t and the transitivity of <: we have t <: ?u
128 // or
129 // If t <: ?u by covariance of ? we have ?t <: ?u and
130 // by idempotence we have ?t <: ??t
131 // so this step preserves the set of solutions
132 Toption(ty_sub_inner) => simp_ty(cfg, env, ty_sub_inner, &ety_sup),
133 // TODO[mjt] Again, this needlessly repeats pattern matching
134 // - lets pull the Tvar case out from `simp_ty_common`
135 Tvar(_) | Tunion(_) => simp_ty_common(cfg, env, &ety_sub, &ety_sup),
136 Tgeneric(_, _) if cfg.ignore_generic_params => {
137 simp_ty_common(cfg, env, &ety_sub, &ety_sup)
138 }
139 Tgeneric(_, _) => simp_disj_sup(cfg, env, &ety_sub, &ety_sup_inner, &ety_sup),
140 // All of these cannot we have t </: null so we have
141 // t < ?u iff t <: u
142 Tnonnull | Tfun(_) | Tclass(_, _, _) => {
143 simp_ty(cfg, env, &ety_sub, &ety_sup_inner)
144 }
145 Tany => {
146 unimplemented!("Subtype propositions involving `Tany` aren't implemented")
147 }
148 }
149 }
150 }
151 // -- Super is generic -------------------------------------------------
152 Tgeneric(tp_name_sup, _) => match ety_sub.deref() {
153 // If subtype and supertype are the same generic parameter, we're done
154 Tgeneric(tp_name_sub, _) if tp_name_sub == tp_name_sup => Ok(Prop::valid()),
155 Tvar(_) | Tunion(_) => simp_ty_common(cfg, env, &ety_sub, &ety_sup),
156 _ if cfg.ignore_generic_params => Ok(Prop::subtype_ty(ety_sub, ety_sup)),
157 _ => simp_ty_typaram(cfg, env, ety_sub, (ety_sup.reason(), tp_name_sup)),
158 },
160 // -- Super is nonnull -------------------------------------------------
161 Tnonnull => match ety_sub.deref() {
162 Tprim(p_sub) => {
163 use Prim::*;
164 // TODO[mjt] test for nullable on prims?
165 match p_sub {
166 Tnull | Tvoid => Ok(Prop::invalid(TypingError::Primary(Primary::Subtype))),
167 Tint | Tbool | Tfloat | Tstring | Tresource | Tnum | Tarraykey | Tnoreturn => {
168 Ok(Prop::valid())
169 }
170 }
171 }
172 Tnonnull | Tfun(_) | Tclass(_, _, _) => Ok(Prop::valid()),
173 Tvar(_) | Tgeneric(_, _) | Toption(_) | Tunion(_) => {
174 simp_ty_common(cfg, env, &ety_sub, &ety_sup)
175 }
176 Tany => unimplemented!("Subtype propositions involving `Tany` aren't implemented"),
177 },
179 // -- Super is prim ----------------------------------------------------
180 Tprim(p_sup) => match ety_sub.deref() {
181 Tprim(p_sub) => Ok(simp_prim(p_sub, p_sup)),
182 Toption(ty_sub_inner) if p_sup.is_tnull() => simp_ty(cfg, env, ty_sub_inner, &ety_sup),
183 Tnonnull
184 | Tfun(_)
185 | Tclass(_, _, _)
186 | Tvar(_)
187 | Tgeneric(_, _)
188 | Toption(_)
189 | Tunion(_) => simp_ty_common(cfg, env, &ety_sub, &ety_sup),
190 Tany => unimplemented!("Subtype propositions involving `Tany` aren't implemented"),
191 },
193 // -- Super is fun -----------------------------------------------------
194 Tfun(fn_sup) => match ety_sub.deref() {
195 Tfun(fn_sub) => simp_fun(cfg, env, fn_sub, fn_sup),
196 Tprim(_)
197 | Toption(_)
198 | Tnonnull
199 | Tclass(_, _, _)
200 | Tvar(_)
201 | Tgeneric(_, _)
202 | Tunion(_) => simp_ty_common(cfg, env, &ety_sub, &ety_sup),
203 Tany => unimplemented!("Subtype propositions involving `Tany` aren't implemented"),
204 },
206 // -- Super is class ---------------------------------------------------
207 Tclass(cn_sup, exact_sup, tp_sups) => {
208 match ety_sub.deref() {
209 Tclass(cn_sub, exact_sub, tp_subs) => simp_class(
210 cfg, env, cn_sub, exact_sub, tp_subs, cn_sup, exact_sup, tp_sups,
211 ),
212 // TODO[mjt] make a call on whether we bring
213 // string <: Stringish
214 // string , arraykey ,int, float, num <: XHPChild
215 // special-cases across
216 Tprim(_) => Ok(Prop::invalid(TypingError::Primary(Primary::Subtype))),
217 Tfun(_) | Toption(_) | Tnonnull | Tvar(_) | Tgeneric(_, _) | Tunion(_) => {
218 simp_ty_common(cfg, env, &ety_sub, &ety_sup)
219 }
220 Tany => unimplemented!("Subtype propositions involving `Tany` aren't implemented"),
221 }
222 }
224 // -- Tany should not be in subtyping ----------------------------------
225 Tany => unimplemented!("Subtype propositions involving `Tany` aren't implemented"),
226 }
227 }
229 fn simp_ty_common<R: Reason>(
230 cfg: &Config,
231 env: &mut Env<R>,
232 ty_sub: &Ty<R>,
233 ty_sup: &Ty<R>,
234 ) -> Result<Prop<R>> {
235 use Ty_::*;
236 let ty_sub = env.inf_env.resolve_ty(ty_sub);
237 let ty_sup = env.inf_env.resolve_ty(ty_sup);
238 match ty_sub.deref() {
239 Tvar(tv) => Ok(simp_tvar_ty(cfg, env, ty_sub.reason(), tv, &ty_sup)),
240 Tprim(p_sub) => {
241 if matches!(p_sub, Prim::Tvoid) {
242 // TODO[mjt]: implicit upper bound reason
243 let reason =
244 R::implicit_upper_bound(ty_sub.reason().pos().clone(), Symbol::new("?nonnull"));
245 let ty_mixed = Ty::mixed(reason);
246 simp_ty(cfg, env, &ty_mixed, &ty_sup)
247 } else {
248 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
249 }
250 }
251 Tunion(ty_subs) => simp_conjs_sub(cfg, env, ty_subs, &ty_sup),
252 // TODO[mjt] we aren't getting anywhere near HKTs so we should tidy up Tgeneric
253 Tgeneric(_, _) if cfg.ignore_generic_params => Ok(Prop::subtype_ty(ty_sub, ty_sup)),
254 Tgeneric(tp_name_sub, _) => {
255 simp_typaram_ty(cfg, env, (ty_sub.reason(), tp_name_sub), ty_sup)
256 }
257 Tclass(_, _, _) | Toption(_) | Tnonnull | Tfun(_) | Tany => {
258 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
259 }
260 }
261 }
263 /// Normalize the proposition `#1 <: T`
264 fn simp_tvar_ty<R: Reason>(
265 _cfg: &Config,
266 env: &mut Env<R>,
267 r_sub: &R,
268 tv_sub: &Tyvar,
269 ty_sup: &Ty<R>,
270 ) -> Prop<R> {
271 let ty_sup = solve::remove_tyvar_from_upper_bound(&mut env.inf_env, *tv_sub, ty_sup);
272 if env.inf_env.is_mixed(&ty_sup) {
273 // The tyvar occurred in the super type and removing it resulted in
274 // ty_sup collapsing to top
275 Prop::valid()
276 } else {
277 let ty_sub = Ty::var(r_sub.clone(), *tv_sub);
278 Prop::subtype_ty(ty_sub, ty_sup)
279 }
280 }
282 /// Normalize the proposition `#class<...> <: #class<...>`
283 fn simp_class<R: Reason>(
284 cfg: &Config,
285 env: &mut Env<R>,
286 cn_sub: &Positioned<TypeName, R::Pos>,
287 exact_sub: &Exact,
288 tp_subs: &[Ty<R>],
289 cn_sup: &Positioned<TypeName, R::Pos>,
290 exact_sup: &Exact,
291 tp_sups: &[Ty<R>],
292 ) -> Result<Prop<R>> {
293 let exact_match = match (exact_sub, exact_sup) {
294 (Exact::Nonexact, Exact::Exact) => false,
295 _ => true,
296 };
297 if cn_sub.id() == cn_sup.id() {
298 if tp_subs.is_empty() && tp_sups.is_empty() && exact_match {
299 Ok(Prop::valid())
300 } else {
301 let class_def_sub = env.decl_env.get_class(cn_sub.id())?;
302 // If class is final then exactness is superfluous
303 let is_final = class_def_sub.clone().map_or(false, |cls| cls.is_final());
304 if !(exact_match || is_final) {
305 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
306 } else if tp_subs.len() != tp_sups.len() {
307 // TODO[mjt] these are different cases due to the errors
308 // we want to raise
309 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
310 } else {
311 let variance_sub = if tp_subs.is_empty() {
312 vec![]
313 } else {
314 class_def_sub.map_or_else(
315 || vec![Variance::Invariant; tp_subs.len()],
316 |cls| cls.get_tparams().iter().map(|t| (t.variance)).collect_vec(),
317 )
318 };
319 simp_conjs_with_variance(cfg, env, cn_sub, variance_sub, tp_subs, tp_sups)
320 }
321 }
322 } else if !exact_match {
323 // class in subtype position is non-exact and class is supertype position is exact
324 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
325 } else {
326 let class_sub_opt = env.decl_env.get_class(cn_sub.id())?;
327 if let Some(class_sub) = class_sub_opt {
328 // is our class is subtype positition a declared subtype of the
329 // class in supertype position
330 match class_sub.get_ancestor(&cn_sup.id()) {
331 Some(_dty_sub) => {
332 // instantiate the declared type at the type parameters for
333 // the class in subtype position
334 // TODO[mjt] class localization
335 unimplemented!(
336 "Proposition normalization is not fully implemented for class types"
337 )
338 }
339 // None if class_sub.kind
340 None => Ok(Prop::invalid(TypingError::Primary(Primary::Subtype))),
341 }
342 } else {
343 // This should have been caught already, in the naming phase
344 // TODO[mjt] should we surface some of these implicit assumptions
345 // in the Result?
346 Ok(Prop::valid())
347 }
348 }
349 }
351 fn simp_conjs_with_variance<R: Reason>(
352 cfg: &Config,
353 env: &mut Env<R>,
354 cn: &Positioned<TypeName, R::Pos>,
355 variances: Vec<Variance>,
356 ty_subs: &[Ty<R>],
357 ty_sups: &[Ty<R>],
358 ) -> Result<Prop<R>> {
359 let mut prop = Prop::valid();
360 for (variance, ty_sub, ty_sup) in izip!(variances.iter(), ty_subs, ty_sups) {
361 let next = simp_with_variance(cfg, env, cn, variance, ty_sub, ty_sup)?;
362 if next.is_unsat() {
363 prop = next;
364 break;
365 } else {
366 prop = prop.conj(next);
367 }
368 }
369 Ok(prop)
370 }
372 fn simp_with_variance<R: Reason>(
373 cfg: &Config,
374 env: &mut Env<R>,
375 _cn: &Positioned<TypeName, R::Pos>,
376 variance: &Variance,
377 ty_sub: &Ty<R>,
378 ty_sup: &Ty<R>,
379 ) -> Result<Prop<R>> {
380 let mut this_ty = None;
381 std::mem::swap(&mut this_ty, &mut env.this_ty);
383 let p = match variance {
384 Variance::Covariant => simp_ty(cfg, env, ty_sub, ty_sup),
385 Variance::Contravariant =>
386 // TODO[mjt] update the reason on the supertype
387 {
388 simp_ty(cfg, env, ty_sup, ty_sub)
389 }
390 Variance::Invariant => {
391 // TODO[mjt] update the reason on the supertype
392 // TODO[mjt] if I use short-circuiting ? here will env be restored?
393 match simp_ty(cfg, env, ty_sub, ty_sup) {
394 Ok(p1) if !p1.is_unsat() => simp_ty(cfg, env, ty_sup, ty_sub).map(|p2| p1.conj(p2)),
395 p1_res => p1_res,
396 }
397 }
398 };
399 std::mem::swap(&mut this_ty, &mut env.this_ty);
400 p
401 }
403 /// Normalize the proposition `prim <: prim`
404 /// TODO[mjt]: move to or wrap `subtype` test for prim impl?
405 fn simp_prim<R: Reason>(prim_sub: &Prim, prim_sup: &Prim) -> Prop<R> {
406 if prim_sub == prim_sup {
407 Prop::valid()
408 } else {
409 use Prim::*;
410 match (prim_sub, prim_sup) {
411 (Tint | Tfloat, Tnum) => Prop::valid(),
412 (Tint | Tstring, Tarraykey) => Prop::valid(),
413 _ => Prop::invalid(TypingError::Primary(Primary::Subtype)),
414 }
415 }
416 }
418 /// Normalize the propostion `fn <: fn`
419 fn simp_fun<R: Reason>(
420 _cfg: &Config,
421 _env: &mut Env<R>,
422 _fn_sub: &FunType<R>,
423 _fn_sup: &FunType<R>,
424 ) -> Result<Prop<R>> {
425 unimplemented!("Subtype propositions involving function types aren't implemented")
426 }
428 /// Normalize the proposition `#T <: U` where `#T` is a generic type parameter
429 fn simp_typaram_ty<R: Reason>(
430 cfg: &Config,
431 env: &mut Env<R>,
432 tp_sub: (&R, &TypeName),
433 ty_sup: Ty<R>,
434 ) -> Result<Prop<R>> {
435 match env
436 .visited_goals
437 .try_add_visited_generic_sub(tp_sub.1.clone(), &ty_sup)
438 {
439 // We've seen this type param before so must have gone round a
440 // cycle so fail
441 // TODO[mjt] do we want indicate failure here? Doesn't a cycle indicate
442 // something is wrong?
443 GoalResult::AlreadyVisited => Ok(Prop::invalid(TypingError::Primary(Primary::Subtype))),
445 // Otherwise, we collect all the upper bounds ("as" constraints) on
446 // the generic parameter, and check each of these in turn against
447 // ty_super until one of them succeeds
448 GoalResult::NewGoal => {
449 let bounds = env
450 .tp_env
451 .upper_bounds(tp_sub.1)
452 .map_or(HashSet::default(), |bs| bs.clone());
453 let p = if bounds.is_empty() {
454 let reason =
455 R::implicit_upper_bound(tp_sub.0.pos().clone(), Symbol::new("?nonnull"));
456 let ty_mixed = Ty::mixed(reason);
457 simp_ty(cfg, env, &ty_mixed, &ty_sup)?
458 } else {
459 simp_disjs_sub(cfg, env, bounds.iter(), &ty_sup)?
460 };
461 // TODO[mjt] we check this here to get a nicer message, presumably?
462 if p.is_unsat() {
463 Ok(Prop::invalid(TypingError::Primary(Primary::Subtype)))
464 } else {
465 Ok(p)
466 }
467 }
468 }
469 }
471 /// Normalize the proposition `T <: #U` where `#U` is a generic type parameter
472 fn simp_ty_typaram<R: Reason>(
473 cfg: &Config,
474 env: &mut Env<R>,
475 ty_sub: Ty<R>,
476 tp_sup: (&R, &TypeName),
477 ) -> Result<Prop<R>> {
478 match env
479 .visited_goals
480 .try_add_visited_generic_sup(tp_sup.1.clone(), &ty_sub)
481 {
482 // We've seen this type param before so must have gone round a
483 // cycle so fail
484 GoalResult::AlreadyVisited => Ok(Prop::invalid(TypingError::Primary(Primary::Subtype))),
486 // Collect all the lower bounds ("super" constraints) on the
487 // generic parameter, and check ty_sub against each of them in turn
488 // until one of them succeeds
489 GoalResult::NewGoal => {
490 let bounds = env
491 .tp_env
492 .lower_bounds(tp_sup.1)
493 .map_or(HashSet::default(), |bs| bs.clone());
494 let prop = simp_disjs_sup(cfg, env, &ty_sub, bounds.iter())?;
495 if prop.is_valid() {
496 Ok(prop)
497 } else {
498 let ty_sup = Ty::generic(tp_sup.0.clone(), tp_sup.1.clone(), vec![]);
499 Ok(prop.disj(
500 Prop::subtype_ty(ty_sub, ty_sup),
501 TypingError::Primary(Primary::Subtype),
502 ))
503 }
504 }
505 }
506 }
508 /// Normalize the propostion `T1 <: U /\ T2 <: U`
509 fn simp_conj_sub<R: Reason>(
510 cfg: &Config,
511 env: &mut Env<R>,
512 ty_sub1: &Ty<R>,
513 ty_sub2: &Ty<R>,
514 ty_sup: &Ty<R>,
515 ) -> Result<Prop<R>> {
516 let p1 = simp_ty(cfg, env, ty_sub1, ty_sup)?;
517 if p1.is_unsat() {
518 Ok(p1)
519 } else {
520 let p2 = simp_ty(cfg, env, ty_sub2, ty_sup)?;
521 Ok(p1.conj(p2))
522 }
523 }
525 /// Normalize the proposition `T <: U1 \/ T <: U2`
526 fn simp_disj_sup<R: Reason>(
527 cfg: &Config,
528 env: &mut Env<R>,
529 ty_sub: &Ty<R>,
530 ty_sup1: &Ty<R>,
531 ty_sup2: &Ty<R>,
532 ) -> Result<Prop<R>> {
533 let p1 = simp_ty(cfg, env, ty_sub, ty_sup1)?;
534 if p1.is_valid() {
535 Ok(p1)
536 } else {
537 let p2 = simp_ty(cfg, env, ty_sub, ty_sup2)?;
538 Ok(p1.conj(p2))
539 }
540 }
542 /// Normalize the proposition `T1 <: U /\ T2 <: U /\ ... /\ Tn <: U`
543 fn simp_conjs_sub<'a, R, I>(
544 cfg: &Config,
545 env: &mut Env<R>,
546 ty_subs: I,
547 ty_sup: &Ty<R>,
548 ) -> Result<Prop<R>>
549 where
550 R: Reason,
551 I: IntoIterator<Item = &'a Ty<R>>,
552 {
553 let mut prop = Prop::valid();
554 for ty_sub in ty_subs {
555 let next = simp_ty(cfg, env, ty_sub, ty_sup)?;
556 if next.is_unsat() {
557 prop = next;
558 break;
559 } else {
560 prop = prop.conj(next);
561 }
562 }
563 Ok(prop)
564 }
566 /// Normalize the proposition `T <: U1 \/ T <: U2`
567 fn simp_disjs_sup<'a, R, I>(
568 cfg: &Config,
569 env: &mut Env<R>,
570 ty_sub: &Ty<R>,
571 ty_sups: I,
572 ) -> Result<Prop<R>>
573 where
574 R: Reason,
575 I: IntoIterator<Item = &'a Ty<R>>,
576 {
577 let mut prop = Prop::invalid(TypingError::Primary(Primary::Subtype));
578 for ty_sup in ty_sups {
579 let next = simp_ty(cfg, env, ty_sub, ty_sup)?;
580 if next.is_valid() {
581 prop = next;
582 break;
583 } else {
584 prop = prop.disj(next, TypingError::Primary(Primary::Subtype));
585 }
586 }
587 Ok(prop)
588 }
590 /// Normalize the proposition `T <: U1 \/ T <: U2`
591 fn simp_disjs_sub<'a, R, I>(
592 cfg: &Config,
593 env: &mut Env<R>,
594 ty_subs: I,
595 ty_sup: &Ty<R>,
596 ) -> Result<Prop<R>>
597 where
598 R: Reason,
599 I: IntoIterator<Item = &'a Ty<R>>,
600 {
601 let mut prop = Prop::invalid(TypingError::Primary(Primary::Subtype));
602 for ty_sub in ty_subs {
603 let next = simp_ty(cfg, env, ty_sub, ty_sup)?;
604 if next.is_valid() {
605 prop = next;
606 break;
607 } else {
608 prop = prop.disj(next, TypingError::Primary(Primary::Subtype));
609 }
610 }
611 Ok(prop)
612 }
614 #[cfg(test)]
615 mod tests {
616 use super::*;
617 use ty::{prop::PropF, reason::NReason};
618 use utils::core::IdentGen;
620 #[test]
621 fn test_tvar_ty() {
622 let mut env = Env::default();
623 let cfg = Config::default();
624 let gen = IdentGen::new();
626 let tv_0: Tyvar = gen.make().into();
628 let also_tv_0: Tyvar = tv_0.clone();
629 let r_tv_0 = NReason::none();
630 let ty_v0 = Ty::var(NReason::none(), tv_0);
632 // #0 <: #0 => true
633 let p0 = simp_tvar_ty(&cfg, &mut env, &r_tv_0, &also_tv_0, &ty_v0);
634 assert!(p0.is_valid());
636 // #0 <: int => #0 <: int
637 let ty_int = Ty::int(NReason::none());
638 let p1 = simp_tvar_ty(&cfg, &mut env, &r_tv_0, &also_tv_0, &ty_int);
639 assert!(matches!(p1.deref(), PropF::Subtype(_, _)));
641 // #0 <: int | 0 => true
642 let ty_int_or_tv0 = Ty::union(NReason::none(), vec![ty_v0.clone(), ty_int.clone()]);
643 let p2 = simp_tvar_ty(&cfg, &mut env, &r_tv_0, &also_tv_0, &ty_int_or_tv0);
644 assert!(p2.is_valid());
646 // #0 <: (int | (int | 0)) => true
647 let ty_int_or_int_or_tv0 = Ty::union(NReason::none(), vec![ty_int.clone(), ty_int_or_tv0]);
648 let p3 = simp_tvar_ty(&cfg, &mut env, &r_tv_0, &also_tv_0, &ty_int_or_int_or_tv0);
649 assert!(p3.is_valid());
651 // #0 <: ?#0 => true
652 let ty_v0_opt = Ty::option(NReason::none(), ty_v0.clone());
653 let p4 = simp_tvar_ty(&cfg, &mut env, &r_tv_0, &also_tv_0, &ty_v0_opt);
654 assert!(p4.is_valid());
655 }
657 #[test]
658 fn test_prim() {
659 let mut env = Env::default();
660 let cfg = Config::default();
662 // Subtypes of arraykey
663 let ty_arraykey = Ty::arraykey(NReason::none());
664 // int <: arraykey
665 let ty_int = Ty::int(NReason::none());
666 assert!(
667 simp_ty(&cfg, &mut env, &ty_int, &ty_arraykey)
668 .unwrap()
669 .is_valid()
670 );
671 // string <: arraykey
672 let ty_string = Ty::string(NReason::none());
673 assert!(
674 simp_ty(&cfg, &mut env, &ty_string, &ty_arraykey)
675 .unwrap()
676 .is_valid()
677 );
679 // Subtypes of num
680 let ty_num = Ty::num(NReason::none());
681 // int <: num
682 assert!(
683 simp_ty(&cfg, &mut env, &ty_int, &ty_num)
684 .unwrap()
685 .is_valid()
686 );
687 // float <: num
688 let ty_float = Ty::float(NReason::none());
689 assert!(
690 simp_ty(&cfg, &mut env, &ty_float, &ty_num)
691 .unwrap()
692 .is_valid()
693 );
695 // num === (int | float)
696 let ty_num_as_union = Ty::union(NReason::none(), vec![ty_int.clone(), ty_float.clone()]);
697 assert!(
698 simp_ty(&cfg, &mut env, &ty_num, &ty_num_as_union)
699 .unwrap()
700 .is_valid()
701 );
703 // Subtypes of nonnull
704 let ty_nonnull = Ty::nonnull(NReason::none());
705 // int <: nonnull
706 assert!(
707 simp_ty(&cfg, &mut env, &ty_int, &ty_nonnull)
708 .unwrap()
709 .is_valid()
710 );
711 // float <: nonnull
712 assert!(
713 simp_ty(&cfg, &mut env, &ty_int, &ty_nonnull)
714 .unwrap()
715 .is_valid()
716 );
717 // string <: nonnull
718 assert!(
719 simp_ty(&cfg, &mut env, &ty_int, &ty_nonnull)
720 .unwrap()
721 .is_valid()
722 );
723 // null </: nonnull
724 let ty_null = Ty::null(NReason::none());
725 assert!(
726 simp_ty(&cfg, &mut env, &ty_null, &ty_nonnull)
727 .unwrap()
728 .is_unsat()
729 );
730 // void </: nonnull
731 let ty_void = Ty::void(NReason::none());
732 assert!(
733 simp_ty(&cfg, &mut env, &ty_void, &ty_nonnull)
734 .unwrap()
735 .is_unsat()
736 );
737 }
739 #[test]
740 fn test_disjs_sub() {
741 let mut env = Env::default();
742 let cfg = Config::default();
743 let ty_num = Ty::num(NReason::none());
744 let ty_subs_all_ok = vec![Ty::int(NReason::none()), Ty::float(NReason::none())];
745 let ty_subs_one_ok = vec![Ty::string(NReason::none()), Ty::float(NReason::none())];
746 let ty_subs_none_ok = vec![Ty::string(NReason::none()), Ty::null(NReason::none())];
747 assert!(
748 simp_disjs_sub(&cfg, &mut env, ty_subs_all_ok.iter(), &ty_num)
749 .unwrap()
750 .is_valid()
751 );
752 assert!(
753 simp_disjs_sub(&cfg, &mut env, ty_subs_one_ok.iter(), &ty_num)
754 .unwrap()
755 .is_valid()
756 );
757 assert!(
758 simp_disjs_sub(&cfg, &mut env, ty_subs_none_ok.iter(), &ty_num)
759 .unwrap()
760 .is_unsat()
761 );
762 }
764 #[test]
765 fn test_ty_param_sup() {
766 let mut env = Env::default();
767 let cfg = Config::default();
768 let tp_name = TypeName::new("T");
769 let tp_reason = NReason::none();
770 let ty_int = Ty::int(NReason::none());
771 let ty_arraykey = Ty::arraykey(NReason::none());
773 env.tp_env.add_upper_bound(tp_name.clone(), ty_int);
774 // subtyping our typaram against arraykey will:
775 // add it to the visited supertypes
776 // check that we can subtype all existing upper bounds against it
777 // since our only upper bound is int, this is int <: arraykey
778 assert!(
779 simp_typaram_ty(&cfg, &mut env, (&tp_reason, &tp_name), ty_arraykey)
780 .unwrap()
781 .is_valid()
782 );
783 }
785 #[test]
786 fn test_ty_param_sub() {
787 let mut env = Env::default();
788 let cfg = Config::default();
789 let tp_name = TypeName::new("T");
790 let tp_reason = NReason::none();
791 let ty_int = Ty::int(NReason::none());
792 let ty_arraykey = Ty::arraykey(NReason::none());
794 env.tp_env.add_lower_bound(tp_name.clone(), ty_arraykey);
795 assert!(
796 simp_ty_typaram(&cfg, &mut env, ty_int, (&tp_reason, &tp_name))
797 .unwrap()
798 .is_valid()
799 );
800 }
801 }