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