flux_fhir_analysis/conv/
struct_compat.rs

1//! Check whether two refinemnt types/signatures are structurally compatible.
2//!
3//! Used to check if a user spec is compatible with the underlying rust type. The code also
4//! infer types annotated with `_` in the surface syntax.
5
6use std::{fmt, iter};
7
8use flux_common::bug;
9use flux_errors::Errors;
10use flux_middle::{
11    def_id::MaybeExternId,
12    fhir,
13    global_env::GlobalEnv,
14    queries::QueryResult,
15    rty::{
16        self,
17        fold::{TypeFoldable, TypeFolder, TypeSuperFoldable},
18        refining::{Refine as _, Refiner},
19    },
20};
21use flux_rustc_bridge::ty::{self, FieldIdx, VariantIdx};
22use rustc_ast::Mutability;
23use rustc_data_structures::unord::UnordMap;
24use rustc_type_ir::{DebruijnIndex, INNERMOST, InferConst};
25
26pub(crate) fn type_alias(
27    genv: GlobalEnv,
28    alias: &fhir::TyAlias,
29    alias_ty: &rty::TyCtor,
30    def_id: MaybeExternId,
31) -> QueryResult<rty::TyCtor> {
32    let rust_ty = genv.lower_type_of(def_id.resolved_id())?.skip_binder();
33    let expected = rust_ty.refine(&Refiner::default_for_item(genv, def_id.resolved_id())?)?;
34    let mut zipper = Zipper::new(genv, def_id);
35
36    if zipper
37        .enter_a_binder(alias_ty, |zipper, ty| zipper.zip_ty(ty, &expected))
38        .is_err()
39    {
40        zipper
41            .errors
42            .emit(errors::IncompatibleRefinement::type_alias(genv, def_id, alias));
43    }
44
45    zipper.errors.to_result()?;
46
47    Ok(zipper.holes.replace_holes(alias_ty))
48}
49
50pub(crate) fn fn_sig(
51    genv: GlobalEnv,
52    decl: &fhir::FnDecl,
53    fn_sig: &rty::PolyFnSig,
54    def_id: MaybeExternId,
55) -> QueryResult<rty::PolyFnSig> {
56    let rust_fn_sig = genv.lower_fn_sig(def_id.resolved_id())?.skip_binder();
57
58    let expected = Refiner::default_for_item(genv, def_id.resolved_id())?.refine(&rust_fn_sig)?;
59
60    let mut zipper = Zipper::new(genv, def_id);
61    if let Err(err) = zipper.zip_poly_fn_sig(fn_sig, &expected) {
62        zipper.emit_fn_sig_err(err, decl);
63    }
64
65    zipper.errors.to_result()?;
66
67    Ok(zipper.holes.replace_holes(fn_sig))
68}
69
70pub(crate) fn variants(
71    genv: GlobalEnv,
72    variants: &[rty::PolyVariant],
73    adt_def_id: MaybeExternId,
74) -> QueryResult<Vec<rty::PolyVariant>> {
75    let refiner = Refiner::default_for_item(genv, adt_def_id.resolved_id())?;
76    let mut zipper = Zipper::new(genv, adt_def_id);
77    // TODO check same number of variants
78    for (i, variant) in variants.iter().enumerate() {
79        let variant_idx = VariantIdx::from_usize(i);
80        let expected = refiner.refine_variant_def(adt_def_id.resolved_id(), variant_idx)?;
81        zipper.zip_variant(variant, &expected, variant_idx);
82    }
83
84    zipper.errors.to_result()?;
85
86    Ok(variants
87        .iter()
88        .map(|v| zipper.holes.replace_holes(v))
89        .collect())
90}
91
92struct Zipper<'genv, 'tcx> {
93    genv: GlobalEnv<'genv, 'tcx>,
94    owner_id: MaybeExternId,
95    locs: UnordMap<rty::Loc, rty::Ty>,
96    holes: Holes,
97    /// Number of binders we've entered in `a`
98    a_binders: u32,
99    /// Each element in the vector correspond to a binder in `b`. For some binders we map it to
100    /// a corresponding binder in `a`. We assume that expressions filling holes will only contain
101    /// variables pointing to some of these mapped binders.
102    b_binder_to_a_binder: Vec<Option<u32>>,
103    errors: Errors<'genv>,
104}
105
106#[derive(Default)]
107struct Holes {
108    sorts: UnordMap<rty::SortVid, rty::Sort>,
109    subset_tys: UnordMap<rty::TyVid, rty::SubsetTy>,
110    types: UnordMap<rty::TyVid, rty::Ty>,
111    regions: UnordMap<rty::RegionVid, rty::Region>,
112    consts: UnordMap<rty::ConstVid, rty::Const>,
113}
114
115impl TypeFolder for &Holes {
116    fn fold_sort(&mut self, sort: &rty::Sort) -> rty::Sort {
117        if let rty::Sort::Infer(vid) = sort {
118            self.sorts
119                .get(vid)
120                .cloned()
121                .unwrap_or_else(|| bug!("unfilled sort hole {vid:?}"))
122        } else {
123            // Erase regions from sorts: they don't affect the sort, and a bound region filled into
124            // a hole can have an index that's only valid under the binder the sort belongs to.
125            sort.super_fold_with(self).erase_regions_including_bound()
126        }
127    }
128
129    fn fold_ty(&mut self, ty: &rty::Ty) -> rty::Ty {
130        if let rty::TyKind::Infer(vid) = ty.kind() {
131            self.types
132                .get(vid)
133                .cloned()
134                .unwrap_or_else(|| bug!("unfilled type hole {vid:?}"))
135        } else {
136            ty.super_fold_with(self)
137        }
138    }
139
140    fn fold_subset_ty(&mut self, constr: &rty::SubsetTy) -> rty::SubsetTy {
141        if let rty::BaseTy::Infer(vid) = &constr.bty {
142            self.subset_tys
143                .get(vid)
144                .cloned()
145                .unwrap_or_else(|| bug!("unfilled type hole {vid:?}"))
146        } else {
147            constr.super_fold_with(self)
148        }
149    }
150
151    fn fold_region(&mut self, r: &rty::Region) -> rty::Region {
152        if let rty::Region::ReVar(vid) = r {
153            self.regions
154                .get(vid)
155                .copied()
156                .unwrap_or_else(|| bug!("unfilled region hole {vid:?}"))
157        } else {
158            *r
159        }
160    }
161
162    fn fold_const(&mut self, ct: &rty::Const) -> rty::Const {
163        if let rty::ConstKind::Infer(InferConst::Var(cid)) = ct.kind {
164            self.consts
165                .get(&cid)
166                .cloned()
167                .unwrap_or_else(|| bug!("unfilled const hole {cid:?}"))
168        } else {
169            ct.super_fold_with(self)
170        }
171    }
172}
173
174impl Holes {
175    fn replace_holes<T: TypeFoldable>(&self, t: &T) -> T {
176        let mut this = self;
177        t.fold_with(&mut this)
178    }
179}
180
181impl<'genv, 'tcx> Zipper<'genv, 'tcx> {
182    fn new(genv: GlobalEnv<'genv, 'tcx>, owner_id: MaybeExternId) -> Self {
183        Self {
184            genv,
185            owner_id,
186            locs: UnordMap::default(),
187            holes: Default::default(),
188            a_binders: 0,
189            b_binder_to_a_binder: vec![],
190            errors: Errors::new(genv.sess()),
191        }
192    }
193
194    fn is_async_fn(&self) -> bool {
195        self.genv
196            .tcx()
197            .asyncness(self.owner_id.resolved_id())
198            .is_async()
199    }
200
201    fn zip_poly_fn_sig(&mut self, a: &rty::PolyFnSig, b: &rty::PolyFnSig) -> Result<(), FnSigErr> {
202        self.enter_binders(a, b, |this, a, b| this.zip_fn_sig(a, b))
203    }
204
205    fn zip_variant(&mut self, a: &rty::PolyVariant, b: &rty::PolyVariant, variant_idx: VariantIdx) {
206        self.enter_binders(a, b, |this, a, b| {
207            // The args are always `GenericArgs::identity_for_item` inside the `EarlyBinder`
208            debug_assert_eq!(a.args, b.args);
209
210            if a.fields.len() != b.fields.len() {
211                this.errors.emit(errors::FieldCountMismatch::new(
212                    this.genv,
213                    a.fields.len(),
214                    this.owner_id,
215                    variant_idx,
216                ));
217                return;
218            }
219            for (i, (ty_a, ty_b)) in iter::zip(&a.fields, &b.fields).enumerate() {
220                let field_idx = FieldIdx::from_usize(i);
221                if this.zip_ty(ty_a, ty_b).is_err() {
222                    this.errors.emit(errors::IncompatibleRefinement::field(
223                        this.genv,
224                        this.owner_id,
225                        variant_idx,
226                        field_idx,
227                    ));
228                }
229            }
230        });
231    }
232
233    fn zip_fn_sig(&mut self, a: &rty::FnSig, b: &rty::FnSig) -> Result<(), FnSigErr> {
234        if a.inputs().len() != b.inputs().len() {
235            Err(FnSigErr::ArgCountMismatch)?;
236        }
237        for (i, (ty_a, ty_b)) in iter::zip(a.inputs(), b.inputs()).enumerate() {
238            self.zip_ty(ty_a, ty_b).map_err(|_| FnSigErr::FnInput(i))?;
239        }
240        self.enter_binders(&a.output, &b.output, |this, output_a, output_b| {
241            this.zip_output(output_a, output_b)
242        })
243    }
244
245    fn zip_output(&mut self, a: &rty::FnOutput, b: &rty::FnOutput) -> Result<(), FnSigErr> {
246        self.zip_ty(&a.ret, &b.ret).map_err(FnSigErr::FnOutput)?;
247
248        for (i, ensures) in a.ensures.iter().enumerate() {
249            if let rty::Ensures::Type(path, ty_a) = ensures {
250                let loc = path.to_loc().unwrap();
251                let ty_b = self.locs.get(&loc).unwrap().shift_in_escaping(1);
252                self.zip_ty(ty_a, &ty_b)
253                    .map_err(|_| FnSigErr::Ensures { i, expected: ty_b })?;
254            }
255        }
256        Ok(())
257    }
258
259    fn zip_ty(&mut self, a: &rty::Ty, b: &rty::Ty) -> Result<(), Mismatch> {
260        match (a.kind(), b.kind()) {
261            (rty::TyKind::Infer(vid), _) => {
262                assert_ne!(vid.as_u32(), 0);
263                let b = self.adjust_bvars(b);
264                self.holes.types.insert(*vid, b);
265                Ok(())
266            }
267            (rty::TyKind::Exists(ctor_a), _) => {
268                self.enter_a_binder(ctor_a, |this, ty_a| this.zip_ty(ty_a, b))
269            }
270            (_, rty::TyKind::Exists(ctor_b)) => {
271                self.enter_b_binder(ctor_b, |this, ty_b| this.zip_ty(a, ty_b))
272            }
273            (rty::TyKind::Constr(_, ty_a), _) => self.zip_ty(ty_a, b),
274            (_, rty::TyKind::Constr(_, ty_b)) => self.zip_ty(a, ty_b),
275            (rty::TyKind::Indexed(bty_a, _), rty::TyKind::Indexed(bty_b, _)) => {
276                self.zip_bty(bty_a, bty_b)
277            }
278            (rty::TyKind::StrgRef(re_a, path, ty_a), rty::Ref!(re_b, ty_b, Mutability::Mut)) => {
279                let loc = path.to_loc().unwrap();
280                self.locs.insert(loc, ty_b.clone());
281
282                self.zip_region(re_a, re_b);
283                self.zip_ty(ty_a, ty_b)
284            }
285            (rty::TyKind::Param(pty_a), rty::TyKind::Param(pty_b)) => {
286                assert_eq_or_incompatible(pty_a, pty_b)
287            }
288            (
289                rty::TyKind::Ptr(_, _)
290                | rty::TyKind::Discr(..)
291                | rty::TyKind::Downcast(_, _, _, _, _)
292                | rty::TyKind::Blocked(_)
293                | rty::TyKind::Uninit,
294                _,
295            ) => {
296                bug!("unexpected type {a:?}");
297            }
298            _ => Err(Mismatch::new(a, b)),
299        }
300    }
301
302    fn zip_bty(&mut self, a: &rty::BaseTy, b: &rty::BaseTy) -> Result<(), Mismatch> {
303        match (a, b) {
304            (rty::BaseTy::Int(ity_a), rty::BaseTy::Int(ity_b)) => {
305                assert_eq_or_incompatible(ity_a, ity_b)
306            }
307            (rty::BaseTy::Uint(uity_a), rty::BaseTy::Uint(uity_b)) => {
308                assert_eq_or_incompatible(uity_a, uity_b)
309            }
310            (rty::BaseTy::Bool, rty::BaseTy::Bool) => Ok(()),
311            (rty::BaseTy::Str, rty::BaseTy::Str) => Ok(()),
312            (rty::BaseTy::Char, rty::BaseTy::Char) => Ok(()),
313            (rty::BaseTy::Float(fty_a), rty::BaseTy::Float(fty_b)) => {
314                assert_eq_or_incompatible(fty_a, fty_b)
315            }
316            (rty::BaseTy::Slice(ty_a), rty::BaseTy::Slice(ty_b)) => self.zip_ty(ty_a, ty_b),
317            (rty::BaseTy::Adt(adt_def_a, args_a), rty::BaseTy::Adt(adt_def_b, args_b)) => {
318                assert_eq_or_incompatible(adt_def_a.did(), adt_def_b.did())?;
319                assert_eq_or_incompatible(args_a.len(), args_b.len())?;
320                for (arg_a, arg_b) in iter::zip(args_a, args_b) {
321                    self.zip_generic_arg(arg_a, arg_b)?;
322                }
323                Ok(())
324            }
325            (rty::BaseTy::RawPtr(ty_a, mutbl_a), rty::BaseTy::RawPtr(ty_b, mutbl_b)) => {
326                assert_eq_or_incompatible(mutbl_a, mutbl_b)?;
327                self.zip_ty(ty_a, ty_b)
328            }
329            (rty::BaseTy::Ref(re_a, ty_a, mutbl_a), rty::BaseTy::Ref(re_b, ty_b, mutbl_b)) => {
330                assert_eq_or_incompatible(mutbl_a, mutbl_b)?;
331                self.zip_region(re_a, re_b);
332                self.zip_ty(ty_a, ty_b)
333            }
334            (rty::BaseTy::FnPtr(poly_sig_a), rty::BaseTy::FnPtr(poly_sig_b)) => {
335                // Check that safety and abi of a fn-ptr in a spec (see `desugar_bare_fn`)
336                // matches the rust one, to not refine an `unsafe fn` pointer with a safe one.
337                let (sig_a, sig_b) = (poly_sig_a.skip_binder_ref(), poly_sig_b.skip_binder_ref());
338                assert_eq_or_incompatible(sig_a.safety, sig_b.safety)?;
339                assert_eq_or_incompatible(sig_a.abi, sig_b.abi)?;
340                self.zip_poly_fn_sig(poly_sig_a, poly_sig_b)
341                    .map_err(|_| Mismatch::new(poly_sig_a, poly_sig_b))
342            }
343            (rty::BaseTy::Tuple(tys_a), rty::BaseTy::Tuple(tys_b)) => {
344                assert_eq_or_incompatible(tys_a.len(), tys_b.len())?;
345                for (ty_a, ty_b) in iter::zip(tys_a, tys_b) {
346                    self.zip_ty(ty_a, ty_b)?;
347                }
348                Ok(())
349            }
350            (rty::BaseTy::Alias(aty_a), rty::BaseTy::Alias(aty_b)) => {
351                assert_eq_or_incompatible(aty_a.kind, aty_b.kind)?;
352                assert_eq_or_incompatible(aty_a.args.len(), aty_b.args.len())?;
353                for (arg_a, arg_b) in iter::zip(&aty_a.args, &aty_b.args) {
354                    self.zip_generic_arg(arg_a, arg_b)?;
355                }
356                Ok(())
357            }
358            (rty::BaseTy::Array(ty_a, len_a), rty::BaseTy::Array(ty_b, len_b)) => {
359                self.zip_const(len_a, len_b)?;
360                self.zip_ty(ty_a, ty_b)
361            }
362            (rty::BaseTy::Never, rty::BaseTy::Never) => Ok(()),
363            (rty::BaseTy::Param(pty_a), rty::BaseTy::Param(pty_b)) => {
364                assert_eq_or_incompatible(pty_a, pty_b)
365            }
366            (rty::BaseTy::Dynamic(preds_a, re_a), rty::BaseTy::Dynamic(preds_b, re_b)) => {
367                assert_eq_or_incompatible(preds_a.len(), preds_b.len())?;
368                for (pred_a, pred_b) in iter::zip(preds_a, preds_b) {
369                    self.zip_poly_existential_pred(pred_a, pred_b)?;
370                }
371                self.zip_region(re_a, re_b);
372                Ok(())
373            }
374            (rty::BaseTy::Foreign(def_id_a), rty::BaseTy::Foreign(def_id_b)) => {
375                assert_eq_or_incompatible(def_id_a, def_id_b)
376            }
377            (rty::BaseTy::Closure(..) | rty::BaseTy::Coroutine(..), _) => {
378                bug!("unexpected type `{a:?}`");
379            }
380            _ => Err(Mismatch::new(a, b)),
381        }
382    }
383
384    fn zip_generic_arg(
385        &mut self,
386        a: &rty::GenericArg,
387        b: &rty::GenericArg,
388    ) -> Result<(), Mismatch> {
389        match (a, b) {
390            (rty::GenericArg::Ty(ty_a), rty::GenericArg::Ty(ty_b)) => self.zip_ty(ty_a, ty_b),
391            (rty::GenericArg::Base(ctor_a), rty::GenericArg::Base(ctor_b)) => {
392                self.zip_sorts(&ctor_a.sort(), &ctor_b.sort());
393                self.enter_binders(ctor_a, ctor_b, |this, sty_a, sty_b| {
394                    this.zip_subset_ty(sty_a, sty_b)
395                })
396            }
397            (rty::GenericArg::Lifetime(re_a), rty::GenericArg::Lifetime(re_b)) => {
398                self.zip_region(re_a, re_b);
399                Ok(())
400            }
401            (rty::GenericArg::Const(ct_a), rty::GenericArg::Const(ct_b)) => {
402                self.zip_const(ct_a, ct_b)
403            }
404            _ => Err(Mismatch::new(a, b)),
405        }
406    }
407
408    fn zip_sorts(&mut self, a: &rty::Sort, b: &rty::Sort) {
409        if let rty::Sort::Infer(vid) = a {
410            assert_ne!(vid.as_u32(), 0);
411            self.holes.sorts.insert(*vid, b.clone());
412        }
413    }
414
415    fn zip_subset_ty(&mut self, a: &rty::SubsetTy, b: &rty::SubsetTy) -> Result<(), Mismatch> {
416        if let rty::BaseTy::Infer(vid) = a.bty {
417            assert_ne!(vid.as_u32(), 0);
418            let b = self.adjust_bvars(b);
419            self.holes.subset_tys.insert(vid, b);
420            Ok(())
421        } else {
422            self.zip_bty(&a.bty, &b.bty)
423        }
424    }
425
426    fn zip_const(&mut self, a: &rty::Const, b: &ty::Const) -> Result<(), Mismatch> {
427        match (&a.kind, &b.kind) {
428            (rty::ConstKind::Infer(ty::InferConst::Var(cid)), _) => {
429                self.holes.consts.insert(*cid, b.clone());
430                Ok(())
431            }
432            (rty::ConstKind::Param(param_const_a), ty::ConstKind::Param(param_const_b)) => {
433                assert_eq_or_incompatible(param_const_a, param_const_b)
434            }
435            (rty::ConstKind::Value(ty_a, val_a), ty::ConstKind::Value(ty_b, val_b)) => {
436                assert_eq_or_incompatible(ty_a, ty_b)?;
437                assert_eq_or_incompatible(val_a, val_b)
438            }
439            (rty::ConstKind::Alias(c1), ty::ConstKind::Alias(c2)) => {
440                assert_eq_or_incompatible(c1, c2)
441            }
442            _ => Err(Mismatch::new(a, b)),
443        }
444    }
445
446    fn zip_region(&mut self, a: &rty::Region, b: &ty::Region) {
447        if let rty::Region::ReVar(vid) = a {
448            let re = self.adjust_bvars(b);
449            self.holes.regions.insert(*vid, re);
450        }
451    }
452
453    fn zip_poly_existential_pred(
454        &mut self,
455        a: &rty::Binder<rty::ExistentialPredicate>,
456        b: &rty::Binder<rty::ExistentialPredicate>,
457    ) -> Result<(), Mismatch> {
458        self.enter_binders(a, b, |this, a, b| {
459            match (a, b) {
460                (
461                    rty::ExistentialPredicate::Trait(trait_ref_a),
462                    rty::ExistentialPredicate::Trait(trait_ref_b),
463                ) => {
464                    assert_eq_or_incompatible(trait_ref_a.def_id, trait_ref_b.def_id)?;
465                    assert_eq_or_incompatible(trait_ref_a.args.len(), trait_ref_b.args.len())?;
466                    for (arg_a, arg_b) in iter::zip(&trait_ref_a.args, &trait_ref_b.args) {
467                        this.zip_generic_arg(arg_a, arg_b)?;
468                    }
469                    Ok(())
470                }
471                (
472                    rty::ExistentialPredicate::Projection(projection_a),
473                    rty::ExistentialPredicate::Projection(projection_b),
474                ) => {
475                    assert_eq_or_incompatible(projection_a.def_id, projection_b.def_id)?;
476                    assert_eq_or_incompatible(projection_a.args.len(), projection_b.args.len())?;
477                    for (arg_a, arg_b) in iter::zip(&projection_a.args, &projection_b.args) {
478                        this.zip_generic_arg(arg_a, arg_b)?;
479                    }
480                    this.enter_binders(&projection_a.term, &projection_b.term, |this, a, b| {
481                        this.zip_bty(&a.bty, &b.bty)
482                    })
483                }
484                (
485                    rty::ExistentialPredicate::AutoTrait(def_id_a),
486                    rty::ExistentialPredicate::AutoTrait(def_id_b),
487                ) => assert_eq_or_incompatible(def_id_a, def_id_b),
488                _ => Err(Mismatch::new(a, b)),
489            }
490        })
491    }
492
493    /// Enter a binder in both `a` and `b` creating a mapping between the two.
494    fn enter_binders<T, R>(
495        &mut self,
496        a: &rty::Binder<T>,
497        b: &rty::Binder<T>,
498        f: impl FnOnce(&mut Self, &T, &T) -> R,
499    ) -> R {
500        self.b_binder_to_a_binder.push(Some(self.a_binders));
501        self.a_binders += 1;
502        let r = f(self, a.skip_binder_ref(), b.skip_binder_ref());
503        self.a_binders -= 1;
504        self.b_binder_to_a_binder.pop();
505        r
506    }
507
508    /// Enter a binder in `a` without a corresponding mapping in `b`
509    fn enter_a_binder<T, R>(
510        &mut self,
511        t: &rty::Binder<T>,
512        f: impl FnOnce(&mut Self, &T) -> R,
513    ) -> R {
514        self.a_binders += 1;
515        let r = f(self, t.skip_binder_ref());
516        self.a_binders -= 1;
517        r
518    }
519
520    /// Enter a binder in `b` without a corresponding mapping in `a`
521    fn enter_b_binder<T, R>(
522        &mut self,
523        t: &rty::Binder<T>,
524        f: impl FnOnce(&mut Self, &T) -> R,
525    ) -> R {
526        self.b_binder_to_a_binder.push(None);
527        let r = f(self, t.skip_binder_ref());
528        self.b_binder_to_a_binder.pop();
529        r
530    }
531
532    fn adjust_bvars<T: TypeFoldable + Clone + std::fmt::Debug>(&self, t: &T) -> T {
533        struct Adjuster<'a, 'genv, 'tcx> {
534            current_index: DebruijnIndex,
535            zipper: &'a Zipper<'genv, 'tcx>,
536        }
537
538        impl Adjuster<'_, '_, '_> {
539            fn adjust(&self, debruijn: DebruijnIndex) -> DebruijnIndex {
540                let b_binders = self.zipper.b_binder_to_a_binder.len();
541                let mapped_binder = self.zipper.b_binder_to_a_binder
542                    [b_binders - debruijn.as_usize() - 1]
543                    .unwrap_or_else(|| {
544                        bug!("bound var without corresponding binder: `{debruijn:?}`")
545                    });
546                DebruijnIndex::from_u32(self.zipper.a_binders - mapped_binder - 1)
547                    .shifted_in(self.current_index.as_u32())
548            }
549        }
550
551        impl TypeFolder for Adjuster<'_, '_, '_> {
552            fn enter_binder(&mut self, _: &rty::BoundVariableKinds) {
553                self.current_index.shift_in(1);
554            }
555
556            fn exit_binder(&mut self) {
557                self.current_index.shift_out(1);
558            }
559
560            fn fold_region(&mut self, re: &rty::Region) -> rty::Region {
561                if let rty::ReBound(debruijn, br) = *re
562                    && debruijn >= self.current_index
563                {
564                    rty::ReBound(self.adjust(debruijn), br)
565                } else {
566                    *re
567                }
568            }
569
570            fn fold_expr(&mut self, expr: &rty::Expr) -> rty::Expr {
571                if let rty::ExprKind::Var(rty::Var::Bound(debruijn, breft)) = expr.kind()
572                    && *debruijn >= self.current_index
573                {
574                    rty::Expr::bvar(self.adjust(*debruijn), breft.var, breft.kind)
575                } else {
576                    expr.super_fold_with(self)
577                }
578            }
579        }
580        t.fold_with(&mut Adjuster { current_index: INNERMOST, zipper: self })
581    }
582
583    fn emit_fn_sig_err(&mut self, err: FnSigErr, decl: &fhir::FnDecl) {
584        match err {
585            FnSigErr::ArgCountMismatch => {
586                self.errors.emit(errors::IncompatibleParamCount::new(
587                    self.genv,
588                    decl,
589                    self.owner_id,
590                ));
591            }
592            FnSigErr::FnInput(i) => {
593                self.errors.emit(errors::IncompatibleRefinement::fn_input(
594                    self.genv,
595                    self.owner_id,
596                    decl,
597                    i,
598                ));
599            }
600            FnSigErr::FnOutput(_) => {
601                self.errors.emit(errors::IncompatibleRefinement::fn_output(
602                    self.genv,
603                    self.owner_id,
604                    decl,
605                    self.is_async_fn(),
606                ));
607            }
608            FnSigErr::Ensures { i, expected } => {
609                self.errors.emit(errors::IncompatibleRefinement::ensures(
610                    self.genv,
611                    self.owner_id,
612                    decl,
613                    &expected,
614                    i,
615                ));
616            }
617        }
618    }
619}
620
621fn assert_eq_or_incompatible<T: Eq + fmt::Debug>(a: T, b: T) -> Result<(), Mismatch> {
622    if a != b {
623        return Err(Mismatch::new(a, b));
624    }
625    Ok(())
626}
627
628#[expect(dead_code, reason = "we use the the String for debugging")]
629struct Mismatch(String);
630
631impl Mismatch {
632    fn new<T: fmt::Debug>(a: T, b: T) -> Self {
633        Self(format!("{a:?} != {b:?}"))
634    }
635}
636
637enum FnSigErr {
638    ArgCountMismatch,
639    FnInput(usize),
640    #[expect(dead_code, reason = "we use the struct for debugging")]
641    FnOutput(Mismatch),
642    Ensures {
643        i: usize,
644        expected: rty::Ty,
645    },
646}
647
648mod errors {
649    use flux_common::span_bug;
650    use flux_errors::E0999;
651    use flux_macros::Diagnostic;
652    use flux_middle::{def_id::MaybeExternId, fhir, global_env::GlobalEnv, rty};
653    use flux_rustc_bridge::{
654        ToRustc,
655        ty::{FieldIdx, VariantIdx},
656    };
657    use rustc_span::{DUMMY_SP, Span};
658
659    #[derive(Diagnostic)]
660    #[diag("{$def_descr} has an incompatible refinement annotation", code = E0999)]
661    #[note("a refinement annotation must match the unrefined definition structurally")]
662    pub(super) struct IncompatibleRefinement<'tcx> {
663        #[primary_span]
664        #[label("expected a refinement of `{$expected_ty}`")]
665        span: Span,
666        #[label("unrefined {$def_descr} found here")]
667        expected_span: Option<Span>,
668        expected_ty: rustc_middle::ty::Ty<'tcx>,
669        def_descr: &'static str,
670        #[help("mark the flux signature as `async fn`")]
671        async_hint: Option<()>,
672    }
673
674    impl<'tcx> IncompatibleRefinement<'tcx> {
675        pub(super) fn type_alias(
676            genv: GlobalEnv<'_, 'tcx>,
677            def_id: MaybeExternId,
678            type_alias: &fhir::TyAlias,
679        ) -> Self {
680            let tcx = genv.tcx();
681            Self {
682                span: type_alias.ty.span,
683                def_descr: tcx.def_descr(def_id.resolved_id()),
684                expected_span: Some(tcx.def_span(def_id)),
685                expected_ty: tcx.type_of(def_id).skip_binder(),
686                async_hint: None,
687            }
688        }
689
690        pub(super) fn fn_input(
691            genv: GlobalEnv<'_, 'tcx>,
692            fn_id: MaybeExternId,
693            decl: &fhir::FnDecl,
694            pos: usize,
695        ) -> Self {
696            let expected_span = match fn_id {
697                MaybeExternId::Local(local_id) => {
698                    genv.tcx()
699                        .hir_node_by_def_id(local_id)
700                        .fn_decl()
701                        .and_then(|fn_decl| fn_decl.inputs.get(pos))
702                        .map(|input| input.span)
703                }
704                MaybeExternId::Extern(_, extern_id) => Some(genv.tcx().def_span(extern_id)),
705            };
706
707            let expected_ty = genv
708                .tcx()
709                .fn_sig(fn_id.resolved_id())
710                .skip_binder()
711                .inputs()
712                .map_bound(|inputs| inputs[pos])
713                .skip_binder();
714
715            Self {
716                span: decl.inputs[pos].span,
717                def_descr: genv.tcx().def_descr(fn_id.resolved_id()),
718                expected_span,
719                expected_ty,
720                async_hint: None,
721            }
722        }
723
724        pub(super) fn fn_output(
725            genv: GlobalEnv<'_, 'tcx>,
726            fn_id: MaybeExternId,
727            decl: &fhir::FnDecl,
728            is_async: bool,
729        ) -> Self {
730            let expected_span = match fn_id {
731                MaybeExternId::Local(local_id) => {
732                    genv.tcx()
733                        .hir_node_by_def_id(local_id)
734                        .fn_decl()
735                        .map(|fn_decl| fn_decl.output.span())
736                }
737                MaybeExternId::Extern(_, extern_id) => Some(genv.tcx().def_span(extern_id)),
738            };
739
740            let expected_ty = genv
741                .tcx()
742                .fn_sig(fn_id.resolved_id())
743                .skip_binder()
744                .output()
745                .skip_binder();
746            let spec_span = decl.output.ret.span;
747
748            let async_hint = if is_async { Some(()) } else { None };
749
750            Self {
751                span: spec_span,
752                def_descr: genv.tcx().def_descr(fn_id.resolved_id()),
753                expected_span,
754                expected_ty,
755                async_hint,
756            }
757        }
758
759        pub(super) fn ensures(
760            genv: GlobalEnv<'_, 'tcx>,
761            fn_id: MaybeExternId,
762            decl: &fhir::FnDecl,
763            expected: &rty::Ty,
764            i: usize,
765        ) -> Self {
766            let fhir::Ensures::Type(_, ty) = &decl.output.ensures[i] else {
767                span_bug!(decl.span, "expected `fhir::Ensures::Type`");
768            };
769            let tcx = genv.tcx();
770            Self {
771                span: ty.span,
772                def_descr: tcx.def_descr(fn_id.resolved_id()),
773                expected_span: None,
774                expected_ty: expected.to_rustc(tcx),
775                async_hint: None,
776            }
777        }
778
779        pub(super) fn field(
780            genv: GlobalEnv<'_, 'tcx>,
781            adt_id: MaybeExternId,
782            variant_idx: VariantIdx,
783            field_idx: FieldIdx,
784        ) -> Self {
785            let tcx = genv.tcx();
786            let adt_def = tcx.adt_def(adt_id);
787            let field_def = &adt_def.variant(variant_idx).fields[field_idx];
788
789            let item = genv.fhir_expect_item(adt_id.local_id()).unwrap();
790            let span = match &item.kind {
791                fhir::ItemKind::Enum(enum_def) => {
792                    enum_def.variants[variant_idx.as_usize()].fields[field_idx.as_usize()]
793                        .ty
794                        .span
795                }
796                fhir::ItemKind::Struct(struct_def)
797                    if let fhir::StructKind::Transparent { fields } = &struct_def.kind =>
798                {
799                    fields[field_idx.as_usize()].ty.span
800                }
801                _ => DUMMY_SP,
802            };
803
804            Self {
805                span,
806                def_descr: tcx.def_descr(field_def.did),
807                expected_span: Some(tcx.def_span(field_def.did)),
808                expected_ty: tcx.type_of(field_def.did).skip_binder(),
809                async_hint: None,
810            }
811        }
812    }
813
814    #[derive(Diagnostic)]
815    #[diag("{$def_descr} has an incompatible refinement annotation", code = E0999)]
816    pub(super) struct IncompatibleParamCount {
817        #[primary_span]
818        #[label(
819            "refined signature has {$found} {$found ->
820                [one] parameter
821                *[other] parameters
822            }"
823        )]
824        span: Span,
825        found: usize,
826        #[label(
827            "unrefined signature has {$expected} {$expected ->
828                [one] parameter
829                *[other] parameters
830            }"
831        )]
832        expected_span: Span,
833        expected: usize,
834        def_descr: &'static str,
835    }
836
837    impl IncompatibleParamCount {
838        pub(super) fn new(genv: GlobalEnv, decl: &fhir::FnDecl, def_id: MaybeExternId) -> Self {
839            let def_descr = genv.tcx().def_descr(def_id.resolved_id());
840
841            let span = if !decl.inputs.is_empty() {
842                decl.inputs[decl.inputs.len() - 1]
843                    .span
844                    .with_lo(decl.inputs[0].span.lo())
845            } else {
846                decl.span
847            };
848
849            let expected_span = if let Some(local_id) = def_id.as_local()
850                && let expected_decl = genv.tcx().hir_node_by_def_id(local_id).fn_decl().unwrap()
851                && !expected_decl.inputs.is_empty()
852            {
853                expected_decl.inputs[expected_decl.inputs.len() - 1]
854                    .span
855                    .with_lo(expected_decl.inputs[0].span.lo())
856            } else {
857                genv.tcx().def_span(def_id)
858            };
859
860            let expected = genv
861                .tcx()
862                .fn_sig(def_id)
863                .skip_binder()
864                .skip_binder()
865                .inputs()
866                .len();
867
868            Self { span, found: decl.inputs.len(), expected_span, expected, def_descr }
869        }
870    }
871
872    #[derive(Diagnostic)]
873    #[diag("variant has an incompatible refinement annotation", code = E0999)]
874    pub(super) struct FieldCountMismatch {
875        #[primary_span]
876        #[label(
877            "expected {$expected_fields} {$expected_fields ->
878                [one] field
879                *[other] fields
880            }, found {$fields}"
881        )]
882        span: Span,
883        fields: usize,
884        #[label("unrefined variant defined here")]
885        expected_span: Span,
886        expected_fields: usize,
887    }
888
889    impl FieldCountMismatch {
890        pub(super) fn new(
891            genv: GlobalEnv,
892            found: usize,
893            adt_def_id: MaybeExternId,
894            variant_idx: VariantIdx,
895        ) -> Self {
896            let adt_def = genv.tcx().adt_def(adt_def_id);
897            let expected_variant = adt_def.variant(variant_idx);
898
899            // Get the span of the variant if this is an enum. Structs cannot have produce a field
900            // count mismatch.
901            let span = if let Ok(fhir::Node::Item(item)) = genv.fhir_node(adt_def_id.local_id())
902                && let fhir::ItemKind::Enum(enum_def) = &item.kind
903                && let Some(variant) = enum_def.variants.get(variant_idx.as_usize())
904            {
905                variant.span
906            } else {
907                DUMMY_SP
908            };
909
910            Self {
911                span,
912                fields: found,
913                expected_span: genv.tcx().def_span(expected_variant.def_id),
914                expected_fields: expected_variant.fields.len(),
915            }
916        }
917    }
918}
flux_fhir_analysis/conv/struct_compat.rs

flux_fhir_analysis/conv/
struct_compat.rs
