1use std::{cell::RefCell, fmt, iter};
2
3use flux_common::{bug, dbg, tracked_span_assert_eq, tracked_span_bug, tracked_span_dbg_assert_eq};
4use flux_config::{self as config, InferOpts, OverflowMode};
5use flux_macros::{TypeFoldable, TypeVisitable};
6use flux_middle::{
7 FixpointQueryKind,
8 def_id::MaybeExternId,
9 global_env::GlobalEnv,
10 queries::{QueryErr, QueryResult},
11 query_bug,
12 rty::{
13 self, AliasKind, AliasTy, BaseTy, Binder, BoundVariableKinds, CoroutineObligPredicate,
14 Ctor, ESpan, EVid, EarlyBinder, Expr, ExprKind, FieldProj, GenericArg, HoleKind, InferMode,
15 Lambda, List, Loc, Mutability, Name, Path, PolyVariant, PtrKind, RefineArgs, RefineArgsExt,
16 Region, Sort, Ty, TyCtor, TyKind, Var,
17 canonicalize::{Hoister, HoisterDelegate},
18 fold::TypeFoldable,
19 },
20};
21use itertools::{Itertools, izip};
22use rustc_hir::def_id::{DefId, LocalDefId};
23use rustc_macros::extension;
24use rustc_middle::{
25 mir::BasicBlock,
26 ty::{TyCtxt, Variance},
27};
28use rustc_span::Span;
29
30use crate::{
31 evars::{EVarState, EVarStore},
32 fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarEncoding, KVarGen},
33 projections::NormalizeExt as _,
34 refine_tree::{Cursor, Marker, RefineTree, Scope},
35};
36
37pub type InferResult<T = ()> = std::result::Result<T, InferErr>;
38
39#[derive(PartialEq, Eq, Clone, Copy, Hash)]
40pub struct Tag {
41 pub reason: ConstrReason,
42 pub src_span: Span,
43 pub dst_span: Option<ESpan>,
44}
45
46impl Tag {
47 pub fn new(reason: ConstrReason, span: Span) -> Self {
48 Self { reason, src_span: span, dst_span: None }
49 }
50
51 pub fn with_dst(self, dst_span: Option<ESpan>) -> Self {
52 Self { dst_span, ..self }
53 }
54}
55
56#[derive(PartialEq, Eq, Clone, Copy, Hash, Debug)]
57pub enum SubtypeReason {
58 Input,
59 Output,
60 Requires,
61 Ensures,
62}
63
64#[derive(PartialEq, Eq, Clone, Copy, Hash, Debug)]
65pub enum ConstrReason {
66 Call,
67 Assign,
68 Ret,
69 Fold,
70 FoldLocal,
71 Predicate,
72 Assert(&'static str),
73 Div,
74 Rem,
75 Goto(BasicBlock),
76 Overflow,
77 Underflow,
78 Subtype(SubtypeReason),
79 Other,
80}
81
82pub struct InferCtxtRoot<'genv, 'tcx> {
83 pub genv: GlobalEnv<'genv, 'tcx>,
84 inner: RefCell<InferCtxtInner>,
85 refine_tree: RefineTree,
86 opts: InferOpts,
87}
88
89pub struct InferCtxtRootBuilder<'a, 'genv, 'tcx> {
90 genv: GlobalEnv<'genv, 'tcx>,
91 opts: InferOpts,
92 params: Vec<(Var, Sort)>,
93 infcx: &'a rustc_infer::infer::InferCtxt<'tcx>,
94 dummy_kvars: bool,
95}
96
97#[extension(pub trait GlobalEnvExt<'genv, 'tcx>)]
98impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> {
99 fn infcx_root<'a>(
100 self,
101 infcx: &'a rustc_infer::infer::InferCtxt<'tcx>,
102 opts: InferOpts,
103 ) -> InferCtxtRootBuilder<'a, 'genv, 'tcx> {
104 InferCtxtRootBuilder { genv: self, infcx, params: vec![], opts, dummy_kvars: false }
105 }
106}
107
108impl<'genv, 'tcx> InferCtxtRootBuilder<'_, 'genv, 'tcx> {
109 pub fn with_dummy_kvars(mut self) -> Self {
110 self.dummy_kvars = true;
111 self
112 }
113
114 pub fn with_const_generics(mut self, def_id: DefId) -> QueryResult<Self> {
115 self.params.extend(
116 self.genv
117 .generics_of(def_id)?
118 .const_params(self.genv)?
119 .into_iter()
120 .map(|(pcst, sort)| (Var::ConstGeneric(pcst), sort)),
121 );
122 Ok(self)
123 }
124
125 pub fn with_refinement_generics(
126 mut self,
127 def_id: DefId,
128 args: &[GenericArg],
129 ) -> QueryResult<Self> {
130 for (index, param) in self
131 .genv
132 .refinement_generics_of(def_id)?
133 .iter_own_params()
134 .enumerate()
135 {
136 let param = param.instantiate(self.genv.tcx(), args, &[]);
137 let sort = param.sort.normalize_sorts(def_id, self.genv, self.infcx)?;
138
139 let var =
140 Var::EarlyParam(rty::EarlyReftParam { index: index as u32, name: param.name });
141 self.params.push((var, sort));
142 }
143 Ok(self)
144 }
145
146 pub fn identity_for_item(mut self, def_id: DefId) -> QueryResult<Self> {
147 self = self.with_const_generics(def_id)?;
148 let offset = self.params.len();
149 self.genv.refinement_generics_of(def_id)?.fill_item(
150 self.genv,
151 &mut self.params,
152 &mut |param, index| {
153 let index = (index - offset) as u32;
154 let param = param.instantiate_identity();
155 let sort = param.sort.normalize_sorts(def_id, self.genv, self.infcx)?;
156
157 let var = Var::EarlyParam(rty::EarlyReftParam { index, name: param.name });
158 Ok((var, sort))
159 },
160 )?;
161 Ok(self)
162 }
163
164 pub fn build(self) -> QueryResult<InferCtxtRoot<'genv, 'tcx>> {
165 Ok(InferCtxtRoot {
166 genv: self.genv,
167 inner: RefCell::new(InferCtxtInner::new(self.dummy_kvars)),
168 refine_tree: RefineTree::new(self.params),
169 opts: self.opts,
170 })
171 }
172}
173
174impl<'genv, 'tcx> InferCtxtRoot<'genv, 'tcx> {
175 pub fn infcx<'a>(
176 &'a mut self,
177 def_id: DefId,
178 region_infcx: &'a rustc_infer::infer::InferCtxt<'tcx>,
179 ) -> InferCtxt<'a, 'genv, 'tcx> {
180 InferCtxt {
181 genv: self.genv,
182 region_infcx,
183 def_id,
184 cursor: self.refine_tree.cursor_at_root(),
185 inner: &self.inner,
186 check_overflow: self.opts.check_overflow,
187 }
188 }
189
190 pub fn fresh_kvar_in_scope(
191 &self,
192 binders: &[BoundVariableKinds],
193 scope: &Scope,
194 encoding: KVarEncoding,
195 ) -> Expr {
196 let inner = &mut *self.inner.borrow_mut();
197 inner.kvars.fresh(binders, scope.iter(), encoding)
198 }
199
200 pub fn execute_fixpoint_query(
201 self,
202 cache: &mut FixQueryCache,
203 def_id: MaybeExternId,
204 kind: FixpointQueryKind,
205 ) -> QueryResult<Vec<Tag>> {
206 let inner = self.inner.into_inner();
207 let kvars = inner.kvars;
208 let evars = inner.evars;
209
210 let ext = kind.ext();
211
212 let mut refine_tree = self.refine_tree;
213
214 refine_tree.replace_evars(&evars).unwrap();
215
216 if config::dump_constraint() {
217 dbg::dump_item_info(self.genv.tcx(), def_id.resolved_id(), ext, &refine_tree).unwrap();
218 }
219 refine_tree.simplify(self.genv);
220 if config::dump_constraint() {
221 let simp_ext = format!("simp.{ext}");
222 dbg::dump_item_info(self.genv.tcx(), def_id.resolved_id(), simp_ext, &refine_tree)
223 .unwrap();
224 }
225
226 let mut fcx = FixpointCtxt::new(self.genv, def_id, kvars);
227 let cstr = refine_tree.into_fixpoint(&mut fcx)?;
228
229 let backend = match self.opts.solver {
230 flux_config::SmtSolver::Z3 => liquid_fixpoint::SmtSolver::Z3,
231 flux_config::SmtSolver::CVC5 => liquid_fixpoint::SmtSolver::CVC5,
232 };
233
234 fcx.check(cache, cstr, kind, self.opts.scrape_quals, backend)
235 }
236
237 pub fn split(self) -> (RefineTree, KVarGen) {
238 (self.refine_tree, self.inner.into_inner().kvars)
239 }
240}
241
242pub struct InferCtxt<'infcx, 'genv, 'tcx> {
243 pub genv: GlobalEnv<'genv, 'tcx>,
244 pub region_infcx: &'infcx rustc_infer::infer::InferCtxt<'tcx>,
245 pub def_id: DefId,
246 pub check_overflow: OverflowMode,
247 cursor: Cursor<'infcx>,
248 inner: &'infcx RefCell<InferCtxtInner>,
249}
250
251struct InferCtxtInner {
252 kvars: KVarGen,
253 evars: EVarStore,
254}
255
256impl InferCtxtInner {
257 fn new(dummy_kvars: bool) -> Self {
258 Self { kvars: KVarGen::new(dummy_kvars), evars: Default::default() }
259 }
260}
261
262impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
263 pub fn at(&mut self, span: Span) -> InferCtxtAt<'_, 'infcx, 'genv, 'tcx> {
264 InferCtxtAt { infcx: self, span }
265 }
266
267 pub fn instantiate_refine_args(
268 &mut self,
269 callee_def_id: DefId,
270 args: &[rty::GenericArg],
271 ) -> InferResult<List<Expr>> {
272 Ok(RefineArgs::for_item(self.genv, callee_def_id, |param, _| {
273 let param = param.instantiate(self.genv.tcx(), args, &[]);
274 Ok(self.fresh_infer_var(¶m.sort, param.mode))
275 })?)
276 }
277
278 pub fn instantiate_generic_args(&mut self, args: &[GenericArg]) -> Vec<GenericArg> {
279 args.iter()
280 .map(|a| a.replace_holes(|binders, kind| self.fresh_infer_var_for_hole(binders, kind)))
281 .collect_vec()
282 }
283
284 pub fn fresh_infer_var(&self, sort: &Sort, mode: InferMode) -> Expr {
285 match mode {
286 InferMode::KVar => {
287 let fsort = sort.expect_func().expect_mono();
288 let vars = fsort.inputs().iter().cloned().map_into().collect();
289 let kvar = self.fresh_kvar(&[vars], KVarEncoding::Single);
290 Expr::abs(Lambda::bind_with_fsort(kvar, fsort))
291 }
292 InferMode::EVar => self.fresh_evar(),
293 }
294 }
295
296 pub fn fresh_infer_var_for_hole(
297 &mut self,
298 binders: &[BoundVariableKinds],
299 kind: HoleKind,
300 ) -> Expr {
301 match kind {
302 HoleKind::Pred => self.fresh_kvar(binders, KVarEncoding::Conj),
303 HoleKind::Expr(_) => {
304 self.fresh_evar()
308 }
309 }
310 }
311
312 pub fn fresh_kvar_in_scope(
314 &self,
315 binders: &[BoundVariableKinds],
316 scope: &Scope,
317 encoding: KVarEncoding,
318 ) -> Expr {
319 let inner = &mut *self.inner.borrow_mut();
320 inner.kvars.fresh(binders, scope.iter(), encoding)
321 }
322
323 pub fn fresh_kvar(&self, binders: &[BoundVariableKinds], encoding: KVarEncoding) -> Expr {
325 let inner = &mut *self.inner.borrow_mut();
326 inner.kvars.fresh(binders, self.cursor.vars(), encoding)
327 }
328
329 fn fresh_evar(&self) -> Expr {
330 let evars = &mut self.inner.borrow_mut().evars;
331 Expr::evar(evars.fresh(self.cursor.marker()))
332 }
333
334 pub fn unify_exprs(&self, a: &Expr, b: &Expr) {
335 if a.has_evars() {
336 return;
337 }
338 let evars = &mut self.inner.borrow_mut().evars;
339 if let ExprKind::Var(Var::EVar(evid)) = b.kind()
340 && let EVarState::Unsolved(marker) = evars.get(*evid)
341 && !marker.has_free_vars(a)
342 {
343 evars.solve(*evid, a.clone());
344 }
345 }
346
347 fn enter_exists<T, U>(
348 &mut self,
349 t: &Binder<T>,
350 f: impl FnOnce(&mut InferCtxt<'_, 'genv, 'tcx>, T) -> U,
351 ) -> U
352 where
353 T: TypeFoldable,
354 {
355 self.ensure_resolved_evars(|infcx| {
356 let t = t.replace_bound_refts_with(|sort, mode, _| infcx.fresh_infer_var(sort, mode));
357 Ok(f(infcx, t))
358 })
359 .unwrap()
360 }
361
362 pub fn push_evar_scope(&mut self) {
367 self.inner.borrow_mut().evars.push_scope();
368 }
369
370 pub fn pop_evar_scope(&mut self) -> InferResult {
373 self.inner
374 .borrow_mut()
375 .evars
376 .pop_scope()
377 .map_err(InferErr::UnsolvedEvar)
378 }
379
380 pub fn ensure_resolved_evars<R>(
382 &mut self,
383 f: impl FnOnce(&mut Self) -> InferResult<R>,
384 ) -> InferResult<R> {
385 self.push_evar_scope();
386 let r = f(self)?;
387 self.pop_evar_scope()?;
388 Ok(r)
389 }
390
391 pub fn fully_resolve_evars<T: TypeFoldable>(&self, t: &T) -> T {
392 self.inner.borrow().evars.replace_evars(t).unwrap()
393 }
394
395 pub fn tcx(&self) -> TyCtxt<'tcx> {
396 self.genv.tcx()
397 }
398
399 pub fn cursor(&self) -> &Cursor<'infcx> {
400 &self.cursor
401 }
402}
403
404impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
406 pub fn change_item<'a>(
407 &'a mut self,
408 def_id: LocalDefId,
409 region_infcx: &'a rustc_infer::infer::InferCtxt<'tcx>,
410 ) -> InferCtxt<'a, 'genv, 'tcx> {
411 InferCtxt {
412 def_id: def_id.to_def_id(),
413 cursor: self.cursor.branch(),
414 region_infcx,
415 ..*self
416 }
417 }
418
419 pub fn move_to(&mut self, marker: &Marker, clear_children: bool) -> InferCtxt<'_, 'genv, 'tcx> {
420 InferCtxt {
421 cursor: self
422 .cursor
423 .move_to(marker, clear_children)
424 .unwrap_or_else(|| tracked_span_bug!()),
425 ..*self
426 }
427 }
428
429 pub fn branch(&mut self) -> InferCtxt<'_, 'genv, 'tcx> {
430 InferCtxt { cursor: self.cursor.branch(), ..*self }
431 }
432
433 pub fn define_var(&mut self, sort: &Sort) -> Name {
434 self.cursor.define_var(sort)
435 }
436
437 pub fn check_pred(&mut self, pred: impl Into<Expr>, tag: Tag) {
438 self.cursor.check_pred(pred, tag);
439 }
440
441 pub fn assume_pred(&mut self, pred: impl Into<Expr>) {
442 self.cursor.assume_pred(pred);
443 }
444
445 pub fn unpack(&mut self, ty: &Ty) -> Ty {
446 self.hoister(false).hoist(ty)
447 }
448
449 pub fn marker(&self) -> Marker {
450 self.cursor.marker()
451 }
452
453 pub fn hoister(
454 &mut self,
455 assume_invariants: bool,
456 ) -> Hoister<Unpacker<'_, 'infcx, 'genv, 'tcx>> {
457 Hoister::with_delegate(Unpacker { infcx: self, assume_invariants }).transparent()
458 }
459
460 pub fn assume_invariants(&mut self, ty: &Ty) {
461 self.cursor
462 .assume_invariants(self.genv.tcx(), ty, self.check_overflow);
463 }
464
465 fn check_impl(&mut self, pred1: impl Into<Expr>, pred2: impl Into<Expr>, tag: Tag) {
466 self.cursor.check_impl(pred1, pred2, tag);
467 }
468}
469
470pub struct Unpacker<'a, 'infcx, 'genv, 'tcx> {
471 infcx: &'a mut InferCtxt<'infcx, 'genv, 'tcx>,
472 assume_invariants: bool,
473}
474
475impl HoisterDelegate for Unpacker<'_, '_, '_, '_> {
476 fn hoist_exists(&mut self, ty_ctor: &TyCtor) -> Ty {
477 let ty =
478 ty_ctor.replace_bound_refts_with(|sort, _, _| Expr::fvar(self.infcx.define_var(sort)));
479 if self.assume_invariants {
480 self.infcx.assume_invariants(&ty);
481 }
482 ty
483 }
484
485 fn hoist_constr(&mut self, pred: Expr) {
486 self.infcx.assume_pred(pred);
487 }
488}
489
490impl std::fmt::Debug for InferCtxt<'_, '_, '_> {
491 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
492 std::fmt::Debug::fmt(&self.cursor, f)
493 }
494}
495
496#[derive(Debug)]
497pub struct InferCtxtAt<'a, 'infcx, 'genv, 'tcx> {
498 pub infcx: &'a mut InferCtxt<'infcx, 'genv, 'tcx>,
499 pub span: Span,
500}
501
502impl<'genv, 'tcx> InferCtxtAt<'_, '_, 'genv, 'tcx> {
503 fn tag(&self, reason: ConstrReason) -> Tag {
504 Tag::new(reason, self.span)
505 }
506
507 pub fn check_pred(&mut self, pred: impl Into<Expr>, reason: ConstrReason) {
508 let tag = self.tag(reason);
509 self.infcx.check_pred(pred, tag);
510 }
511
512 pub fn check_non_closure_clauses(
513 &mut self,
514 clauses: &[rty::Clause],
515 reason: ConstrReason,
516 ) -> InferResult {
517 for clause in clauses {
518 if let rty::ClauseKind::Projection(projection_pred) = clause.kind_skipping_binder() {
519 let impl_elem = BaseTy::projection(projection_pred.projection_ty)
520 .to_ty()
521 .normalize_projections(self)?;
522 let term = projection_pred.term.to_ty().normalize_projections(self)?;
523
524 self.subtyping(&impl_elem, &term, reason)?;
526 self.subtyping(&term, &impl_elem, reason)?;
527 }
528 }
529 Ok(())
530 }
531
532 pub fn subtyping_with_env(
535 &mut self,
536 env: &mut impl LocEnv,
537 a: &Ty,
538 b: &Ty,
539 reason: ConstrReason,
540 ) -> InferResult {
541 let mut sub = Sub::new(env, reason, self.span);
542 sub.tys(self.infcx, a, b)
543 }
544
545 pub fn subtyping(
550 &mut self,
551 a: &Ty,
552 b: &Ty,
553 reason: ConstrReason,
554 ) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
555 let mut env = DummyEnv;
556 let mut sub = Sub::new(&mut env, reason, self.span);
557 sub.tys(self.infcx, a, b)?;
558 Ok(sub.obligations)
559 }
560
561 pub fn subtyping_generic_args(
562 &mut self,
563 variance: Variance,
564 a: &GenericArg,
565 b: &GenericArg,
566 reason: ConstrReason,
567 ) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
568 let mut env = DummyEnv;
569 let mut sub = Sub::new(&mut env, reason, self.span);
570 sub.generic_args(self.infcx, variance, a, b)?;
571 Ok(sub.obligations)
572 }
573
574 pub fn check_constructor(
578 &mut self,
579 variant: EarlyBinder<PolyVariant>,
580 generic_args: &[GenericArg],
581 fields: &[Ty],
582 reason: ConstrReason,
583 ) -> InferResult<Ty> {
584 let ret = self.ensure_resolved_evars(|this| {
585 let generic_args = this.instantiate_generic_args(generic_args);
587
588 let variant = variant
589 .instantiate(this.tcx(), &generic_args, &[])
590 .replace_bound_refts_with(|sort, mode, _| this.fresh_infer_var(sort, mode));
591
592 for (actual, formal) in iter::zip(fields, variant.fields()) {
594 this.subtyping(actual, formal, reason)?;
595 }
596
597 for require in &variant.requires {
599 this.check_pred(require, ConstrReason::Fold);
600 }
601
602 Ok(variant.ret())
603 })?;
604 Ok(self.fully_resolve_evars(&ret))
605 }
606
607 pub fn ensure_resolved_evars<R>(
608 &mut self,
609 f: impl FnOnce(&mut InferCtxtAt<'_, '_, 'genv, 'tcx>) -> InferResult<R>,
610 ) -> InferResult<R> {
611 self.infcx
612 .ensure_resolved_evars(|infcx| f(&mut infcx.at(self.span)))
613 }
614}
615
616impl<'a, 'genv, 'tcx> std::ops::Deref for InferCtxtAt<'_, 'a, 'genv, 'tcx> {
617 type Target = InferCtxt<'a, 'genv, 'tcx>;
618
619 fn deref(&self) -> &Self::Target {
620 self.infcx
621 }
622}
623
624impl std::ops::DerefMut for InferCtxtAt<'_, '_, '_, '_> {
625 fn deref_mut(&mut self) -> &mut Self::Target {
626 self.infcx
627 }
628}
629
630#[derive(TypeVisitable, TypeFoldable)]
634pub(crate) enum TypeTrace {
635 Types(Ty, Ty),
636 BaseTys(BaseTy, BaseTy),
637}
638
639#[expect(dead_code, reason = "we use this for debugging some time")]
640impl TypeTrace {
641 fn tys(a: &Ty, b: &Ty) -> Self {
642 Self::Types(a.clone(), b.clone())
643 }
644
645 fn btys(a: &BaseTy, b: &BaseTy) -> Self {
646 Self::BaseTys(a.clone(), b.clone())
647 }
648}
649
650impl fmt::Debug for TypeTrace {
651 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
652 match self {
653 TypeTrace::Types(a, b) => write!(f, "{a:?} - {b:?}"),
654 TypeTrace::BaseTys(a, b) => write!(f, "{a:?} - {b:?}"),
655 }
656 }
657}
658
659pub trait LocEnv {
660 fn ptr_to_ref(
661 &mut self,
662 infcx: &mut InferCtxtAt,
663 reason: ConstrReason,
664 re: Region,
665 path: &Path,
666 bound: Ty,
667 ) -> InferResult<Ty>;
668
669 fn unfold_strg_ref(&mut self, infcx: &mut InferCtxt, path: &Path, ty: &Ty) -> InferResult<Loc>;
670
671 fn get(&self, path: &Path) -> Ty;
672}
673
674struct DummyEnv;
675
676impl LocEnv for DummyEnv {
677 fn ptr_to_ref(
678 &mut self,
679 _: &mut InferCtxtAt,
680 _: ConstrReason,
681 _: Region,
682 _: &Path,
683 _: Ty,
684 ) -> InferResult<Ty> {
685 bug!("call to `ptr_to_ref` on `DummyEnv`")
686 }
687
688 fn unfold_strg_ref(&mut self, _: &mut InferCtxt, _: &Path, _: &Ty) -> InferResult<Loc> {
689 bug!("call to `unfold_str_ref` on `DummyEnv`")
690 }
691
692 fn get(&self, _: &Path) -> Ty {
693 bug!("call to `get` on `DummyEnv`")
694 }
695}
696
697struct Sub<'a, E> {
699 env: &'a mut E,
701 reason: ConstrReason,
702 span: Span,
703 obligations: Vec<Binder<rty::CoroutineObligPredicate>>,
707}
708
709impl<'a, E: LocEnv> Sub<'a, E> {
710 fn new(env: &'a mut E, reason: ConstrReason, span: Span) -> Self {
711 Self { env, reason, span, obligations: vec![] }
712 }
713
714 fn tag(&self) -> Tag {
715 Tag::new(self.reason, self.span)
716 }
717
718 fn tys(&mut self, infcx: &mut InferCtxt, a: &Ty, b: &Ty) -> InferResult {
719 let infcx = &mut infcx.branch();
720 let a = infcx.unpack(a);
726
727 match (a.kind(), b.kind()) {
728 (TyKind::Exists(..), _) => {
729 bug!("existentials should have been removed by the unpacking above");
730 }
731 (TyKind::Constr(..), _) => {
732 bug!("constraint types should have been removed by the unpacking above");
733 }
734
735 (_, TyKind::Exists(ctor_b)) => {
736 infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b))
737 }
738 (_, TyKind::Constr(pred_b, ty_b)) => {
739 infcx.check_pred(pred_b, self.tag());
740 self.tys(infcx, &a, ty_b)
741 }
742
743 (TyKind::Ptr(PtrKind::Mut(_), path_a), TyKind::StrgRef(_, path_b, ty_b)) => {
744 let ty_a = self.env.get(path_a);
748 infcx.unify_exprs(&path_a.to_expr(), &path_b.to_expr());
749 self.tys(infcx, &ty_a, ty_b)
750 }
751 (TyKind::StrgRef(_, path_a, ty_a), TyKind::StrgRef(_, path_b, ty_b)) => {
752 self.env.unfold_strg_ref(infcx, path_a, ty_a)?;
764 let ty_a = self.env.get(path_a);
765 infcx.unify_exprs(&path_a.to_expr(), &path_b.to_expr());
766 self.tys(infcx, &ty_a, ty_b)
767 }
768 (
769 TyKind::Ptr(PtrKind::Mut(re), path),
770 TyKind::Indexed(BaseTy::Ref(_, bound, Mutability::Mut), idx),
771 ) => {
772 self.idxs_eq(infcx, &Expr::unit(), idx);
775
776 self.env.ptr_to_ref(
777 &mut infcx.at(self.span),
778 self.reason,
779 *re,
780 path,
781 bound.clone(),
782 )?;
783 Ok(())
784 }
785
786 (TyKind::Indexed(bty_a, idx_a), TyKind::Indexed(bty_b, idx_b)) => {
787 self.btys(infcx, bty_a, bty_b)?;
788 self.idxs_eq(infcx, idx_a, idx_b);
789 Ok(())
790 }
791 (TyKind::Ptr(pk_a, path_a), TyKind::Ptr(pk_b, path_b)) => {
792 debug_assert_eq!(pk_a, pk_b);
793 debug_assert_eq!(path_a, path_b);
794 Ok(())
795 }
796 (TyKind::Param(param_ty_a), TyKind::Param(param_ty_b)) => {
797 debug_assert_eq!(param_ty_a, param_ty_b);
798 Ok(())
799 }
800 (_, TyKind::Uninit) => Ok(()),
801 (TyKind::Downcast(.., fields_a), TyKind::Downcast(.., fields_b)) => {
802 debug_assert_eq!(fields_a.len(), fields_b.len());
803 for (ty_a, ty_b) in iter::zip(fields_a, fields_b) {
804 self.tys(infcx, ty_a, ty_b)?;
805 }
806 Ok(())
807 }
808 _ => Err(query_bug!("incompatible types: `{a:?}` - `{b:?}`"))?,
809 }
810 }
811
812 fn btys(&mut self, infcx: &mut InferCtxt, a: &BaseTy, b: &BaseTy) -> InferResult {
813 match (a, b) {
816 (BaseTy::Int(int_ty_a), BaseTy::Int(int_ty_b)) => {
817 debug_assert_eq!(int_ty_a, int_ty_b);
818 Ok(())
819 }
820 (BaseTy::Uint(uint_ty_a), BaseTy::Uint(uint_ty_b)) => {
821 debug_assert_eq!(uint_ty_a, uint_ty_b);
822 Ok(())
823 }
824 (BaseTy::Adt(a_adt, a_args), BaseTy::Adt(b_adt, b_args)) => {
825 tracked_span_dbg_assert_eq!(a_adt.did(), b_adt.did());
826 tracked_span_dbg_assert_eq!(a_args.len(), b_args.len());
827 let variances = infcx.genv.variances_of(a_adt.did());
828 for (variance, ty_a, ty_b) in izip!(variances, a_args.iter(), b_args.iter()) {
829 self.generic_args(infcx, *variance, ty_a, ty_b)?;
830 }
831 Ok(())
832 }
833 (BaseTy::FnDef(a_def_id, a_args), BaseTy::FnDef(b_def_id, b_args)) => {
834 debug_assert_eq!(a_def_id, b_def_id);
835 debug_assert_eq!(a_args.len(), b_args.len());
836 for (arg_a, arg_b) in iter::zip(a_args, b_args) {
844 match (arg_a, arg_b) {
845 (GenericArg::Ty(ty_a), GenericArg::Ty(ty_b)) => {
846 let bty_a = ty_a.as_bty_skipping_existentials();
847 let bty_b = ty_b.as_bty_skipping_existentials();
848 tracked_span_dbg_assert_eq!(bty_a, bty_b);
849 }
850 (GenericArg::Base(ctor_a), GenericArg::Base(ctor_b)) => {
851 let bty_a = ctor_a.as_bty_skipping_binder();
852 let bty_b = ctor_b.as_bty_skipping_binder();
853 tracked_span_dbg_assert_eq!(bty_a, bty_b);
854 }
855 (_, _) => tracked_span_dbg_assert_eq!(arg_a, arg_b),
856 }
857 }
858 Ok(())
859 }
860 (BaseTy::Float(float_ty_a), BaseTy::Float(float_ty_b)) => {
861 debug_assert_eq!(float_ty_a, float_ty_b);
862 Ok(())
863 }
864 (BaseTy::Slice(ty_a), BaseTy::Slice(ty_b)) => self.tys(infcx, ty_a, ty_b),
865 (BaseTy::Ref(_, ty_a, Mutability::Mut), BaseTy::Ref(_, ty_b, Mutability::Mut)) => {
866 if ty_a.is_slice()
867 && let TyKind::Indexed(_, idx_a) = ty_a.kind()
868 && let TyKind::Exists(bty_b) = ty_b.kind()
869 {
870 self.tys(infcx, ty_a, ty_b)?;
875 self.tys(infcx, &bty_b.replace_bound_reft(idx_a), ty_a)
876 } else {
877 self.tys(infcx, ty_a, ty_b)?;
878 self.tys(infcx, ty_b, ty_a)
879 }
880 }
881 (BaseTy::Ref(_, ty_a, Mutability::Not), BaseTy::Ref(_, ty_b, Mutability::Not)) => {
882 self.tys(infcx, ty_a, ty_b)
883 }
884 (BaseTy::Tuple(tys_a), BaseTy::Tuple(tys_b)) => {
885 debug_assert_eq!(tys_a.len(), tys_b.len());
886 for (ty_a, ty_b) in iter::zip(tys_a, tys_b) {
887 self.tys(infcx, ty_a, ty_b)?;
888 }
889 Ok(())
890 }
891 (_, BaseTy::Alias(AliasKind::Opaque, alias_ty_b)) => {
892 if let BaseTy::Alias(AliasKind::Opaque, alias_ty_a) = a {
893 debug_assert_eq!(alias_ty_a.refine_args.len(), alias_ty_b.refine_args.len());
894 iter::zip(alias_ty_a.refine_args.iter(), alias_ty_b.refine_args.iter())
895 .for_each(|(expr_a, expr_b)| infcx.unify_exprs(expr_a, expr_b));
896 }
897 self.handle_opaque_type(infcx, a, alias_ty_b)
898 }
899 (
900 BaseTy::Alias(AliasKind::Projection, alias_ty_a),
901 BaseTy::Alias(AliasKind::Projection, alias_ty_b),
902 ) => {
903 tracked_span_dbg_assert_eq!(alias_ty_a, alias_ty_b);
904 Ok(())
905 }
906 (BaseTy::Array(ty_a, len_a), BaseTy::Array(ty_b, len_b)) => {
907 tracked_span_dbg_assert_eq!(len_a, len_b);
908 self.tys(infcx, ty_a, ty_b)
909 }
910 (BaseTy::Param(param_a), BaseTy::Param(param_b)) => {
911 debug_assert_eq!(param_a, param_b);
912 Ok(())
913 }
914 (BaseTy::Bool, BaseTy::Bool)
915 | (BaseTy::Str, BaseTy::Str)
916 | (BaseTy::Char, BaseTy::Char)
917 | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _))
918 | (BaseTy::RawPtrMetadata(_), BaseTy::RawPtrMetadata(_)) => Ok(()),
919 (BaseTy::Dynamic(preds_a, _), BaseTy::Dynamic(preds_b, _)) => {
920 tracked_span_assert_eq!(preds_a.erase_regions(), preds_b.erase_regions());
921 Ok(())
922 }
923 (BaseTy::Closure(did1, tys_a, _), BaseTy::Closure(did2, tys_b, _)) if did1 == did2 => {
924 debug_assert_eq!(tys_a.len(), tys_b.len());
925 for (ty_a, ty_b) in iter::zip(tys_a, tys_b) {
926 self.tys(infcx, ty_a, ty_b)?;
927 }
928 Ok(())
929 }
930 (BaseTy::FnPtr(sig_a), BaseTy::FnPtr(sig_b)) => {
931 tracked_span_assert_eq!(sig_a.erase_regions(), sig_b.erase_regions());
932 Ok(())
933 }
934 (BaseTy::Never, BaseTy::Never) => Ok(()),
935 _ => Err(query_bug!("incompatible base types: `{a:?}` - `{b:?}`"))?,
936 }
937 }
938
939 fn generic_args(
940 &mut self,
941 infcx: &mut InferCtxt,
942 variance: Variance,
943 a: &GenericArg,
944 b: &GenericArg,
945 ) -> InferResult {
946 let (ty_a, ty_b) = match (a, b) {
947 (GenericArg::Ty(ty_a), GenericArg::Ty(ty_b)) => (ty_a.clone(), ty_b.clone()),
948 (GenericArg::Base(ctor_a), GenericArg::Base(ctor_b)) => {
949 tracked_span_dbg_assert_eq!(ctor_a.sort(), ctor_b.sort());
950 (ctor_a.to_ty(), ctor_b.to_ty())
951 }
952 (GenericArg::Lifetime(_), GenericArg::Lifetime(_)) => return Ok(()),
953 (GenericArg::Const(cst_a), GenericArg::Const(cst_b)) => {
954 debug_assert_eq!(cst_a, cst_b);
955 return Ok(());
956 }
957 _ => Err(query_bug!("incompatible generic args: `{a:?}` `{b:?}`"))?,
958 };
959 match variance {
960 Variance::Covariant => self.tys(infcx, &ty_a, &ty_b),
961 Variance::Invariant => {
962 self.tys(infcx, &ty_a, &ty_b)?;
963 self.tys(infcx, &ty_b, &ty_a)
964 }
965 Variance::Contravariant => self.tys(infcx, &ty_b, &ty_a),
966 Variance::Bivariant => Ok(()),
967 }
968 }
969
970 fn idxs_eq(&mut self, infcx: &mut InferCtxt, a: &Expr, b: &Expr) {
971 if a == b {
972 return;
973 }
974 match (a.kind(), b.kind()) {
975 (
976 ExprKind::Ctor(Ctor::Struct(did_a), flds_a),
977 ExprKind::Ctor(Ctor::Struct(did_b), flds_b),
978 ) => {
979 debug_assert_eq!(did_a, did_b);
980 for (a, b) in iter::zip(flds_a, flds_b) {
981 self.idxs_eq(infcx, a, b);
982 }
983 }
984 (ExprKind::Tuple(flds_a), ExprKind::Tuple(flds_b)) => {
985 for (a, b) in iter::zip(flds_a, flds_b) {
986 self.idxs_eq(infcx, a, b);
987 }
988 }
989 (_, ExprKind::Tuple(flds_b)) => {
990 for (f, b) in flds_b.iter().enumerate() {
991 let proj = FieldProj::Tuple { arity: flds_b.len(), field: f as u32 };
992 let a = a.proj_and_reduce(proj);
993 self.idxs_eq(infcx, &a, b);
994 }
995 }
996
997 (_, ExprKind::Ctor(Ctor::Struct(def_id), flds_b)) => {
998 for (f, b) in flds_b.iter().enumerate() {
999 let proj = FieldProj::Adt { def_id: *def_id, field: f as u32 };
1000 let a = a.proj_and_reduce(proj);
1001 self.idxs_eq(infcx, &a, b);
1002 }
1003 }
1004
1005 (ExprKind::Tuple(flds_a), _) => {
1006 infcx.unify_exprs(a, b);
1007 for (f, a) in flds_a.iter().enumerate() {
1008 let proj = FieldProj::Tuple { arity: flds_a.len(), field: f as u32 };
1009 let b = b.proj_and_reduce(proj);
1010 self.idxs_eq(infcx, a, &b);
1011 }
1012 }
1013 (ExprKind::Ctor(Ctor::Struct(def_id), flds_a), _) => {
1014 infcx.unify_exprs(a, b);
1015 for (f, a) in flds_a.iter().enumerate() {
1016 let proj = FieldProj::Adt { def_id: *def_id, field: f as u32 };
1017 let b = b.proj_and_reduce(proj);
1018 self.idxs_eq(infcx, a, &b);
1019 }
1020 }
1021 (ExprKind::Abs(lam_a), ExprKind::Abs(lam_b)) => {
1022 self.abs_eq(infcx, lam_a, lam_b);
1023 }
1024 (_, ExprKind::Abs(lam_b)) => {
1025 self.abs_eq(infcx, &a.eta_expand_abs(lam_b.vars(), lam_b.output()), lam_b);
1026 }
1027 (ExprKind::Abs(lam_a), _) => {
1028 infcx.unify_exprs(a, b);
1029 self.abs_eq(infcx, lam_a, &b.eta_expand_abs(lam_a.vars(), lam_a.output()));
1030 }
1031 (ExprKind::KVar(_), _) | (_, ExprKind::KVar(_)) => {
1032 infcx.check_impl(a, b, self.tag());
1033 infcx.check_impl(b, a, self.tag());
1034 }
1035 _ => {
1036 infcx.unify_exprs(a, b);
1037 let span = b.span();
1038 infcx.check_pred(Expr::binary_op(rty::BinOp::Eq, a, b).at_opt(span), self.tag());
1039 }
1040 }
1041 }
1042
1043 fn abs_eq(&mut self, infcx: &mut InferCtxt, a: &Lambda, b: &Lambda) {
1044 debug_assert_eq!(a.vars().len(), b.vars().len());
1045 let vars = a
1046 .vars()
1047 .iter()
1048 .map(|kind| Expr::fvar(infcx.define_var(kind.expect_sort())))
1049 .collect_vec();
1050 let body_a = a.apply(&vars);
1051 let body_b = b.apply(&vars);
1052 self.idxs_eq(infcx, &body_a, &body_b);
1053 }
1054
1055 fn handle_opaque_type(
1056 &mut self,
1057 infcx: &mut InferCtxt,
1058 bty: &BaseTy,
1059 alias_ty: &AliasTy,
1060 ) -> InferResult {
1061 if let BaseTy::Coroutine(def_id, resume_ty, upvar_tys) = bty {
1062 let obligs = mk_coroutine_obligations(
1063 infcx.genv,
1064 def_id,
1065 resume_ty,
1066 upvar_tys,
1067 &alias_ty.def_id,
1068 )?;
1069 self.obligations.extend(obligs);
1070 } else {
1071 let bounds = infcx.genv.item_bounds(alias_ty.def_id)?.instantiate(
1072 infcx.tcx(),
1073 &alias_ty.args,
1074 &alias_ty.refine_args,
1075 );
1076 for clause in &bounds {
1077 if !clause.kind().vars().is_empty() {
1078 Err(query_bug!("handle_opaque_types: clause with bound vars: `{clause:?}`"))?;
1079 }
1080 if let rty::ClauseKind::Projection(pred) = clause.kind_skipping_binder() {
1081 let alias_ty = pred.projection_ty.with_self_ty(bty.to_subset_ty_ctor());
1082 let ty1 = BaseTy::Alias(AliasKind::Projection, alias_ty)
1083 .to_ty()
1084 .normalize_projections(&mut infcx.at(self.span))?;
1085 let ty2 = pred.term.to_ty();
1086 self.tys(infcx, &ty1, &ty2)?;
1087 }
1088 }
1089 }
1090 Ok(())
1091 }
1092}
1093
1094fn mk_coroutine_obligations(
1095 genv: GlobalEnv,
1096 generator_did: &DefId,
1097 resume_ty: &Ty,
1098 upvar_tys: &List<Ty>,
1099 opaque_def_id: &DefId,
1100) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
1101 let bounds = genv.item_bounds(*opaque_def_id)?.skip_binder();
1102 for bound in &bounds {
1103 if let Some(proj_clause) = bound.as_projection_clause() {
1104 return Ok(vec![proj_clause.map(|proj_clause| {
1105 let output = proj_clause.term;
1106 CoroutineObligPredicate {
1107 def_id: *generator_did,
1108 resume_ty: resume_ty.clone(),
1109 upvar_tys: upvar_tys.clone(),
1110 output: output.to_ty(),
1111 }
1112 })]);
1113 }
1114 }
1115 bug!("no projection predicate")
1116}
1117
1118#[derive(Debug)]
1119pub enum InferErr {
1120 UnsolvedEvar(EVid),
1121 Query(QueryErr),
1122}
1123
1124impl From<QueryErr> for InferErr {
1125 fn from(v: QueryErr) -> Self {
1126 Self::Query(v)
1127 }
1128}
1129
1130mod pretty {
1131 use std::fmt;
1132
1133 use flux_middle::pretty::*;
1134
1135 use super::*;
1136
1137 impl Pretty for Tag {
1138 fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1139 w!(cx, f, "{:?} at {:?}", ^self.reason, self.src_span)
1140 }
1141 }
1142
1143 impl_debug_with_default_cx!(Tag);
1144}