flux_infer/
projections.rs

1use std::iter;
2
3use flux_common::{bug, iter::IterExt, tracked_span_bug};
4use flux_middle::{
5    global_env::GlobalEnv,
6    queries::{QueryErr, QueryResult},
7    query_bug,
8    rty::{
9        self, AliasKind, AliasReft, AliasTy, BaseTy, Binder, Clause, ClauseKind, Const, ConstKind,
10        EarlyBinder, Expr, ExprKind, GenericArg, List, ProjectionPredicate, RefineArgs, Region,
11        Sort, SubsetTy, SubsetTyCtor, Ty, TyKind,
12        fold::{FallibleTypeFolder, TypeFoldable, TypeSuperFoldable, TypeVisitable},
13        refining::Refiner,
14        subst::{GenericsSubstDelegate, GenericsSubstFolder},
15    },
16};
17use flux_rustc_bridge::{ToRustc, lowering::Lower};
18use itertools::izip;
19use rustc_hir::def_id::DefId;
20use rustc_infer::traits::Obligation;
21use rustc_middle::{
22    traits::{ImplSource, ObligationCause},
23    ty::{TyCtxt, Variance},
24};
25use rustc_trait_selection::{
26    solve::deeply_normalize,
27    traits::{FulfillmentError, SelectionContext},
28};
29use rustc_type_ir::TypeVisitableExt;
30
31use crate::{
32    fixpoint_encoding::KVarEncoding,
33    infer::{InferCtxtAt, InferResult},
34    refine_tree::Scope,
35};
36
37pub trait NormalizeExt: TypeFoldable {
38    fn deeply_normalize(&self, infcx: &mut InferCtxtAt) -> QueryResult<Self>;
39
40    /// Deeply normalize projections but only inside sorts
41    fn deeply_normalize_sorts<'tcx>(
42        &self,
43        def_id: DefId,
44        genv: GlobalEnv<'_, 'tcx>,
45        infcx: &rustc_infer::infer::InferCtxt<'tcx>,
46    ) -> QueryResult<Self>;
47}
48
49impl<T: TypeFoldable> NormalizeExt for T {
50    fn deeply_normalize(&self, infcx: &mut InferCtxtAt) -> QueryResult<Self> {
51        let span = infcx.span;
52        let infcx_orig = &mut infcx.infcx;
53        let mut infcx = infcx_orig.branch();
54        let infcx = infcx.at(span);
55        let mut normalizer = Normalizer::new(infcx)?;
56        self.erase_regions().try_fold_with(&mut normalizer)
57    }
58
59    fn deeply_normalize_sorts<'tcx>(
60        &self,
61        def_id: DefId,
62        genv: GlobalEnv<'_, 'tcx>,
63        infcx: &rustc_infer::infer::InferCtxt<'tcx>,
64    ) -> QueryResult<Self> {
65        let mut normalizer = SortNormalizer::new(def_id, genv, infcx);
66        self.erase_regions().try_fold_with(&mut normalizer)
67    }
68}
69
70struct Normalizer<'a, 'infcx, 'genv, 'tcx> {
71    infcx: InferCtxtAt<'a, 'infcx, 'genv, 'tcx>,
72    selcx: SelectionContext<'infcx, 'tcx>,
73    param_env: List<Clause>,
74    scope: Scope,
75}
76
77impl<'a, 'infcx, 'genv, 'tcx> Normalizer<'a, 'infcx, 'genv, 'tcx> {
78    fn new(infcx: InferCtxtAt<'a, 'infcx, 'genv, 'tcx>) -> QueryResult<Self> {
79        let predicates = infcx.genv.predicates_of(infcx.def_id)?;
80        let param_env = predicates.instantiate_identity().predicates.clone();
81        let selcx = SelectionContext::new(infcx.region_infcx);
82        let scope = infcx.cursor().marker().scope().unwrap();
83        Ok(Normalizer { infcx, selcx, param_env, scope })
84    }
85
86    fn normalize_projection_ty(
87        &mut self,
88        obligation: &AliasTy,
89    ) -> QueryResult<(bool, SubsetTyCtor)> {
90        let mut candidates = vec![];
91        self.assemble_candidates_from_param_env(obligation, &mut candidates);
92        self.assemble_candidates_from_trait_def(obligation, &mut candidates)
93            .unwrap_or_else(|err| tracked_span_bug!("{err:?}"));
94        self.assemble_candidates_from_impls(obligation, &mut candidates)?;
95        if candidates.is_empty() {
96            // TODO: This is a temporary hack that uses rustc's trait selection when FLUX fails;
97            //       The correct thing, e.g for `trait09.rs` is to make sure FLUX's param_env mirrors RUSTC,
98            //       by suitably chasing down the super-trait predicates,
99            //       see https://github.com/flux-rs/flux/issues/737
100            let (changed, ty_ctor) = normalize_projection_ty_with_rustc(
101                self.genv(),
102                self.def_id(),
103                self.infcx.region_infcx,
104                obligation,
105            )?;
106            return Ok((changed, ty_ctor));
107        }
108        if candidates.len() > 1 {
109            bug!("ambiguity when resolving `{obligation:?}` in {:?}", self.def_id());
110        }
111        let ctor = self.confirm_candidate(candidates.pop().unwrap(), obligation)?;
112        Ok((true, ctor))
113    }
114
115    fn find_resolved_predicates(
116        &self,
117        subst: &mut TVarSubst,
118        preds: Vec<EarlyBinder<ProjectionPredicate>>,
119    ) -> (Vec<ProjectionPredicate>, Vec<EarlyBinder<ProjectionPredicate>>) {
120        let mut resolved = vec![];
121        let mut unresolved = vec![];
122        for pred in preds {
123            let term = pred.clone().skip_binder().term;
124            let alias_ty = pred.clone().map(|p| p.projection_ty);
125            match subst.instantiate_partial(alias_ty) {
126                Some(projection_ty) => {
127                    let pred = ProjectionPredicate { projection_ty, term };
128                    resolved.push(pred);
129                }
130                None => unresolved.push(pred.clone()),
131            }
132        }
133        (resolved, unresolved)
134    }
135
136    // See issue-829*.rs for an example of what this function is for.
137    fn resolve_projection_predicates(
138        &mut self,
139        subst: &mut TVarSubst,
140        impl_def_id: DefId,
141    ) -> QueryResult {
142        let mut projection_preds: Vec<_> = self
143            .genv()
144            .predicates_of(impl_def_id)?
145            .skip_binder()
146            .predicates
147            .iter()
148            .filter_map(|pred| {
149                if let ClauseKind::Projection(pred) = pred.kind_skipping_binder() {
150                    Some(EarlyBinder(pred.clone()))
151                } else {
152                    None
153                }
154            })
155            .collect();
156
157        while !projection_preds.is_empty() {
158            let (resolved, unresolved) = self.find_resolved_predicates(subst, projection_preds);
159
160            if resolved.is_empty() {
161                break; // failed: there is some unresolved projection pred!
162            }
163            for p in resolved {
164                let obligation = &p.projection_ty;
165                let (_, ctor) = self.normalize_projection_ty(obligation)?;
166                subst.subset_tys(&p.term, &ctor);
167            }
168            projection_preds = unresolved;
169        }
170        Ok(())
171    }
172
173    fn confirm_candidate(
174        &mut self,
175        candidate: Candidate,
176        obligation: &AliasTy,
177    ) -> QueryResult<SubsetTyCtor> {
178        let tcx = self.tcx();
179        match candidate {
180            Candidate::ParamEnv(pred) | Candidate::TraitDef(pred) => {
181                let rustc_obligation = obligation.to_rustc(tcx);
182                let parent_id = rustc_obligation.trait_ref(tcx).def_id;
183                // Do fn-subtyping if the candidate was a fn-trait
184                if tcx.is_fn_trait(parent_id) {
185                    let res = self
186                        .fn_subtype_projection_ty(pred, obligation)
187                        .unwrap_or_else(|err| tracked_span_bug!("{err:?}"));
188                    Ok(res)
189                } else {
190                    Ok(pred.skip_binder().term)
191                }
192            }
193            Candidate::UserDefinedImpl(impl_def_id) => {
194                // Given a projection obligation
195                //     <IntoIter<{v. i32[v] | v > 0}, Global> as Iterator>::Item
196                // and the id of a rust impl block
197                //     impl<T, A: Allocator> Iterator for IntoIter<T, A>
198
199                // 1. MATCH the self type of the rust impl block and the flux self type of the obligation
200                //    to infer a substitution
201                //        IntoIter<{v. i32[v] | v > 0}, Global> MATCH IntoIter<T, A>
202                //            => {T -> {v. i32[v] | v > 0}, A -> Global}
203
204                let impl_trait_ref = self.genv().impl_trait_ref(impl_def_id)?.skip_binder();
205
206                let generics = self.tcx().generics_of(impl_def_id);
207
208                let mut subst = TVarSubst::new(generics);
209                for (a, b) in iter::zip(&impl_trait_ref.args, &obligation.args) {
210                    subst.generic_args(a, b);
211                }
212
213                // 2. Gather the ProjectionPredicates and solve them see issue-808.rs
214                self.resolve_projection_predicates(&mut subst, impl_def_id)?;
215
216                let args = subst.finish(self.tcx(), generics)?;
217
218                // 3. Get the associated type in the impl block and apply the substitution to it
219                let assoc_type_id = tcx
220                    .associated_items(impl_def_id)
221                    .in_definition_order()
222                    .find(|item| item.trait_item_def_id() == Some(obligation.def_id))
223                    .map(|item| item.def_id)
224                    .ok_or_else(|| {
225                        query_bug!("no associated type for {obligation:?} in impl {impl_def_id:?}")
226                    })?;
227                Ok(self
228                    .genv()
229                    .type_of(assoc_type_id)?
230                    .instantiate(tcx, &args, &[])
231                    .expect_subset_ty_ctor())
232            }
233        }
234    }
235
236    fn fn_subtype_projection_ty(
237        &mut self,
238        actual: Binder<ProjectionPredicate>,
239        oblig: &AliasTy,
240    ) -> InferResult<SubsetTyCtor> {
241        // Step 1: bs <- unpack(b1...)
242        let obligs: Vec<_> = oblig
243            .args
244            .iter()
245            .map(|arg| {
246                match arg {
247                    GenericArg::Ty(ty) => GenericArg::Ty(self.infcx.unpack(ty)),
248                    GenericArg::Base(ctor) => GenericArg::Ty(self.infcx.unpack(&ctor.to_ty())),
249                    _ => arg.clone(),
250                }
251            })
252            .collect();
253
254        let span = self.infcx.span;
255        let mut infcx = self.infcx.at(span);
256
257        let actual = infcx.ensure_resolved_evars(|infcx| {
258            // Step 2: as <- fresh(a1...)
259            let actual = actual
260                .replace_bound_vars(
261                    |_| rty::ReErased,
262                    |sort, mode, _| infcx.fresh_infer_var(sort, mode),
263                )
264                .deeply_normalize(infcx)?;
265
266            let actuals = actual.projection_ty.args.iter().map(|arg| {
267                match arg {
268                    GenericArg::Base(ctor) => GenericArg::Ty(ctor.to_ty()),
269                    _ => arg.clone(),
270                }
271            });
272
273            // Step 3: bs <: as
274            for (a, b) in izip!(actuals.skip(1), obligs.iter().skip(1)) {
275                infcx.subtyping_generic_args(
276                    Variance::Contravariant,
277                    &a,
278                    b,
279                    crate::infer::ConstrReason::Predicate,
280                )?;
281            }
282            Ok(actual)
283        })?;
284        // Step 4: check all evars are solved, plug back into ProjectionPredicate
285        let actual = infcx.fully_resolve_evars(&actual);
286
287        // Step 5: generate "fresh" type for actual.term,
288        let oblig_term = actual.term.with_holes().replace_holes(|binders, kind| {
289            assert!(kind == rty::HoleKind::Pred);
290            let scope = &self.scope;
291            infcx.fresh_kvar_in_scope(binders, scope, KVarEncoding::Conj)
292        });
293
294        // Step 6: subtyping obligation on output
295        infcx.subtyping(
296            &actual.term.to_ty(),
297            &oblig_term.to_ty(),
298            crate::infer::ConstrReason::Predicate,
299        )?;
300        // Ok(ProjectionPredicate { projection_ty: actual.projection_ty, term: oblig_term })
301        Ok(oblig_term)
302    }
303
304    fn assemble_candidates_from_predicates(
305        &mut self,
306        predicates: &List<Clause>,
307        obligation: &AliasTy,
308        ctor: fn(Binder<ProjectionPredicate>) -> Candidate,
309        candidates: &mut Vec<Candidate>,
310    ) {
311        let tcx = self.tcx();
312        let rustc_obligation = obligation.to_rustc(tcx);
313
314        for predicate in predicates {
315            if let Some(pred) = predicate.as_projection_clause()
316                && pred.skip_binder_ref().projection_ty.to_rustc(tcx) == rustc_obligation
317            {
318                candidates.push(ctor(pred));
319            }
320        }
321    }
322
323    fn assemble_candidates_from_param_env(
324        &mut self,
325        obligation: &AliasTy,
326        candidates: &mut Vec<Candidate>,
327    ) {
328        let predicates = self.param_env.clone();
329        self.assemble_candidates_from_predicates(
330            &predicates,
331            obligation,
332            Candidate::ParamEnv,
333            candidates,
334        );
335    }
336
337    fn assemble_candidates_from_trait_def(
338        &mut self,
339        obligation: &AliasTy,
340        candidates: &mut Vec<Candidate>,
341    ) -> InferResult {
342        if let GenericArg::Base(ctor) = &obligation.args[0]
343            && let BaseTy::Alias(AliasKind::Opaque, alias_ty) = ctor.as_bty_skipping_binder()
344        {
345            debug_assert!(!alias_ty.has_escaping_bvars());
346            let bounds = self.genv().item_bounds(alias_ty.def_id)?.instantiate(
347                self.tcx(),
348                &alias_ty.args,
349                &alias_ty.refine_args,
350            );
351            self.assemble_candidates_from_predicates(
352                &bounds,
353                obligation,
354                Candidate::TraitDef,
355                candidates,
356            );
357        }
358        Ok(())
359    }
360
361    fn assemble_candidates_from_impls(
362        &mut self,
363        obligation: &AliasTy,
364        candidates: &mut Vec<Candidate>,
365    ) -> QueryResult {
366        let trait_ref = obligation.to_rustc(self.tcx()).trait_ref(self.tcx());
367        let trait_ref = self.tcx().erase_and_anonymize_regions(trait_ref);
368        let trait_pred = Obligation::new(
369            self.tcx(),
370            ObligationCause::dummy(),
371            self.rustc_param_env(),
372            trait_ref,
373        );
374        // FIXME(nilehmann) This is a patch to not panic inside rustc so we are
375        // able to catch the bug
376        if trait_pred.has_escaping_bound_vars() {
377            tracked_span_bug!();
378        }
379        match self.selcx.select(&trait_pred) {
380            Ok(Some(ImplSource::UserDefined(impl_data))) => {
381                candidates.push(Candidate::UserDefinedImpl(impl_data.impl_def_id));
382            }
383            Ok(_) => (),
384            Err(e) => bug!("error selecting {trait_pred:?}: {e:?}"),
385        }
386        Ok(())
387    }
388
389    fn def_id(&self) -> DefId {
390        self.infcx.def_id
391    }
392
393    fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
394        self.infcx.genv
395    }
396
397    fn tcx(&self) -> TyCtxt<'tcx> {
398        self.selcx.tcx()
399    }
400
401    fn rustc_param_env(&self) -> rustc_middle::ty::ParamEnv<'tcx> {
402        self.selcx.tcx().param_env(self.def_id())
403    }
404}
405
406impl FallibleTypeFolder for Normalizer<'_, '_, '_, '_> {
407    type Error = QueryErr;
408
409    fn try_fold_sort(&mut self, sort: &Sort) -> Result<Sort, Self::Error> {
410        match sort {
411            Sort::Alias(AliasKind::Free, alias_ty) => {
412                self.genv()
413                    .normalize_free_alias_sort(alias_ty)?
414                    .try_fold_with(self)
415            }
416            Sort::Alias(AliasKind::Projection, alias_ty) => {
417                let (changed, ctor) = self.normalize_projection_ty(alias_ty)?;
418                let sort = ctor.sort();
419                if changed { sort.try_fold_with(self) } else { Ok(sort) }
420            }
421            _ => sort.try_super_fold_with(self),
422        }
423    }
424
425    // As shown in https://github.com/flux-rs/flux/issues/711 one round of `normalize_projections`
426    // can replace one projection e.g. `<Rev<Iter<[i32]> as Iterator>::Item` with another e.g.
427    // `<Iter<[i32]> as Iterator>::Item` We want to compute a "fixpoint" i.e. keep going until no
428    // change, so that e.g. the above is normalized all the way to `i32`, which is what the `changed`
429    // is for.
430    fn try_fold_ty(&mut self, ty: &Ty) -> Result<Ty, Self::Error> {
431        match ty.kind() {
432            TyKind::Indexed(BaseTy::Alias(AliasKind::Free, alias_ty), idx) => {
433                Ok(self
434                    .genv()
435                    .type_of(alias_ty.def_id)?
436                    .instantiate(self.tcx(), &alias_ty.args, &alias_ty.refine_args)
437                    .expect_ctor()
438                    .replace_bound_reft(idx))
439            }
440            TyKind::Indexed(BaseTy::Alias(AliasKind::Projection, alias_ty), idx) => {
441                let (changed, ctor) = self.normalize_projection_ty(alias_ty)?;
442                let ty = ctor.replace_bound_reft(idx).to_ty();
443                if changed { ty.try_fold_with(self) } else { Ok(ty) }
444            }
445            _ => ty.try_super_fold_with(self),
446        }
447    }
448
449    fn try_fold_subset_ty(&mut self, sty: &SubsetTy) -> Result<SubsetTy, Self::Error> {
450        match &sty.bty {
451            BaseTy::Alias(AliasKind::Free, _alias_ty) => {
452                // Weak aliases are always expanded during conversion. We could in theory normalize
453                // them here but we don't guaranatee that type aliases expand to a subset ty. If we
454                // ever stop expanding aliases during conv we would need to guarantee that aliases
455                // used as a generic base expand to a subset type.
456                tracked_span_bug!()
457            }
458            BaseTy::Alias(AliasKind::Projection, alias_ty) => {
459                let (changed, ctor) = self.normalize_projection_ty(alias_ty)?;
460                let ty = ctor.replace_bound_reft(&sty.idx).strengthen(&sty.pred);
461                if changed { ty.try_fold_with(self) } else { Ok(ty) }
462            }
463            _ => sty.try_super_fold_with(self),
464        }
465    }
466
467    fn try_fold_expr(&mut self, expr: &Expr) -> Result<Expr, Self::Error> {
468        if let ExprKind::Alias(alias_pred, refine_args) = expr.kind() {
469            let (changed, e) = normalize_alias_reft(
470                self.genv(),
471                self.def_id(),
472                self.selcx.infcx,
473                alias_pred,
474                refine_args,
475            )?;
476            if changed { e.try_fold_with(self) } else { Ok(e) }
477        } else {
478            expr.try_super_fold_with(self)
479        }
480    }
481
482    fn try_fold_const(&mut self, c: &Const) -> Result<Const, Self::Error> {
483        let c = c.to_rustc(self.tcx());
484        rustc_trait_selection::traits::evaluate_const(self.selcx.infcx, c, self.rustc_param_env())
485            .lower(self.tcx())
486            .map_err(|e| QueryErr::unsupported(self.def_id(), e.into_err()))
487    }
488}
489
490#[derive(Debug)]
491pub enum Candidate {
492    UserDefinedImpl(DefId),
493    ParamEnv(Binder<ProjectionPredicate>),
494    TraitDef(Binder<ProjectionPredicate>),
495}
496
497#[derive(Debug)]
498struct TVarSubst {
499    args: Vec<Option<GenericArg>>,
500}
501
502impl GenericsSubstDelegate for &TVarSubst {
503    type Error = ();
504
505    fn ty_for_param(&mut self, param_ty: rustc_middle::ty::ParamTy) -> Result<Ty, Self::Error> {
506        match self.args.get(param_ty.index as usize) {
507            Some(Some(GenericArg::Ty(ty))) => Ok(ty.clone()),
508            Some(None) => Err(()),
509            arg => tracked_span_bug!("expected type for generic parameter, found `{arg:?}`"),
510        }
511    }
512
513    fn sort_for_param(&mut self, param_ty: rustc_middle::ty::ParamTy) -> Result<Sort, Self::Error> {
514        match self.args.get(param_ty.index as usize) {
515            Some(Some(GenericArg::Base(ctor))) => Ok(ctor.sort()),
516            Some(None) => Err(()),
517            arg => tracked_span_bug!("expected type for generic parameter, found `{arg:?}`"),
518        }
519    }
520
521    fn ctor_for_param(
522        &mut self,
523        param_ty: rustc_middle::ty::ParamTy,
524    ) -> Result<SubsetTyCtor, Self::Error> {
525        match self.args.get(param_ty.index as usize) {
526            Some(Some(GenericArg::Base(ctor))) => Ok(ctor.clone()),
527            Some(None) => Err(()),
528            arg => tracked_span_bug!("expected type for generic parameter, found `{arg:?}`"),
529        }
530    }
531
532    fn region_for_param(
533        &mut self,
534        ebr: rustc_middle::ty::EarlyParamRegion,
535    ) -> Result<Region, Self::Error> {
536        match self.args.get(ebr.index as usize) {
537            Some(Some(GenericArg::Lifetime(region))) => Ok(*region),
538            Some(None) => Err(()),
539            arg => tracked_span_bug!("expected region for generic parameter, found `{arg:?}`"),
540        }
541    }
542
543    fn expr_for_param_const(&self, _param_const: rustc_middle::ty::ParamConst) -> Expr {
544        tracked_span_bug!()
545    }
546
547    fn const_for_param(&mut self, _param: &Const) -> Const {
548        tracked_span_bug!()
549    }
550}
551
552struct SortNormalizer<'infcx, 'genv, 'tcx> {
553    def_id: DefId,
554    infcx: &'infcx rustc_infer::infer::InferCtxt<'tcx>,
555    genv: GlobalEnv<'genv, 'tcx>,
556}
557
558impl<'infcx, 'genv, 'tcx> SortNormalizer<'infcx, 'genv, 'tcx> {
559    fn new(
560        def_id: DefId,
561        genv: GlobalEnv<'genv, 'tcx>,
562        infcx: &'infcx rustc_infer::infer::InferCtxt<'tcx>,
563    ) -> Self {
564        Self { def_id, infcx, genv }
565    }
566}
567
568impl FallibleTypeFolder for SortNormalizer<'_, '_, '_> {
569    type Error = QueryErr;
570    fn try_fold_sort(&mut self, sort: &Sort) -> Result<Sort, Self::Error> {
571        match sort {
572            Sort::Alias(AliasKind::Free, alias_ty) => {
573                self.genv
574                    .normalize_free_alias_sort(alias_ty)?
575                    .try_fold_with(self)
576            }
577            Sort::Alias(AliasKind::Projection, alias_ty) => {
578                let (changed, ctor) = normalize_projection_ty_with_rustc(
579                    self.genv,
580                    self.def_id,
581                    self.infcx,
582                    alias_ty,
583                )?;
584                let sort = ctor.sort();
585                if changed { sort.try_fold_with(self) } else { Ok(sort) }
586            }
587            _ => sort.try_super_fold_with(self),
588        }
589    }
590}
591
592impl TVarSubst {
593    fn new(generics: &rustc_middle::ty::Generics) -> Self {
594        Self { args: vec![None; generics.count()] }
595    }
596
597    fn instantiate_partial<T: TypeFoldable>(&mut self, pred: EarlyBinder<T>) -> Option<T> {
598        let mut folder = GenericsSubstFolder::new(&*self, &[]);
599        pred.skip_binder().try_fold_with(&mut folder).ok()
600    }
601
602    fn finish<'tcx>(
603        self,
604        tcx: TyCtxt<'tcx>,
605        generics: &'tcx rustc_middle::ty::Generics,
606    ) -> QueryResult<Vec<GenericArg>> {
607        self.args
608            .into_iter()
609            .enumerate()
610            .map(|(idx, arg)| {
611                if let Some(arg) = arg {
612                    Ok(arg)
613                } else {
614                    let param = generics.param_at(idx, tcx);
615                    Err(QueryErr::bug(
616                        None,
617                        format!("cannot infer substitution for {param:?} at index {idx}"),
618                    ))
619                }
620            })
621            .try_collect_vec()
622    }
623
624    fn generic_args(&mut self, a: &GenericArg, b: &GenericArg) {
625        match (a, b) {
626            (GenericArg::Ty(a), GenericArg::Ty(b)) => self.tys(a, b),
627            (GenericArg::Lifetime(a), GenericArg::Lifetime(b)) => self.regions(*a, *b),
628            (GenericArg::Base(a), GenericArg::Base(b)) => {
629                self.subset_tys(a, b);
630            }
631            (GenericArg::Const(a), GenericArg::Const(b)) => self.consts(a, b),
632            _ => {}
633        }
634    }
635
636    fn tys(&mut self, a: &Ty, b: &Ty) {
637        if let TyKind::Param(param_ty) = a.kind() {
638            if !b.has_escaping_bvars() {
639                self.insert_generic_arg(param_ty.index, GenericArg::Ty(b.clone()));
640            }
641        } else {
642            let Some(a_bty) = a.as_bty_skipping_existentials() else { return };
643            let Some(b_bty) = b.as_bty_skipping_existentials() else { return };
644            self.btys(a_bty, b_bty);
645        }
646    }
647
648    fn subset_tys(&mut self, a: &SubsetTyCtor, b: &SubsetTyCtor) {
649        let bty_a = a.as_bty_skipping_binder();
650        let bty_b = b.as_bty_skipping_binder();
651        if let BaseTy::Param(param_ty) = bty_a {
652            if !b.has_escaping_bvars() {
653                self.insert_generic_arg(param_ty.index, GenericArg::Base(b.clone()));
654            }
655        } else {
656            self.btys(bty_a, bty_b);
657        }
658    }
659
660    fn btys(&mut self, a: &BaseTy, b: &BaseTy) {
661        match (a, b) {
662            (BaseTy::Param(param_ty), _) => {
663                if !b.has_escaping_bvars() {
664                    let sort = b.sort();
665                    let ctor =
666                        Binder::bind_with_sort(SubsetTy::trivial(b.clone(), Expr::nu()), sort);
667                    self.insert_generic_arg(param_ty.index, GenericArg::Base(ctor));
668                }
669            }
670            (BaseTy::Adt(_, a_args), BaseTy::Adt(_, b_args)) => {
671                debug_assert_eq!(a_args.len(), b_args.len());
672                for (a_arg, b_arg) in iter::zip(a_args, b_args) {
673                    self.generic_args(a_arg, b_arg);
674                }
675            }
676            (BaseTy::Array(a_ty, a_n), BaseTy::Array(b_ty, b_n)) => {
677                self.tys(a_ty, b_ty);
678                self.consts(a_n, b_n);
679            }
680            (BaseTy::Tuple(a_tys), BaseTy::Tuple(b_tys)) => {
681                debug_assert_eq!(a_tys.len(), b_tys.len());
682                for (a_ty, b_ty) in iter::zip(a_tys, b_tys) {
683                    self.tys(a_ty, b_ty);
684                }
685            }
686            (BaseTy::Ref(a_re, a_ty, _), BaseTy::Ref(b_re, b_ty, _)) => {
687                self.regions(*a_re, *b_re);
688                self.tys(a_ty, b_ty);
689            }
690            (BaseTy::Slice(a_ty), BaseTy::Slice(b_ty)) => {
691                self.tys(a_ty, b_ty);
692            }
693            _ => {}
694        }
695    }
696
697    fn regions(&mut self, a: Region, b: Region) {
698        if let Region::ReEarlyParam(ebr) = a {
699            self.insert_generic_arg(ebr.index, GenericArg::Lifetime(b));
700        }
701    }
702
703    fn consts(&mut self, a: &Const, b: &Const) {
704        if let ConstKind::Param(param_const) = a.kind {
705            self.insert_generic_arg(param_const.index, GenericArg::Const(b.clone()));
706        }
707    }
708
709    fn insert_generic_arg(&mut self, idx: u32, arg: GenericArg) {
710        if let Some(old) = &self.args[idx as usize]
711            && old != &arg
712        {
713            tracked_span_bug!("ambiguous substitution: old=`{old:?}`, new: `{arg:?}`");
714        }
715        self.args[idx as usize].replace(arg);
716    }
717}
718
719/// Normalize an [`rty::AliasTy`] by converting it to rustc, normalizing it using rustc api, and
720/// then mapping the result back to `rty`. This will lose refinements and it should only be used
721/// to normalize sorts because they should only contain unrefined types. However, we are also using
722/// it as a hack to normalize types in cases where we fail to collect a candidate, this is unsound
723/// and should be removed.
724///
725/// [`rty::AliasTy`]: AliasTy
726fn normalize_projection_ty_with_rustc<'tcx>(
727    genv: GlobalEnv<'_, 'tcx>,
728    def_id: DefId,
729    infcx: &rustc_infer::infer::InferCtxt<'tcx>,
730    obligation: &AliasTy,
731) -> QueryResult<(bool, SubsetTyCtor)> {
732    let tcx = genv.tcx();
733    let projection_ty = obligation.to_rustc(tcx);
734    let projection_ty = tcx.erase_and_anonymize_regions(projection_ty);
735    let cause = ObligationCause::dummy();
736    let param_env = tcx.param_env(def_id);
737
738    let pre_ty = projection_ty.to_ty(tcx);
739    let at = infcx.at(&cause, param_env);
740    let ty = deeply_normalize::<rustc_middle::ty::Ty<'tcx>, FulfillmentError>(at, pre_ty)
741        .map_err(|err| query_bug!("{err:?}"))?;
742
743    let changed = pre_ty != ty;
744    let rustc_ty = ty.lower(tcx).map_err(|reason| query_bug!("{reason:?}"))?;
745
746    Ok((
747        changed,
748        Refiner::default_for_item(genv, def_id)?
749            .refine_ty_or_base(&rustc_ty)?
750            .expect_base(),
751    ))
752}
753
754/// Do one step of normalization, unfolding associated refinements if they are concrete.
755///
756/// Use this if you are about to match structurally on an [`ExprKind`] and you need associated
757/// refinements to be normalized.
758pub fn structurally_normalize_expr<'tcx>(
759    genv: GlobalEnv<'_, 'tcx>,
760    def_id: DefId,
761    infcx: &rustc_infer::infer::InferCtxt<'tcx>,
762    expr: &Expr,
763) -> QueryResult<Expr> {
764    if let ExprKind::Alias(alias_pred, refine_args) = expr.kind() {
765        let (_, e) = normalize_alias_reft(genv, def_id, infcx, alias_pred, refine_args)?;
766        Ok(e)
767    } else {
768        Ok(expr.clone())
769    }
770}
771
772/// Normalizes an [`AliasReft`]. This uses the trait solver to find the [`ImplSourceUserDefinedData`]
773/// and uses the `args` there, which we map back to Flux via refining. This loses refinements,
774/// but that's fine because [`AliasReft`] should not rely on refinements for trait solving.
775fn normalize_alias_reft<'tcx>(
776    genv: GlobalEnv<'_, 'tcx>,
777    def_id: DefId,
778    infcx: &rustc_infer::infer::InferCtxt<'tcx>,
779    alias_reft: &AliasReft,
780    refine_args: &RefineArgs,
781) -> QueryResult<(bool, Expr)> {
782    let tcx = genv.tcx();
783
784    let is_final = genv.assoc_refinement(alias_reft.assoc_id)?.final_;
785    if is_final {
786        let e = genv
787            .default_assoc_refinement_body(alias_reft.assoc_id)?
788            .unwrap_or_else(|| {
789                bug!("final associated refinement without body - should be caught in desugar")
790            })
791            .instantiate(genv.tcx(), &alias_reft.args, &[])
792            .apply(refine_args);
793        return Ok((true, e));
794    }
795
796    // Get impl source
797    let mut selcx = SelectionContext::new(infcx);
798    let param_env = tcx.param_env(def_id);
799    let trait_ref = alias_reft.to_rustc_trait_ref(tcx);
800    let trait_ref = tcx.erase_and_anonymize_regions(trait_ref);
801    let trait_pred = Obligation::new(tcx, ObligationCause::dummy(), param_env, trait_ref);
802    let impl_source = selcx
803        .select(&trait_pred)
804        .map_err(|e| query_bug!("error selecting {trait_pred:?}: {e:?}"))?;
805
806    match impl_source {
807        Some(ImplSource::UserDefined(impl_data)) => {
808            let impl_def_id = impl_data.impl_def_id;
809            let args = Refiner::default_for_item(genv, def_id)?.refine_generic_args(
810                impl_def_id,
811                &impl_data
812                    .args
813                    .lower(tcx)
814                    .map_err(|reason| query_bug!("{reason:?}"))?,
815            )?;
816            let e = genv
817                .assoc_refinement_body_for_impl(alias_reft.assoc_id, impl_def_id)?
818                .instantiate(tcx, &args, &[])
819                .apply(refine_args);
820            Ok((true, e))
821        }
822        Some(ImplSource::Builtin(..)) => {
823            let e = genv
824                .builtin_assoc_reft_body(infcx.typing_env(param_env), alias_reft)
825                .apply(refine_args);
826            Ok((true, e))
827        }
828        _ => Ok((false, Expr::alias(alias_reft.clone(), refine_args.clone()))),
829    }
830}