flux_refineck/
compare_impl_item.rs

1use flux_common::result::ErrorEmitter;
2use flux_infer::{
3    infer::{GlobalEnvExt as _, InferCtxt},
4    projections::NormalizeExt as _,
5};
6use flux_middle::{
7    def_id::{FluxDefId, MaybeExternId},
8    def_id_to_string,
9    global_env::GlobalEnv,
10    queries::QueryResult,
11    rty::TraitRef,
12};
13use rustc_hash::FxHashSet;
14use rustc_infer::infer::TyCtxtInferExt;
15use rustc_middle::ty::TypingMode;
16
17pub fn check_impl_against_trait(genv: GlobalEnv, impl_id: MaybeExternId) -> QueryResult {
18    let trait_id = genv.tcx().trait_id_of_impl(impl_id.resolved_id()).unwrap();
19
20    let impl_assoc_refts = genv.assoc_refinements_of(impl_id)?;
21    let trait_assoc_refts = genv.assoc_refinements_of(trait_id)?;
22    let impl_names: FxHashSet<_> = impl_assoc_refts.items.iter().map(|x| x.name()).collect();
23
24    for trait_assoc_id in &trait_assoc_refts.items {
25        let has_default = genv
26            .default_assoc_refinement_body(*trait_assoc_id)?
27            .is_some();
28        if !impl_names.contains(&trait_assoc_id.name()) && !has_default {
29            let span = genv.tcx().def_span(impl_id);
30            Err(genv.emit(errors::MissingAssocReft::new(span, trait_assoc_id.name())))?;
31        }
32    }
33
34    let impl_trait_ref = genv
35        .impl_trait_ref(impl_id.resolved_id())?
36        .unwrap()
37        .instantiate_identity();
38
39    let rustc_infcx = genv
40        .tcx()
41        .infer_ctxt()
42        .with_next_trait_solver(true)
43        .build(TypingMode::non_body_analysis());
44    let mut root_ctxt = genv
45        .infcx_root(&rustc_infcx, genv.infer_opts(impl_id.local_id()))
46        .with_const_generics(impl_id.resolved_id())?
47        .build()?;
48    let mut infcx = root_ctxt.infcx(impl_id.resolved_id(), &rustc_infcx);
49
50    for impl_assoc_id in &impl_assoc_refts.items {
51        let name = impl_assoc_id.name();
52        if let Some(trait_assoc_id) = trait_assoc_refts.find(name) {
53            check_assoc_reft(&mut infcx, impl_id, &impl_trait_ref, trait_assoc_id, *impl_assoc_id)?;
54        } else {
55            let fhir_impl_assoc_reft = genv
56                .map()
57                .expect_item(impl_id.local_id())?
58                .expect_impl()
59                .find_assoc_reft(name)
60                .unwrap();
61            Err(genv.emit(errors::InvalidAssocReft::new(
62                fhir_impl_assoc_reft.span,
63                name,
64                def_id_to_string(trait_id),
65            )))?;
66        }
67    }
68
69    Ok(())
70}
71
72fn check_assoc_reft(
73    infcx: &mut InferCtxt,
74    impl_id: MaybeExternId,
75    impl_trait_ref: &TraitRef,
76    trait_assoc_id: FluxDefId,
77    impl_assoc_id: FluxDefId,
78) -> QueryResult {
79    debug_assert_eq!(trait_assoc_id.name(), impl_assoc_id.name());
80
81    let impl_span = infcx
82        .genv
83        .map()
84        .expect_item(impl_id.local_id())?
85        .expect_impl()
86        .find_assoc_reft(impl_assoc_id.name())
87        .unwrap()
88        .span;
89
90    let impl_sort = infcx
91        .genv
92        .sort_of_assoc_reft(impl_assoc_id)?
93        .instantiate_identity()
94        .normalize_projections(&mut infcx.at(impl_span))?;
95
96    let trait_sort = infcx.genv.sort_of_assoc_reft(trait_assoc_id)?;
97    let trait_sort = trait_sort.instantiate(infcx.tcx(), &impl_trait_ref.args, &[]);
98    let trait_sort = trait_sort.normalize_projections(&mut infcx.at(impl_span))?;
99
100    if impl_sort != trait_sort {
101        Err(infcx.genv.emit(errors::IncompatibleSort::new(
102            impl_span,
103            impl_assoc_id.name(),
104            trait_sort,
105            impl_sort,
106        )))?;
107    }
108
109    Ok(())
110}
111
112pub(crate) mod errors {
113    use flux_errors::E0999;
114    use flux_macros::Diagnostic;
115    use flux_middle::rty;
116    use rustc_span::{Span, Symbol};
117
118    #[derive(Diagnostic)]
119    #[diag(refineck_incompatible_sort, code = E0999)]
120    pub(super) struct IncompatibleSort {
121        #[primary_span]
122        #[label]
123        span: Span,
124        name: Symbol,
125        expected: rty::FuncSort,
126        found: rty::FuncSort,
127    }
128
129    impl IncompatibleSort {
130        pub(super) fn new(
131            span: Span,
132            name: Symbol,
133            expected: rty::FuncSort,
134            found: rty::FuncSort,
135        ) -> Self {
136            Self { span, name, expected, found }
137        }
138    }
139
140    #[derive(Diagnostic)]
141    #[diag(refineck_missing_assoc_reft, code = E0999)]
142    pub struct MissingAssocReft {
143        #[primary_span]
144        span: Span,
145        name: Symbol,
146    }
147
148    impl MissingAssocReft {
149        pub(crate) fn new(span: Span, name: Symbol) -> Self {
150            Self { span, name }
151        }
152    }
153
154    #[derive(Diagnostic)]
155    #[diag(refineck_invalid_assoc_reft, code = E0999)]
156    pub struct InvalidAssocReft {
157        #[primary_span]
158        span: Span,
159        trait_: String,
160        name: Symbol,
161    }
162
163    impl InvalidAssocReft {
164        pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
165            Self { span, trait_, name }
166        }
167    }
168}
flux_refineck/compare_impl_item.rs

flux_refineck/
compare_impl_item.rs
