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::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 { name } => {
930                if !path.args.is_empty() {
931                    let err = errors::GenericsOnUserDefinedOpaqueSort::new(
932                        path.segments.last().unwrap().span,
933                        path.args.len(),
934                    );
935                    Err(self.emit(err))?;
936                }
937                rty::SortCtor::User { name }
938            }
939            fhir::SortRes::Adt(def_id) => {
940                let sort_def = self.genv().adt_sort_def_of(def_id)?;
941                if path.args.len() != sort_def.param_count() {
942                    let err = errors::IncorrectGenericsOnSort::new(
943                        self.genv(),
944                        def_id,
945                        path.segments.last().unwrap().span,
946                        path.args.len(),
947                        sort_def.param_count(),
948                    );
949                    Err(self.emit(err))?;
950                }
951                rty::SortCtor::Adt(sort_def)
952            }
953        };
954        let args = path.args.iter().map(|t| self.conv_sort(t)).try_collect()?;
955
956        Ok(rty::Sort::app(ctor, args))
957    }
958
959    fn check_prim_sort_generics(
960        &mut self,
961        path: &fhir::SortPath<'_>,
962        prim_sort: fhir::PrimSort,
963    ) -> QueryResult {
964        if path.args.len() != prim_sort.generics() {
965            let err = errors::GenericsOnPrimitiveSort::new(
966                path.segments.last().unwrap().span,
967                prim_sort.name_str(),
968                path.args.len(),
969                prim_sort.generics(),
970            );
971            Err(self.emit(err))?;
972        }
973        Ok(())
974    }
975}
976
977/// Conversion of types
978impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
979    fn conv_fn_decl(
980        &mut self,
981        env: &mut Env,
982        safety: Safety,
983        abi: rustc_abi::ExternAbi,
984        decl: &fhir::FnDecl,
985        body_id: Option<BodyId>,
986    ) -> QueryResult<rty::FnSig> {
987        let mut requires = vec![];
988        for req in decl.requires {
989            requires.push(self.conv_requires(env, req)?);
990        }
991
992        let mut inputs = vec![];
993        let params =
994            if let Some(body_id) = body_id { self.tcx().hir_body(body_id).params } else { &[] };
995        for (i, ty) in decl.inputs.iter().enumerate() {
996            let ty = if let Some(param) = params.get(i)
997                && let hir::PatKind::Binding(_, _, ident, _) = param.pat.kind
998            {
999                self.conv_ty_with_name(env, ty, ident.name)?
1000            } else {
1001                self.conv_ty(env, ty)?
1002            };
1003            inputs.push(ty);
1004        }
1005
1006        let output = self.conv_fn_output(env, &decl.output)?;
1007
1008        Ok(rty::FnSig::new(safety, abi, requires.into(), inputs.into(), output))
1009    }
1010
1011    fn conv_requires(
1012        &mut self,
1013        env: &mut Env,
1014        requires: &fhir::Requires,
1015    ) -> QueryResult<rty::Expr> {
1016        if requires.params.is_empty() {
1017            self.conv_expr(env, &requires.pred)
1018        } else {
1019            env.push_layer(Layer::list(self.results(), 0, requires.params));
1020            let pred = self.conv_expr(env, &requires.pred)?;
1021            let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1022            Ok(rty::Expr::forall(rty::Binder::bind_with_vars(pred, sorts)))
1023        }
1024    }
1025
1026    fn conv_ensures(
1027        &mut self,
1028        env: &mut Env,
1029        ensures: &fhir::Ensures,
1030    ) -> QueryResult<rty::Ensures> {
1031        match ensures {
1032            fhir::Ensures::Type(loc, ty) => {
1033                Ok(rty::Ensures::Type(self.conv_loc(env, *loc)?, self.conv_ty(env, ty)?))
1034            }
1035            fhir::Ensures::Pred(pred) => Ok(rty::Ensures::Pred(self.conv_expr(env, pred)?)),
1036        }
1037    }
1038
1039    fn conv_fn_output(
1040        &mut self,
1041        env: &mut Env,
1042        output: &fhir::FnOutput,
1043    ) -> QueryResult<rty::Binder<rty::FnOutput>> {
1044        env.push_layer(Layer::list(self.results(), 0, output.params));
1045
1046        let ret = self.conv_ty(env, &output.ret)?;
1047
1048        let ensures: List<rty::Ensures> = output
1049            .ensures
1050            .iter()
1051            .map(|ens| self.conv_ensures(env, ens))
1052            .try_collect()?;
1053        let output = rty::FnOutput::new(ret, ensures);
1054
1055        let vars = env.pop_layer().into_bound_vars(self.genv())?;
1056        Ok(rty::Binder::bind_with_vars(output, vars))
1057    }
1058
1059    fn conv_generic_bounds(
1060        &mut self,
1061        env: &mut Env,
1062        bounded_ty_span: Span,
1063        bounded_ty: rty::Ty,
1064        bounds: fhir::GenericBounds,
1065    ) -> QueryResult<Vec<rty::Clause>> {
1066        let mut clauses = vec![];
1067        for bound in bounds {
1068            match bound {
1069                fhir::GenericBound::Trait(poly_trait_ref) => {
1070                    match poly_trait_ref.modifiers {
1071                        fhir::TraitBoundModifier::None => {
1072                            self.conv_poly_trait_ref(
1073                                env,
1074                                bounded_ty_span,
1075                                &bounded_ty,
1076                                poly_trait_ref,
1077                                &mut clauses,
1078                            )?;
1079                        }
1080                        fhir::TraitBoundModifier::Maybe => {
1081                            // Maybe bounds are only supported for `?Sized`. The effect of the maybe
1082                            // bound is to relax the default which is `Sized` to not have the `Sized`
1083                            // bound, so we just skip it here.
1084                        }
1085                    }
1086                }
1087                fhir::GenericBound::Outlives(lft) => {
1088                    let re = self.conv_lifetime(env, *lft, bounded_ty_span);
1089                    clauses.push(rty::Clause::new(
1090                        List::empty(),
1091                        rty::ClauseKind::TypeOutlives(rty::OutlivesPredicate(
1092                            bounded_ty.clone(),
1093                            re,
1094                        )),
1095                    ));
1096                }
1097            }
1098        }
1099        Ok(clauses)
1100    }
1101
1102    /// Converts a `T: Trait<T0, ..., A0 = S0, ...>` bound
1103    fn conv_poly_trait_ref(
1104        &mut self,
1105        env: &mut Env,
1106        span: Span,
1107        bounded_ty: &rty::Ty,
1108        poly_trait_ref: &fhir::PolyTraitRef,
1109        clauses: &mut Vec<rty::Clause>,
1110    ) -> QueryResult {
1111        let generic_params = &poly_trait_ref.bound_generic_params;
1112        let layer =
1113            Layer::list(self.results(), generic_params.len() as u32, poly_trait_ref.refine_params);
1114        env.push_layer(layer);
1115
1116        let trait_id = poly_trait_ref.trait_def_id();
1117        let generics = self.genv().generics_of(trait_id)?;
1118        let trait_segment = poly_trait_ref.trait_ref.last_segment();
1119
1120        let self_param = generics.param_at(0, self.genv())?;
1121        let mut args = vec![
1122            self.try_to_ty_or_base(self_param.kind, span, bounded_ty)?
1123                .into(),
1124        ];
1125        self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1126
1127        let vars = env.top_layer().to_bound_vars(self.genv())?;
1128        let poly_trait_ref = rty::Binder::bind_with_vars(
1129            rty::TraitRef { def_id: trait_id, args: args.into() },
1130            vars,
1131        );
1132
1133        clauses.push(
1134            poly_trait_ref
1135                .clone()
1136                .map(|trait_ref| {
1137                    rty::ClauseKind::Trait(rty::TraitPredicate { trait_ref: trait_ref.clone() })
1138                })
1139                .into(),
1140        );
1141
1142        for cstr in trait_segment.constraints {
1143            self.conv_assoc_item_constraint(env, &poly_trait_ref, cstr, clauses)?;
1144        }
1145
1146        env.pop_layer();
1147
1148        Ok(())
1149    }
1150
1151    fn conv_assoc_item_constraint(
1152        &mut self,
1153        env: &mut Env,
1154        poly_trait_ref: &rty::PolyTraitRef,
1155        constraint: &fhir::AssocItemConstraint,
1156        clauses: &mut Vec<rty::Clause>,
1157    ) -> QueryResult {
1158        let tcx = self.tcx();
1159
1160        let candidate = self.probe_single_bound_for_assoc_item(
1161            || traits::supertraits(tcx, poly_trait_ref.to_rustc(tcx)),
1162            constraint.ident,
1163            AssocTag::Type,
1164        )?;
1165        let assoc_item_id = AssocTag::Type
1166            .trait_defines_item_named(self.genv(), candidate.def_id(), constraint.ident)?
1167            .unwrap()
1168            .def_id;
1169
1170        let fhir::AssocItemConstraintKind::Equality { term } = &constraint.kind;
1171        let span = term.span;
1172        let term = self.conv_ty(env, term)?;
1173        let term = self.ty_to_subset_ty_ctor(span, &term)?;
1174
1175        let clause = poly_trait_ref
1176            .clone()
1177            .map(|trait_ref| {
1178                // TODO: when we support generic associated types, we need to also attach the associated generics here
1179                let args = trait_ref.args;
1180                let refine_args = List::empty();
1181                let projection_ty = rty::AliasTy { def_id: assoc_item_id, args, refine_args };
1182
1183                rty::ClauseKind::Projection(rty::ProjectionPredicate { projection_ty, term })
1184            })
1185            .into();
1186
1187        clauses.push(clause);
1188        Ok(())
1189    }
1190
1191    fn conv_ty_with_name(
1192        &mut self,
1193        env: &mut Env,
1194        ty: &fhir::Ty,
1195        name: Symbol,
1196    ) -> QueryResult<rty::Ty> {
1197        if let fhir::TyKind::BaseTy(bty) = &ty.kind {
1198            Ok(self.conv_bty(env, bty, Some(name))?.to_ty())
1199        } else {
1200            self.conv_ty(env, ty)
1201        }
1202    }
1203
1204    fn conv_ty(&mut self, env: &mut Env, ty: &fhir::Ty) -> QueryResult<rty::Ty> {
1205        match &ty.kind {
1206            fhir::TyKind::BaseTy(bty) => Ok(self.conv_bty(env, bty, None)?.to_ty()),
1207            fhir::TyKind::Indexed(bty, idx) => {
1208                let fhir_id = bty.fhir_id;
1209                let rty::TyOrCtor::Ctor(ty_ctor) = self.conv_bty(env, bty, None)? else {
1210                    return Err(self.emit(errors::RefinedUnrefinableType::new(bty.span)))?;
1211                };
1212                let idx = self.conv_expr(env, idx)?;
1213                self.0.insert_node_sort(fhir_id, ty_ctor.sort());
1214                Ok(ty_ctor.replace_bound_reft(&idx))
1215            }
1216            fhir::TyKind::Exists(params, ty) => {
1217                let layer = Layer::list(self.results(), 0, params);
1218                env.push_layer(layer);
1219                let ty = self.conv_ty(env, ty)?;
1220                let sorts = env.pop_layer().into_bound_vars(self.genv())?;
1221                if sorts.is_empty() {
1222                    Ok(ty.shift_out_escaping(1))
1223                } else {
1224                    Ok(rty::Ty::exists(rty::Binder::bind_with_vars(ty, sorts)))
1225                }
1226            }
1227            fhir::TyKind::StrgRef(lft, loc, ty) => {
1228                let re = self.conv_lifetime(env, *lft, ty.span);
1229                let loc = self.conv_loc(env, **loc)?;
1230                let ty = self.conv_ty(env, ty)?;
1231                Ok(rty::Ty::strg_ref(re, loc, ty))
1232            }
1233            fhir::TyKind::Ref(lft, fhir::MutTy { ty, mutbl }) => {
1234                let region = self.conv_lifetime(env, *lft, ty.span);
1235                Ok(rty::Ty::mk_ref(region, self.conv_ty(env, ty)?, *mutbl))
1236            }
1237            fhir::TyKind::BareFn(bare_fn) => {
1238                let mut env = Env::empty();
1239                env.push_layer(Layer::list(
1240                    self.results(),
1241                    bare_fn.generic_params.len() as u32,
1242                    &[],
1243                ));
1244                let fn_sig =
1245                    self.conv_fn_decl(&mut env, bare_fn.safety, bare_fn.abi, bare_fn.decl, None)?;
1246                let vars = bare_fn
1247                    .generic_params
1248                    .iter()
1249                    .map(|param| self.param_as_bound_var(param))
1250                    .try_collect()?;
1251                let poly_fn_sig = rty::Binder::bind_with_vars(fn_sig, vars);
1252                Ok(rty::BaseTy::FnPtr(poly_fn_sig).to_ty())
1253            }
1254            fhir::TyKind::Tuple(tys) => {
1255                let tys: List<rty::Ty> =
1256                    tys.iter().map(|ty| self.conv_ty(env, ty)).try_collect()?;
1257                Ok(rty::Ty::tuple(tys))
1258            }
1259            fhir::TyKind::Array(ty, len) => {
1260                Ok(rty::Ty::array(self.conv_ty(env, ty)?, self.conv_const_arg(*len)))
1261            }
1262            fhir::TyKind::Never => Ok(rty::Ty::never()),
1263            fhir::TyKind::Constr(pred, ty) => {
1264                let pred = self.conv_expr(env, pred)?;
1265                Ok(rty::Ty::constr(pred, self.conv_ty(env, ty)?))
1266            }
1267            fhir::TyKind::RawPtr(ty, mutability) => {
1268                Ok(rty::Ty::indexed(
1269                    rty::BaseTy::RawPtr(self.conv_ty(env, ty)?, *mutability),
1270                    rty::Expr::unit(),
1271                ))
1272            }
1273            fhir::TyKind::OpaqueDef(opaque_ty) => self.conv_opaque_def(env, opaque_ty, ty.span),
1274            fhir::TyKind::TraitObject(trait_bounds, lft, syn) => {
1275                if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) {
1276                    self.conv_trait_object(env, trait_bounds, *lft, ty.span)
1277                } else {
1278                    span_bug!(ty.span, "dyn* traits not supported yet")
1279                }
1280            }
1281            fhir::TyKind::Infer => Ok(rty::Ty::infer(self.next_type_vid())),
1282            fhir::TyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1283        }
1284    }
1285
1286    /// Code adapted from <https://github.com/rust-lang/rust/blob/b5723af3457b9cd3795eeb97e9af2d34964854f2/compiler/rustc_hir_analysis/src/hir_ty_lowering/mod.rs#L2099>
1287    fn conv_opaque_def(
1288        &mut self,
1289        env: &mut Env,
1290        opaque_ty: &fhir::OpaqueTy,
1291        span: Span,
1292    ) -> QueryResult<rty::Ty> {
1293        let def_id = opaque_ty.def_id;
1294
1295        if P::HAS_ELABORATED_INFORMATION {
1296            let lifetimes = self.tcx().opaque_captured_lifetimes(def_id.local_id());
1297
1298            let generics = self.tcx().generics_of(opaque_ty.def_id);
1299
1300            let offset = generics.parent_count;
1301
1302            let args = rty::GenericArg::for_item(self.genv(), def_id.resolved_id(), |param, _| {
1303                if let Some(i) = (param.index as usize).checked_sub(offset) {
1304                    let (lifetime, _) = lifetimes[i];
1305                    rty::GenericArg::Lifetime(self.conv_resolved_lifetime(env, lifetime, span))
1306                } else {
1307                    rty::GenericArg::from_param_def(param)
1308                }
1309            })?;
1310            let reft_args = rty::RefineArgs::identity_for_item(self.genv(), def_id.resolved_id())?;
1311            let alias_ty = rty::AliasTy::new(def_id.resolved_id(), args, reft_args);
1312            Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1313        } else {
1314            // During sortck we need to run conv on the opaque type to collect sorts for base types
1315            // in the opaque type's bounds. After sortck, we don't need to because opaque types are
1316            // converted as part of `genv.item_bounds`.
1317            self.conv_opaque_ty(opaque_ty)?;
1318
1319            // `RefineArgs::identity_for_item` uses `genv.refinement_generics_of` which in turn
1320            // requires `genv.check_wf`, so we simply return all empty here to avoid the circularity
1321            let alias_ty = rty::AliasTy::new(def_id.resolved_id(), List::empty(), List::empty());
1322            Ok(rty::BaseTy::opaque(alias_ty).to_ty())
1323        }
1324    }
1325
1326    fn conv_trait_object(
1327        &mut self,
1328        env: &mut Env,
1329        trait_bounds: &[fhir::PolyTraitRef],
1330        lifetime: fhir::Lifetime,
1331        span: Span,
1332    ) -> QueryResult<rty::Ty> {
1333        // We convert all the trait bounds into existential predicates. Some combinations won't yield
1334        // valid rust types (e.g., only one regular (non-auto) trait is allowed). We don't detect those
1335        // errors here, but that's fine because we should catch them when we check structural
1336        // compatibility with the unrefined rust type. We must be careful with producing predicates
1337        // in the same order that rustc does.
1338
1339        let mut bounds = vec![];
1340        let dummy_self = rty::Ty::trait_object_dummy_self();
1341        for trait_bound in trait_bounds.iter().rev() {
1342            self.conv_poly_trait_ref(env, trait_bound.span, &dummy_self, trait_bound, &mut bounds)?;
1343        }
1344
1345        // Separate trait bounds and projections bounds
1346        let mut trait_bounds = vec![];
1347        let mut projection_bounds = vec![];
1348        for pred in bounds {
1349            let bound_pred = pred.kind();
1350            let vars = bound_pred.vars().clone();
1351            match bound_pred.skip_binder() {
1352                rty::ClauseKind::Trait(trait_pred) => {
1353                    trait_bounds.push(rty::Binder::bind_with_vars(trait_pred.trait_ref, vars));
1354                }
1355                rty::ClauseKind::Projection(proj) => {
1356                    projection_bounds.push(rty::Binder::bind_with_vars(proj, vars));
1357                }
1358                rty::ClauseKind::RegionOutlives(_) => {}
1359                rty::ClauseKind::TypeOutlives(_) => {}
1360                rty::ClauseKind::ConstArgHasType(..) => {
1361                    bug!("did not expect {pred:?} clause in object bounds");
1362                }
1363            }
1364        }
1365
1366        // Separate between regular from auto traits
1367        let (mut auto_traits, regular_traits): (Vec<_>, Vec<_>) = trait_bounds
1368            .into_iter()
1369            .partition(|trait_ref| self.tcx().trait_is_auto(trait_ref.def_id()));
1370
1371        // De-duplicate auto traits preserving order
1372        {
1373            let mut duplicates = FxHashSet::default();
1374            auto_traits.retain(|trait_ref| duplicates.insert(trait_ref.def_id()));
1375        }
1376
1377        let regular_trait_predicates = regular_traits.into_iter().map(|poly_trait_ref| {
1378            poly_trait_ref.map(|trait_ref| {
1379                // Remove dummy self
1380                let args = trait_ref.args.iter().skip(1).cloned().collect();
1381                rty::ExistentialPredicate::Trait(rty::ExistentialTraitRef {
1382                    def_id: trait_ref.def_id,
1383                    args,
1384                })
1385            })
1386        });
1387
1388        let auto_trait_predicates = auto_traits.into_iter().map(|trait_def| {
1389            rty::Binder::dummy(rty::ExistentialPredicate::AutoTrait(trait_def.def_id()))
1390        });
1391
1392        let existential_projections = projection_bounds.into_iter().map(|bound| {
1393            bound.map(|proj| {
1394                // Remove dummy self
1395                let args = proj.projection_ty.args.iter().skip(1).cloned().collect();
1396                rty::ExistentialPredicate::Projection(rty::ExistentialProjection {
1397                    def_id: proj.projection_ty.def_id,
1398                    args,
1399                    term: proj.term.clone(),
1400                })
1401            })
1402        });
1403
1404        let existential_predicates = {
1405            let mut v = regular_trait_predicates
1406                .chain(existential_projections)
1407                .chain(auto_trait_predicates)
1408                .collect_vec();
1409            v.sort_by(|a, b| {
1410                a.as_ref()
1411                    .skip_binder()
1412                    .stable_cmp(self.tcx(), b.as_ref().skip_binder())
1413            });
1414            List::from_vec(v)
1415        };
1416
1417        let region = self.conv_lifetime(env, lifetime, span);
1418        Ok(rty::Ty::dynamic(existential_predicates, region))
1419    }
1420
1421    pub(crate) fn conv_bty(
1422        &mut self,
1423        env: &mut Env,
1424        bty: &fhir::BaseTy,
1425        name: Option<Symbol>,
1426    ) -> QueryResult<rty::TyOrCtor> {
1427        match &bty.kind {
1428            fhir::BaseTyKind::Path(fhir::QPath::Resolved(qself, path)) => {
1429                self.conv_qpath(env, *qself, path, name)
1430            }
1431            fhir::BaseTyKind::Path(fhir::QPath::TypeRelative(qself, segment)) => {
1432                let qself_res =
1433                    if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
1434                let alias_ty = self
1435                    .conv_type_relative_type_path(env, qself.span, qself_res, segment)?
1436                    .shift_in_escaping(1);
1437                let bty = rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty);
1438                let sort = bty.sort();
1439                let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1440                Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1441            }
1442            fhir::BaseTyKind::Slice(ty) => {
1443                let bty = rty::BaseTy::Slice(self.conv_ty(env, ty)?).shift_in_escaping(1);
1444                let sort = bty.sort();
1445                let ty = rty::Ty::indexed(bty, rty::Expr::nu());
1446                Ok(rty::TyOrCtor::Ctor(rty::Binder::bind_with_sort(ty, sort)))
1447            }
1448            fhir::BaseTyKind::Err(err) => Err(QueryErr::Emitted(*err)),
1449        }
1450    }
1451
1452    fn conv_type_relative_path<Tag: AssocItemTag>(
1453        &mut self,
1454        tag: Tag,
1455        qself_span: Span,
1456        qself_res: fhir::Res,
1457        assoc_ident: Ident,
1458    ) -> QueryResult<(Tag::AssocItem<'tcx>, rty::TraitRef)> {
1459        let tcx = self.tcx();
1460
1461        let bound = match qself_res {
1462            fhir::Res::SelfTyAlias { alias_to: impl_def_id, is_trait_impl: true } => {
1463                let Some(trait_ref) = tcx.impl_trait_ref(impl_def_id) else {
1464                    // A cycle error occurred most likely (comment copied from rustc)
1465                    span_bug!(qself_span, "expected cycle error");
1466                };
1467
1468                self.probe_single_bound_for_assoc_item(
1469                    || {
1470                        traits::supertraits(
1471                            tcx,
1472                            ty::Binder::dummy(trait_ref.instantiate_identity()),
1473                        )
1474                    },
1475                    assoc_ident,
1476                    tag,
1477                )?
1478            }
1479            fhir::Res::Def(DefKind::TyParam, param_id)
1480            | fhir::Res::SelfTyParam { trait_: param_id } => {
1481                let predicates = type_param_predicates(tcx, param_id);
1482                self.probe_single_bound_for_assoc_item(
1483                    || {
1484                        tag.transitive_bounds_that_define_assoc_item(
1485                            self.genv(),
1486                            predicates.map(|pred| pred.map_bound(|t| t.trait_ref)),
1487                            assoc_ident,
1488                        )
1489                    },
1490                    assoc_ident,
1491                    tag,
1492                )?
1493            }
1494            _ => self.report_assoc_item_not_found(assoc_ident.span, tag)?,
1495        };
1496
1497        let Some(trait_ref) = bound.no_bound_vars() else {
1498            // This is a programmer error and we should gracefully report it. It's triggered
1499            // by code like this
1500            // ```
1501            // trait Super<'a> { type Assoc; }
1502            // trait Child: for<'a> Super<'a> {}
1503            // fn foo<T: Child>(x: T::Assoc) {}
1504            // ```
1505            Err(self.emit(
1506                query_bug!("associated path with uninferred generic parameters")
1507                    .at(assoc_ident.span),
1508            ))?
1509        };
1510
1511        let trait_ref = trait_ref
1512            .lower(tcx)
1513            .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?
1514            .refine(&self.refiner()?)?;
1515
1516        let assoc_item = tag
1517            .trait_defines_item_named(self.genv(), trait_ref.def_id, assoc_ident)?
1518            .unwrap();
1519
1520        Ok((assoc_item, trait_ref))
1521    }
1522
1523    fn conv_type_relative_type_path(
1524        &mut self,
1525        env: &mut Env,
1526        qself_span: Span,
1527        qself_res: fhir::Res,
1528        assoc_segment: &fhir::PathSegment,
1529    ) -> QueryResult<rty::AliasTy> {
1530        let (assoc_item, trait_ref) = self.conv_type_relative_path(
1531            AssocTag::Type,
1532            qself_span,
1533            qself_res,
1534            assoc_segment.ident,
1535        )?;
1536
1537        let assoc_id = assoc_item.def_id;
1538        let mut args = trait_ref.args.to_vec();
1539        self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1540
1541        let args = List::from_vec(args);
1542        let refine_args = List::empty();
1543        let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1544        Ok(alias_ty)
1545    }
1546
1547    fn conv_type_relative_const_path(
1548        &mut self,
1549        fhir_expr: &fhir::Expr,
1550        qself: &rty::Ty,
1551        assoc: Ident,
1552    ) -> QueryResult<rty::Expr> {
1553        let tcx = self.genv().tcx();
1554
1555        let mut candidates = vec![];
1556        if let Some(simplified_type) = qself.simplify_type() {
1557            candidates = tcx
1558                .incoherent_impls(simplified_type)
1559                .iter()
1560                .filter_map(|impl_id| {
1561                    tcx.associated_items(impl_id).find_by_ident_and_kind(
1562                        tcx,
1563                        assoc,
1564                        AssocTag::Const,
1565                        *impl_id,
1566                    )
1567                })
1568                .collect_vec();
1569        }
1570        let (expr, sort) = match &candidates[..] {
1571            [candidate] => self.conv_const(fhir_expr.span, candidate.def_id)?,
1572            [] => self.report_assoc_item_not_found(fhir_expr.span, AssocTag::Const)?,
1573            _ => self.report_ambiguous_assoc_item(fhir_expr.span, AssocTag::Const, assoc)?,
1574        };
1575        self.0.insert_node_sort(fhir_expr.fhir_id, sort);
1576        Ok(expr)
1577    }
1578
1579    /// Return the generics of the containing owner item
1580    fn refiner(&self) -> QueryResult<Refiner<'genv, 'tcx>> {
1581        match self.owner() {
1582            FluxOwnerId::Rust(owner_id) => {
1583                let def_id = self.genv().maybe_extern_id(owner_id.def_id);
1584                Refiner::default_for_item(self.genv(), def_id.resolved_id())
1585            }
1586            FluxOwnerId::Flux(_) => Err(query_bug!("cannot refine types insicde flux item")),
1587        }
1588    }
1589
1590    fn probe_single_bound_for_assoc_item<I, Tag: AssocItemTag>(
1591        &self,
1592        all_candidates: impl FnOnce() -> I,
1593        assoc_name: Ident,
1594        tag: Tag,
1595    ) -> QueryResult<ty::PolyTraitRef<'tcx>>
1596    where
1597        I: Iterator<Item = ty::PolyTraitRef<'tcx>>,
1598    {
1599        let mut matching_candidates = vec![];
1600        for candidate in all_candidates() {
1601            if tag
1602                .trait_defines_item_named(self.genv(), candidate.def_id(), assoc_name)?
1603                .is_some()
1604            {
1605                matching_candidates.push(candidate);
1606            }
1607        }
1608
1609        let Some(bound) = matching_candidates.pop() else {
1610            self.report_assoc_item_not_found(assoc_name.span, tag)?;
1611        };
1612
1613        if !matching_candidates.is_empty() {
1614            self.report_ambiguous_assoc_item(assoc_name.span, tag, assoc_name)?;
1615        }
1616
1617        Ok(bound)
1618    }
1619
1620    fn conv_lifetime(&mut self, env: &Env, lft: fhir::Lifetime, span: Span) -> rty::Region {
1621        let res = match lft {
1622            fhir::Lifetime::Hole(_) => return rty::Region::ReVar(self.next_region_vid()),
1623            fhir::Lifetime::Resolved(res) => res,
1624        };
1625        self.conv_resolved_lifetime(env, res, span)
1626    }
1627
1628    fn conv_resolved_lifetime(&mut self, env: &Env, res: ResolvedArg, span: Span) -> rty::Region {
1629        let tcx = self.tcx();
1630        let lifetime_name = |def_id| tcx.item_name(def_id);
1631        match res {
1632            ResolvedArg::StaticLifetime => rty::ReStatic,
1633            ResolvedArg::EarlyBound(def_id) => {
1634                let index = self.genv().def_id_to_param_index(def_id.to_def_id());
1635                let name = lifetime_name(def_id.to_def_id());
1636                rty::ReEarlyParam(rty::EarlyParamRegion { index, name })
1637            }
1638            ResolvedArg::LateBound(_, index, def_id) => {
1639                let Some(depth) = env.depth().checked_sub(1) else {
1640                    span_bug!(span, "late-bound variable at depth 0")
1641                };
1642                let kind = rty::BoundRegionKind::Named(def_id.to_def_id());
1643                let var = BoundVar::from_u32(index);
1644                let bound_region = rty::BoundRegion { var, kind };
1645                rty::ReBound(rty::DebruijnIndex::from_usize(depth), bound_region)
1646            }
1647            ResolvedArg::Free(scope, id) => {
1648                let kind = rty::LateParamRegionKind::Named(id.to_def_id());
1649                rty::ReLateParam(rty::LateParamRegion { scope: scope.to_def_id(), kind })
1650            }
1651            ResolvedArg::Error(_) => bug!("lifetime resolved to an error"),
1652        }
1653    }
1654
1655    fn conv_const_arg(&mut self, cst: fhir::ConstArg) -> rty::Const {
1656        match cst.kind {
1657            fhir::ConstArgKind::Lit(lit) => rty::Const::from_usize(self.tcx(), lit),
1658            fhir::ConstArgKind::Param(def_id) => {
1659                rty::Const {
1660                    kind: rty::ConstKind::Param(def_id_to_param_const(self.genv(), def_id)),
1661                }
1662            }
1663            fhir::ConstArgKind::Infer => {
1664                rty::Const {
1665                    kind: rty::ConstKind::Infer(ty::InferConst::Var(self.next_const_vid())),
1666                }
1667            }
1668        }
1669    }
1670
1671    fn conv_qpath(
1672        &mut self,
1673        env: &mut Env,
1674        qself: Option<&fhir::Ty>,
1675        path: &fhir::Path,
1676        name: Option<Symbol>,
1677    ) -> QueryResult<rty::TyOrCtor> {
1678        let bty = match path.res {
1679            fhir::Res::PrimTy(prim_ty) => {
1680                self.check_prim_ty_generics(path, prim_ty)?;
1681                prim_ty_to_bty(prim_ty)
1682            }
1683            fhir::Res::Def(DefKind::Struct | DefKind::Enum | DefKind::Union, did) => {
1684                let adt_def = self.genv().adt_def(did)?;
1685                let args = self.conv_generic_args(env, did, path.last_segment())?;
1686                rty::BaseTy::adt(adt_def, args)
1687            }
1688            fhir::Res::Def(DefKind::TyParam, def_id) => {
1689                let owner_id = ty_param_owner(self.genv(), def_id);
1690                let param_ty = def_id_to_param_ty(self.genv(), def_id);
1691                self.check_ty_param_generics(path, param_ty)?;
1692                let param = self
1693                    .genv()
1694                    .generics_of(owner_id)?
1695                    .param_at(param_ty.index as usize, self.genv())?;
1696                match param.kind {
1697                    rty::GenericParamDefKind::Type { .. } => {
1698                        return Ok(rty::TyOrCtor::Ty(rty::Ty::param(param_ty)));
1699                    }
1700                    rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(param_ty),
1701                    _ => return Err(query_bug!("unexpected param kind")),
1702                }
1703            }
1704            fhir::Res::SelfTyParam { trait_ } => {
1705                self.check_self_ty_generics(path)?;
1706                let param = &self.genv().generics_of(trait_)?.own_params[0];
1707                match param.kind {
1708                    rty::GenericParamDefKind::Type { .. } => {
1709                        return Ok(rty::TyOrCtor::Ty(rty::Ty::param(rty::SELF_PARAM_TY)));
1710                    }
1711                    rty::GenericParamDefKind::Base { .. } => rty::BaseTy::Param(rty::SELF_PARAM_TY),
1712                    _ => return Err(query_bug!("unexpected param kind")),
1713                }
1714            }
1715            fhir::Res::SelfTyAlias { alias_to, .. } => {
1716                self.check_self_ty_generics(path)?;
1717                if P::EXPAND_TYPE_ALIASES {
1718                    return Ok(self.genv().type_of(alias_to)?.instantiate_identity());
1719                } else {
1720                    rty::BaseTy::Alias(
1721                        rty::AliasKind::Free,
1722                        rty::AliasTy {
1723                            def_id: alias_to,
1724                            args: List::empty(),
1725                            refine_args: List::empty(),
1726                        },
1727                    )
1728                }
1729            }
1730            fhir::Res::Def(DefKind::AssocTy, assoc_id) => {
1731                let trait_id = self.tcx().trait_of_assoc(assoc_id).unwrap();
1732
1733                let [.., trait_segment, assoc_segment] = path.segments else {
1734                    span_bug!(path.span, "expected at least two segments");
1735                };
1736
1737                let Some(qself) = qself else {
1738                    self.report_ambiguous_assoc_item(
1739                        path.span,
1740                        AssocTag::Type,
1741                        assoc_segment.ident,
1742                    )?
1743                };
1744
1745                let trait_generics = self.genv().generics_of(trait_id)?;
1746                let qself =
1747                    self.conv_ty_to_generic_arg(env, &trait_generics.own_params[0], qself)?;
1748                let mut args = vec![qself];
1749                self.conv_generic_args_into(env, trait_id, trait_segment, &mut args)?;
1750                self.conv_generic_args_into(env, assoc_id, assoc_segment, &mut args)?;
1751                let args = List::from_vec(args);
1752
1753                let refine_args = List::empty();
1754                let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id };
1755                rty::BaseTy::Alias(rty::AliasKind::Projection, alias_ty)
1756            }
1757            fhir::Res::Def(DefKind::TyAlias, def_id) => {
1758                self.check_refinement_generics(path, def_id)?;
1759                let args = self.conv_generic_args(env, def_id, path.last_segment())?;
1760                self.0.insert_path_args(path.fhir_id, args.clone());
1761                let refine_args = path
1762                    .refine
1763                    .iter()
1764                    .map(|expr| self.conv_expr(env, expr))
1765                    .try_collect_vec()?;
1766
1767                if P::EXPAND_TYPE_ALIASES {
1768                    let tcx = self.tcx();
1769                    return Ok(self
1770                        .genv()
1771                        .type_of(def_id)?
1772                        .instantiate(tcx, &args, &refine_args));
1773                } else {
1774                    rty::BaseTy::Alias(
1775                        rty::AliasKind::Free,
1776                        rty::AliasTy { def_id, args, refine_args: List::from(refine_args) },
1777                    )
1778                }
1779            }
1780            fhir::Res::Def(DefKind::ForeignTy, def_id) => {
1781                self.check_foreign_ty_generics(path)?;
1782                rty::BaseTy::Foreign(def_id)
1783            }
1784            fhir::Res::Def(kind, def_id) => self.report_expected_type(path.span, kind, def_id)?,
1785            fhir::Res::Param(..) | fhir::Res::GlobalFunc(..) | fhir::Res::Err => {
1786                span_bug!(path.span, "unexpected resolution in conv_ty_ctor: {:?}", path.res)
1787            }
1788        };
1789        let sort = bty.sort();
1790        let bty = bty.shift_in_escaping(1);
1791        let kind = match name {
1792            Some(name) => BoundReftKind::Named(name),
1793            None => BoundReftKind::Anon,
1794        };
1795        let var = rty::BoundVariableKind::Refine(sort, rty::InferMode::EVar, kind);
1796        let ctor = rty::Binder::bind_with_vars(
1797            rty::Ty::indexed(bty, rty::Expr::nu()),
1798            List::singleton(var),
1799        );
1800        Ok(rty::TyOrCtor::Ctor(ctor))
1801    }
1802
1803    fn param_as_bound_var(
1804        &mut self,
1805        param: &fhir::GenericParam,
1806    ) -> QueryResult<rty::BoundVariableKind> {
1807        let def_id = param.def_id.resolved_id();
1808        match param.kind {
1809            fhir::GenericParamKind::Lifetime => {
1810                Ok(rty::BoundVariableKind::Region(rty::BoundRegionKind::Named(def_id)))
1811            }
1812            fhir::GenericParamKind::Const { .. } | fhir::GenericParamKind::Type { .. } => {
1813                Err(query_bug!(def_id, "unsupported param kind `{:?}`", param.kind))
1814            }
1815        }
1816    }
1817
1818    fn conv_generic_args(
1819        &mut self,
1820        env: &mut Env,
1821        def_id: DefId,
1822        segment: &fhir::PathSegment,
1823    ) -> QueryResult<List<rty::GenericArg>> {
1824        let mut into = vec![];
1825        self.conv_generic_args_into(env, def_id, segment, &mut into)?;
1826        Ok(List::from(into))
1827    }
1828
1829    fn conv_generic_args_into(
1830        &mut self,
1831        env: &mut Env,
1832        def_id: DefId,
1833        segment: &fhir::PathSegment,
1834        into: &mut Vec<rty::GenericArg>,
1835    ) -> QueryResult {
1836        let generics = self.genv().generics_of(def_id)?;
1837
1838        self.check_generic_arg_count(&generics, def_id, segment)?;
1839
1840        let len = into.len();
1841        for (idx, arg) in segment.args.iter().enumerate() {
1842            let param = generics.param_at(idx + len, self.genv())?;
1843            match arg {
1844                fhir::GenericArg::Lifetime(lft) => {
1845                    into.push(rty::GenericArg::Lifetime(self.conv_lifetime(
1846                        env,
1847                        *lft,
1848                        segment.ident.span,
1849                    )));
1850                }
1851                fhir::GenericArg::Type(ty) => {
1852                    into.push(self.conv_ty_to_generic_arg(env, &param, ty)?);
1853                }
1854                fhir::GenericArg::Const(cst) => {
1855                    into.push(rty::GenericArg::Const(self.conv_const_arg(*cst)));
1856                }
1857                fhir::GenericArg::Infer => {
1858                    into.push(self.conv_generic_arg_hole(env, param, segment.ident.span)?);
1859                }
1860            }
1861        }
1862        self.fill_generic_args_defaults(def_id, into)
1863    }
1864
1865    fn conv_generic_arg_hole(
1866        &mut self,
1867        env: &mut Env,
1868        param: rty::GenericParamDef,
1869        span: Span,
1870    ) -> QueryResult<rty::GenericArg> {
1871        match param.kind {
1872            rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::Base { .. } => {
1873                let ty = fhir::Ty { kind: fhir::TyKind::Infer, span };
1874                Ok(self.conv_ty_to_generic_arg(env, &param, &ty)?)
1875            }
1876            rty::GenericParamDefKind::Const { .. } => {
1877                let cst = fhir::ConstArg { kind: fhir::ConstArgKind::Infer, span };
1878                Ok(rty::GenericArg::Const(self.conv_const_arg(cst)))
1879            }
1880            rty::GenericParamDefKind::Lifetime => {
1881                let re = rty::Region::ReVar(self.next_region_vid());
1882                Ok(rty::GenericArg::Lifetime(re))
1883            }
1884        }
1885    }
1886
1887    fn check_generic_arg_count(
1888        &mut self,
1889        generics: &rty::Generics,
1890        def_id: DefId,
1891        segment: &fhir::PathSegment,
1892    ) -> QueryResult {
1893        let found = segment.args.len();
1894        let mut param_count = generics.own_params.len();
1895
1896        // The self parameter is not provided explicitly in the path so we skip it
1897        if let DefKind::Trait = self.genv().def_kind(def_id) {
1898            param_count -= 1;
1899        }
1900
1901        let min = param_count - generics.own_default_count();
1902        let max = param_count;
1903        if min == max && found != min {
1904            Err(self.emit(errors::GenericArgCountMismatch::new(
1905                self.genv(),
1906                def_id,
1907                segment,
1908                min,
1909            )))?;
1910        }
1911        if found < min {
1912            Err(self.emit(errors::TooFewGenericArgs::new(self.genv(), def_id, segment, min)))?;
1913        }
1914        if found > max {
1915            Err(self.emit(errors::TooManyGenericArgs::new(self.genv(), def_id, segment, min)))?;
1916        }
1917        Ok(())
1918    }
1919
1920    fn fill_generic_args_defaults(
1921        &mut self,
1922        def_id: DefId,
1923        into: &mut Vec<rty::GenericArg>,
1924    ) -> QueryResult {
1925        let generics = self.genv().generics_of(def_id)?;
1926        for param in generics.own_params.iter().skip(into.len()) {
1927            debug_assert!(matches!(
1928                param.kind,
1929                rty::GenericParamDefKind::Type { has_default: true }
1930                    | rty::GenericParamDefKind::Base { has_default: true }
1931            ));
1932            let span = self.tcx().def_span(param.def_id);
1933            // FIXME(nilehmann) we already know whether this is a type or a constructor so we could
1934            // directly check if the constructor returns a subset type.
1935            let ty = self
1936                .genv()
1937                .type_of(param.def_id)?
1938                .instantiate(self.tcx(), into, &[])
1939                .to_ty();
1940            into.push(self.try_to_ty_or_base(param.kind, span, &ty)?.into());
1941        }
1942        Ok(())
1943    }
1944
1945    fn conv_ty_to_generic_arg(
1946        &mut self,
1947        env: &mut Env,
1948        param: &rty::GenericParamDef,
1949        ty: &fhir::Ty,
1950    ) -> QueryResult<rty::GenericArg> {
1951        let rty_ty = self.conv_ty(env, ty)?;
1952        Ok(self.try_to_ty_or_base(param.kind, ty.span, &rty_ty)?.into())
1953    }
1954
1955    fn try_to_ty_or_base(
1956        &mut self,
1957        kind: rty::GenericParamDefKind,
1958        span: Span,
1959        ty: &rty::Ty,
1960    ) -> QueryResult<rty::TyOrBase> {
1961        match kind {
1962            rty::GenericParamDefKind::Type { .. } => Ok(rty::TyOrBase::Ty(ty.clone())),
1963            rty::GenericParamDefKind::Base { .. } => {
1964                Ok(rty::TyOrBase::Base(self.ty_to_subset_ty_ctor(span, ty)?))
1965            }
1966            _ => span_bug!(span, "unexpected param kind `{kind:?}`"),
1967        }
1968    }
1969
1970    fn ty_to_subset_ty_ctor(&mut self, span: Span, ty: &rty::Ty) -> QueryResult<rty::SubsetTyCtor> {
1971        let ctor = if let rty::TyKind::Infer(vid) = ty.kind() {
1972            // do not generate sort holes for dummy self types
1973            let sort_vid =
1974                if vid.as_u32() == 0 { rty::SortVid::from_u32(0) } else { self.next_sort_vid() };
1975            rty::SubsetTyCtor::bind_with_sort(
1976                rty::SubsetTy::trivial(rty::BaseTy::Infer(*vid), rty::Expr::nu()),
1977                rty::Sort::Infer(rty::SortInfer::SortVar(sort_vid)),
1978            )
1979        } else {
1980            ty.shallow_canonicalize()
1981                .as_ty_or_base()
1982                .as_base()
1983                .ok_or_else(|| self.emit(errors::InvalidBaseInstance::new(span)))?
1984        };
1985        Ok(ctor)
1986    }
1987
1988    #[track_caller]
1989    fn emit(&self, err: impl Diagnostic<'genv>) -> ErrorGuaranteed {
1990        self.genv().sess().emit_err(err)
1991    }
1992
1993    fn report_assoc_item_not_found<Tag: AssocItemTag>(
1994        &self,
1995        span: Span,
1996        assoc_tag: Tag,
1997    ) -> Result<!, ErrorGuaranteed> {
1998        Err(self.emit(errors::AssocItemNotFound { span, tag: assoc_tag.descr() }))?
1999    }
2000
2001    fn report_ambiguous_assoc_item<Tag: AssocItemTag>(
2002        &self,
2003        span: Span,
2004        assoc_tag: Tag,
2005        assoc_name: Ident,
2006    ) -> Result<!, ErrorGuaranteed> {
2007        Err(self.emit(errors::AmbiguousAssocItem {
2008            span,
2009            name: assoc_name,
2010            tag: assoc_tag.descr(),
2011        }))?
2012    }
2013
2014    #[track_caller]
2015    fn report_expected_type(
2016        &self,
2017        span: Span,
2018        kind: DefKind,
2019        def_id: DefId,
2020    ) -> Result<!, ErrorGuaranteed> {
2021        Err(self.emit(errors::ExpectedType {
2022            span,
2023            def_descr: self.tcx().def_kind_descr(kind, def_id),
2024            name: self.tcx().def_path_str(def_id),
2025        }))?
2026    }
2027}
2028
2029/// Check generic params for types
2030impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2031    fn check_refinement_generics(&mut self, path: &fhir::Path, def_id: DefId) -> QueryResult {
2032        let generics = self.genv().refinement_generics_of(def_id)?;
2033        if generics.count() != path.refine.len() {
2034            let err = errors::RefineArgMismatch {
2035                span: path.span,
2036                expected: generics.count(),
2037                found: path.refine.len(),
2038                kind: self.tcx().def_descr(def_id),
2039            };
2040            Err(self.emit(err))?;
2041        }
2042        Ok(())
2043    }
2044
2045    fn check_prim_ty_generics(
2046        &mut self,
2047        path: &fhir::Path<'_>,
2048        prim_ty: rustc_hir::PrimTy,
2049    ) -> QueryResult {
2050        if !path.last_segment().args.is_empty() {
2051            let err = errors::GenericsOnPrimTy { span: path.span, name: prim_ty.name_str() };
2052            Err(self.emit(err))?;
2053        }
2054        Ok(())
2055    }
2056
2057    fn check_ty_param_generics(
2058        &mut self,
2059        path: &fhir::Path<'_>,
2060        param_ty: rty::ParamTy,
2061    ) -> QueryResult {
2062        if !path.last_segment().args.is_empty() {
2063            let err = errors::GenericsOnTyParam { span: path.span, name: param_ty.name };
2064            Err(self.emit(err))?;
2065        }
2066        Ok(())
2067    }
2068
2069    fn check_self_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2070        if !path.last_segment().args.is_empty() {
2071            let err = errors::GenericsOnSelfTy { span: path.span };
2072            Err(self.emit(err))?;
2073        }
2074        Ok(())
2075    }
2076
2077    fn check_foreign_ty_generics(&mut self, path: &fhir::Path<'_>) -> QueryResult {
2078        if !path.last_segment().args.is_empty() {
2079            let err = errors::GenericsOnForeignTy { span: path.span };
2080            Err(self.emit(err))?;
2081        }
2082        Ok(())
2083    }
2084}
2085
2086fn prim_ty_to_bty(prim_ty: rustc_hir::PrimTy) -> rty::BaseTy {
2087    match prim_ty {
2088        rustc_hir::PrimTy::Int(int_ty) => rty::BaseTy::Int(int_ty),
2089        rustc_hir::PrimTy::Uint(uint_ty) => rty::BaseTy::Uint(uint_ty),
2090        rustc_hir::PrimTy::Float(float_ty) => rty::BaseTy::Float(float_ty),
2091        rustc_hir::PrimTy::Str => rty::BaseTy::Str,
2092        rustc_hir::PrimTy::Bool => rty::BaseTy::Bool,
2093        rustc_hir::PrimTy::Char => rty::BaseTy::Char,
2094    }
2095}
2096
2097/// Conversion of expressions
2098impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
2099    fn conv_lit(&self, lit: fhir::Lit, fhir_id: FhirId, span: Span) -> QueryResult<rty::Constant> {
2100        match lit {
2101            fhir::Lit::Int(n, kind) => {
2102                match kind {
2103                    Some(fhir::NumLitKind::Int) => Ok(rty::Constant::from(n)),
2104                    Some(fhir::NumLitKind::Real) => Ok(rty::Constant::Real(rty::Real(n))),
2105                    None => {
2106                        let sort = self.results().node_sort(fhir_id);
2107                        if let rty::Sort::BitVec(bvsize) = sort {
2108                            if let rty::BvSize::Fixed(size) = bvsize
2109                                && (n == 0 || n.ilog2() < size)
2110                            {
2111                                Ok(rty::Constant::BitVec(n, size))
2112                            } else {
2113                                Err(self.emit(errors::InvalidBitVectorConstant::new(span, sort)))?
2114                            }
2115                        } else {
2116                            Ok(rty::Constant::from(n))
2117                        }
2118                    }
2119                }
2120            }
2121            fhir::Lit::Bool(b) => Ok(rty::Constant::from(b)),
2122            fhir::Lit::Str(s) => Ok(rty::Constant::from(s)),
2123            fhir::Lit::Char(c) => Ok(rty::Constant::from(c)),
2124        }
2125    }
2126
2127    fn conv_expr(&mut self, env: &mut Env, expr: &fhir::Expr) -> QueryResult<rty::Expr> {
2128        let fhir_id = expr.fhir_id;
2129        let espan = ESpan::new(expr.span);
2130        let expr = match expr.kind {
2131            fhir::ExprKind::Var(QPathExpr::Resolved(path, _)) => self.conv_path_expr(env, path)?,
2132            fhir::ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
2133                let qself = self.conv_ty(env, qself)?;
2134                self.conv_type_relative_const_path(expr, &qself, assoc)?
2135            }
2136            fhir::ExprKind::Literal(lit) => {
2137                rty::Expr::constant(self.conv_lit(lit, fhir_id, expr.span)?).at(espan)
2138            }
2139            fhir::ExprKind::BinaryOp(op, e1, e2) => {
2140                rty::Expr::binary_op(
2141                    self.conv_bin_op(op, expr.fhir_id),
2142                    self.conv_expr(env, e1)?,
2143                    self.conv_expr(env, e2)?,
2144                )
2145                .at(espan)
2146            }
2147            fhir::ExprKind::UnaryOp(op, e) => {
2148                rty::Expr::unary_op(conv_un_op(op), self.conv_expr(env, e)?).at(espan)
2149            }
2150
2151            fhir::ExprKind::PrimApp(op, e1, e2) => {
2152                rty::Expr::prim_val(
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::App(func, args) => {
2160                let sort_args = self.results().node_sort_args(fhir_id);
2161                rty::Expr::app(self.conv_func(env, &func)?, sort_args, self.conv_exprs(env, args)?)
2162                    .at(espan)
2163            }
2164            fhir::ExprKind::Alias(alias, args) => {
2165                let args = args
2166                    .iter()
2167                    .map(|arg| self.conv_expr(env, arg))
2168                    .try_collect()?;
2169                let alias = self.conv_alias_reft(env, expr.fhir_id, &alias)?;
2170                rty::Expr::alias(alias, args).at(espan)
2171            }
2172            fhir::ExprKind::IfThenElse(p, e1, e2) => {
2173                rty::Expr::ite(
2174                    self.conv_expr(env, p)?,
2175                    self.conv_expr(env, e1)?,
2176                    self.conv_expr(env, e2)?,
2177                )
2178                .at(espan)
2179            }
2180            fhir::ExprKind::Dot(base, _) => {
2181                let proj = self.results().field_proj(fhir_id);
2182                rty::Expr::field_proj(self.conv_expr(env, base)?, proj)
2183            }
2184            fhir::ExprKind::Abs(params, body) => {
2185                env.push_layer(Layer::list(self.results(), 0, params));
2186                let pred = self.conv_expr(env, body)?;
2187                let vars = env.pop_layer().into_bound_vars(self.genv())?;
2188                let output = self.results().node_sort(body.fhir_id);
2189                let lam = rty::Lambda::bind_with_vars(pred, vars, output);
2190                rty::Expr::abs(lam)
2191            }
2192            fhir::ExprKind::Block(decls, body) => {
2193                for decl in decls {
2194                    env.push_layer(Layer::list(self.results(), 0, &[decl.param]));
2195                }
2196                let mut body = self.conv_expr(env, body)?;
2197                for decl in decls.iter().rev() {
2198                    let vars = env.pop_layer().into_bound_vars(self.genv())?;
2199                    let init = self.conv_expr(env, &decl.init)?;
2200                    body = rty::Expr::let_(init, rty::Binder::bind_with_vars(body, vars));
2201                }
2202                body
2203            }
2204            fhir::ExprKind::BoundedQuant(kind, param, rng, body) => {
2205                env.push_layer(Layer::list(self.results(), 0, &[param]));
2206                let pred = self.conv_expr(env, body)?;
2207                let vars = env.pop_layer().into_bound_vars(self.genv())?;
2208                let body = rty::Binder::bind_with_vars(pred, vars);
2209                rty::Expr::bounded_quant(kind, rng, body)
2210            }
2211            fhir::ExprKind::Record(flds) => {
2212                let def_id = self.results().record_ctor(expr.fhir_id);
2213                let flds = flds
2214                    .iter()
2215                    .map(|expr| self.conv_expr(env, expr))
2216                    .try_collect()?;
2217                rty::Expr::ctor_struct(def_id, flds)
2218            }
2219            fhir::ExprKind::Constructor(path, exprs, spread) => {
2220                let def_id = if let Some(path) = path {
2221                    match path.res {
2222                        fhir::Res::Def(DefKind::Enum | DefKind::Struct, def_id) => def_id,
2223                        _ => span_bug!(path.span, "unexpected path in constructor"),
2224                    }
2225                } else {
2226                    self.results().record_ctor(expr.fhir_id)
2227                };
2228                let assns = self.conv_constructor_exprs(def_id, env, exprs, &spread)?;
2229                rty::Expr::ctor_struct(def_id, assns)
2230            }
2231            fhir::ExprKind::Err(err) => Err(QueryErr::Emitted(err))?,
2232        };
2233        Ok(self.add_coercions(expr, fhir_id))
2234    }
2235
2236    fn conv_loc(&mut self, env: &mut Env, loc: fhir::PathExpr) -> QueryResult<rty::Path> {
2237        Ok(self
2238            .conv_path_expr(env, loc)?
2239            .to_path()
2240            .unwrap_or_else(|| span_bug!(loc.span, "expected path, found `{loc:?}`")))
2241    }
2242
2243    fn conv_path_expr(&mut self, env: &mut Env, path: fhir::PathExpr) -> QueryResult<rty::Expr> {
2244        let genv = self.genv();
2245        let tcx = self.genv().tcx();
2246        let espan = ESpan::new(path.span);
2247        let (expr, sort) = match path.res {
2248            fhir::Res::Param(_, id) => (env.lookup(&path).to_expr(), self.results().param_sort(id)),
2249            fhir::Res::Def(DefKind::Const, def_id) => {
2250                self.hyperlink(path.span, tcx.def_ident_span(def_id));
2251                let (expr, sort) = self.conv_const(path.span, def_id)?;
2252                (expr.at(espan), sort)
2253            }
2254            fhir::Res::Def(DefKind::Ctor(..), ctor_id) => {
2255                let Some(sort) = genv.sort_of_def_id(ctor_id).emit(&genv)? else {
2256                    span_bug!(path.span, "unexpected variant {ctor_id:?}")
2257                };
2258
2259                let variant_id = self.tcx().parent(ctor_id);
2260                let enum_id = self.tcx().parent(variant_id);
2261                self.hyperlink(path.span, tcx.def_ident_span(variant_id));
2262                let idx = variant_idx(self.tcx(), variant_id);
2263                (rty::Expr::ctor_enum(enum_id, idx), sort)
2264            }
2265            fhir::Res::Def(DefKind::ConstParam, def_id) => {
2266                self.hyperlink(path.span, tcx.def_ident_span(def_id));
2267                // FIXME(nilehmann) generalize this to other sorts
2268                let sort = rty::Sort::Int;
2269                (rty::Expr::const_generic(def_id_to_param_const(genv, def_id)).at(espan), sort)
2270            }
2271            _ => {
2272                Err(self.emit(errors::InvalidRes { span: path.span, res_descr: path.res.descr() }))?
2273            }
2274        };
2275        self.0.insert_node_sort(path.fhir_id, sort);
2276        Ok(expr)
2277    }
2278
2279    fn conv_const(&self, span: Span, def_id: DefId) -> QueryResult<(rty::Expr, rty::Sort)> {
2280        let genv = self.genv();
2281        let Some(sort) = genv.sort_of_def_id(def_id).emit(&genv)? else {
2282            span_bug!(span, "unsupported const: `{def_id:?}`")
2283        };
2284        let info = genv.constant_info(def_id).emit(&genv)?;
2285        // non-integral constant
2286        if sort != rty::Sort::Int && matches!(info, rty::ConstantInfo::Uninterpreted) {
2287            Err(self.emit(errors::ConstantAnnotationNeeded::new(span)))?;
2288        }
2289        Ok((rty::Expr::const_def_id(def_id).at(ESpan::new(span)), sort))
2290    }
2291
2292    fn conv_constructor_exprs(
2293        &mut self,
2294        struct_def_id: DefId,
2295        env: &mut Env,
2296        exprs: &[fhir::FieldExpr],
2297        spread: &Option<&fhir::Spread>,
2298    ) -> QueryResult<List<rty::Expr>> {
2299        let spread = spread
2300            .map(|spread| self.conv_expr(env, &spread.expr))
2301            .transpose()?;
2302        let mut field_exprs_by_name: FxHashMap<Symbol, rty::Expr> = exprs
2303            .iter()
2304            .map(|field_expr| -> QueryResult<_> {
2305                Ok((field_expr.ident.name, self.conv_expr(env, &field_expr.expr)?))
2306            })
2307            .try_collect()?;
2308
2309        if !P::HAS_ELABORATED_INFORMATION {
2310            return Ok(List::default());
2311        };
2312
2313        let adt_def = self.genv().adt_sort_def_of(struct_def_id)?;
2314        let struct_variant = adt_def.struct_variant();
2315        let mut assns = Vec::new();
2316        for (idx, field_name) in struct_variant.field_names().iter().enumerate() {
2317            if let Some(expr) = field_exprs_by_name.remove(field_name) {
2318                assns.push(expr);
2319            } else if let Some(spread) = &spread {
2320                let proj = rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 };
2321                assns.push(rty::Expr::field_proj(spread, proj));
2322            }
2323        }
2324        Ok(List::from_vec(assns))
2325    }
2326
2327    fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult<List<rty::Expr>> {
2328        exprs.iter().map(|e| self.conv_expr(env, e)).collect()
2329    }
2330
2331    fn conv_bin_op(&self, op: fhir::BinOp, fhir_id: FhirId) -> rty::BinOp {
2332        match op {
2333            fhir::BinOp::Iff => rty::BinOp::Iff,
2334            fhir::BinOp::Imp => rty::BinOp::Imp,
2335            fhir::BinOp::Or => rty::BinOp::Or,
2336            fhir::BinOp::And => rty::BinOp::And,
2337            fhir::BinOp::Eq => rty::BinOp::Eq,
2338            fhir::BinOp::Ne => rty::BinOp::Ne,
2339            fhir::BinOp::Gt => rty::BinOp::Gt(self.results().bin_op_sort(fhir_id)),
2340            fhir::BinOp::Ge => rty::BinOp::Ge(self.results().bin_op_sort(fhir_id)),
2341            fhir::BinOp::Lt => rty::BinOp::Lt(self.results().bin_op_sort(fhir_id)),
2342            fhir::BinOp::Le => rty::BinOp::Le(self.results().bin_op_sort(fhir_id)),
2343            fhir::BinOp::Add => rty::BinOp::Add(self.results().bin_op_sort(fhir_id)),
2344            fhir::BinOp::Sub => rty::BinOp::Sub(self.results().bin_op_sort(fhir_id)),
2345            fhir::BinOp::Mul => rty::BinOp::Mul(self.results().bin_op_sort(fhir_id)),
2346            fhir::BinOp::Mod => rty::BinOp::Mod(self.results().bin_op_sort(fhir_id)),
2347            fhir::BinOp::Div => rty::BinOp::Div(self.results().bin_op_sort(fhir_id)),
2348            fhir::BinOp::BitAnd => rty::BinOp::BitAnd,
2349            fhir::BinOp::BitOr => rty::BinOp::BitOr,
2350            fhir::BinOp::BitXor => rty::BinOp::BitXor,
2351            fhir::BinOp::BitShl => rty::BinOp::BitShl,
2352            fhir::BinOp::BitShr => rty::BinOp::BitShr,
2353        }
2354    }
2355
2356    fn add_coercions(&self, mut expr: rty::Expr, fhir_id: FhirId) -> rty::Expr {
2357        let span = expr.span();
2358        for coercion in self.results().coercions_for(fhir_id) {
2359            expr = match *coercion {
2360                rty::Coercion::Inject(def_id) => {
2361                    rty::Expr::ctor_struct(def_id, List::singleton(expr)).at_opt(span)
2362                }
2363                rty::Coercion::Project(def_id) => {
2364                    rty::Expr::field_proj(expr, rty::FieldProj::Adt { def_id, field: 0 })
2365                        .at_opt(span)
2366                }
2367            };
2368        }
2369        expr
2370    }
2371
2372    fn hyperlink(&self, span: Span, dst_span: Option<Span>) {
2373        if P::HAS_ELABORATED_INFORMATION
2374            && let Some(dst_span) = dst_span
2375        {
2376            dbg::hyperlink!(self.genv().tcx(), span, dst_span);
2377        }
2378    }
2379
2380    fn conv_func(&mut self, env: &Env, func: &fhir::PathExpr) -> QueryResult<rty::Expr> {
2381        let genv = self.genv();
2382        let span = func.span;
2383        let (expr, sort) = match func.res {
2384            fhir::Res::Param(_, id) => {
2385                let sort = self.results().param_sort(id);
2386                (env.lookup(func).to_expr(), sort)
2387            }
2388            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Def(did)) => {
2389                self.hyperlink(span, Some(genv.func_span(did)));
2390                let sort = rty::Sort::Func(genv.func_sort(did));
2391                (rty::Expr::global_func(rty::SpecFuncKind::Def(did)), sort)
2392            }
2393            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Uif(did)) => {
2394                self.hyperlink(span, Some(genv.func_span(did)));
2395                let sort = rty::Sort::Func(genv.func_sort(did));
2396                (rty::Expr::global_func(rty::SpecFuncKind::Uif(did)), sort)
2397            }
2398            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Thy(itf)) => {
2399                let sort = THEORY_FUNCS.get(&itf).unwrap().sort.clone();
2400                (rty::Expr::global_func(rty::SpecFuncKind::Thy(itf)), rty::Sort::Func(sort))
2401            }
2402            fhir::Res::GlobalFunc(fhir::SpecFuncKind::Cast) => {
2403                let fsort = rty::PolyFuncSort::new(
2404                    List::from_arr([rty::SortParamKind::Sort, rty::SortParamKind::Sort]),
2405                    rty::FuncSort::new(
2406                        vec![rty::Sort::Var(rty::ParamSort::from(0_usize))],
2407                        rty::Sort::Var(rty::ParamSort::from(1_usize)),
2408                    ),
2409                );
2410                (rty::Expr::internal_func(InternalFuncKind::Cast), rty::Sort::Func(fsort))
2411            }
2412            _ => {
2413                return Err(
2414                    self.emit(errors::InvalidRes { span: func.span, res_descr: func.res.descr() })
2415                )?;
2416            }
2417        };
2418        self.0.insert_node_sort(func.fhir_id, sort);
2419        Ok(self.add_coercions(expr, func.fhir_id))
2420    }
2421
2422    fn conv_alias_reft(
2423        &mut self,
2424        env: &mut Env,
2425        fhir_id: FhirId,
2426        alias: &fhir::AliasReft,
2427    ) -> QueryResult<rty::AliasReft> {
2428        let alias_reft = match alias {
2429            fhir::AliasReft::Qualified { qself, trait_, name } => {
2430                let fhir::Res::Def(DefKind::Trait, trait_id) = trait_.res else {
2431                    span_bug!(trait_.span, "expected trait")
2432                };
2433                let trait_segment = trait_.last_segment();
2434
2435                let generics = self.genv().generics_of(trait_id)?;
2436                let self_ty =
2437                    self.conv_ty_to_generic_arg(env, &generics.param_at(0, self.genv())?, qself)?;
2438                let mut generic_args = vec![self_ty];
2439                self.conv_generic_args_into(env, trait_id, trait_segment, &mut generic_args)?;
2440
2441                let Some(assoc_reft) = self.genv().assoc_refinements_of(trait_id)?.find(name.name)
2442                else {
2443                    return Err(self.emit(errors::InvalidAssocReft::new(
2444                        trait_.span,
2445                        name.name,
2446                        format!("{:?}", trait_),
2447                    )))?;
2448                };
2449
2450                let assoc_id = assoc_reft.def_id;
2451
2452                dbg::hyperlink!(self.genv().tcx(), name.span, assoc_reft.span);
2453
2454                rty::AliasReft { assoc_id, args: List::from_vec(generic_args) }
2455            }
2456            fhir::AliasReft::TypeRelative { qself, name } => {
2457                let qself_res =
2458                    if let Some(path) = qself.as_path() { path.res } else { fhir::Res::Err };
2459                let (assoc_reft, trait_ref) =
2460                    self.conv_type_relative_path(AssocReftTag, qself.span, qself_res, *name)?;
2461                rty::AliasReft { assoc_id: assoc_reft.def_id, args: trait_ref.args }
2462            }
2463        };
2464        let fsort = alias_reft.fsort(self.genv())?;
2465        self.0.insert_alias_reft_sort(fhir_id, fsort);
2466        Ok(alias_reft)
2467    }
2468
2469    pub(crate) fn conv_invariants(
2470        &mut self,
2471        adt_id: MaybeExternId,
2472        params: &[fhir::RefineParam],
2473        invariants: &[fhir::Expr],
2474    ) -> QueryResult<Vec<rty::Invariant>> {
2475        let mut env = Env::new(&[]);
2476        env.push_layer(Layer::coalesce(self.results(), adt_id.resolved_id(), params));
2477        invariants
2478            .iter()
2479            .map(|invariant| self.conv_invariant(&mut env, invariant))
2480            .collect()
2481    }
2482
2483    fn conv_invariant(
2484        &mut self,
2485        env: &mut Env,
2486        invariant: &fhir::Expr,
2487    ) -> QueryResult<rty::Invariant> {
2488        Ok(rty::Invariant::new(rty::Binder::bind_with_vars(
2489            self.conv_expr(env, invariant)?,
2490            env.top_layer().to_bound_vars(self.genv())?,
2491        )))
2492    }
2493}
2494
2495impl Env {
2496    fn new(early_params: &[fhir::RefineParam]) -> Self {
2497        let early_params = early_params
2498            .iter()
2499            .map(|param| (param.id, param.name))
2500            .collect();
2501        Self { layers: vec![], early_params }
2502    }
2503
2504    pub(crate) fn empty() -> Self {
2505        Self { layers: vec![], early_params: Default::default() }
2506    }
2507
2508    fn depth(&self) -> usize {
2509        self.layers.len()
2510    }
2511
2512    fn push_layer(&mut self, layer: Layer) {
2513        self.layers.push(layer);
2514    }
2515
2516    fn pop_layer(&mut self) -> Layer {
2517        self.layers.pop().expect("bottom of layer stack")
2518    }
2519
2520    fn top_layer(&self) -> &Layer {
2521        self.layers.last().expect("bottom of layer stack")
2522    }
2523
2524    fn lookup(&self, var: &fhir::PathExpr) -> LookupResult<'_> {
2525        let (_, id) = var.res.expect_param();
2526        for (i, layer) in self.layers.iter().rev().enumerate() {
2527            if let Some((idx, entry)) = layer.get(id) {
2528                let debruijn = DebruijnIndex::from_usize(i);
2529                let kind = LookupResultKind::Bound {
2530                    debruijn,
2531                    entry,
2532                    index: idx as u32,
2533                    kind: layer.kind,
2534                };
2535                return LookupResult { var_span: var.span, kind };
2536            }
2537        }
2538        if let Some((idx, _, name)) = self.early_params.get_full(&id) {
2539            LookupResult {
2540                var_span: var.span,
2541                kind: LookupResultKind::EarlyParam { index: idx as u32, name: *name },
2542            }
2543        } else {
2544            span_bug!(var.span, "no entry found for key: `{:?}`", id);
2545        }
2546    }
2547
2548    fn to_early_param_args(&self) -> List<rty::Expr> {
2549        self.early_params
2550            .iter()
2551            .enumerate()
2552            .map(|(idx, (_, name))| rty::Expr::early_param(idx as u32, *name))
2553            .collect()
2554    }
2555}
2556
2557impl Layer {
2558    fn new<R: WfckResultsProvider>(
2559        results: &R,
2560        params: &[fhir::RefineParam],
2561        kind: LayerKind,
2562    ) -> Self {
2563        let map = params
2564            .iter()
2565            .map(|param| {
2566                let sort = results.param_sort(param.id);
2567                let infer_mode = rty::InferMode::from_param_kind(param.kind);
2568                let entry = ParamEntry::new(sort, infer_mode, param.name);
2569                (param.id, entry)
2570            })
2571            .collect();
2572        Self { map, kind }
2573    }
2574
2575    fn list<R: WfckResultsProvider>(
2576        results: &R,
2577        bound_regions: u32,
2578        params: &[fhir::RefineParam],
2579    ) -> Self {
2580        Self::new(results, params, LayerKind::List { bound_regions })
2581    }
2582
2583    fn coalesce<R: WfckResultsProvider>(
2584        results: &R,
2585        def_id: DefId,
2586        params: &[fhir::RefineParam],
2587    ) -> Self {
2588        Self::new(results, params, LayerKind::Coalesce(def_id))
2589    }
2590
2591    fn get(&self, name: impl Borrow<fhir::ParamId>) -> Option<(usize, &ParamEntry)> {
2592        let (idx, _, entry) = self.map.get_full(name.borrow())?;
2593        Some((idx, entry))
2594    }
2595
2596    fn into_bound_vars(self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2597        match self.kind {
2598            LayerKind::List { .. } => {
2599                Ok(self
2600                    .into_iter()
2601                    .map(|entry| {
2602                        let kind = rty::BoundReftKind::Named(entry.name);
2603                        rty::BoundVariableKind::Refine(entry.sort, entry.mode, kind)
2604                    })
2605                    .collect())
2606            }
2607            LayerKind::Coalesce(def_id) => {
2608                let sort_def = genv.adt_sort_def_of(def_id)?;
2609                let args = sort_def.identity_args();
2610                let ctor = rty::SortCtor::Adt(sort_def);
2611                Ok(List::singleton(rty::BoundVariableKind::Refine(
2612                    rty::Sort::App(ctor, args),
2613                    rty::InferMode::EVar,
2614                    rty::BoundReftKind::Anon,
2615                )))
2616            }
2617        }
2618    }
2619
2620    fn to_bound_vars(&self, genv: GlobalEnv) -> QueryResult<List<rty::BoundVariableKind>> {
2621        self.clone().into_bound_vars(genv)
2622    }
2623
2624    fn into_iter(self) -> impl Iterator<Item = ParamEntry> {
2625        self.map.into_values()
2626    }
2627}
2628
2629impl ParamEntry {
2630    fn new(sort: rty::Sort, mode: fhir::InferMode, name: Symbol) -> Self {
2631        ParamEntry { name, sort, mode }
2632    }
2633}
2634
2635impl LookupResult<'_> {
2636    fn to_expr(&self) -> rty::Expr {
2637        let espan = ESpan::new(self.var_span);
2638        match &self.kind {
2639            LookupResultKind::Bound { debruijn, entry: ParamEntry { name, .. }, kind, index } => {
2640                match *kind {
2641                    LayerKind::List { bound_regions } => {
2642                        rty::Expr::bvar(
2643                            *debruijn,
2644                            BoundVar::from_u32(bound_regions + *index),
2645                            rty::BoundReftKind::Named(*name),
2646                        )
2647                        .at(espan)
2648                    }
2649                    LayerKind::Coalesce(def_id) => {
2650                        let var =
2651                            rty::Expr::bvar(*debruijn, BoundVar::ZERO, rty::BoundReftKind::Anon)
2652                                .at(espan);
2653                        rty::Expr::field_proj(var, rty::FieldProj::Adt { def_id, field: *index })
2654                            .at(espan)
2655                    }
2656                }
2657            }
2658            &LookupResultKind::EarlyParam { index, name, .. } => {
2659                rty::Expr::early_param(index, name).at(espan)
2660            }
2661        }
2662    }
2663}
2664
2665pub fn conv_func_decl(genv: GlobalEnv, func: &fhir::SpecFunc) -> QueryResult<rty::PolyFuncSort> {
2666    let wfckresults = WfckResults::new(FluxOwnerId::Flux(func.def_id));
2667    let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
2668    let inputs_and_output = func
2669        .args
2670        .iter()
2671        .map(|p| &p.sort)
2672        .chain(iter::once(&func.sort))
2673        .map(|sort| cx.conv_sort(sort))
2674        .try_collect()?;
2675    let params = iter::repeat_n(rty::SortParamKind::Sort, func.params).collect();
2676    Ok(rty::PolyFuncSort::new(params, rty::FuncSort { inputs_and_output }))
2677}
2678
2679fn conv_un_op(op: fhir::UnOp) -> rty::UnOp {
2680    match op {
2681        fhir::UnOp::Not => rty::UnOp::Not,
2682        fhir::UnOp::Neg => rty::UnOp::Neg,
2683    }
2684}
2685
2686fn def_id_to_param_ty(genv: GlobalEnv, def_id: DefId) -> rty::ParamTy {
2687    rty::ParamTy { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2688}
2689
2690fn def_id_to_param_const(genv: GlobalEnv, def_id: DefId) -> rty::ParamConst {
2691    rty::ParamConst { index: genv.def_id_to_param_index(def_id), name: ty_param_name(genv, def_id) }
2692}
2693
2694fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
2695    let def_kind = genv.def_kind(def_id);
2696    match def_kind {
2697        DefKind::Trait | DefKind::TraitAlias => def_id,
2698        DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2699            genv.tcx().parent(def_id)
2700        }
2701        _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
2702    }
2703}
2704
2705fn ty_param_name(genv: GlobalEnv, def_id: DefId) -> Symbol {
2706    let def_kind = genv.tcx().def_kind(def_id);
2707    match def_kind {
2708        DefKind::Trait | DefKind::TraitAlias => kw::SelfUpper,
2709        DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
2710            genv.tcx().item_name(def_id)
2711        }
2712        _ => bug!("ty_param_name: {:?} is a {:?} not a type parameter", def_id, def_kind),
2713    }
2714}
2715
2716/// This trait is used to define functions generically over both _associated refinements_
2717/// and _associated items_ (types, consts, and functions).
2718trait AssocItemTag: Copy {
2719    type AssocItem<'tcx>;
2720
2721    fn descr(self) -> &'static str;
2722
2723    fn trait_defines_item_named<'tcx>(
2724        self,
2725        genv: GlobalEnv<'_, 'tcx>,
2726        trait_def_id: DefId,
2727        assoc_name: Ident,
2728    ) -> QueryResult<Option<Self::AssocItem<'tcx>>>;
2729
2730    fn transitive_bounds_that_define_assoc_item<'tcx>(
2731        self,
2732        genv: GlobalEnv<'_, 'tcx>,
2733        trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2734        assoc_name: Ident,
2735    ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>>;
2736}
2737
2738impl AssocItemTag for AssocTag {
2739    type AssocItem<'tcx> = &'tcx AssocItem;
2740
2741    fn descr(self) -> &'static str {
2742        match self {
2743            AssocTag::Const => "constant",
2744            AssocTag::Fn => "function",
2745            AssocTag::Type => "type",
2746        }
2747    }
2748
2749    fn trait_defines_item_named<'tcx>(
2750        self,
2751        genv: GlobalEnv<'_, 'tcx>,
2752        trait_def_id: DefId,
2753        assoc_name: Ident,
2754    ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2755        Ok(genv
2756            .tcx()
2757            .associated_items(trait_def_id)
2758            .find_by_ident_and_kind(genv.tcx(), assoc_name, self, trait_def_id))
2759    }
2760
2761    fn transitive_bounds_that_define_assoc_item<'tcx>(
2762        self,
2763        genv: GlobalEnv<'_, 'tcx>,
2764        trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2765        assoc_name: Ident,
2766    ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2767        traits::transitive_bounds_that_define_assoc_item(genv.tcx(), trait_refs, assoc_name)
2768    }
2769}
2770
2771#[derive(Copy, Clone)]
2772struct AssocReftTag;
2773
2774impl AssocItemTag for AssocReftTag {
2775    type AssocItem<'tcx> = AssocReft;
2776
2777    fn descr(self) -> &'static str {
2778        "refinement"
2779    }
2780
2781    fn trait_defines_item_named<'tcx>(
2782        self,
2783        genv: GlobalEnv<'_, 'tcx>,
2784        trait_def_id: DefId,
2785        assoc_name: Ident,
2786    ) -> QueryResult<Option<Self::AssocItem<'tcx>>> {
2787        Ok(genv
2788            .assoc_refinements_of(trait_def_id)?
2789            .find(assoc_name.name))
2790    }
2791
2792    fn transitive_bounds_that_define_assoc_item<'tcx>(
2793        self,
2794        genv: GlobalEnv<'_, 'tcx>,
2795        trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2796        _assoc_name: Ident,
2797    ) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2798        transitive_bounds(genv.tcx(), trait_refs)
2799    }
2800}
2801
2802/// This is like [`TyCtxt::type_param_predicates`] but computes all bounds not just the ones defining
2803/// an associated item. We *must* compute this ourselves to resolve type-relative associated refinements,
2804/// but we also use it to resolve type-relative type paths.
2805///
2806/// NOTE: [`TyCtxt::type_param_predicates`] is defined specifically to avoid cycles which is not a
2807/// problem for us so we can use it instead of [`TyCtxt::type_param_predicates`].
2808fn type_param_predicates<'tcx>(
2809    tcx: TyCtxt<'tcx>,
2810    param_id: DefId,
2811) -> impl Iterator<Item = ty::PolyTraitPredicate<'tcx>> {
2812    let parent = if tcx.def_kind(param_id) == DefKind::Trait {
2813        // If the param_id is a trait then this is the `Self` parameter and the parent is the trait itself
2814        param_id
2815    } else {
2816        tcx.parent(param_id)
2817    };
2818    let param_index = tcx
2819        .generics_of(parent)
2820        .param_def_id_to_index(tcx, param_id)
2821        .unwrap();
2822    let predicates = tcx.predicates_of(parent).instantiate_identity(tcx);
2823    predicates.into_iter().filter_map(move |(clause, _)| {
2824        clause
2825            .as_trait_clause()
2826            .filter(|trait_pred| trait_pred.self_ty().skip_binder().is_param(param_index))
2827    })
2828}
2829
2830/// This is like [`traits::transitive_bounds_that_define_assoc_item`] but computes all bounds not just
2831/// the ones defining an associated item. We *must* compute this ourselves to resolve type-relative
2832/// associated refinements.
2833///
2834/// NOTE: [`traits::transitive_bounds_that_define_assoc_item`] is defined specifically to avoid cycles
2835/// which is not a problem for us. So instead of using `explicit_supertraits_containing_assoc_item` we
2836/// can simply use `explicit_super_predicates_of`.
2837fn transitive_bounds<'tcx>(
2838    tcx: TyCtxt<'tcx>,
2839    trait_refs: impl Iterator<Item = ty::PolyTraitRef<'tcx>>,
2840) -> impl Iterator<Item = ty::PolyTraitRef<'tcx>> {
2841    let mut seen = FxHashSet::default();
2842    let mut stack: Vec<_> = trait_refs.collect();
2843
2844    std::iter::from_fn(move || {
2845        while let Some(trait_ref) = stack.pop() {
2846            if !seen.insert(tcx.anonymize_bound_vars(trait_ref)) {
2847                continue;
2848            }
2849
2850            stack.extend(
2851                tcx.explicit_super_predicates_of(trait_ref.def_id())
2852                    .iter_identity_copied()
2853                    .map(|(clause, _)| clause.instantiate_supertrait(tcx, trait_ref))
2854                    .filter_map(|clause| clause.as_trait_clause())
2855                    .filter(|clause| clause.polarity() == ty::PredicatePolarity::Positive)
2856                    .map(|clause| clause.map_bound(|clause| clause.trait_ref)),
2857            );
2858
2859            return Some(trait_ref);
2860        }
2861
2862        None
2863    })
2864}
2865
2866mod errors {
2867    use flux_errors::E0999;
2868    use flux_macros::Diagnostic;
2869    use flux_middle::{fhir, global_env::GlobalEnv, rty::Sort};
2870    use rustc_hir::def_id::DefId;
2871    use rustc_span::{Span, Symbol, symbol::Ident};
2872
2873    #[derive(Diagnostic)]
2874    #[diag(fhir_analysis_assoc_item_not_found, code = E0999)]
2875    #[note]
2876    pub(super) struct AssocItemNotFound {
2877        #[primary_span]
2878        #[label]
2879        pub span: Span,
2880        pub tag: &'static str,
2881    }
2882
2883    #[derive(Diagnostic)]
2884    #[diag(fhir_analysis_ambiguous_assoc_item, code = E0999)]
2885    pub(super) struct AmbiguousAssocItem {
2886        #[primary_span]
2887        pub span: Span,
2888        pub name: Ident,
2889        pub tag: &'static str,
2890    }
2891
2892    #[derive(Diagnostic)]
2893    #[diag(fhir_analysis_invalid_base_instance, code = E0999)]
2894    pub(super) struct InvalidBaseInstance {
2895        #[primary_span]
2896        span: Span,
2897    }
2898
2899    impl InvalidBaseInstance {
2900        pub(super) fn new(span: Span) -> Self {
2901            Self { span }
2902        }
2903    }
2904
2905    #[derive(Diagnostic)]
2906    #[diag(fhir_analysis_generic_argument_count_mismatch, code = E0999)]
2907    pub(super) struct GenericArgCountMismatch {
2908        #[primary_span]
2909        #[label]
2910        span: Span,
2911        found: usize,
2912        expected: usize,
2913        def_descr: &'static str,
2914    }
2915
2916    impl GenericArgCountMismatch {
2917        pub(super) fn new(
2918            genv: GlobalEnv,
2919            def_id: DefId,
2920            segment: &fhir::PathSegment,
2921            expected: usize,
2922        ) -> Self {
2923            GenericArgCountMismatch {
2924                span: segment.ident.span,
2925                found: segment.args.len(),
2926                expected,
2927                def_descr: genv.tcx().def_descr(def_id),
2928            }
2929        }
2930    }
2931
2932    #[derive(Diagnostic)]
2933    #[diag(fhir_analysis_too_few_generic_args, code = E0999)]
2934    pub(super) struct TooFewGenericArgs {
2935        #[primary_span]
2936        #[label]
2937        span: Span,
2938        found: usize,
2939        min: usize,
2940        def_descr: &'static str,
2941    }
2942
2943    impl TooFewGenericArgs {
2944        pub(super) fn new(
2945            genv: GlobalEnv,
2946            def_id: DefId,
2947            segment: &fhir::PathSegment,
2948            min: usize,
2949        ) -> Self {
2950            Self {
2951                span: segment.ident.span,
2952                found: segment.args.len(),
2953                min,
2954                def_descr: genv.tcx().def_descr(def_id),
2955            }
2956        }
2957    }
2958
2959    #[derive(Diagnostic)]
2960    #[diag(fhir_analysis_too_many_generic_args, code = E0999)]
2961    pub(super) struct TooManyGenericArgs {
2962        #[primary_span]
2963        #[label]
2964        span: Span,
2965        found: usize,
2966        max: usize,
2967        def_descr: &'static str,
2968    }
2969
2970    impl TooManyGenericArgs {
2971        pub(super) fn new(
2972            genv: GlobalEnv,
2973            def_id: DefId,
2974            segment: &fhir::PathSegment,
2975            max: usize,
2976        ) -> Self {
2977            Self {
2978                span: segment.ident.span,
2979                found: segment.args.len(),
2980                max,
2981                def_descr: genv.tcx().def_descr(def_id),
2982            }
2983        }
2984    }
2985
2986    #[derive(Diagnostic)]
2987    #[diag(fhir_analysis_refined_unrefinable_type, code = E0999)]
2988    pub(super) struct RefinedUnrefinableType {
2989        #[primary_span]
2990        span: Span,
2991    }
2992
2993    impl RefinedUnrefinableType {
2994        pub(super) fn new(span: Span) -> Self {
2995            Self { span }
2996        }
2997    }
2998
2999    #[derive(Diagnostic)]
3000    #[diag(fhir_analysis_generics_on_primitive_sort, code = E0999)]
3001    pub(super) struct GenericsOnPrimitiveSort {
3002        #[primary_span]
3003        #[label]
3004        span: Span,
3005        name: &'static str,
3006        found: usize,
3007        expected: usize,
3008    }
3009
3010    impl GenericsOnPrimitiveSort {
3011        pub(super) fn new(span: Span, name: &'static str, found: usize, expected: usize) -> Self {
3012            Self { span, found, expected, name }
3013        }
3014    }
3015
3016    #[derive(Diagnostic)]
3017    #[diag(fhir_analysis_incorrect_generics_on_sort, code = E0999)]
3018    pub(super) struct IncorrectGenericsOnSort {
3019        #[primary_span]
3020        #[label]
3021        span: Span,
3022        found: usize,
3023        expected: usize,
3024        def_descr: &'static str,
3025    }
3026
3027    impl IncorrectGenericsOnSort {
3028        pub(super) fn new(
3029            genv: GlobalEnv,
3030            def_id: DefId,
3031            span: Span,
3032            found: usize,
3033            expected: usize,
3034        ) -> Self {
3035            Self { span, found, expected, def_descr: genv.tcx().def_descr(def_id) }
3036        }
3037    }
3038
3039    #[derive(Diagnostic)]
3040    #[diag(fhir_analysis_generics_on_sort_ty_param, code = E0999)]
3041    pub(super) struct GenericsOnSortTyParam {
3042        #[primary_span]
3043        #[label]
3044        span: Span,
3045        found: usize,
3046    }
3047
3048    impl GenericsOnSortTyParam {
3049        pub(super) fn new(span: Span, found: usize) -> Self {
3050            Self { span, found }
3051        }
3052    }
3053
3054    #[derive(Diagnostic)]
3055    #[diag(fhir_analysis_generics_on_self_alias, code = E0999)]
3056    pub(super) struct GenericsOnSelf {
3057        #[primary_span]
3058        #[label]
3059        span: Span,
3060        found: usize,
3061    }
3062
3063    impl GenericsOnSelf {
3064        pub(super) fn new(span: Span, found: usize) -> Self {
3065            Self { span, found }
3066        }
3067    }
3068
3069    #[derive(Diagnostic)]
3070    #[diag(fhir_analysis_fields_on_reflected_enum_variant, code = E0999)]
3071    pub(super) struct FieldsOnReflectedEnumVariant {
3072        #[primary_span]
3073        #[label]
3074        span: Span,
3075    }
3076
3077    impl FieldsOnReflectedEnumVariant {
3078        pub(super) fn new(span: Span) -> Self {
3079            Self { span }
3080        }
3081    }
3082
3083    #[derive(Diagnostic)]
3084    #[diag(fhir_analysis_generics_on_opaque_sort, code = E0999)]
3085    pub(super) struct GenericsOnUserDefinedOpaqueSort {
3086        #[primary_span]
3087        #[label]
3088        span: Span,
3089        found: usize,
3090    }
3091
3092    impl GenericsOnUserDefinedOpaqueSort {
3093        pub(super) fn new(span: Span, found: usize) -> Self {
3094            Self { span, found }
3095        }
3096    }
3097
3098    #[derive(Diagnostic)]
3099    #[diag(fhir_analysis_generics_on_prim_ty, code = E0999)]
3100    pub(super) struct GenericsOnPrimTy {
3101        #[primary_span]
3102        pub span: Span,
3103        pub name: &'static str,
3104    }
3105
3106    #[derive(Diagnostic)]
3107    #[diag(fhir_analysis_generics_on_ty_param, code = E0999)]
3108    pub(super) struct GenericsOnTyParam {
3109        #[primary_span]
3110        pub span: Span,
3111        pub name: Symbol,
3112    }
3113
3114    #[derive(Diagnostic)]
3115    #[diag(fhir_analysis_generics_on_self_ty, code = E0999)]
3116    pub(super) struct GenericsOnSelfTy {
3117        #[primary_span]
3118        pub span: Span,
3119    }
3120
3121    #[derive(Diagnostic)]
3122    #[diag(fhir_analysis_generics_on_foreign_ty, code = E0999)]
3123    pub(super) struct GenericsOnForeignTy {
3124        #[primary_span]
3125        pub span: Span,
3126    }
3127
3128    #[derive(Diagnostic)]
3129    #[diag(fhir_analysis_invalid_bitvector_constant, code = E0999)]
3130    pub struct InvalidBitVectorConstant {
3131        #[primary_span]
3132        #[label]
3133        span: Span,
3134        sort: Sort,
3135    }
3136
3137    impl InvalidBitVectorConstant {
3138        pub(crate) fn new(span: Span, sort: Sort) -> Self {
3139            Self { span, sort }
3140        }
3141    }
3142
3143    #[derive(Diagnostic)]
3144    #[diag(fhir_analysis_invalid_assoc_reft, code = E0999)]
3145    pub struct InvalidAssocReft {
3146        #[primary_span]
3147        span: Span,
3148        trait_: String,
3149        name: Symbol,
3150    }
3151
3152    impl InvalidAssocReft {
3153        pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
3154            Self { span, trait_, name }
3155        }
3156    }
3157
3158    #[derive(Diagnostic)]
3159    #[diag(fhir_analysis_refine_arg_mismatch, code = E0999)]
3160    pub(super) struct RefineArgMismatch {
3161        #[primary_span]
3162        #[label]
3163        pub span: Span,
3164        pub expected: usize,
3165        pub found: usize,
3166        pub kind: &'static str,
3167    }
3168
3169    #[derive(Diagnostic)]
3170    #[diag(fhir_analysis_expected_type, code = E0999)]
3171    pub(super) struct ExpectedType {
3172        #[primary_span]
3173        pub span: Span,
3174        pub def_descr: &'static str,
3175        pub name: String,
3176    }
3177
3178    #[derive(Diagnostic)]
3179    #[diag(fhir_analysis_fail_to_match_predicates, code = E0999)]
3180    pub(super) struct FailToMatchPredicates {
3181        #[primary_span]
3182        pub span: Span,
3183    }
3184
3185    #[derive(Diagnostic)]
3186    #[diag(fhir_analysis_invalid_res, code = E0999)]
3187    pub(super) struct InvalidRes {
3188        #[primary_span]
3189        pub span: Span,
3190        pub res_descr: &'static str,
3191    }
3192
3193    #[derive(Diagnostic)]
3194    #[diag(fhir_analysis_constant_annotation_needed, code = E0999)]
3195    pub(super) struct ConstantAnnotationNeeded {
3196        #[primary_span]
3197        #[label]
3198        span: Span,
3199    }
3200    impl ConstantAnnotationNeeded {
3201        pub(super) fn new(span: Span) -> Self {
3202            Self { span }
3203        }
3204    }
3205}