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_reft in &trait_assoc_refts.items {
25        let trait_assoc_def_id = trait_assoc_reft.def_id();
26        let has_default = genv
27            .default_assoc_refinement_body(trait_assoc_def_id)?
28            .is_some();
29        if !impl_names.contains(&trait_assoc_reft.name()) && !has_default {
30            let span = genv.tcx().def_span(impl_id);
31            Err(genv.emit(errors::MissingAssocReft::new(span, trait_assoc_reft.name())))?;
32        } else if impl_names.contains(&trait_assoc_reft.name()) && trait_assoc_reft.final_ {
33            let span = genv.tcx().def_span(impl_id);
34            Err(genv.emit(errors::ImplAssocReftOnFinal::new(span, trait_assoc_reft.name())))?;
35        }
36    }
37
38    let impl_trait_ref = genv
39        .impl_trait_ref(impl_id.resolved_id())?
40        .unwrap()
41        .instantiate_identity();
42
43    let rustc_infcx = genv
44        .tcx()
45        .infer_ctxt()
46        .with_next_trait_solver(true)
47        .build(TypingMode::non_body_analysis());
48    let mut root_ctxt = genv
49        .infcx_root(&rustc_infcx, genv.infer_opts(impl_id.local_id()))
50        .with_const_generics(impl_id.resolved_id())?
51        .build()?;
52    let mut infcx = root_ctxt.infcx(impl_id.resolved_id(), &rustc_infcx);
53
54    for impl_assoc_reft in &impl_assoc_refts.items {
55        let name = impl_assoc_reft.name();
56        if let Some(trait_assoc_id) = trait_assoc_refts.find(name) {
57            check_assoc_reft(
58                &mut infcx,
59                impl_id,
60                &impl_trait_ref,
61                trait_assoc_id,
62                impl_assoc_reft.def_id(),
63            )?;
64        } else {
65            let fhir_impl_assoc_reft = genv
66                .map()
67                .expect_item(impl_id.local_id())?
68                .expect_impl()
69                .find_assoc_reft(name)
70                .unwrap();
71            Err(genv.emit(errors::InvalidAssocReft::new(
72                fhir_impl_assoc_reft.span,
73                name,
74                def_id_to_string(trait_id),
75            )))?;
76        }
77    }
78
79    Ok(())
80}
81
82fn check_assoc_reft(
83    infcx: &mut InferCtxt,
84    impl_id: MaybeExternId,
85    impl_trait_ref: &TraitRef,
86    trait_assoc_id: FluxDefId,
87    impl_assoc_id: FluxDefId,
88) -> QueryResult {
89    debug_assert_eq!(trait_assoc_id.name(), impl_assoc_id.name());
90
91    let impl_span = infcx
92        .genv
93        .map()
94        .expect_item(impl_id.local_id())?
95        .expect_impl()
96        .find_assoc_reft(impl_assoc_id.name())
97        .unwrap()
98        .span;
99
100    let impl_sort = infcx
101        .genv
102        .sort_of_assoc_reft(impl_assoc_id)?
103        .instantiate_identity()
104        .normalize_projections(&mut infcx.at(impl_span))?;
105
106    let trait_sort = infcx.genv.sort_of_assoc_reft(trait_assoc_id)?;
107    let trait_sort = trait_sort.instantiate(infcx.tcx(), &impl_trait_ref.args, &[]);
108    let trait_sort = trait_sort.normalize_projections(&mut infcx.at(impl_span))?;
109
110    if impl_sort != trait_sort {
111        Err(infcx.genv.emit(errors::IncompatibleSort::new(
112            impl_span,
113            impl_assoc_id.name(),
114            trait_sort,
115            impl_sort,
116        )))?;
117    }
118
119    Ok(())
120}
121
122pub(crate) mod errors {
123    use flux_errors::E0999;
124    use flux_macros::Diagnostic;
125    use flux_middle::rty;
126    use rustc_span::{Span, Symbol};
127
128    #[derive(Diagnostic)]
129    #[diag(refineck_incompatible_sort, code = E0999)]
130    pub(super) struct IncompatibleSort {
131        #[primary_span]
132        #[label]
133        span: Span,
134        name: Symbol,
135        expected: rty::FuncSort,
136        found: rty::FuncSort,
137    }
138
139    impl IncompatibleSort {
140        pub(super) fn new(
141            span: Span,
142            name: Symbol,
143            expected: rty::FuncSort,
144            found: rty::FuncSort,
145        ) -> Self {
146            Self { span, name, expected, found }
147        }
148    }
149
150    #[derive(Diagnostic)]
151    #[diag(refineck_missing_assoc_reft, code = E0999)]
152    pub struct MissingAssocReft {
153        #[primary_span]
154        span: Span,
155        name: Symbol,
156    }
157
158    impl MissingAssocReft {
159        pub(crate) fn new(span: Span, name: Symbol) -> Self {
160            Self { span, name }
161        }
162    }
163
164    #[derive(Diagnostic)]
165    #[diag(refineck_impl_assoc_reft_final, code = E0999)]
166    pub struct ImplAssocReftOnFinal {
167        #[primary_span]
168        span: Span,
169        name: Symbol,
170    }
171
172    impl ImplAssocReftOnFinal {
173        pub(crate) fn new(span: Span, name: Symbol) -> Self {
174            Self { span, name }
175        }
176    }
177
178    #[derive(Diagnostic)]
179    #[diag(refineck_invalid_assoc_reft, code = E0999)]
180    pub struct InvalidAssocReft {
181        #[primary_span]
182        span: Span,
183        trait_: String,
184        name: Symbol,
185    }
186
187    impl InvalidAssocReft {
188        pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
189            Self { span, trait_, name }
190        }
191    }
192}
flux_refineck/compare_impl_item.rs

flux_refineck/
compare_impl_item.rs
