flux_fhir_analysis/conv/
mod.rs

1//! Conversion from types in [`fhir`] to types in [`rty`]
2//!
3//! Conversion assumes well-formedness and will panic if type are not well-formed. Among other things,
4//! well-formedness implies:
5//! 1. Names are bound correctly.
6//! 2. Refinement parameters appear in allowed positions. This is particularly important for
7//!    refinement predicates, aka abstract refinements, since the syntax in [`rty`] has
8//!    syntactic restrictions on predicates.
9//! 3. Refinements are well-sorted.
10
11pub mod struct_compat;
12use std::{borrow::Borrow, iter};
13
14use flux_common::{
15    bug,
16    dbg::{self, SpanTrace},
17    iter::IterExt,
18    result::ResultExt as _,
19    span_bug,
20};
21use flux_middle::{
22    THEORY_FUNCS,
23    def_id::{FluxDefId, MaybeExternId},
24    fhir::{self, FhirId, FluxOwnerId, QPathExpr},
25    global_env::GlobalEnv,
26    queries::{QueryErr, QueryResult},
27    query_bug,
28    rty::{
29        self, AssocReft, BoundReftKind, ESpan, INNERMOST, InternalFuncKind, List, RefineArgsExt,
30        WfckResults,
31        fold::TypeFoldable,
32        refining::{self, Refine, Refiner},
33    },
34};
35use flux_rustc_bridge::{
36    ToRustc,
37    lowering::{Lower, UnsupportedErr},
38};
39use itertools::Itertools;
40use rustc_data_structures::{
41    fx::{FxHashMap, FxIndexMap},
42    unord::UnordMap,
43};
44use rustc_errors::Diagnostic;
45use rustc_hash::FxHashSet;
46use rustc_hir::{self as hir, BodyId, OwnerId, Safety, def::DefKind, def_id::DefId};
47use rustc_index::IndexVec;
48use rustc_middle::{
49    middle::resolve_bound_vars::ResolvedArg,
50    ty::{self, AssocItem, AssocTag, BoundVar, TyCtxt},
51};
52use rustc_span::{
53    DUMMY_SP, ErrorGuaranteed, Span, Symbol,
54    symbol::{Ident, kw},
55};
56use rustc_trait_selection::traits;
57use rustc_type_ir::DebruijnIndex;
58
59/// Wrapper over a type implementing [`ConvPhase`]. We have this to implement most functionality as
60/// inherent methods instead of defining them as default implementation in the trait definition.
61#[repr(transparent)]
62pub struct ConvCtxt<P>(P);
63
64pub(crate) struct AfterSortck<'a, 'genv, 'tcx> {
65    genv: GlobalEnv<'genv, 'tcx>,
66    wfckresults: &'a WfckResults,
67    next_sort_index: u32,
68    next_type_index: u32,
69    next_region_index: u32,
70    next_const_index: u32,
71}
72
73/// We do conversion twice: once before sort checking when we don't have elaborated information
74/// and then again after sort checking after all information has been elaborated. This is the
75/// interface to configure conversion for both *phases*.
76pub trait ConvPhase<'genv, 'tcx>: Sized {
77    /// Whether to expand type aliases or to generate a *weak* [`rty::AliasTy`].
78    const EXPAND_TYPE_ALIASES: bool;
79
80    /// Whether we have elaborated information or not (in the first phase we will not, but in the
81    /// second we will).
82    const HAS_ELABORATED_INFORMATION: bool;
83
84    type Results: WfckResultsProvider;
85
86    fn genv(&self) -> GlobalEnv<'genv, 'tcx>;
87
88    fn owner(&self) -> FluxOwnerId;
89
90    fn next_sort_vid(&mut self) -> rty::SortVid;
91
92    fn next_type_vid(&mut self) -> rty::TyVid;
93
94    fn next_region_vid(&mut self) -> rty::RegionVid;
95
96    fn next_const_vid(&mut self) -> rty::ConstVid;
97
98    fn results(&self) -> &Self::Results;
99
100    /// Called during the first phase to collect the sort associated to a node which
101    /// would be hard to recompute from `fhir` otherwise. Currently, this is being
102    /// called when converting:
103    /// * An indexed type `b[e]` with the `fhir_id` and sort of `b`.
104    /// * A [`fhir::PathExpr`] with the `fhir_id` and sort of the path.
105    fn insert_node_sort(&mut self, fhir_id: FhirId, sort: rty::Sort);
106
107    /// Called after converting a path with the generic arguments. Using during the first phase
108    /// to instantiate sort of generic refinements.
109    fn insert_path_args(&mut self, fhir_id: FhirId, args: rty::GenericArgs);
110
111    /// Called after converting an [`fhir::ExprKind::Alias`] with the sort of the resulting
112    /// [`rty::AliasReft`]. Used during the first phase to collect the sorts of refinement aliases.
113    fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: rty::FuncSort);
114
115    fn into_conv_ctxt(self) -> ConvCtxt<Self> {
116        ConvCtxt(self)
117    }
118
119    fn as_conv_ctxt(&mut self) -> &mut ConvCtxt<Self> {
120        // SAFETY: `ConvCtxt` is `repr(transparent)` and it doesn't have any safety invariants.
121        unsafe { std::mem::transmute(self) }
122    }
123}
124
125/// An interface to the information elaborated during sort checking. We mock these results in
126/// the first conversion phase during sort checking.
127pub trait WfckResultsProvider: Sized {
128    fn bin_op_sort(&self, fhir_id: FhirId) -> rty::Sort;
129
130    fn coercions_for(&self, fhir_id: FhirId) -> &[rty::Coercion];
131
132    fn field_proj(&self, fhir_id: FhirId) -> rty::FieldProj;
133
134    fn record_ctor(&self, fhir_id: FhirId) -> DefId;
135
136    fn param_sort(&self, param_id: fhir::ParamId) -> rty::Sort;
137
138    fn node_sort(&self, fhir_id: FhirId) -> rty::Sort;
139
140    fn node_sort_args(&self, fhir_id: FhirId) -> List<rty::SortArg>;
141}
142
143impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for AfterSortck<'_, 'genv, 'tcx> {
144    const EXPAND_TYPE_ALIASES: bool = true;
145    const HAS_ELABORATED_INFORMATION: bool = true;
146
147    type Results = WfckResults;
148
149    fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
150        self.genv
151    }
152
153    fn owner(&self) -> FluxOwnerId {
154        self.wfckresults.owner
155    }
156
157    fn next_sort_vid(&mut self) -> rty::SortVid {
158        self.next_sort_index = self.next_sort_index.checked_add(1).unwrap();
159        rty::SortVid::from_u32(self.next_sort_index - 1)
160    }
161
162    fn next_type_vid(&mut self) -> rty::TyVid {
163        self.next_type_index = self.next_type_index.checked_add(1).unwrap();
164        rty::TyVid::from_u32(self.next_type_index - 1)
165    }
166
167    fn next_region_vid(&mut self) -> rty::RegionVid {
168        self.next_region_index = self.next_region_index.checked_add(1).unwrap();
169        rty::RegionVid::from_u32(self.next_region_index - 1)
170    }
171
172    fn next_const_vid(&mut self) -> rty::ConstVid {
173        self.next_const_index = self.next_const_index.checked_add(1).unwrap();
174        rty::ConstVid::from_u32(self.next_const_index - 1)
175    }
176
177    fn results(&self) -> &Self::Results {
178        self.wfckresults
179    }
180
181    fn insert_node_sort(&mut self, _: FhirId, _: rty::Sort) {}
182
183    fn insert_path_args(&mut self, _: FhirId, _: rty::GenericArgs) {}
184
185    fn insert_alias_reft_sort(&mut self, _: FhirId, _: rty::FuncSort) {}
186}
187
188impl WfckResultsProvider for WfckResults {
189    fn bin_op_sort(&self, fhir_id: FhirId) -> rty::Sort {
190        self.bin_op_sorts()
191            .get(fhir_id)
192            .cloned()
193            .unwrap_or_else(|| bug!("binary relation without elaborated sort `{fhir_id:?}`"))
194    }
195
196    fn coercions_for(&self, fhir_id: FhirId) -> &[rty::Coercion] {
197        self.coercions().get(fhir_id).map_or(&[][..], Vec::as_slice)
198    }
199
200    fn field_proj(&self, fhir_id: FhirId) -> rty::FieldProj {
201        *self
202            .field_projs()
203            .get(fhir_id)
204            .unwrap_or_else(|| bug!("field projection without elaboration `{fhir_id:?}`"))
205    }
206
207    fn record_ctor(&self, fhir_id: FhirId) -> DefId {
208        *self
209            .record_ctors()
210            .get(fhir_id)
211            .unwrap_or_else(|| bug!("unelaborated record constructor `{fhir_id:?}`"))
212    }
213
214    fn param_sort(&self, param_id: fhir::ParamId) -> rty::Sort {
215        self.param_sorts()
216            .get(&param_id)
217            .unwrap_or_else(|| bug!("unresolved sort for param `{param_id:?}`"))
218            .clone()
219    }
220
221    fn node_sort(&self, fhir_id: FhirId) -> rty::Sort {
222        self.node_sorts()
223            .get(fhir_id)
224            .unwrap_or_else(|| bug!("node without elaborated sort for `{fhir_id:?}`"))
225            .clone()
226    }
227
228    fn node_sort_args(&self, fhir_id: FhirId) -> List<rty::SortArg> {
229        self.fn_app_sorts()
230            .get(fhir_id)
231            .unwrap_or_else(|| bug!("fn-app node without elaborated sort_args for `{fhir_id:?}`"))
232            .clone()
233    }
234}
235
236#[derive(Debug)]
237pub(crate) struct Env {
238    layers: Vec<Layer>,
239    early_params: FxIndexMap<fhir::ParamId, Symbol>,
240}
241
242#[derive(Debug, Clone)]
243struct Layer {
244    map: FxIndexMap<fhir::ParamId, ParamEntry>,
245    kind: LayerKind,
246}
247
248/// Whether the list of parameters in a layer is converted into a list of bound variables or
249/// coalesced into a single parameter of [adt] sort.
250///
251/// [adt]: rty::SortCtor::Adt
252#[derive(Debug, Clone, Copy)]
253enum LayerKind {
254    List {
255        /// The number of regions bound in this layer. Since regions and refinements are both
256        /// bound with a [`rty::Binder`] we need to keep track of the number of bound regions
257        /// to skip them when assigning an index to refinement parameters.
258        bound_regions: u32,
259    },
260    Coalesce(DefId),
261}
262
263#[derive(Debug, Clone)]
264struct ParamEntry {
265    name: Symbol,
266    sort: rty::Sort,
267    mode: rty::InferMode,
268}
269
270#[derive(Debug)]
271struct LookupResult<'a> {
272    kind: LookupResultKind<'a>,
273    /// The span of the variable that originated the lookup.
274    var_span: Span,
275}
276
277#[derive(Debug)]
278enum LookupResultKind<'a> {
279    Bound {
280        debruijn: DebruijnIndex,
281        entry: &'a ParamEntry,
282        kind: LayerKind,
283        /// The index of the parameter in the layer.
284        index: u32,
285    },
286    EarlyParam {
287        name: Symbol,
288        /// The index of the parameter.
289        index: u32,
290    },
291}
292
293pub(crate) fn conv_adt_sort_def(
294    genv: GlobalEnv,
295    def_id: MaybeExternId,
296    kind: &fhir::RefinementKind,
297) -> QueryResult<rty::AdtSortDef> {
298    let wfckresults = &WfckResults::new(OwnerId { def_id: def_id.local_id() });
299    let mut cx = AfterSortck::new(genv, wfckresults).into_conv_ctxt();
300    match kind {
301        fhir::RefinementKind::Refined(refined_by) => {
302            let params = refined_by
303                .sort_params
304                .iter()
305                .map(|def_id| def_id_to_param_ty(genv, *def_id))
306                .collect();
307            let fields = refined_by
308                .fields
309                .iter()
310                .map(|(name, sort)| -> QueryResult<_> { Ok((*name, cx.conv_sort(sort)?)) })
311                .try_collect_vec()?;
312            let variants = IndexVec::from([rty::AdtSortVariant::new(fields)]);
313            let def_id = def_id.resolved_id();
314            Ok(rty::AdtSortDef::new(def_id, params, variants, false, true))
315        }
316        fhir::RefinementKind::Reflected => {
317            let enum_def_id = def_id.resolved_id();
318            let mut variants = IndexVec::new();
319            for variant in genv.tcx().adt_def(enum_def_id).variants() {
320                if let Some(field) = variant.fields.iter().next() {
321                    let span = genv.tcx().def_span(field.did);
322                    let err = genv
323                        .sess()
324                        .emit_err(errors::FieldsOnReflectedEnumVariant::new(span));
325                    Err(err)?;
326                }
327                variants.push(rty::AdtSortVariant::new(vec![]));
328            }
329            Ok(rty::AdtSortDef::new(enum_def_id, vec![], variants, true, false))
330        }
331    }
332}
333
334pub(crate) fn conv_generics(
335    genv: GlobalEnv,
336    generics: &fhir::Generics,
337    def_id: MaybeExternId,
338    is_trait: bool,
339) -> rty::Generics {
340    let opt_self = is_trait.then(|| {
341        let kind = rty::GenericParamDefKind::Base { has_default: false };
342        rty::GenericParamDef { index: 0, name: kw::SelfUpper, def_id: def_id.resolved_id(), kind }
343    });
344    let rust_generics = genv.tcx().generics_of(def_id.resolved_id());
345    let params = {
346        opt_self
347            .into_iter()
348            .chain(rust_generics.own_params.iter().flat_map(|rust_param| {
349                // We have to filter out late bound parameters
350                let param = generics
351                    .params
352                    .iter()
353                    .find(|param| param.def_id.resolved_id() == rust_param.def_id)?;
354                Some(rty::GenericParamDef {
355                    kind: conv_generic_param_kind(&param.kind),
356                    def_id: param.def_id.resolved_id(),
357                    index: rust_param.index,
358                    name: rust_param.name,
359                })
360            }))
361            .collect_vec()
362    };
363
364    let rust_generics = genv.tcx().generics_of(def_id.resolved_id());
365    rty::Generics {
366        own_params: List::from_vec(params),
367        parent: rust_generics.parent,
368        parent_count: rust_generics.parent_count,
369        has_self: rust_generics.has_self,
370    }
371}
372
373pub(crate) fn conv_refinement_generics(
374    params: &[fhir::RefineParam],
375    wfckresults: &WfckResults,
376) -> QueryResult<List<rty::RefineParam>> {
377    params
378        .iter()
379        .map(|param| {
380            let sort = wfckresults.param_sort(param.id);
381            let mode = rty::InferMode::from_param_kind(param.kind);
382            Ok(rty::RefineParam { sort, name: param.name, mode })
383        })
384        .try_collect()
385}
386
387fn conv_generic_param_kind(kind: &fhir::GenericParamKind) -> rty::GenericParamDefKind {
388    match kind {
389        fhir::GenericParamKind::Type { default } => {
390            rty::GenericParamDefKind::Base { has_default: default.is_some() }
391        }
392        fhir::GenericParamKind::Lifetime => rty::GenericParamDefKind::Lifetime,
393        fhir::GenericParamKind::Const { .. } => {
394            rty::GenericParamDefKind::Const { has_default: false }
395        }
396    }
397}
398
399pub(crate) fn conv_constant(genv: GlobalEnv, def_id: DefId) -> QueryResult<rty::ConstantInfo> {
400    let ty = genv.tcx().type_of(def_id).no_bound_vars().unwrap();
401    if ty.is_integral() {
402        let val = genv.tcx().const_eval_poly(def_id).ok().and_then(|val| {
403            let val = val.try_to_scalar_int()?;
404            rty::Constant::from_scalar_int(genv.tcx(), val, &ty)
405        });
406        if let Some(constant_) = val {
407            return Ok(rty::ConstantInfo::Interpreted(
408                rty::Expr::constant(constant_),
409                rty::Sort::Int,
410            ));
411        }
412        // FIXME(nilehmann) we should probably report an error in case const evaluation
413        // fails instead of silently ignore it.
414    }
415    Ok(rty::ConstantInfo::Uninterpreted)
416}
417
418pub(crate) fn conv_default_type_parameter(
419    genv: GlobalEnv,
420    def_id: MaybeExternId,
421    ty: &fhir::Ty,
422    wfckresults: &WfckResults,
423) -> QueryResult<rty::TyOrBase> {
424    let mut env = Env::new(&[]);
425    let idx = genv.def_id_to_param_index(def_id.resolved_id());
426    let owner = ty_param_owner(genv, def_id.resolved_id());
427    let param = genv.generics_of(owner)?.param_at(idx as usize, genv)?;
428    let mut cx = AfterSortck::new(genv, wfckresults).into_conv_ctxt();
429    let rty_ty = cx.conv_ty(&mut env, ty)?;
430    cx.try_to_ty_or_base(param.kind, ty.span, &rty_ty)
431}
432
433impl<'a, 'genv, 'tcx> AfterSortck<'a, 'genv, 'tcx> {
434    pub(crate) fn new(genv: GlobalEnv<'genv, 'tcx>, wfckresults: &'a WfckResults) -> Self {
435        Self {
436            genv,
437            wfckresults,
438            // We start sorts and types from 1 to skip the trait object dummy self type.
439            // See [`rty::Ty::trait_object_dummy_self`]
440            next_sort_index: 1,
441            next_type_index: 1,
442            next_region_index: 0,
443            next_const_index: 0,
444        }
445    }
446}
447
448/// Delegate methods to P
449impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
450    fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
451        self.0.genv()
452    }
453
454    fn tcx(&self) -> TyCtxt<'tcx> {
455        self.0.genv().tcx()
456    }
457
458    fn owner(&self) -> FluxOwnerId {
459        self.0.owner()
460    }
461
462    fn results(&self) -> &P::Results {
463        self.0.results()
464    }
465
466    fn next_sort_vid(&mut self) -> rty::SortVid {
467        self.0.next_sort_vid()
468    }
469
470    fn next_type_vid(&mut self) -> rty::TyVid {
471        self.0.next_type_vid()
472    }
473
474    fn next_region_vid(&mut self) -> rty::RegionVid {
475        self.0.next_region_vid()
476    }
477
478    fn next_const_vid(&mut self) -> rty::ConstVid {
479        self.0.next_const_vid()
480    }
481}
482
483fn variant_idx(tcx: TyCtxt, variant_def_id: DefId) -> rty::VariantIdx {
484    let enum_def_id = tcx.parent(variant_def_id);
485    tcx.adt_def(enum_def_id)
486        .variant_index_with_id(variant_def_id)
487}
488
489/// Conversion of Flux items
490impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
491    pub(crate) fn conv_qualifier(
492        &mut self,
493        qualifier: &fhir::Qualifier,
494    ) -> QueryResult<rty::Qualifier> {
495        let mut env = Env::new(&[]);
496        env.push_layer(Layer::list(self.results(), 0, qualifier.args));
497        let body = self.conv_expr(&mut env, &qualifier.expr)?;
498        let body = rty::Binder::bind_with_vars(body, env.pop_layer().into_bound_vars(self.genv())?);
499        Ok(rty::Qualifier { def_id: qualifier.def_id, body, global: qualifier.global })
500    }
501
502    pub(crate) fn conv_defn(
503        &mut self,
504        func: &fhir::SpecFunc,
505    ) -> QueryResult<Option<rty::Binder<rty::Expr>>> {
506        if let Some(body) = &func.body {
507            let mut env = Env::new(&[]);
508            env.push_layer(Layer::list(self.results(), 0, func.args));
509            let expr = self.conv_expr(&mut env, body)?;
510            let body =
511                rty::Binder::bind_with_vars(expr, env.pop_layer().into_bound_vars(self.genv())?);
512            Ok(Some(body))
513        } else {
514            Ok(None)
515        }
516    }
517
518    pub(crate) fn conv_primop_prop(
519        &mut self,
520        primop_prop: &fhir::PrimOpProp,
521    ) -> QueryResult<rty::PrimOpProp> {
522        let mut env = Env::new(&[]);
523        env.push_layer(Layer::list(self.results(), 0, primop_prop.args));
524        let body = self.conv_expr(&mut env, &primop_prop.body)?;
525        let body = rty::Binder::bind_with_vars(body, env.pop_layer().into_bound_vars(self.genv())?);
526        let op = match primop_prop.op {
527            fhir::BinOp::BitAnd => rty::BinOp::BitAnd,
528            fhir::BinOp::BitOr => rty::BinOp::BitOr,
529            fhir::BinOp::BitXor => rty::BinOp::BitXor,
530            fhir::BinOp::BitShl => rty::BinOp::BitShl,
531            fhir::BinOp::BitShr => rty::BinOp::BitShr,
532            _ => {
533                span_bug!(
534                    primop_prop.span,
535                    "unexpected binary operator in primitive property: {:?}",
536                    primop_prop.op
537                )
538            }
539        };
540        Ok(rty::PrimOpProp { def_id: primop_prop.def_id, op, body })
541    }
542}
543
544/// Conversion of definitions
545impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
546    pub(crate) fn conv_constant_expr(&mut self, expr: &fhir::Expr) -> QueryResult<rty::Expr> {
547        let mut env = Env::new(&[]);
548        self.conv_expr(&mut env, expr)
549    }
550
551    pub(crate) fn conv_enum_variants(
552        &mut self,
553        enum_id: MaybeExternId,
554        enum_def: &fhir::EnumDef,
555    ) -> QueryResult<Vec<rty::PolyVariant>> {
556        let reflected = enum_def.refinement.is_reflected();
557        enum_def
558            .variants
559            .iter()
560            .map(|variant| self.conv_enum_variant(enum_id, variant, reflected))
561            .try_collect_vec()
562    }
563
564    fn conv_enum_variant(
565        &mut self,
566        enum_id: MaybeExternId,
567        variant: &fhir::VariantDef,
568        reflected: bool,
569    ) -> QueryResult<rty::PolyVariant> {
570        let mut env = Env::new(&[]);
571        env.push_layer(Layer::list(self.results(), 0, variant.params));
572
573        // TODO(RJ): just "lift" the fields, ignore any `variant` signatures if reflected?
574        let fields = variant
575            .fields
576            .iter()
577            .map(|field| self.conv_ty(&mut env, &field.ty))
578            .try_collect()?;
579
580        let adt_def = self.genv().adt_def(enum_id)?;
581        let idxs = if reflected {
582            let enum_def_id = enum_id.resolved_id();
583            let idx = variant_idx(self.tcx(), variant.def_id.to_def_id());
584            rty::Expr::ctor_enum(enum_def_id, idx)
585        } else {
586            self.conv_expr(&mut env, &variant.ret.idx)?
587        };
588        let variant = rty::VariantSig::new(
589            adt_def,
590            rty::GenericArg::identity_for_item(self.genv(), enum_id.resolved_id())?,
591            fields,
592            idxs,
593            List::empty(),
594        );
595
596        Ok(rty::Binder::bind_with_vars(variant, env.pop_layer().into_bound_vars(self.genv())?))
597    }
598
599    pub(crate) fn conv_struct_variant(
600        &mut self,
601        struct_id: MaybeExternId,
602        struct_def: &fhir::StructDef,
603    ) -> QueryResult<rty::Opaqueness<rty::PolyVariant>> {
604        let mut env = Env::new(&[]);
605        env.push_layer(Layer::list(self.results(), 0, struct_def.params));
606
607        if let fhir::StructKind::Transparent { fields } = &struct_def.kind {
608            let adt_def = self.genv().adt_def(struct_id)?;
609
610            let fields = fields
611                .iter()
612                .map(|field_def| self.conv_ty(&mut env, &field_def.ty))
613                .try_collect()?;
614
615            let vars = env.pop_layer().into_bound_vars(self.genv())?;
616            let idx = rty::Expr::ctor_struct(
617                struct_id.resolved_id(),
618                (0..vars.len())
619                    .map(|idx| {
620                        rty::Expr::bvar(
621                            INNERMOST,
622                            BoundVar::from_usize(idx),
623                            rty::BoundReftKind::Anon,
624                        )
625                    })
626                    .collect(),
627            );
628
629            let requires = adt_def
630                .invariants()
631                .iter_identity()
632                .map(|inv| inv.apply(&idx))
633                .collect();
634
635            let variant = rty::VariantSig::new(
636                adt_def,
637                rty::GenericArg::identity_for_item(self.genv(), struct_id.resolved_id())?,
638                fields,
639                idx,
640                requires,
641            );
642            let variant = rty::Binder::bind_with_vars(variant, vars);
643            Ok(rty::Opaqueness::Transparent(variant))
644        } else {
645            Ok(rty::Opaqueness::Opaque)
646        }
647    }
648
649    pub(crate) fn conv_type_alias(
650        &mut self,
651        ty_alias_id: MaybeExternId,
652        ty_alias: &fhir::TyAlias,
653    ) -> QueryResult<rty::TyCtor> {
654        let generics = self
655            .genv()
656            .fhir_get_generics(ty_alias_id.local_id())?
657            .unwrap();
658
659        let mut env = Env::new(generics.refinement_params);
660
661        if let Some(index) = &ty_alias.index {
662            env.push_layer(Layer::list(self.results(), 0, std::slice::from_ref(index)));
663            let ty = self.conv_ty(&mut env, &ty_alias.ty)?;
664
665            Ok(rty::Binder::bind_with_vars(ty, env.pop_layer().into_bound_vars(self.genv())?))
666        } else {
667            let ctor = self
668                .conv_ty(&mut env, &ty_alias.ty)?
669                .shallow_canonicalize()
670                .as_ty_or_base()
671                .as_base()
672                .ok_or_else(|| self.emit(errors::InvalidBaseInstance::new(ty_alias.span)))?;
673            Ok(ctor.to_ty_ctor())
674        }
675    }
676
677    pub(crate) fn conv_fn_sig(
678        &mut self,
679        fn_id: MaybeExternId,
680        fn_sig: &fhir::FnSig,
681    ) -> QueryResult<rty::PolyFnSig> {
682        let decl = &fn_sig.decl;
683        let header = fn_sig.header;
684
685        let late_bound_regions =
686            refining::refine_bound_variables(&self.genv().lower_late_bound_vars(fn_id.local_id())?);
687
688        let generics = self.genv().fhir_get_generics(fn_id.local_id())?.unwrap();
689        let mut env = Env::new(generics.refinement_params);
690        env.push_layer(Layer::list(self.results(), late_bound_regions.len() as u32, &[]));
691
692        let body_id = self.tcx().hir_node_by_def_id(fn_id.local_id()).body_id();
693        let fn_sig = self.conv_fn_decl(&mut env, header.safety(), header.abi, decl, body_id)?;
694
695        let vars = late_bound_regions
696            .iter()
697            .chain(env.pop_layer().into_bound_vars(self.genv())?.iter())
698            .cloned()
699            .collect();
700
701        Ok(rty::PolyFnSig::bind_with_vars(fn_sig, vars))
702    }
703
704    pub(crate) fn conv_generic_predicates(
705        &mut self,
706        def_id: MaybeExternId,
707        generics: &fhir::Generics,
708    ) -> QueryResult<rty::EarlyBinder<rty::GenericPredicates>> {
709        let env = &mut Env::new(generics.refinement_params);
710
711        let predicates = if let Some(fhir_predicates) = generics.predicates {
712            let mut clauses = vec![];
713            for pred in fhir_predicates {
714                let span = pred.bounded_ty.span;
715                let bounded_ty = self.conv_ty(env, &pred.bounded_ty)?;
716                for clause in self.conv_generic_bounds(env, span, bounded_ty, pred.bounds)? {
717                    clauses.push(clause);
718                }
719            }
720            self.match_clauses(def_id, &clauses)?
721        } else {
722            self.genv()
723                .lower_predicates_of(def_id)?
724                .refine(&Refiner::default_for_item(self.genv(), def_id.resolved_id())?)?
725        };
726        Ok(rty::EarlyBinder(predicates))
727    }
728
729    fn match_clauses(
730        &self,
731        def_id: MaybeExternId,
732        refined_clauses: &[rty::Clause],
733    ) -> QueryResult<rty::GenericPredicates> {
734        let tcx = self.genv().tcx();
735        let predicates = tcx.predicates_of(def_id);
736        let unrefined_clauses = predicates.predicates;
737
738        // For each *refined clause* at index `j` find a corresponding *unrefined clause* at index
739        // `i` and save a mapping `i -> j`.
740        let mut map = UnordMap::default();
741        for (j, clause) in refined_clauses.iter().enumerate() {
742            let clause = clause.to_rustc(tcx);
743            let Some((i, _)) = unrefined_clauses.iter().find_position(|it| it.0 == clause) else {
744                self.emit_fail_to_match_predicates(def_id)?;
745            };
746            if map.insert(i, j).is_some() {
747                self.emit_fail_to_match_predicates(def_id)?;
748            }
749        }
750
751        // For each unrefined clause, create a default refined clause or use corresponding refined
752        // clause if one was found.
753        let refiner = Refiner::default_for_item(self.genv(), def_id.resolved_id())?;
754        let mut clauses = vec![];
755        for (i, (clause, span)) in unrefined_clauses.iter().enumerate() {
756            let clause = if let Some(j) = map.get(&i) {
757                refined_clauses[*j].clone()
758            } else {
759                clause
760                    .lower(tcx)
761                    .map_err(|reason| {
762                        let err = UnsupportedErr::new(reason).with_span(*span);
763                        QueryErr::unsupported(def_id.resolved_id(), err)
764                    })?
765                    .refine(&refiner)?
766            };
767            clauses.push(clause);
768        }
769
770        Ok(rty::GenericPredicates {
771            parent: predicates.parent,
772            predicates: List::from_vec(clauses),
773        })
774    }
775
776    fn emit_fail_to_match_predicates(&self, def_id: MaybeExternId) -> Result<!, ErrorGuaranteed> {
777        let span = self.tcx().def_span(def_id.resolved_id());
778        Err(self.emit(errors::FailToMatchPredicates { span }))
779    }
780
781    pub(crate) fn conv_opaque_ty(
782        &mut self,
783        opaque_ty: &fhir::OpaqueTy,
784    ) -> QueryResult<rty::Clauses> {
785        let def_id = opaque_ty.def_id;
786        let parent = self.tcx().local_parent(def_id.local_id());
787        let refparams = &self
788            .genv()
789            .fhir_get_generics(parent)?
790            .unwrap()
791            .refinement_params;
792
793        let env = &mut Env::new(refparams);
794
795        let args = rty::GenericArg::identity_for_item(self.genv(), def_id.resolved_id())?;
796        let alias_ty = rty::AliasTy::new(def_id.resolved_id(), args, env.to_early_param_args());
797        let self_ty = rty::BaseTy::opaque(alias_ty).to_ty();
798        // FIXME(nilehmann) use a good span here
799        Ok(self
800            .conv_generic_bounds(env, DUMMY_SP, self_ty, opaque_ty.bounds)?
801            .into_iter()
802            .collect())
803    }
804
805    pub(crate) fn conv_assoc_reft_body(
806        &mut self,
807        params: &[fhir::RefineParam],
808        body: &fhir::Expr,
809        output: &fhir::Sort,
810    ) -> QueryResult<rty::Lambda> {
811        let mut env = Env::new(&[]);
812        env.push_layer(Layer::list(self.results(), 0, params));
813        let expr = self.conv_expr(&mut env, body)?;
814        let output = self.conv_sort(output)?;
815        let inputs = env.pop_layer().into_bound_vars(self.genv())?;
816        Ok(rty::Lambda::bind_with_vars(expr, inputs, output))
817    }
818}
819
820/// Conversion of sorts
821impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
822    pub(crate) fn conv_sort(&mut self, sort: &fhir::Sort) -> QueryResult<rty::Sort> {
823        let sort = match sort {
824            fhir::Sort::Path(path) => self.conv_sort_path(path)?,
825            fhir::Sort::BitVec(size) => rty::Sort::BitVec(rty::BvSize::Fixed(*size)),
826            fhir::Sort::Loc => rty::Sort::Loc,
827            fhir::Sort::Func(fsort) => rty::Sort::Func(self.conv_poly_func_sort(fsort)?),
828            fhir::Sort::SortOf(bty) => {
829                let rty::TyOrCtor::Ctor(ty_ctor) = self.conv_bty(&mut Env::empty(), bty, None)?
830                else {
831                    // FIXME: maybe we should have a dedicated error for this
832                    return Err(self.emit(errors::RefinedUnrefinableType::new(bty.span)))?;
833                };
834                ty_ctor.sort()
835            }
836            fhir::Sort::Infer => rty::Sort::Infer(rty::SortVar(self.next_sort_vid())),
837            fhir::Sort::Err(_) => rty::Sort::Err,
838        };
839        Ok(sort)
840    }
841
842    fn conv_poly_func_sort(&mut self, sort: &fhir::PolyFuncSort) -> QueryResult<rty::PolyFuncSort> {
843        let params = iter::repeat_n(rty::SortParamKind::Sort, sort.params).collect();
844        Ok(rty::PolyFuncSort::new(params, self.conv_func_sort(&sort.fsort)?))
845    }
846
847    fn conv_func_sort(&mut self, fsort: &fhir::FuncSort) -> QueryResult<rty::FuncSort> {
848        let inputs = fsort
849            .inputs()
850            .iter()
851            .map(|sort| self.conv_sort(sort))
852            .try_collect()?;
853        Ok(rty::FuncSort::new(inputs, self.conv_sort(fsort.output())?))
854    }
855
856    fn conv_sort_path(&mut self, path: &fhir::SortPath) -> QueryResult<rty::Sort> {
857        let ctor = match path.res {
858            fhir::SortRes::PrimSort(fhir::PrimSort::Int) => {
859                self.check_prim_sort_generics(path, fhir::PrimSort::Int)?;
860                return Ok(rty::Sort::Int);
861            }
862            fhir::SortRes::PrimSort(fhir::PrimSort::Bool) => {
863                self.check_prim_sort_generics(path, fhir::PrimSort::Bool)?;
864                return Ok(rty::Sort::Bool);
865            }
866            fhir::SortRes::PrimSort(fhir::PrimSort::Real) => {
867                self.check_prim_sort_generics(path, fhir::PrimSort::Real)?;
868                return Ok(rty::Sort::Real);
869            }
870            fhir::SortRes::PrimSort(fhir::PrimSort::Char) => {
871                self.check_prim_sort_generics(path, fhir::PrimSort::Char)?;
872                return Ok(rty::Sort::Char);
873            }
874            fhir::SortRes::PrimSort(fhir::PrimSort::Str) => {
875                self.check_prim_sort_generics(path, fhir::PrimSort::Str)?;
876                return Ok(rty::Sort::Str);
877            }
878            fhir::SortRes::SortParam(n) => return Ok(rty::Sort::Var(rty::ParamSort::from(n))),
879            fhir::SortRes::TyParam(def_id) => {
880                if !path.args.is_empty() {
881                    let err = errors::GenericsOnSortTyParam::new(
882                        path.segments.last().unwrap().span,
883                        path.args.len(),
884                    );
885                    Err(self.emit(err))?;
886                }
887                return Ok(rty::Sort::Param(def_id_to_param_ty(self.genv(), def_id)));
888            }
889            fhir::SortRes::SelfParam { .. } => {
890                if !path.args.is_empty() {
891                    let err = errors::GenericsOnSelf::new(
892                        path.segments.last().unwrap().span,
893                        path.args.len(),
894                    );
895                    Err(self.emit(err))?;
896                }
897                return Ok(rty::Sort::Param(rty::SELF_PARAM_TY));
898            }
899            fhir::SortRes::SelfAlias { alias_to } => {
900                if !path.args.is_empty() {
901                    let err = errors::GenericsOnSelf::new(
902                        path.segments.last().unwrap().span,
903                        path.args.len(),
904                    );
905                    Err(self.emit(err))?;
906                }
907                return Ok(self
908                    .genv()
909                    .sort_of_self_ty_alias(alias_to)?
910                    .unwrap_or(rty::Sort::Err));
911            }
912            fhir::SortRes::SelfParamAssoc { trait_id, ident } => {
913                let res = fhir::Res::SelfTyParam { trait_: trait_id };
914                let assoc_segment =
915                    fhir::PathSegment { args: &[], constraints: &[], ident, res: fhir::Res::Err };
916                let mut env = Env::empty();
917                let alias_ty =
918                    self.conv_type_relative_type_path(&mut env, ident.span, res, &assoc_segment)?;
919                return Ok(rty::Sort::Alias(rty::AliasKind::Projection, alias_ty));
920            }
921            fhir::SortRes::PrimSort(fhir::PrimSort::Set) => {
922                self.check_prim_sort_generics(path, fhir::PrimSort::Set)?;
923                rty::SortCtor::Set
924            }
925            fhir::SortRes::PrimSort(fhir::PrimSort::Map) => {
926                self.check_prim_sort_generics(path, fhir::PrimSort::Map)?;
927                rty::SortCtor::Map
928            }
929            fhir::SortRes::User(def_id) => {
930                self.check_user_defined_sort_param_count(path, def_id)?;
931                rty::SortCtor::User(def_id)
932            }
933            fhir::SortRes::Adt(def_id) => {
934                let sort_def = self.genv().adt_sort_def_of(def_id)?;
935                if path.args.len() != sort_def.param_count() {
936                    let err = errors::IncorrectGenericsOnSort::new(
937                        self.genv(),
938                        def_id,
939                        path.segments.last().unwrap().span,
940                        path.args.len(),
941                        sort_def.param_count(),
942                    );
943                    Err(self.emit(err))?;
944                }
945                rty::SortCtor::Adt(sort_def)
946            }
947        };
948        let args = path.args.iter().map(|t| self.conv_sort(t)).try_collect()?;
949
950        Ok(rty::Sort::app(ctor, args))
951    }
952
953    fn check_user_defined_sort_param_count(
954        &mut self,
955        path: &fhir::SortPath<'_>,
956        def_id: FluxDefId,
957    ) -> QueryResult {
958        let expected_param_count = self.genv().sort_decl_param_count(def_id);
959        if path.args.len() != expected_param_count {
960            let err = errors::IncorrectGenericsOnUserDefinedOpaqueSort::new(
961                path.segments.last().unwrap().span,
962                def_id.name(),
963                expected_param_count,
964                path.args.len(),
965            );
966            Err(self.emit(err))?;
967        }
968        Ok(())
969    }
970
971    fn check_prim_sort_generics(
972        &mut self,
973        path: &fhir::SortPath<'_>,
974        prim_sort: fhir::PrimSort,
975    ) -> QueryResult {
976        if path.args.len() != prim_sort.generics() {
977            let err = errors::GenericsOnPrimitiveSort::new(
978                path.segments.last().unwrap().span,
979                prim_sort.name_str(),
980                path.args.len(),
981                prim_sort.generics(),
982            );
983            Err(self.emit(err))?;
984        }
985        Ok(())
986    }
987}
988
989/// Conversion of types
990impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
991    fn conv_fn_decl(
992        &mut self,
993        env: &mut Env,
994        safety: Safety,
995        abi: rustc_abi::ExternAbi,
996        decl: &fhir::FnDecl,
997        body_id: Option<BodyId>,
998    ) -> QueryResult<rty::FnSig> {
999        let mut requires = vec![];
1000        for req in decl.requires {
1001            requires.push(self.conv_requires(env, req)?);
1002        }
1003
1004        let mut inputs = vec![];
1005        let params =
1006            if let Some(body_id) = body_id { self.tcx().hir_body(body_id).params } else { &[] };
1007        for (i, ty) in decl.inputs.iter().enumerate() {
1008            let ty = if let Some(param) = params.get(i)
1009                && let hir::PatKind::Binding(_, _, ident, _) = param.pat.kind
1010            {
1011                self.conv_ty_with_name(env, ty, ident.name)?
1012            } else {
1013                self.conv_ty(env, ty)?
1014            };
1015            inputs.push(ty);
1016        }
1017
1018        let output = self.conv_fn_output(env, &decl.output)?;
1019
1020        Ok(rty::FnSig::new(safety, abi, requires.into(), inputs.into(), output))
1021    }
1022
1023    fn conv_requires(
1024        &mut self,
1025        env: &mut Env,
1026        requires: &fhir::Requires,
1027    ) -> QueryResult<rty::Expr> {
1028        if requires.params.is_empty() {
1029            self.conv_expr(env, &requires.pred)
1030        } else {
1031            env.push_layer(Layer::list(self.results(), 0, requires.params));
1032            let pred = self.conv_expr(env, &requires.pred)?;
1033            let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1034            Ok(rty::Expr::forall(rty::Binder::bind_with_vars(pred, sorts)))
1035        }
1036    }
1037
1038    fn conv_ensures(
1039        &mut self,
1040        env: &mut Env,
1041        ensures: &fhir::Ensures,
1042    ) -> QueryResult<rty::Ensures> {
1043        match ensures {
1044            fhir::Ensures::Type(loc, ty) => {
1045                Ok(rty::Ensures::Type(self.conv_loc(env, *loc)?, self.conv_ty(env, ty)?))
1046            }
1047            fhir::Ensures::Pred(pred) => Ok(rty::Ensures::Pred(self.conv_expr(env, pred)?)),
1048        }
1049    }
1050
1051    fn conv_fn_output(
1052        &mut self,
1053        env: &mut Env,
1054        output: &fhir::FnOutput,
1055    ) -> QueryResult<rty::Binder<rty::FnOutput>> {
1056        env.push_layer(Layer::list(self.results(), 0, output.params));
1057
1058        let ret = self.conv_ty(env, &output.ret)?;
1059
1060        let ensures: List<rty::Ensures> = output
1061            .ensures
1062            .iter()
1063            .map(|ens| self.conv_ensures(env, ens))
1064            .try_collect()?;
1065        let output = rty::FnOutput::new(ret, ensures);
1066
1067        let vars = env.pop_layer().into_bound_vars(self.genv())?;
1068        Ok(rty::Binder::bind_with_vars(output, vars))
1069    }
1070
1071    fn conv_generic_bounds(
1072        &mut self,
1073        env: &mut Env,
1074        bounded_ty_span: Span,
1075        bounded_ty: rty::Ty,
1076        bounds: fhir::GenericBounds,
1077    ) -> QueryResult<Vec<rty::Clause>> {
1078        let mut clauses = vec![];
1079        for bound in bounds {
1080            match bound {
1081                fhir::GenericBound::Trait(poly_trait_ref) => {
1082                    match poly_trait_ref.modifiers {
1083                        fhir::TraitBoundModifier::None => {
1084                            self.conv_poly_trait_ref(
1085                                env,
1086                                bounded_ty_span,
1087                                &bounded_ty,
1088                                poly_trait_ref,
1089                                &mut clauses,
1090                            )?;
1091                        }
1092                        fhir::TraitBoundModifier::Maybe => {
1093                            // Maybe bounds are only supported for `?Sized`. The effect of the maybe
1094                            // bound is to relax the default which is `Sized` to not have the `Sized`
1095                            // bound, so we just skip it here.
1096                        }
1097                    }
1098                }
1099                fhir::GenericBound::Outlives(lft) => {
1100                    let re = self.conv_lifetime(env, *lft, bounded_ty_span);
1101                    clauses.push(rty::Clause::new(
1102                        List::empty(),
1103                        rty::ClauseKind::TypeOutlives(rty::OutlivesPredicate(
1104                            bounded_ty.clone(),
1105                            re,
1106                        )),
1107                    ));
1108                }
1109            }
1110        }
1111        Ok(clauses)
1112    }
1113
1114    /// Converts a `T: Trait<T0, ..., A0 = S0, ...>` bound
1115    fn conv_poly_trait_ref(
1116        &mut self,
1117        env: &mut Env,
1118        span: Span,
1119        bounded_ty: &rty::Ty,
1120        poly_trait_ref: &fhir::PolyTraitRef,
1121        clauses: &mut Vec<rty::Clause>,
1122    ) -> QueryResult {
1123        let generic_params = &poly_trait_ref.bound_generic_params;
1124        let layer =
1125            Layer::list(self.results(), generic_params.len() as u32, poly_trait_ref.refine_params);
1126        env.push_layer(layer);
1127
1128        let trait_id = poly_trait_ref.trait_def_id();
1129        let generics = self.genv().generics_of(trait_id)?;
1130        let trait_segment = poly_trait_ref.trait_ref.last_segment();
1131
1132        let self_param = generics.param_at(0, self.genv())?;
1133        let mut args = vec![
1134            self.try_to_ty_or_base(self_param.kind, span, bounded_ty)?
1135                .into(),
1136        ];
1137        self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1138
1139        let vars = env.top_layer().to_bound_vars(self.genv())?;
1140        let poly_trait_ref = rty::Binder::bind_with_vars(
1141            rty::TraitRef { def_id: trait_id, args: args.into() },
1142            vars,
1143        );
1144
1145        clauses.push(
1146            poly_trait_ref
1147                .clone()
1148                .map(|trait_ref| {
1149                    rty::ClauseKind::Trait(rty::TraitPredicate { trait_ref: trait_ref.clone() })
1150                })
1151                .into(),
1152        );
1153
1154        for cstr in trait_segment.constraints {
1155            self.conv_assoc_item_constraint(env, &poly_trait_ref, cstr, clauses)?;
1156        }
1157
1158        env.pop_layer();
1159
1160        Ok(())
1161    }
1162
1163    fn conv_assoc_item_constraint(
1164        &mut self,
1165        env: &mut Env,
1166        poly_trait_ref: &rty::PolyTraitRef,
1167        constraint: &fhir::AssocItemConstraint,
1168        clauses: &mut Vec<rty::Clause>,
1169    ) -> QueryResult {
1170        let tcx = self.tcx();
1171
1172        let candidate = self.probe_single_bound_for_assoc_item(
1173            || traits::supertraits(tcx, poly_trait_ref.to_rustc(tcx)),
1174            constraint.ident,
1175            AssocTag::Type,
1176        )?;
1177        let assoc_item_id = AssocTag::Type
1178            .trait_defines_item_named(self.genv(), candidate.def_id(), constraint.ident)?
1179            .unwrap()
1180            .def_id;
1181
1182        let fhir::AssocItemConstraintKind::Equality { term } = &constraint.kind;
1183        let span = term.span;
1184        let term = self.conv_ty(env, term)?;
1185        let term = self.ty_to_subset_ty_ctor(span, &term)?;
1186
1187        let clause = poly_trait_ref
1188            .clone()
1189            .map(|trait_ref| {
1190                // TODO: when we support generic associated types, we need to also attach the associated generics here
1191                let args = trait_ref.args;
1192                let refine_args = List::empty();
1193                let projection_ty = rty::AliasTy { def_id: assoc_item_id, args, refine_args };
1194
1195                rty::ClauseKind::Projection(rty::ProjectionPredicate { projection_ty, term })
1196            })
1197            .into();
1198
1199        clauses.push(clause);
1200        Ok(())
1201    }
1202
1203    fn conv_ty_with_name(
1204        &mut self,
1205        env: &mut Env,
1206        ty: &fhir::Ty,
1207        name: Symbol,
1208    ) -> QueryResult<rty::Ty> {
1209        if let fhir::TyKind::BaseTy(bty) = &ty.kind {
1210            Ok(self.conv_bty(env, bty, Some(name))?.to_ty())
1211        } else {
1212            self.conv_ty(env, ty)
1213        }
1214    }
1215
1216    fn conv_ty(&mut self, env: &mut Env, ty: &fhir::Ty) -> QueryResult<rty::Ty> {
1217        match &ty.kind {
1218            fhir::TyKind::BaseTy(bty) => Ok(self.conv_bty(env, bty, None)?.to_ty()),
1219            fhir::TyKind::Indexed(bty, idx) => {
1220                let fhir_id = bty.fhir_id;
1221                let rty::TyOrCtor::Ctor(ty_ctor) = self.conv_bty(env, bty, None)? else {
1222                    return Err(self.emit(errors::RefinedUnrefinableType::new(bty.span)))?;
1223                };
1224                let idx = self.conv_expr(env, idx)?;
1225                self.0.insert_node_sort(fhir_id, ty_ctor.sort());
1226                Ok(ty_ctor.replace_bound_reft(&idx))
1227            }
1228            fhir::TyKind::Exists(params, ty) => {
1229                let layer = Layer::list(self.results(), 0, params);
1230                env.push_layer(layer);
1231                let ty = self.conv_ty(env, ty)?;
1232                let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1233                if sorts.is_empty() {
1234                    Ok(ty.shift_out_escaping(1))
1235                } else {
1236                    Ok(rty::Ty::exists(rty::Binder::bind_with_vars(ty, sorts)))
1237                }
1238            }
1239            fhir::TyKind::StrgRef(lft, loc, ty) => {
1240                let re = self.conv_lifetime(env, *lft, ty.span);
1241                let loc = self.conv_loc(env, **loc)?;
1242                let ty = self.conv_ty(env, ty)?;
1243                Ok(rty::Ty::strg_ref(re, loc, ty))
1244            }
1245            fhir::TyKind::Ref(lft, fhir::MutTy { ty, mutbl }) => {
1246                let region = self.conv_lifetime(env, *lft, ty.span);
1247                Ok(rty::Ty::mk_ref(region, self.conv_ty(env, ty)?, *mutbl))
1248            }
1249            fhir::TyKind::BareFn(bare_fn) => {
1250                let mut env = Env::empty();
1251                env.push_layer(Layer::list(
1252                    self.results(),
1253                    bare_fn.generic_params.len() as u32,
1254                    &[],
1255                ));
1256                let fn_sig =
1257                    self.conv_fn_decl(&mut env, bare_fn.safety, bare_fn.abi, bare_fn.decl, None)?;
1258                let vars = bare_fn
1259                    .generic_params
1260                    .iter()
1261                    .map(|param| self.param_as_bound_var(param))
1262                    .try_collect()?;
1263                let poly_fn_sig = rty::Binder::bind_with_vars(fn_sig, vars);
1264                Ok(rty::BaseTy::FnPtr(poly_fn_sig).to_ty())
1265            }
1266            fhir::TyKind::Tuple(tys) => {
1267                let tys: List<rty::Ty> =
1268                    tys.iter().map(|ty| self.conv_ty(env, ty)).try_collect()?;
1269                Ok(rty::Ty::tuple(tys))
1270            }
1271            fhir::TyKind::Array(ty, len) => {
1272                Ok(rty::Ty::array(self.conv_ty(env, ty)?, self.conv_const_arg(*len)))
1273            }
1274            fhir::TyKind::Never => Ok(rty::Ty::never()),
1275            fhir::TyKind::Constr(pred, ty) => {
1276                let pred = self.conv_expr(env, pred)?;
1277                Ok(rty::Ty::constr(pred, self.conv_ty(env, ty)?))
1278            }
1279            fhir::TyKind::RawPtr(ty, mutability) => {
1280                Ok(rty::Ty::indexed(
1281                    rty::BaseTy::RawPtr(self.conv_ty(env, ty)?, *mutability),
1282                    rty::Expr::unit(),
1283                ))
1284            }
1285            fhir::TyKind::OpaqueDef(opaque_ty) => self.conv_opaque_def(env, opaque_ty, ty.span),
1286            fhir::TyKind::TraitObject(trait_bounds, lft, syn) => {
1287                if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) {
1288                    self.conv_trait_object(env, trait_bounds, *lft, ty.span)
1289                } else {
1290                    span_bug!(ty.span, "dyn* traits not supported yet")
1291                }
1292            }
1293            fhir::TyKind::Infer => Ok(rty::Ty::infer(self.next_type_vid())),
1294            fhir::TyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1295        }
1296    }
1297
1298    /// Code adapted from <https://github.com/rust-lang/rust/blob/b5723af3457b9cd3795eeb97e9af2d34964854f2/compiler/rustc_hir_analysis/src/hir_ty_lowering/mod.rs#L2099>
1299    fn conv_opaque_def(
1300        &mut self,
1301        env: &mut Env,
1302        opaque_ty: &fhir::OpaqueTy,
1303        span: Span,
1304    ) -> QueryResult<rty::Ty> {
1305        let def_id = opaque_ty.def_id;
1306
1307        if P::HAS_ELABORATED_INFORMATION {
1308            let lifetimes = self.tcx().opaque_captured_lifetimes(def_id.local_id());
1309
1310            let generics = self.tcx().generics_of(opaque_ty.def_id);
1311
1312            let offset = generics.parent_count;
1313
1314            let args = rty::GenericArg::for_item(self.genv(), def_id.resolved_id(), |param, _| {
1315                if let Some(i) = (param.index as usize).checked_sub(offset) {
1316                    let (lifetime, _) = lifetimes[i];
1317                    rty::GenericArg::Lifetime(self.conv_resolved_lifetime(env, lifetime, span))
1318                } else {
1319                    rty::GenericArg::from_param_def(param)
1320                }
1321            })?;
1322            let reft_args = rty::RefineArgs::identity_for_item(self.genv(), def_id.resolved_id())?;
1323            let alias_ty = rty::AliasTy::new(def_id.resolved_id(), args, reft_args);
1324            Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1325        } else {
1326            // During sortck we need to run conv on the opaque type to collect sorts for base types
1327            // in the opaque type's bounds. After sortck, we don't need to because opaque types are
1328            // converted as part of `genv.item_bounds`.
1329            self.conv_opaque_ty(opaque_ty)?;
1330
1331            // `RefineArgs::identity_for_item` uses `genv.refinement_generics_of` which in turn
1332            // requires `genv.check_wf`, so we simply return all empty here to avoid the circularity
1333            let alias_ty = rty::AliasTy::new(def_id.resolved_id(), List::empty(), List::empty());
1334            Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1335        }
1336    }
1337
1338    fn conv_trait_object(
1339        &mut self,
1340        env: &mut Env,
1341        trait_bounds: &[fhir::PolyTraitRef],
1342        lifetime: fhir::Lifetime,
1343        span: Span,
1344    ) -> QueryResult<rty::Ty> {
1345        // We convert all the trait bounds into existential predicates. Some combinations won't yield
1346        // valid rust types (e.g., only one regular (non-auto) trait is allowed). We don't detect those
1347        // errors here, but that's fine because we should catch them when we check structural
1348        // compatibility with the unrefined rust type. We must be careful with producing predicates
1349        // in the same order that rustc does.
1350
1351        let mut bounds = vec![];
1352        let dummy_self = rty::Ty::trait_object_dummy_self();
1353        for trait_bound in trait_bounds.iter().rev() {
1354            self.conv_poly_trait_ref(env, trait_bound.span, &dummy_self, trait_bound, &mut bounds)?;
1355        }
1356
1357        // Separate trait bounds and projections bounds
1358        let mut trait_bounds = vec![];
1359        let mut projection_bounds = vec![];
1360        for pred in bounds {
1361            let bound_pred = pred.kind();
1362            let vars = bound_pred.vars().clone();
1363            match bound_pred.skip_binder() {
1364                rty::ClauseKind::Trait(trait_pred) => {
1365                    trait_bounds.push(rty::Binder::bind_with_vars(trait_pred.trait_ref, vars));
1366                }
1367                rty::ClauseKind::Projection(proj) => {
1368                    projection_bounds.push(rty::Binder::bind_with_vars(proj, vars));
1369                }
1370                rty::ClauseKind::RegionOutlives(_) => {}
1371                rty::ClauseKind::TypeOutlives(_) => {}
1372                rty::ClauseKind::ConstArgHasType(..) => {
1373                    bug!("did not expect {pred:?} clause in object bounds");
1374                }
1375            }
1376        }
1377
1378        // Separate between regular from auto traits
1379        let (mut auto_traits, regular_traits): (Vec<_>, Vec<_>) = trait_bounds
1380            .into_iter()
1381            .partition(|trait_ref| self.tcx().trait_is_auto(trait_ref.def_id()));
1382
1383        // De-duplicate auto traits preserving order
1384        {
1385            let mut duplicates = FxHashSet::default();
1386            auto_traits.retain(|trait_ref| duplicates.insert(trait_ref.def_id()));
1387        }
1388
1389        let regular_trait_predicates = regular_traits.into_iter().map(|poly_trait_ref| {
1390            poly_trait_ref.map(|trait_ref| {
1391                // Remove dummy self
1392                let args = trait_ref.args.iter().skip(1).cloned().collect();
1393                rty::ExistentialPredicate::Trait(rty::ExistentialTraitRef {
1394                    def_id: trait_ref.def_id,
1395                    args,
1396                })
1397            })
1398        });
1399
1400        let auto_trait_predicates = auto_traits.into_iter().map(|trait_def| {
1401            rty::Binder::dummy(rty::ExistentialPredicate::AutoTrait(trait_def.def_id()))
1402        });
1403
1404        let existential_projections = projection_bounds.into_iter().map(|bound| {
1405            bound.map(|proj| {
1406                // Remove dummy self
1407                let args = proj.projection_ty.args.iter().skip(1).cloned().collect();
1408                rty::ExistentialPredicate::Projection(rty::ExistentialProjection {
1409                    def_id: proj.projection_ty.def_id,
1410                    args,
1411                    term: proj.term.clone(),
1412                })
1413            })
1414        });
1415
1416        let existential_predicates = {
1417            let mut v = regular_trait_predicates
1418                .chain(existential_projections)
1419                .chain(auto_trait_predicates)
1420                .collect_vec();
1421            v.sort_by(|a, b| {
1422                a.as_ref()
1423                    .skip_binder()
1424                    .stable_cmp(self.tcx(), b.as_ref().skip_binder())
1425            });
1426            List::from_vec(v)
1427        };
1428
1429        let region = self.conv_lifetime(env, lifetime, span);
1430        Ok(rty::Ty::dynamic(existential_predicates, region))
1431    }
1432
1433    pub(crate) fn conv_bty(
1434        &mut self,
1435        env: &mut Env,
1436        bty: &fhir::BaseTy,
1437        name: Option<Symbol>,
1438    ) -> QueryResult<rty::TyOrCtor> {
1439        match &bty.kind {
1440            fhir::BaseTyKind::Path(fhir::QPath::Resolved(qself, path)) => {
1441                self.conv_qpath(env, *qself, path, name)
1442            }
1443            fhir::BaseTyKind::Path(fhir::QPath::TypeRelative(qself, segment)) => {
1444                let qself_res =
1445                    if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
1446                let alias_ty = self
1447                    .conv_type_relative_type_path(env, qself.span, qself_res, segment)?
1448                    .shift_in_escaping(1);
1449                let bty = rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty);
1450                let sort = bty.sort();
1451                let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1452                Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1453            }
1454            fhir::BaseTyKind::Slice(ty) => {
1455                let bty = rty::BaseTy::Slice(self.conv_ty(env, ty)?).shift_in_escaping(1);
1456                let sort = bty.sort();
1457                let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1458                Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1459            }
1460            fhir::BaseTyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1461        }
1462    }
1463
1464    fn conv_type_relative_path<Tag: AssocItemTag>(
1465        &mut self,
1466        tag: Tag,
1467        qself_span: Span,
1468        qself_res: fhir::Res,
1469        assoc_ident: Ident,
1470    ) -> QueryResult<(Tag::AssocItem<'tcx>, rty::TraitRef)> {
1471        let tcx = self.tcx();
1472
1473        let bound = match qself_res {
1474            fhir::Res::SelfTyAlias { alias_to: impl_def_id, is_trait_impl: true } => {
1475                let Some(trait_ref) = tcx.impl_trait_ref(impl_def_id) else {
1476                    // A cycle error occurred most likely (comment copied from rustc)
1477                    span_bug!(qself_span, "expected cycle error");
1478                };
1479
1480                self.probe_single_bound_for_assoc_item(
1481                    || {
1482                        traits::supertraits(
1483                            tcx,
1484                            ty::Binder::dummy(trait_ref.instantiate_identity()),
1485                        )
1486                    },
1487                    assoc_ident,
1488                    tag,
1489                )?
1490            }
1491            fhir::Res::Def(DefKind::TyParam, param_id)
1492            | fhir::Res::SelfTyParam { trait_: param_id } => {
1493                let predicates = type_param_predicates(tcx, param_id);
1494                self.probe_single_bound_for_assoc_item(
1495                    || {
1496                        tag.transitive_bounds_that_define_assoc_item(
1497                            self.genv(),
1498                            predicates.map(|pred| pred.map_bound(|t| t.trait_ref)),
1499                            assoc_ident,
1500                        )
1501                    },
1502                    assoc_ident,
1503                    tag,
1504                )?
1505            }
1506            _ => self.report_assoc_item_not_found(assoc_ident.span, tag)?,
1507        };
1508
1509        let Some(trait_ref) = bound.no_bound_vars() else {
1510            // This is a programmer error and we should gracefully report it. It's triggered
1511            // by code like this
1512            // ```
1513            // trait Super<'a> { type Assoc; }
1514            // trait Child: for<'a> Super<'a> {}
1515            // fn foo<T: Child>(x: T::Assoc) {}
1516            // ```
1517            Err(self.emit(
1518                query_bug!("associated path with uninferred generic parameters")
1519                    .at(assoc_ident.span),
1520            ))?
1521        };
1522
1523        let trait_ref = trait_ref
1524            .lower(tcx)
1525            .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?
1526            .refine(&self.refiner()?)?;
1527
1528        let assoc_item = tag
1529            .trait_defines_item_named(self.genv(), trait_ref.def_id, assoc_ident)?
1530            .unwrap();
1531
1532        Ok((assoc_item, trait_ref))
1533    }
1534
1535    fn conv_type_relative_type_path(
1536        &mut self,
1537        env: &mut Env,
1538        qself_span: Span,
1539        qself_res: fhir::Res,
1540        assoc_segment: &fhir::PathSegment,
1541    ) -> QueryResult<rty::AliasTy> {
1542        let (assoc_item, trait_ref) = self.conv_type_relative_path(
1543            AssocTag::Type,
1544            qself_span,
1545            qself_res,
1546            assoc_segment.ident,
1547        )?;
1548
1549        let assoc_id = assoc_item.def_id;
1550        let mut args = trait_ref.args.to_vec();
1551        self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1552
1553        let args = List::from_vec(args);
1554        let refine_args = List::empty();
1555        let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1556        Ok(alias_ty)
1557    }
1558
1559    fn conv_type_relative_const_path(
1560        &mut self,
1561        fhir_expr: &fhir::Expr,
1562        qself: &rty::Ty,
1563        assoc: Ident,
1564    ) -> QueryResult<rty::Expr> {
1565        let tcx = self.genv().tcx();
1566
1567        let mut candidates = vec![];
1568        if let Some(simplified_type) = qself.simplify_type() {
1569            candidates = tcx
1570                .incoherent_impls(simplified_type)
1571                .iter()
1572                .filter_map(|impl_id| {
1573                    tcx.associated_items(impl_id).find_by_ident_and_kind(
1574                        tcx,
1575                        assoc,
1576                        AssocTag::Const,
1577                        *impl_id,
1578                    )
1579                })
1580                .collect_vec();
1581        }
1582        let (expr, sort) = match &candidates[..] {
1583            [candidate] => self.conv_const(fhir_expr.span, candidate.def_id)?,
1584            [] => self.report_assoc_item_not_found(fhir_expr.span, AssocTag::Const)?,
1585            _ => self.report_ambiguous_assoc_item(fhir_expr.span, AssocTag::Const, assoc)?,
1586        };
1587        self.0.insert_node_sort(fhir_expr.fhir_id, sort);
1588        Ok(expr)
1589    }
1590
1591    /// Return the generics of the containing owner item
1592    fn refiner(&self) -> QueryResult<Refiner<'genv, 'tcx>> {
1593        match self.owner() {
1594            FluxOwnerId::Rust(owner_id) => {
1595                let def_id = self.genv().maybe_extern_id(owner_id.def_id);
1596                Refiner::default_for_item(self.genv(), def_id.resolved_id())
1597            }
1598            FluxOwnerId::Flux(_) => Err(query_bug!("cannot refine types insicde flux item")),
1599        }
1600    }
1601
1602    fn probe_single_bound_for_assoc_item<I, Tag: AssocItemTag>(
1603        &self,
1604        all_candidates: impl FnOnce() -> I,
1605        assoc_name: Ident,
1606        tag: Tag,
1607    ) -> QueryResult<ty::PolyTraitRef<'tcx>>
1608    where
1609        I: Iterator<Item = ty::PolyTraitRef<'tcx>>,
1610    {
1611        let mut matching_candidates = vec![];
1612        for candidate in all_candidates() {
1613            if tag
1614                .trait_defines_item_named(self.genv(), candidate.def_id(), assoc_name)?
1615                .is_some()
1616            {
1617                matching_candidates.push(candidate);
1618            }
1619        }
1620
1621        let Some(bound) = matching_candidates.pop() else {
1622            self.report_assoc_item_not_found(assoc_name.span, tag)?;
1623        };
1624
1625        if !matching_candidates.is_empty() {
1626            self.report_ambiguous_assoc_item(assoc_name.span, tag, assoc_name)?;
1627        }
1628
1629        Ok(bound)
1630    }
1631
1632    fn conv_lifetime(&mut self, env: &Env, lft: fhir::Lifetime, span: Span) -> rty::Region {
1633        let res = match lft {
1634            fhir::Lifetime::Hole(_) => return rty::Region::ReVar(self.next_region_vid()),
1635            fhir::Lifetime::Resolved(res) => res,
1636        };
1637        self.conv_resolved_lifetime(env, res, span)
1638    }
1639
1640    fn conv_resolved_lifetime(&mut self, env: &Env, res: ResolvedArg, span: Span) -> rty::Region {
1641        let tcx = self.tcx();
1642        let lifetime_name = |def_id| tcx.item_name(def_id);
1643        match res {
1644            ResolvedArg::StaticLifetime => rty::ReStatic,
1645            ResolvedArg::EarlyBound(def_id) => {
1646                let index = self.genv().def_id_to_param_index(def_id.to_def_id());
1647                let name = lifetime_name(def_id.to_def_id());
1648                rty::ReEarlyParam(rty::EarlyParamRegion { index, name })
1649            }
1650            ResolvedArg::LateBound(_, index, def_id) => {
1651                let Some(depth) = env.depth().checked_sub(1) else {
1652                    span_bug!(span, "late-bound variable at depth 0")
1653                };
1654                let kind = rty::BoundRegionKind::Named(def_id.to_def_id());
1655                let var = BoundVar::from_u32(index);
1656                let bound_region = rty::BoundRegion { var, kind };
1657                rty::ReBound(rty::DebruijnIndex::from_usize(depth), bound_region)
1658            }
1659            ResolvedArg::Free(scope, id) => {
1660                let kind = rty::LateParamRegionKind::Named(id.to_def_id());
1661                rty::ReLateParam(rty::LateParamRegion { scope: scope.to_def_id(), kind })
1662            }
1663            ResolvedArg::Error(_) => bug!("lifetime resolved to an error"),
1664        }
1665    }
1666
1667    fn conv_const_arg(&mut self, cst: fhir::ConstArg) -> rty::Const {
1668        match cst.kind {
1669            fhir::ConstArgKind::Lit(lit) => rty::Const::from_usize(self.tcx(), lit),
1670            fhir::ConstArgKind::Param(def_id) => {
1671                rty::Const {
1672                    kind: rty::ConstKind::Param(def_id_to_param_const(self.genv(), def_id)),
1673                }
1674            }
1675            fhir::ConstArgKind::Infer => {
1676                rty::Const {
1677                    kind: rty::ConstKind::Infer(ty::InferConst::Var(self.next_const_vid())),
1678                }
1679            }
1680        }
1681    }
1682
1683    fn conv_qpath(
1684        &mut self,
1685        env: &mut Env,
1686        qself: Option<&fhir::Ty>,
1687        path: &fhir::Path,
1688        name: Option<Symbol>,
1689    ) -> QueryResult<rty::TyOrCtor> {
1690        let bty = match path.res {
1691            fhir::Res::PrimTy(prim_ty) => {
1692                self.check_prim_ty_generics(path, prim_ty)?;
1693                prim_ty_to_bty(prim_ty)
1694            }
1695            fhir::Res::Def(DefKind::Struct | DefKind::Enum | DefKind::Union, did) => {
1696                let adt_def = self.genv().adt_def(did)?;
1697                let args = self.conv_generic_args(env, did, path.last_segment())?;
1698                rty::BaseTy::adt(adt_def, args)
1699            }
1700            fhir::Res::Def(DefKind::TyParam, def_id) => {
1701                let owner_id = ty_param_owner(self.genv(), def_id);
1702                let param_ty = def_id_to_param_ty(self.genv(), def_id);
1703                self.check_ty_param_generics(path, param_ty)?;
1704                let param = self
1705                    .genv()
1706                    .generics_of(owner_id)?
1707                    .param_at(param_ty.index as usize, self.genv())?;
1708                match param.kind {
1709                    rty::GenericParamDefKind::Type { .. } => {
1710                        return Ok(rty::TyOrCtor::Ty(rty::Ty::param(param_ty)));
1711                    }
1712                    rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(param_ty),
1713                    _ => return Err(query_bug!("unexpected param kind")),
1714                }
1715            }
1716            fhir::Res::SelfTyParam { trait_ } => {
1717                self.check_self_ty_generics(path)?;
1718                let param = &self.genv().generics_of(trait_)?.own_params[0];
1719                match param.kind {
1720                    rty::GenericParamDefKind::Type { .. } => {
1721                        return Ok(rty::TyOrCtor::Ty(rty::Ty::param(rty::SELF_PARAM_TY)));
1722                    }
1723                    rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(rty::SELF_PARAM_TY),
1724                    _ => return Err(query_bug!("unexpected param kind")),
1725                }
1726            }
1727            fhir::Res::SelfTyAlias { alias_to, .. } => {
1728                self.check_self_ty_generics(path)?;
1729                if P::EXPAND_TYPE_ALIASES {
1730                    return Ok(self.genv().type_of(alias_to)?.instantiate_identity());
1731                } else {
1732                    rty::BaseTy::Alias(
1733                        rty::AliasKind::Free,
1734                        rty::AliasTy {
1735                            def_id: alias_to,
1736                            args: List::empty(),
1737                            refine_args: List::empty(),
1738                        },
1739                    )
1740                }
1741            }
1742            fhir::Res::Def(DefKind::AssocTy, assoc_id) => {
1743                let trait_id = self.tcx().trait_of_assoc(assoc_id).unwrap();
1744
1745                let [.., trait_segment, assoc_segment] = path.segments else {
1746                    span_bug!(path.span, "expected at least two segments");
1747                };
1748
1749                let Some(qself) = qself else {
1750                    self.report_ambiguous_assoc_item(
1751                        path.span,
1752                        AssocTag::Type,
1753                        assoc_segment.ident,
1754                    )?
1755                };
1756
1757                let trait_generics = self.genv().generics_of(trait_id)?;
1758                let qself =
1759                    self.conv_ty_to_generic_arg(env, &trait_generics.own_params[0], qself)?;
1760                let mut args = vec![qself];
1761                self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1762                self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1763                let args = List::from_vec(args);
1764
1765                let refine_args = List::empty();
1766                let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1767                rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty)
1768            }
1769            fhir::Res::Def(DefKind::TyAlias, def_id) => {
1770                self.check_refinement_generics(path, def_id)?;
1771                let args = self.conv_generic_args(env, def_id, path.last_segment())?;
1772                self.0.insert_path_args(path.fhir_id, args.clone());
1773                let refine_args = path
1774                    .refine
1775                    .iter()
1776                    .map(|expr| self.conv_expr(env, expr))
1777                    .try_collect_vec()?;
1778
1779                if P::EXPAND_TYPE_ALIASES {
1780                    let tcx = self.tcx();
1781                    return Ok(self
1782                        .genv()
1783                        .type_of(def_id)?
1784                        .instantiate(tcx, &args, &refine_args));
1785                } else {
1786                    rty::BaseTy::Alias(
1787                        rty::AliasKind::Free,
1788                        rty::AliasTy { def_id, args, refine_args: List::from(refine_args) },
1789                    )
1790                }
1791            }
1792            fhir::Res::Def(DefKind::ForeignTy, def_id) => {
1793                self.check_foreign_ty_generics(path)?;
1794                rty::BaseTy::Foreign(def_id)
1795            }
1796            fhir::Res::Def(kind, def_id) => self.report_expected_type(path.span, kind, def_id)?,
1797            fhir::Res::Param(..) | fhir::Res::GlobalFunc(..) | fhir::Res::Err => {
1798                span_bug!(path.span, "unexpected resolution in conv_ty_ctor: {:?}", path.res)
1799            }
1800        };
1801        let sort = bty.sort();
1802        let bty = bty.shift_in_escaping(1);
1803        let kind = match name {
1804            Some(name) => BoundReftKind::Named(name),
1805            None => BoundReftKind::Anon,
1806        };
1807        let var = rty::BoundVariableKind::Refine(sort, rty::InferMode::EVar, kind);
1808        let ctor = rty::Binder::bind_with_vars(
1809            rty::Ty::indexed(bty, rty::Expr::nu()),
1810            List::singleton(var),
1811        );
1812        Ok(rty::TyOrCtor::Ctor(ctor))
1813    }
1814
1815    fn param_as_bound_var(
1816        &mut self,
1817        param: &fhir::GenericParam,
1818    ) -> QueryResult<rty::BoundVariableKind> {
1819        let def_id = param.def_id.resolved_id();
1820        match param.kind {
1821            fhir::GenericParamKind::Lifetime => {
1822                Ok(rty::BoundVariableKind::Region(rty::BoundRegionKind::Named(def_id)))
1823            }
1824            fhir::GenericParamKind::Const { .. } | fhir::GenericParamKind::Type { .. } => {
1825                Err(query_bug!(def_id, "unsupported param kind `{:?}`", param.kind))
1826            }
1827        }
1828    }
1829
1830    fn conv_generic_args(
1831        &mut self,
1832        env: &mut Env,
1833        def_id: DefId,
1834        segment: &fhir::PathSegment,
1835    ) -> QueryResult<List<rty::GenericArg>> {
1836        let mut into = vec![];
1837        self.conv_generic_args_into(env, def_id, segment, &mut into)?;
1838        Ok(List::from(into))
1839    }
1840
1841    fn conv_generic_args_into(
1842        &mut self,
1843        env: &mut Env,
1844        def_id: DefId,
1845        segment: &fhir::PathSegment,
1846        into: &mut Vec<rty::GenericArg>,
1847    ) -> QueryResult {
1848        let generics = self.genv().generics_of(def_id)?;
1849
1850        self.check_generic_arg_count(&generics, def_id, segment)?;
1851
1852        let len = into.len();
1853        for (idx, arg) in segment.args.iter().enumerate() {
1854            let param = generics.param_at(idx + len, self.genv())?;
1855            match arg {
1856                fhir::GenericArg::Lifetime(lft) => {
1857                    into.push(rty::GenericArg::Lifetime(self.conv_lifetime(
1858                        env,
1859                        *lft,
1860                        segment.ident.span,
1861                    )));
1862                }
1863                fhir::GenericArg::Type(ty) => {
1864                    into.push(self.conv_ty_to_generic_arg(env, &param, ty)?);
1865                }
1866                fhir::GenericArg::Const(cst) => {
1867                    into.push(rty::GenericArg::Const(self.conv_const_arg(*cst)));
1868                }
1869                fhir::GenericArg::Infer => {
1870                    into.push(self.conv_generic_arg_hole(env, param, segment.ident.span)?);
1871                }
1872            }
1873        }
1874        self.fill_generic_args_defaults(def_id, into)
1875    }
1876
1877    fn conv_generic_arg_hole(
1878        &mut self,
1879        env: &mut Env,
1880        param: rty::GenericParamDef,
1881        span: Span,
1882    ) -> QueryResult<rty::GenericArg> {
1883        match param.kind {
1884            rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::Base { .. } => {
1885                let ty = fhir::Ty { kind: fhir::TyKind::Infer, span };
1886                Ok(self.conv_ty_to_generic_arg(env, &param, &ty)?)
1887            }
1888            rty::GenericParamDefKind::Const { .. } => {
1889                let cst = fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span };
1890                Ok(rty::GenericArg::Const(self.conv_const_arg(cst)))
1891            }
1892            rty::GenericParamDefKind::Lifetime => {
1893                let re = rty::Region::ReVar(self.next_region_vid());
1894                Ok(rty::GenericArg::Lifetime(re))
1895            }
1896        }
1897    }
1898
1899    fn check_generic_arg_count(
1900        &mut self,
1901        generics: &rty::Generics,
1902        def_id: DefId,
1903        segment: &fhir::PathSegment,
1904    ) -> QueryResult {
1905        let found = segment.args.len();
1906        let mut param_count = generics.own_params.len();
1907
1908        // The self parameter is not provided explicitly in the path so we skip it
1909        if let DefKind::Trait = self.genv().def_kind(def_id) {
1910            param_count -= 1;
1911        }
1912
1913        let min = param_count - generics.own_default_count();
1914        let max = param_count;
1915        if min == max && found != min {
1916            Err(self.emit(errors::GenericArgCountMismatch::new(
1917                self.genv(),
1918                def_id,
1919                segment,
1920                min,
1921            )))?;
1922        }
1923        if found < min {
1924            Err(self.emit(errors::TooFewGenericArgs::new(self.genv(), def_id, segment, min)))?;
1925        }
1926        if found > max {
1927            Err(self.emit(errors::TooManyGenericArgs::new(self.genv(), def_id, segment, min)))?;
1928        }
1929        Ok(())
1930    }
1931
1932    fn fill_generic_args_defaults(
1933        &mut self,
1934        def_id: DefId,
1935        into: &mut Vec<rty::GenericArg>,
1936    ) -> QueryResult {
1937        let generics = self.genv().generics_of(def_id)?;
1938        for param in generics.own_params.iter().skip(into.len()) {
1939            debug_assert!(matches!(
1940                param.kind,
1941                rty::GenericParamDefKind::Type { has_default: true }
1942                    | rty::GenericParamDefKind::Base { has_default: true }
1943            ));
1944            let span = self.tcx().def_span(param.def_id);
1945            // FIXME(nilehmann) we already know whether this is a type or a constructor so we could
1946            // directly check if the constructor returns a subset type.
1947            let ty = self
1948                .genv()
1949                .type_of(param.def_id)?
1950                .instantiate(self.tcx(), into, &[])
1951                .to_ty();
1952            into.push(self.try_to_ty_or_base(param.kind, span, &ty)?.into());
1953        }
1954        Ok(())
1955    }
1956
1957    fn conv_ty_to_generic_arg(
1958        &mut self,
1959        env: &mut Env,
1960        param: &rty::GenericParamDef,
1961        ty: &fhir::Ty,
1962    ) -> QueryResult<rty::GenericArg> {
1963        let rty_ty = self.conv_ty(env, ty)?;
1964        Ok(self.try_to_ty_or_base(param.kind, ty.span, &rty_ty)?.into())
1965    }
1966
1967    fn try_to_ty_or_base(
1968        &mut self,
1969        kind: rty::GenericParamDefKind,
1970        span: Span,
1971        ty: &rty::Ty,
1972    ) -> QueryResult<rty::TyOrBase> {
1973        match kind {
1974            rty::GenericParamDefKind::Type { .. } => Ok(rty::TyOrBase::Ty(ty.clone())),
1975            rty::GenericParamDefKind::Base { .. } => {
1976                Ok(rty::TyOrBase::Base(self.ty_to_subset_ty_ctor(span, ty)?))
1977            }
1978            _ => span_bug!(span, "unexpected param kind `{kind:?}`"),
1979        }
1980    }
1981
1982    fn ty_to_subset_ty_ctor(&mut self, span: Span, ty: &rty::Ty) -> QueryResult<rty::SubsetTyCtor> {
1983        let ctor = if let rty::TyKind::Infer(vid) = ty.kind() {
1984            // do not generate sort holes for dummy self types
1985            let sort_vid =
1986                if vid.as_u32() == 0 { rty::SortVid::from_u32(0) } else { self.next_sort_vid() };
1987            rty::SubsetTyCtor::bind_with_sort(
1988                rty::SubsetTy::trivial(rty::BaseTy::Infer(*vid), rty::Expr::nu()),
1989                rty::Sort::Infer(rty::SortInfer::SortVar(sort_vid)),
1990            )
1991        } else {
1992            ty.shallow_canonicalize()
1993                .as_ty_or_base()
1994                .as_base()
1995                .ok_or_else(|| self.emit(errors::InvalidBaseInstance::new(span)))?
1996        };
1997        Ok(ctor)
1998    }
1999
2000    #[track_caller]
2001    fn emit(&self, err: impl Diagnostic<'genv>) -> ErrorGuaranteed {
2002        self.genv().sess().emit_err(err)
2003    }
2004
2005    fn report_assoc_item_not_found<Tag: AssocItemTag>(
2006        &self,
2007        span: Span,
2008        assoc_tag: Tag,
2009    ) -> Result<!, ErrorGuaranteed> {
2010        Err(self.emit(errors::AssocItemNotFound { span, tag: assoc_tag.descr() }))?
2011    }
2012
2013    fn report_ambiguous_assoc_item<Tag: AssocItemTag>(
2014        &self,
2015        span: Span,
2016        assoc_tag: Tag,
2017        assoc_name: Ident,
2018    ) -> Result<!, ErrorGuaranteed> {
2019        Err(self.emit(errors::AmbiguousAssocItem {
2020            span,
2021            name: assoc_name,
2022            tag: assoc_tag.descr(),
2023        }))?
2024    }
2025
2026    #[track_caller]
2027    fn report_expected_type(
2028        &self,
2029        span: Span,
2030        kind: DefKind,
2031        def_id: DefId,
2032    ) -> Result<!, ErrorGuaranteed> {
2033        Err(self.emit(errors::ExpectedType {
2034            span,
2035            def_descr: self.tcx().def_kind_descr(kind, def_id),
2036            name: self.tcx().def_path_str(def_id),
2037        }))?
2038    }
2039}
2040
2041/// Check generic params for types
2042impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2043    fn check_refinement_generics(&mut self, path: &fhir::Path, def_id: DefId) -> QueryResult {
2044        let generics = self.genv().refinement_generics_of(def_id)?;
2045        if generics.count() != path.refine.len() {
2046            let err = errors::RefineArgMismatch {
2047                span: path.span,
2048                expected: generics.count(),
2049                found: path.refine.len(),
2050                kind: self.tcx().def_descr(def_id),
2051            };
2052            Err(self.emit(err))?;
2053        }
2054        Ok(())
2055    }
2056
2057    fn check_prim_ty_generics(
2058        &mut self,
2059        path: &fhir::Path<'_>,
2060        prim_ty: rustc_hir::PrimTy,
2061    ) -> QueryResult {
2062        if !path.last_segment().args.is_empty() {
2063            let err = errors::GenericsOnPrimTy { span: path.span, name: prim_ty.name_str() };
2064            Err(self.emit(err))?;
2065        }
2066        Ok(())
2067    }
2068
2069    fn check_ty_param_generics(
2070        &mut self,
2071        path: &fhir::Path<'_>,
2072        param_ty: rty::ParamTy,
2073    ) -> QueryResult {
2074        if !path.last_segment().args.is_empty() {
2075            let err = errors::GenericsOnTyParam { span: path.span, name: param_ty.name };
2076            Err(self.emit(err))?;
2077        }
2078        Ok(())
2079    }
2080
2081    fn check_self_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2082        if !path.last_segment().args.is_empty() {
2083            let err = errors::GenericsOnSelfTy { span: path.span };
2084            Err(self.emit(err))?;
2085        }
2086        Ok(())
2087    }
2088
2089    fn check_foreign_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2090        if !path.last_segment().args.is_empty() {
2091            let err = errors::GenericsOnForeignTy { span: path.span };
2092            Err(self.emit(err))?;
2093        }
2094        Ok(())
2095    }
2096}
2097
2098fn prim_ty_to_bty(prim_ty: rustc_hir::PrimTy) -> rty::BaseTy {
2099    match prim_ty {
2100        rustc_hir::PrimTy::Int(int_ty) => rty::BaseTy::Int(int_ty),
2101        rustc_hir::PrimTy::Uint(uint_ty) => rty::BaseTy::Uint(uint_ty),
2102        rustc_hir::PrimTy::Float(float_ty) => rty::BaseTy::Float(float_ty),
2103        rustc_hir::PrimTy::Str => rty::BaseTy::Str,
2104        rustc_hir::PrimTy::Bool => rty::BaseTy::Bool,
2105        rustc_hir::PrimTy::Char => rty::BaseTy::Char,
2106    }
2107}
2108
2109/// Conversion of expressions
2110impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2111    fn conv_lit(&self, lit: fhir::Lit, fhir_id: FhirId, span: Span) -> QueryResult<rty::Constant> {
2112        match lit {
2113            fhir::Lit::Int(n, kind) => {
2114                match kind {
2115                    Some(fhir::NumLitKind::Int) => Ok(rty::Constant::from(n)),
2116                    Some(fhir::NumLitKind::Real) => Ok(rty::Constant::Real(rty::Real(n))),
2117                    None => {
2118                        let sort = self.results().node_sort(fhir_id);
2119                        if let rty::Sort::BitVec(bvsize) = sort {
2120                            if let rty::BvSize::Fixed(size) = bvsize
2121                                && (n == 0 || n.ilog2() < size)
2122                            {
2123                                Ok(rty::Constant::BitVec(n, size))
2124                            } else {
2125                                Err(self.emit(errors::InvalidBitVectorConstant::new(span, sort)))?
2126                            }
2127                        } else {
2128                            Ok(rty::Constant::from(n))
2129                        }
2130                    }
2131                }
2132            }
2133            fhir::Lit::Bool(b) => Ok(rty::Constant::from(b)),
2134            fhir::Lit::Str(s) => Ok(rty::Constant::from(s)),
2135            fhir::Lit::Char(c) => Ok(rty::Constant::from(c)),
2136        }
2137    }
2138
2139    fn conv_expr(&mut self, env: &mut Env, expr: &fhir::Expr) -> QueryResult<rty::Expr> {
2140        let fhir_id = expr.fhir_id;
2141        let espan = ESpan::new(expr.span);
2142        let expr = match expr.kind {
2143            fhir::ExprKind::Var(QPathExpr::Resolved(path, _)) => self.conv_path_expr(env, path)?,
2144            fhir::ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
2145                let qself = self.conv_ty(env, qself)?;
2146                self.conv_type_relative_const_path(expr, &qself, assoc)?
2147            }
2148            fhir::ExprKind::Literal(lit) => {
2149                rty::Expr::constant(self.conv_lit(lit, fhir_id, expr.span)?).at(espan)
2150            }
2151            fhir::ExprKind::BinaryOp(op, e1, e2) => {
2152                rty::Expr::binary_op(
2153                    self.conv_bin_op(op, expr.fhir_id),
2154                    self.conv_expr(env, e1)?,
2155                    self.conv_expr(env, e2)?,
2156                )
2157                .at(espan)
2158            }
2159            fhir::ExprKind::UnaryOp(op, e) => {
2160                rty::Expr::unary_op(conv_un_op(op), self.conv_expr(env, e)?).at(espan)
2161            }
2162
2163            fhir::ExprKind::PrimApp(op, e1, e2) => {
2164                rty::Expr::prim_val(
2165                    self.conv_bin_op(op, expr.fhir_id),
2166                    self.conv_expr(env, e1)?,
2167                    self.conv_expr(env, e2)?,
2168                )
2169                .at(espan)
2170            }
2171            fhir::ExprKind::App(func, args) => {
2172                let sort_args = self.results().node_sort_args(fhir_id);
2173                rty::Expr::app(self.conv_func(env, &func)?, sort_args, self.conv_exprs(env, args)?)
2174                    .at(espan)
2175            }
2176            fhir::ExprKind::Alias(alias, args) => {
2177                let args = args
2178                    .iter()
2179                    .map(|arg| self.conv_expr(env, arg))
2180                    .try_collect()?;
2181                let alias = self.conv_alias_reft(env, expr.fhir_id, &alias)?;
2182                rty::Expr::alias(alias, args).at(espan)
2183            }
2184            fhir::ExprKind::IfThenElse(p, e1, e2) => {
2185                rty::Expr::ite(
2186                    self.conv_expr(env, p)?,
2187                    self.conv_expr(env, e1)?,
2188                    self.conv_expr(env, e2)?,
2189                )
2190                .at(espan)
2191            }
2192            fhir::ExprKind::Dot(base, _) => {
2193                let proj = self.results().field_proj(fhir_id);
2194                rty::Expr::field_proj(self.conv_expr(env, base)?, proj)
2195            }
2196            fhir::ExprKind::Abs(params, body) => {
2197                env.push_layer(Layer::list(self.results(), 0, params));
2198                let pred = self.conv_expr(env, body)?;
2199                let vars = env.pop_layer().into_bound_vars(self.genv())?;
2200                let output = self.results().node_sort(body.fhir_id);
2201                let lam = rty::Lambda::bind_with_vars(pred, vars, output);
2202                rty::Expr::abs(lam)
2203            }
2204            fhir::ExprKind::Block(decls, body) => {
2205                for decl in decls {
2206                    env.push_layer(Layer::list(self.results(), 0, &[decl.param]));
2207                }
2208                let mut body = self.conv_expr(env, body)?;
2209                for decl in decls.iter().rev() {
2210                    let vars = env.pop_layer().into_bound_vars(self.genv())?;
2211                    let init = self.conv_expr(env, &decl.init)?;
2212                    body = rty::Expr::let_(init, rty::Binder::bind_with_vars(body, vars));
2213                }
2214                body
2215            }
2216            fhir::ExprKind::BoundedQuant(kind, param, rng, body) => {
2217                env.push_layer(Layer::list(self.results(), 0, &[param]));
2218                let pred = self.conv_expr(env, body)?;
2219                let vars = env.pop_layer().into_bound_vars(self.genv())?;
2220                let body = rty::Binder::bind_with_vars(pred, vars);
2221                rty::Expr::bounded_quant(kind, rng, body)
2222            }
2223            fhir::ExprKind::Record(flds) => {
2224                let def_id = self.results().record_ctor(expr.fhir_id);
2225                let flds = flds
2226                    .iter()
2227                    .map(|expr| self.conv_expr(env, expr))
2228                    .try_collect()?;
2229                rty::Expr::ctor_struct(def_id, flds)
2230            }
2231            fhir::ExprKind::Constructor(path, exprs, spread) => {
2232                let def_id = if let Some(path) = path {
2233                    match path.res {
2234                        fhir::Res::Def(DefKind::Enum | DefKind::Struct, def_id) => def_id,
2235                        _ => span_bug!(path.span, "unexpected path in constructor"),
2236                    }
2237                } else {
2238                    self.results().record_ctor(expr.fhir_id)
2239                };
2240                let assns = self.conv_constructor_exprs(def_id, env, exprs, &spread)?;
2241                rty::Expr::ctor_struct(def_id, assns)
2242            }
2243            fhir::ExprKind::Err(err) => Err(QueryErr::Emitted(err))?,
2244        };
2245        Ok(self.add_coercions(expr, fhir_id))
2246    }
2247
2248    fn conv_loc(&mut self, env: &mut Env, loc: fhir::PathExpr) -> QueryResult<rty::Path> {
2249        Ok(self
2250            .conv_path_expr(env, loc)?
2251            .to_path()
2252            .unwrap_or_else(|| span_bug!(loc.span, "expected path, found `{loc:?}`")))
2253    }
2254
2255    fn conv_path_expr(&mut self, env: &mut Env, path: fhir::PathExpr) -> QueryResult<rty::Expr> {
2256        let genv = self.genv();
2257        let tcx = self.genv().tcx();
2258        let espan = ESpan::new(path.span);
2259        let (expr, sort) = match path.res {
2260            fhir::Res::Param(_, id) => (env.lookup(&path).to_expr(), self.results().param_sort(id)),
2261            fhir::Res::Def(DefKind::Const, def_id) => {
2262                self.hyperlink(path.span, tcx.def_ident_span(def_id));
2263                let (expr, sort) = self.conv_const(path.span, def_id)?;
2264                (expr.at(espan), sort)
2265            }
2266            fhir::Res::Def(DefKind::Ctor(..), ctor_id) => {
2267                let Some(sort) = genv.sort_of_def_id(ctor_id).emit(&genv)? else {
2268                    span_bug!(path.span, "unexpected variant {ctor_id:?}")
2269                };
2270
2271                let variant_id = self.tcx().parent(ctor_id);
2272                let enum_id = self.tcx().parent(variant_id);
2273                self.hyperlink(path.span, tcx.def_ident_span(variant_id));
2274                let idx = variant_idx(self.tcx(), variant_id);
2275                (rty::Expr::ctor_enum(enum_id, idx), sort)
2276            }
2277            fhir::Res::Def(DefKind::ConstParam, def_id) => {
2278                self.hyperlink(path.span, tcx.def_ident_span(def_id));
2279                // FIXME(nilehmann) generalize this to other sorts
2280                let sort = rty::Sort::Int;
2281                (rty::Expr::const_generic(def_id_to_param_const(genv, def_id)).at(espan), sort)
2282            }
2283            _ => {
2284                Err(self.emit(errors::InvalidRes { span: path.span, res_descr: path.res.descr() }))?
2285            }
2286        };
2287        self.0.insert_node_sort(path.fhir_id, sort);
2288        Ok(expr)
2289    }
2290
2291    fn conv_const(&self, span: Span, def_id: DefId) -> QueryResult<(rty::Expr, rty::Sort)> {
2292        let genv = self.genv();
2293        let Some(sort) = genv.sort_of_def_id(def_id).emit(&genv)? else {
2294            span_bug!(span, "unsupported const: `{def_id:?}`")
2295        };
2296        let info = genv.constant_info(def_id).emit(&genv)?;
2297        // non-integral constant
2298        if sort != rty::Sort::Int && matches!(info, rty::ConstantInfo::Uninterpreted) {
2299            Err(self.emit(errors::ConstantAnnotationNeeded::new(span)))?;
2300        }
2301        Ok((rty::Expr::const_def_id(def_id).at(ESpan::new(span)), sort))
2302    }
2303
2304    fn conv_constructor_exprs(
2305        &mut self,
2306        struct_def_id: DefId,
2307        env: &mut Env,
2308        exprs: &[fhir::FieldExpr],
2309        spread: &Option<&fhir::Spread>,
2310    ) -> QueryResult<List<rty::Expr>> {
2311        let spread = spread
2312            .map(|spread| self.conv_expr(env, &spread.expr))
2313            .transpose()?;
2314        let mut field_exprs_by_name: FxHashMap<Symbol, rty::Expr> = exprs
2315            .iter()
2316            .map(|field_expr| -> QueryResult<_> {
2317                Ok((field_expr.ident.name, self.conv_expr(env, &field_expr.expr)?))
2318            })
2319            .try_collect()?;
2320
2321        if !P::HAS_ELABORATED_INFORMATION {
2322            return Ok(List::default());
2323        };
2324
2325        let adt_def = self.genv().adt_sort_def_of(struct_def_id)?;
2326        let struct_variant = adt_def.struct_variant();
2327        let mut assns = Vec::new();
2328        for (idx, field_name) in struct_variant.field_names().iter().enumerate() {
2329            if let Some(expr) = field_exprs_by_name.remove(field_name) {
2330                assns.push(expr);
2331            } else if let Some(spread) = &spread {
2332                let proj = rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 };
2333                assns.push(rty::Expr::field_proj(spread, proj));
2334            }
2335        }
2336        Ok(List::from_vec(assns))
2337    }
2338
2339    fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult<List<rty::Expr>> {
2340        exprs.iter().map(|e| self.conv_expr(env, e)).collect()
2341    }
2342
2343    fn conv_bin_op(&self, op: fhir::BinOp, fhir_id: FhirId) -> rty::BinOp {
2344        match op {
2345            fhir::BinOp::Iff => rty::BinOp::Iff,
2346            fhir::BinOp::Imp => rty::BinOp::Imp,
2347            fhir::BinOp::Or => rty::BinOp::Or,
2348            fhir::BinOp::And => rty::BinOp::And,
2349            fhir::BinOp::Eq => rty::BinOp::Eq,
2350            fhir::BinOp::Ne => rty::BinOp::Ne,
2351            fhir::BinOp::Gt => rty::BinOp::Gt(self.results().bin_op_sort(fhir_id)),
2352            fhir::BinOp::Ge => rty::BinOp::Ge(self.results().bin_op_sort(fhir_id)),
2353            fhir::BinOp::Lt => rty::BinOp::Lt(self.results().bin_op_sort(fhir_id)),
2354            fhir::BinOp::Le => rty::BinOp::Le(self.results().bin_op_sort(fhir_id)),
2355            fhir::BinOp::Add => rty::BinOp::Add(self.results().bin_op_sort(fhir_id)),
2356            fhir::BinOp::Sub => rty::BinOp::Sub(self.results().bin_op_sort(fhir_id)),
2357            fhir::BinOp::Mul => rty::BinOp::Mul(self.results().bin_op_sort(fhir_id)),
2358            fhir::BinOp::Mod => rty::BinOp::Mod(self.results().bin_op_sort(fhir_id)),
2359            fhir::BinOp::Div => rty::BinOp::Div(self.results().bin_op_sort(fhir_id)),
2360            fhir::BinOp::BitAnd => rty::BinOp::BitAnd,
2361            fhir::BinOp::BitOr => rty::BinOp::BitOr,
2362            fhir::BinOp::BitXor => rty::BinOp::BitXor,
2363            fhir::BinOp::BitShl => rty::BinOp::BitShl,
2364            fhir::BinOp::BitShr => rty::BinOp::BitShr,
2365        }
2366    }
2367
2368    fn add_coercions(&self, mut expr: rty::Expr, fhir_id: FhirId) -> rty::Expr {
2369        let span = expr.span();
2370        for coercion in self.results().coercions_for(fhir_id) {
2371            expr = match *coercion {
2372                rty::Coercion::Inject(def_id) => {
2373                    rty::Expr::ctor_struct(def_id, List::singleton(expr)).at_opt(span)
2374                }
2375                rty::Coercion::Project(def_id) => {
2376                    rty::Expr::field_proj(expr, rty::FieldProj::Adt { def_id, field: 0 })
2377                        .at_opt(span)
2378                }
2379            };
2380        }
2381        expr
2382    }
2383
2384    fn hyperlink(&self, span: Span, dst_span: Option<Span>) {
2385        if P::HAS_ELABORATED_INFORMATION
2386            && let Some(dst_span) = dst_span
2387        {
2388            dbg::hyperlink!(self.genv().tcx(), span, dst_span);
2389        }
2390    }
2391
2392    fn conv_func(&mut self, env: &Env, func: &fhir::PathExpr) -> QueryResult<rty::Expr> {
2393        let genv = self.genv();
2394        let span = func.span;
2395        let (expr, sort) = match func.res {
2396            fhir::Res::Param(_, id) => {
2397                let sort = self.results().param_sort(id);
2398                (env.lookup(func).to_expr(), sort)
2399            }
2400            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Def(did)) => {
2401                self.hyperlink(span, Some(genv.func_span(did)));
2402                let sort = rty::Sort::Func(genv.func_sort(did));
2403                (rty::Expr::global_func(rty::SpecFuncKind::Def(did)), sort)
2404            }
2405            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Uif(did)) => {
2406                self.hyperlink(span, Some(genv.func_span(did)));
2407                let sort = rty::Sort::Func(genv.func_sort(did));
2408                (rty::Expr::global_func(rty::SpecFuncKind::Uif(did)), sort)
2409            }
2410            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Thy(itf)) => {
2411                let sort = THEORY_FUNCS.get(&itf).unwrap().sort.clone();
2412                (rty::Expr::global_func(rty::SpecFuncKind::Thy(itf)), rty::Sort::Func(sort))
2413            }
2414            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Cast) => {
2415                let fsort = rty::PolyFuncSort::new(
2416                    List::from_arr([rty::SortParamKind::Sort, rty::SortParamKind::Sort]),
2417                    rty::FuncSort::new(
2418                        vec![rty::Sort::Var(rty::ParamSort::from(0_usize))],
2419                        rty::Sort::Var(rty::ParamSort::from(1_usize)),
2420                    ),
2421                );
2422                (rty::Expr::internal_func(InternalFuncKind::Cast), rty::Sort::Func(fsort))
2423            }
2424            _ => {
2425                return Err(
2426                    self.emit(errors::InvalidRes { span: func.span, res_descr: func.res.descr() })
2427                )?;
2428            }
2429        };
2430        self.0.insert_node_sort(func.fhir_id, sort);
2431        Ok(self.add_coercions(expr, func.fhir_id))
2432    }
2433
2434    fn conv_alias_reft(
2435        &mut self,
2436        env: &mut Env,
2437        fhir_id: FhirId,
2438        alias: &fhir::AliasReft,
2439    ) -> QueryResult<rty::AliasReft> {
2440        let alias_reft = match alias {
2441            fhir::AliasReft::Qualified { qself, trait_, name } => {
2442                let fhir::Res::Def(DefKind::Trait, trait_id) = trait_.res else {
2443                    span_bug!(trait_.span, "expected trait")
2444                };
2445                let trait_segment = trait_.last_segment();
2446
2447                let generics = self.genv().generics_of(trait_id)?;
2448                let self_ty =
2449                    self.conv_ty_to_generic_arg(env, &generics.param_at(0, self.genv())?, qself)?;
2450                let mut generic_args = vec![self_ty];
2451                self.conv_generic_args_into(env, trait_id, trait_segment, &mut generic_args)?;
2452
2453                let Some(assoc_reft) = self.genv().assoc_refinements_of(trait_id)?.find(name.name)
2454                else {
2455                    return Err(self.emit(errors::InvalidAssocReft::new(
2456                        trait_.span,
2457                        name.name,
2458                        format!("{:?}", trait_),
2459                    )))?;
2460                };
2461
2462                let assoc_id = assoc_reft.def_id;
2463
2464                dbg::hyperlink!(self.genv().tcx(), name.span, assoc_reft.span);
2465
2466                rty::AliasReft { assoc_id, args: List::from_vec(generic_args) }
2467            }
2468            fhir::AliasReft::TypeRelative { qself, name } => {
2469                let qself_res =
2470                    if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
2471                let (assoc_reft, trait_ref) =
2472                    self.conv_type_relative_path(AssocReftTag, qself.span, qself_res, *name)?;
2473                rty::AliasReft { assoc_id: assoc_reft.def_id, args: trait_ref.args }
2474            }
2475        };
2476        let fsort = alias_reft.fsort(self.genv())?;
2477        self.0.insert_alias_reft_sort(fhir_id, fsort);
2478        Ok(alias_reft)
2479    }
2480
2481    pub(crate) fn conv_invariants(
2482        &mut self,
2483        adt_id: MaybeExternId,
2484        params: &[fhir::RefineParam],
2485        invariants: &[fhir::Expr],
2486    ) -> QueryResult<Vec<rty::Invariant>> {
2487        let mut env = Env::new(&[]);
2488        env.push_layer(Layer::coalesce(self.results(), adt_id.resolved_id(), params));
2489        invariants
2490            .iter()
2491            .map(|invariant| self.conv_invariant(&mut env, invariant))
2492            .collect()
2493    }
2494
2495    fn conv_invariant(
2496        &mut self,
2497        env: &mut Env,
2498        invariant: &fhir::Expr,
2499    ) -> QueryResult<rty::Invariant> {
2500        Ok(rty::Invariant::new(rty::Binder::bind_with_vars(
2501            self.conv_expr(env, invariant)?,
2502            env.top_layer().to_bound_vars(self.genv())?,
2503        )))
2504    }
2505}
2506
2507impl Env {
2508    fn new(early_params: &[fhir::RefineParam]) -> Self {
2509        let early_params = early_params
2510            .iter()
2511            .map(|param| (param.id, param.name))
2512            .collect();
2513        Self { layers: vec![], early_params }
2514    }
2515
2516    pub(crate) fn empty() -> Self {
2517        Self { layers: vec![], early_params: Default::default() }
2518    }
2519
2520    fn depth(&self) -> usize {
2521        self.layers.len()
2522    }
2523
2524    fn push_layer(&mut self, layer: Layer) {
2525        self.layers.push(layer);
2526    }
2527
2528    fn pop_layer(&mut self) -> Layer {
2529        self.layers.pop().expect("bottom of layer stack")
2530    }
2531
2532    fn top_layer(&self) -> &Layer {
2533        self.layers.last().expect("bottom of layer stack")
2534    }
2535
2536    fn lookup(&self, var: &fhir::PathExpr) -> LookupResult<'_> {
2537        let (_, id) = var.res.expect_param();
2538        for (i, layer) in self.layers.iter().rev().enumerate() {
2539            if let Some((idx, entry)) = layer.get(id) {
2540                let debruijn = DebruijnIndex::from_usize(i);
2541                let kind = LookupResultKind::Bound {
2542                    debruijn,
2543                    entry,
2544                    index: idx as u32,
2545                    kind: layer.kind,
2546                };
2547                return LookupResult { var_span: var.span, kind };
2548            }
2549        }
2550        if let Some((idx, _, name)) = self.early_params.get_full(&id) {
2551            LookupResult {
2552                var_span: var.span,
2553                kind: LookupResultKind::EarlyParam { index: idx as u32, name: *name },
2554            }
2555        } else {
2556            span_bug!(var.span, "no entry found for key: `{:?}`", id);
2557        }
2558    }
2559
2560    fn to_early_param_args(&self) -> List<rty::Expr> {
2561        self.early_params
2562            .iter()
2563            .enumerate()
2564            .map(|(idx, (_, name))| rty::Expr::early_param(idx as u32, *name))
2565            .collect()
2566    }
2567}
2568
2569impl Layer {
2570    fn new<R: WfckResultsProvider>(
2571        results: &R,
2572        params: &[fhir::RefineParam],
2573        kind: LayerKind,
2574    ) -> Self {
2575        let map = params
2576            .iter()
2577            .map(|param| {
2578                let sort = results.param_sort(param.id);
2579                let infer_mode = rty::InferMode::from_param_kind(param.kind);
2580                let entry = ParamEntry::new(sort, infer_mode, param.name);
2581                (param.id, entry)
2582            })
2583            .collect();
2584        Self { map, kind }
2585    }
2586
2587    fn list<R: WfckResultsProvider>(
2588        results: &R,
2589        bound_regions: u32,
2590        params: &[fhir::RefineParam],
2591    ) -> Self {
2592        Self::new(results, params, LayerKind::List { bound_regions })
2593    }
2594
2595    fn coalesce<R: WfckResultsProvider>(
2596        results: &R,
2597        def_id: DefId,
2598        params: &[fhir::RefineParam],
2599    ) -> Self {
2600        Self::new(results, params, LayerKind::Coalesce(def_id))
2601    }
2602
2603    fn get(&self, name: impl Borrow<fhir::ParamId>) -> Option<(usize, &ParamEntry)> {
2604        let (idx, _, entry) = self.map.get_full(name.borrow())?;
2605        Some((idx, entry))
2606    }
2607
2608    fn into_bound_vars(self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2609        match self.kind {
2610            LayerKind::List { .. } => {
2611                Ok(self
2612                    .into_iter()
2613                    .map(|entry| {
2614                        let kind = rty::BoundReftKind::Named(entry.name);
2615                        rty::BoundVariableKind::Refine(entry.sort, entry.mode, kind)
2616                    })
2617                    .collect())
2618            }
2619            LayerKind::Coalesce(def_id) => {
2620                let sort_def = genv.adt_sort_def_of(def_id)?;
2621                let args = sort_def.identity_args();
2622                let ctor = rty::SortCtor::Adt(sort_def);
2623                Ok(List::singleton(rty::BoundVariableKind::Refine(
2624                    rty::Sort::App(ctor, args),
2625                    rty::InferMode::EVar,
2626                    rty::BoundReftKind::Anon,
2627                )))
2628            }
2629        }
2630    }
2631
2632    fn to_bound_vars(&self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2633        self.clone().into_bound_vars(genv)
2634    }
2635
2636    fn into_iter(self) -> impl Iterator<Item = ParamEntry> {
2637        self.map.into_values()
2638    }
2639}
2640
2641impl ParamEntry {
2642    fn new(sort: rty::Sort, mode: fhir::InferMode, name: Symbol) -> Self {
2643        ParamEntry { name, sort, mode }
2644    }
2645}
2646
2647impl LookupResult<'_> {
2648    fn to_expr(&self) -> rty::Expr {
2649        let espan = ESpan::new(self.var_span);
2650        match &self.kind {
2651            LookupResultKind::Bound { debruijn, entry: ParamEntry { name, .. }, kind, index } => {
2652                match *kind {
2653                    LayerKind::List { bound_regions } => {
2654                        rty::Expr::bvar(
2655                            *debruijn,
2656                            BoundVar::from_u32(bound_regions + *index),
2657                            rty::BoundReftKind::Named(*name),
2658                        )
2659                        .at(espan)
2660                    }
2661                    LayerKind::Coalesce(def_id) => {
2662                        let var =
2663                            rty::Expr::bvar(*debruijn, BoundVar::ZERO, rty::BoundReftKind::Anon)
2664                                .at(espan);
2665                        rty::Expr::field_proj(var, rty::FieldProj::Adt { def_id, field: *index })
2666                            .at(espan)
2667                    }
2668                }
2669            }
2670            &LookupResultKind::EarlyParam { index, name, .. } => {
2671                rty::Expr::early_param(index, name).at(espan)
2672            }
2673        }
2674    }
2675}
2676
2677pub fn conv_func_decl(genv: GlobalEnv, func: &fhir::SpecFunc) -> QueryResult<rty::PolyFuncSort> {
2678    let wfckresults = WfckResults::new(FluxOwnerId::Flux(func.def_id));
2679    let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
2680    let inputs_and_output = func
2681        .args
2682        .iter()
2683        .map(|p| &p.sort)
2684        .chain(iter::once(&func.sort))
2685        .map(|sort| cx.conv_sort(sort))
2686        .try_collect()?;
2687    let params = iter::repeat_n(rty::SortParamKind::Sort, func.params).collect();
2688    Ok(rty::PolyFuncSort::new(params, rty::FuncSort { inputs_and_output }))
2689}
2690
2691fn conv_un_op(op: fhir::UnOp) -> rty::UnOp {
2692    match op {
2693        fhir::UnOp::Not => rty::UnOp::Not,
2694        fhir::UnOp::Neg => rty::UnOp::Neg,
2695    }
2696}
2697
2698fn def_id_to_param_ty(genv: GlobalEnv, def_id: DefId) -> rty::ParamTy {
2699    rty::ParamTy { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2700}
2701
2702fn def_id_to_param_const(genv: GlobalEnv, def_id: DefId) -> rty::ParamConst {
2703    rty::ParamConst { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2704}
2705
2706fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
2707    let def_kind = genv.def_kind(def_id);
2708    match def_kind {
2709        DefKind::Trait | DefKind::TraitAlias => def_id,
2710        DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2711            genv.tcx().parent(def_id)
2712        }
2713        _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
2714    }
2715}
2716
2717fn ty_param_name(genv: GlobalEnv, def_id: DefId) -> Symbol {
2718    let def_kind = genv.tcx().def_kind(def_id);
2719    match def_kind {
2720        DefKind::Trait | DefKind::TraitAlias => kw::SelfUpper,
2721        DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2722            genv.tcx().item_name(def_id)
2723        }
2724        _ => bug!("ty_param_name: {:?} is a {:?} not a type parameter", def_id, def_kind),
2725    }
2726}
2727
2728/// This trait is used to define functions generically over both _associated refinements_
2729/// and _associated items_ (types, consts, and functions).
2730trait AssocItemTag: Copy {
2731    type AssocItem<'tcx>;
2732
2733    fn descr(self) -> &'static str;
2734
2735    fn trait_defines_item_named<'tcx>(
2736        self,
2737        genv: GlobalEnv<'_, 'tcx>,
2738        trait_def_id: DefId,
2739        assoc_name: Ident,
2740    ) -> QueryResult<Option<Self::AssocItem<'tcx>>>;
2741
2742    fn transitive_bounds_that_define_assoc_item<'tcx>(
2743        self,
2744        genv: GlobalEnv<'_, 'tcx>,
2745        trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2746        assoc_name: Ident,
2747    ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>>;
2748}
2749
2750impl AssocItemTag for AssocTag {
2751    type AssocItem<'tcx> = &'tcx AssocItem;
2752
2753    fn descr(self) -> &'static str {
2754        match self {
2755            AssocTag::Const => "constant",
2756            AssocTag::Fn => "function",
2757            AssocTag::Type => "type",
2758        }
2759    }
2760
2761    fn trait_defines_item_named<'tcx>(
2762        self,
2763        genv: GlobalEnv<'_, 'tcx>,
2764        trait_def_id: DefId,
2765        assoc_name: Ident,
2766    ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2767        Ok(genv
2768            .tcx()
2769            .associated_items(trait_def_id)
2770            .find_by_ident_and_kind(genv.tcx(), assoc_name, self, trait_def_id))
2771    }
2772
2773    fn transitive_bounds_that_define_assoc_item<'tcx>(
2774        self,
2775        genv: GlobalEnv<'_, 'tcx>,
2776        trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2777        assoc_name: Ident,
2778    ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2779        traits::transitive_bounds_that_define_assoc_item(genv.tcx(), trait_refs, assoc_name)
2780    }
2781}
2782
2783#[derive(Copy, Clone)]
2784struct AssocReftTag;
2785
2786impl AssocItemTag for AssocReftTag {
2787    type AssocItem<'tcx> = AssocReft;
2788
2789    fn descr(self) -> &'static str {
2790        "refinement"
2791    }
2792
2793    fn trait_defines_item_named<'tcx>(
2794        self,
2795        genv: GlobalEnv<'_, 'tcx>,
2796        trait_def_id: DefId,
2797        assoc_name: Ident,
2798    ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2799        Ok(genv
2800            .assoc_refinements_of(trait_def_id)?
2801            .find(assoc_name.name))
2802    }
2803
2804    fn transitive_bounds_that_define_assoc_item<'tcx>(
2805        self,
2806        genv: GlobalEnv<'_, 'tcx>,
2807        trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2808        _assoc_name: Ident,
2809    ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2810        transitive_bounds(genv.tcx(), trait_refs)
2811    }
2812}
2813
2814/// This is like [`TyCtxt::type_param_predicates`] but computes all bounds not just the ones defining
2815/// an associated item. We *must* compute this ourselves to resolve type-relative associated refinements,
2816/// but we also use it to resolve type-relative type paths.
2817///
2818/// NOTE: [`TyCtxt::type_param_predicates`] is defined specifically to avoid cycles which is not a
2819/// problem for us so we can use it instead of [`TyCtxt::type_param_predicates`].
2820fn type_param_predicates<'tcx>(
2821    tcx: TyCtxt<'tcx>,
2822    param_id: DefId,
2823) -> impl Iterator<Item = ty::PolyTraitPredicate<'tcx>> {
2824    let parent = if tcx.def_kind(param_id) == DefKind::Trait {
2825        // If the param_id is a trait then this is the `Self` parameter and the parent is the trait itself
2826        param_id
2827    } else {
2828        tcx.parent(param_id)
2829    };
2830    let param_index = tcx
2831        .generics_of(parent)
2832        .param_def_id_to_index(tcx, param_id)
2833        .unwrap();
2834    let predicates = tcx.predicates_of(parent).instantiate_identity(tcx);
2835    predicates.into_iter().filter_map(move |(clause, _)| {
2836        clause
2837            .as_trait_clause()
2838            .filter(|trait_pred| trait_pred.self_ty().skip_binder().is_param(param_index))
2839    })
2840}
2841
2842/// This is like [`traits::transitive_bounds_that_define_assoc_item`] but computes all bounds not just
2843/// the ones defining an associated item. We *must* compute this ourselves to resolve type-relative
2844/// associated refinements.
2845///
2846/// NOTE: [`traits::transitive_bounds_that_define_assoc_item`] is defined specifically to avoid cycles
2847/// which is not a problem for us. So instead of using `explicit_supertraits_containing_assoc_item` we
2848/// can simply use `explicit_super_predicates_of`.
2849fn transitive_bounds<'tcx>(
2850    tcx: TyCtxt<'tcx>,
2851    trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2852) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2853    let mut seen = FxHashSet::default();
2854    let mut stack: Vec<_> = trait_refs.collect();
2855
2856    std::iter::from_fn(move || {
2857        while let Some(trait_ref) = stack.pop() {
2858            if !seen.insert(tcx.anonymize_bound_vars(trait_ref)) {
2859                continue;
2860            }
2861
2862            stack.extend(
2863                tcx.explicit_super_predicates_of(trait_ref.def_id())
2864                    .iter_identity_copied()
2865                    .map(|(clause, _)| clause.instantiate_supertrait(tcx, trait_ref))
2866                    .filter_map(|clause| clause.as_trait_clause())
2867                    .filter(|clause| clause.polarity() == ty::PredicatePolarity::Positive)
2868                    .map(|clause| clause.map_bound(|clause| clause.trait_ref)),
2869            );
2870
2871            return Some(trait_ref);
2872        }
2873
2874        None
2875    })
2876}
2877
2878mod errors {
2879    use flux_errors::E0999;
2880    use flux_macros::Diagnostic;
2881    use flux_middle::{fhir, global_env::GlobalEnv, rty::Sort};
2882    use rustc_hir::def_id::DefId;
2883    use rustc_span::{Span, Symbol, symbol::Ident};
2884
2885    #[derive(Diagnostic)]
2886    #[diag(fhir_analysis_assoc_item_not_found, code = E0999)]
2887    #[note]
2888    pub(super) struct AssocItemNotFound {
2889        #[primary_span]
2890        #[label]
2891        pub span: Span,
2892        pub tag: &'static str,
2893    }
2894
2895    #[derive(Diagnostic)]
2896    #[diag(fhir_analysis_ambiguous_assoc_item, code = E0999)]
2897    pub(super) struct AmbiguousAssocItem {
2898        #[primary_span]
2899        pub span: Span,
2900        pub name: Ident,
2901        pub tag: &'static str,
2902    }
2903
2904    #[derive(Diagnostic)]
2905    #[diag(fhir_analysis_invalid_base_instance, code = E0999)]
2906    pub(super) struct InvalidBaseInstance {
2907        #[primary_span]
2908        span: Span,
2909    }
2910
2911    impl InvalidBaseInstance {
2912        pub(super) fn new(span: Span) -> Self {
2913            Self { span }
2914        }
2915    }
2916
2917    #[derive(Diagnostic)]
2918    #[diag(fhir_analysis_generic_argument_count_mismatch, code = E0999)]
2919    pub(super) struct GenericArgCountMismatch {
2920        #[primary_span]
2921        #[label]
2922        span: Span,
2923        found: usize,
2924        expected: usize,
2925        def_descr: &'static str,
2926    }
2927
2928    impl GenericArgCountMismatch {
2929        pub(super) fn new(
2930            genv: GlobalEnv,
2931            def_id: DefId,
2932            segment: &fhir::PathSegment,
2933            expected: usize,
2934        ) -> Self {
2935            GenericArgCountMismatch {
2936                span: segment.ident.span,
2937                found: segment.args.len(),
2938                expected,
2939                def_descr: genv.tcx().def_descr(def_id),
2940            }
2941        }
2942    }
2943
2944    #[derive(Diagnostic)]
2945    #[diag(fhir_analysis_too_few_generic_args, code = E0999)]
2946    pub(super) struct TooFewGenericArgs {
2947        #[primary_span]
2948        #[label]
2949        span: Span,
2950        found: usize,
2951        min: usize,
2952        def_descr: &'static str,
2953    }
2954
2955    impl TooFewGenericArgs {
2956        pub(super) fn new(
2957            genv: GlobalEnv,
2958            def_id: DefId,
2959            segment: &fhir::PathSegment,
2960            min: usize,
2961        ) -> Self {
2962            Self {
2963                span: segment.ident.span,
2964                found: segment.args.len(),
2965                min,
2966                def_descr: genv.tcx().def_descr(def_id),
2967            }
2968        }
2969    }
2970
2971    #[derive(Diagnostic)]
2972    #[diag(fhir_analysis_too_many_generic_args, code = E0999)]
2973    pub(super) struct TooManyGenericArgs {
2974        #[primary_span]
2975        #[label]
2976        span: Span,
2977        found: usize,
2978        max: usize,
2979        def_descr: &'static str,
2980    }
2981
2982    impl TooManyGenericArgs {
2983        pub(super) fn new(
2984            genv: GlobalEnv,
2985            def_id: DefId,
2986            segment: &fhir::PathSegment,
2987            max: usize,
2988        ) -> Self {
2989            Self {
2990                span: segment.ident.span,
2991                found: segment.args.len(),
2992                max,
2993                def_descr: genv.tcx().def_descr(def_id),
2994            }
2995        }
2996    }
2997
2998    #[derive(Diagnostic)]
2999    #[diag(fhir_analysis_refined_unrefinable_type, code = E0999)]
3000    pub(super) struct RefinedUnrefinableType {
3001        #[primary_span]
3002        span: Span,
3003    }
3004
3005    impl RefinedUnrefinableType {
3006        pub(super) fn new(span: Span) -> Self {
3007            Self { span }
3008        }
3009    }
3010
3011    #[derive(Diagnostic)]
3012    #[diag(fhir_analysis_generics_on_primitive_sort, code = E0999)]
3013    pub(super) struct GenericsOnPrimitiveSort {
3014        #[primary_span]
3015        #[label]
3016        span: Span,
3017        name: &'static str,
3018        found: usize,
3019        expected: usize,
3020    }
3021
3022    impl GenericsOnPrimitiveSort {
3023        pub(super) fn new(span: Span, name: &'static str, found: usize, expected: usize) -> Self {
3024            Self { span, found, expected, name }
3025        }
3026    }
3027
3028    #[derive(Diagnostic)]
3029    #[diag(fhir_analysis_incorrect_generics_on_sort, code = E0999)]
3030    pub(super) struct IncorrectGenericsOnSort {
3031        #[primary_span]
3032        #[label]
3033        span: Span,
3034        found: usize,
3035        expected: usize,
3036        def_descr: &'static str,
3037    }
3038
3039    impl IncorrectGenericsOnSort {
3040        pub(super) fn new(
3041            genv: GlobalEnv,
3042            def_id: DefId,
3043            span: Span,
3044            found: usize,
3045            expected: usize,
3046        ) -> Self {
3047            Self { span, found, expected, def_descr: genv.tcx().def_descr(def_id) }
3048        }
3049    }
3050
3051    #[derive(Diagnostic)]
3052    #[diag(fhir_analysis_generics_on_sort_ty_param, code = E0999)]
3053    pub(super) struct GenericsOnSortTyParam {
3054        #[primary_span]
3055        #[label]
3056        span: Span,
3057        found: usize,
3058    }
3059
3060    impl GenericsOnSortTyParam {
3061        pub(super) fn new(span: Span, found: usize) -> Self {
3062            Self { span, found }
3063        }
3064    }
3065
3066    #[derive(Diagnostic)]
3067    #[diag(fhir_analysis_generics_on_self_alias, code = E0999)]
3068    pub(super) struct GenericsOnSelf {
3069        #[primary_span]
3070        #[label]
3071        span: Span,
3072        found: usize,
3073    }
3074
3075    impl GenericsOnSelf {
3076        pub(super) fn new(span: Span, found: usize) -> Self {
3077            Self { span, found }
3078        }
3079    }
3080
3081    #[derive(Diagnostic)]
3082    #[diag(fhir_analysis_fields_on_reflected_enum_variant, code = E0999)]
3083    pub(super) struct FieldsOnReflectedEnumVariant {
3084        #[primary_span]
3085        #[label]
3086        span: Span,
3087    }
3088
3089    impl FieldsOnReflectedEnumVariant {
3090        pub(super) fn new(span: Span) -> Self {
3091            Self { span }
3092        }
3093    }
3094
3095    #[derive(Diagnostic)]
3096    #[diag(fhir_analysis_incorrect_generics_on_opaque_sort, code = E0999)]
3097    pub(super) struct IncorrectGenericsOnUserDefinedOpaqueSort {
3098        #[primary_span]
3099        #[label]
3100        span: Span,
3101        name: Symbol,
3102        expected: usize,
3103        found: usize,
3104    }
3105
3106    impl IncorrectGenericsOnUserDefinedOpaqueSort {
3107        pub(super) fn new(span: Span, name: Symbol, expected: usize, found: usize) -> Self {
3108            Self { span, name, expected, found }
3109        }
3110    }
3111
3112    #[derive(Diagnostic)]
3113    #[diag(fhir_analysis_generics_on_prim_ty, code = E0999)]
3114    pub(super) struct GenericsOnPrimTy {
3115        #[primary_span]
3116        pub span: Span,
3117        pub name: &'static str,
3118    }
3119
3120    #[derive(Diagnostic)]
3121    #[diag(fhir_analysis_generics_on_ty_param, code = E0999)]
3122    pub(super) struct GenericsOnTyParam {
3123        #[primary_span]
3124        pub span: Span,
3125        pub name: Symbol,
3126    }
3127
3128    #[derive(Diagnostic)]
3129    #[diag(fhir_analysis_generics_on_self_ty, code = E0999)]
3130    pub(super) struct GenericsOnSelfTy {
3131        #[primary_span]
3132        pub span: Span,
3133    }
3134
3135    #[derive(Diagnostic)]
3136    #[diag(fhir_analysis_generics_on_foreign_ty, code = E0999)]
3137    pub(super) struct GenericsOnForeignTy {
3138        #[primary_span]
3139        pub span: Span,
3140    }
3141
3142    #[derive(Diagnostic)]
3143    #[diag(fhir_analysis_invalid_bitvector_constant, code = E0999)]
3144    pub struct InvalidBitVectorConstant {
3145        #[primary_span]
3146        #[label]
3147        span: Span,
3148        sort: Sort,
3149    }
3150
3151    impl InvalidBitVectorConstant {
3152        pub(crate) fn new(span: Span, sort: Sort) -> Self {
3153            Self { span, sort }
3154        }
3155    }
3156
3157    #[derive(Diagnostic)]
3158    #[diag(fhir_analysis_invalid_assoc_reft, code = E0999)]
3159    pub struct InvalidAssocReft {
3160        #[primary_span]
3161        span: Span,
3162        trait_: String,
3163        name: Symbol,
3164    }
3165
3166    impl InvalidAssocReft {
3167        pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
3168            Self { span, trait_, name }
3169        }
3170    }
3171
3172    #[derive(Diagnostic)]
3173    #[diag(fhir_analysis_refine_arg_mismatch, code = E0999)]
3174    pub(super) struct RefineArgMismatch {
3175        #[primary_span]
3176        #[label]
3177        pub span: Span,
3178        pub expected: usize,
3179        pub found: usize,
3180        pub kind: &'static str,
3181    }
3182
3183    #[derive(Diagnostic)]
3184    #[diag(fhir_analysis_expected_type, code = E0999)]
3185    pub(super) struct ExpectedType {
3186        #[primary_span]
3187        pub span: Span,
3188        pub def_descr: &'static str,
3189        pub name: String,
3190    }
3191
3192    #[derive(Diagnostic)]
3193    #[diag(fhir_analysis_fail_to_match_predicates, code = E0999)]
3194    pub(super) struct FailToMatchPredicates {
3195        #[primary_span]
3196        pub span: Span,
3197    }
3198
3199    #[derive(Diagnostic)]
3200    #[diag(fhir_analysis_invalid_res, code = E0999)]
3201    pub(super) struct InvalidRes {
3202        #[primary_span]
3203        pub span: Span,
3204        pub res_descr: &'static str,
3205    }
3206
3207    #[derive(Diagnostic)]
3208    #[diag(fhir_analysis_constant_annotation_needed, code = E0999)]
3209    pub(super) struct ConstantAnnotationNeeded {
3210        #[primary_span]
3211        #[label]
3212        span: Span,
3213    }
3214    impl ConstantAnnotationNeeded {
3215        pub(super) fn new(span: Span) -> Self {
3216            Self { span }
3217        }
3218    }
3219}