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_reft) = trait_assoc_refts.find(name) {
57            check_assoc_reft(
58                &mut infcx,
59                impl_id,
60                &impl_trait_ref,
61                trait_assoc_reft.def_id(),
62                impl_assoc_reft.def_id(),
63            )?;
64        } else {
65            let fhir_impl_assoc_reft = genv
66                .fhir_expect_item(impl_id.local_id())?
67                .expect_impl()
68                .find_assoc_reft(name)
69                .unwrap();
70            Err(genv.emit(errors::InvalidAssocReft::new(
71                fhir_impl_assoc_reft.span,
72                name,
73                def_id_to_string(trait_id),
74            )))?;
75        }
76    }
77
78    Ok(())
79}
80
81fn check_assoc_reft(
82    infcx: &mut InferCtxt,
83    impl_id: MaybeExternId,
84    impl_trait_ref: &TraitRef,
85    trait_assoc_id: FluxDefId,
86    impl_assoc_id: FluxDefId,
87) -> QueryResult {
88    debug_assert_eq!(trait_assoc_id.name(), impl_assoc_id.name());
89
90    let impl_span = infcx
91        .genv
92        .fhir_expect_item(impl_id.local_id())?
93        .expect_impl()
94        .find_assoc_reft(impl_assoc_id.name())
95        .unwrap()
96        .span;
97
98    let impl_sort = infcx
99        .genv
100        .sort_of_assoc_reft(impl_assoc_id)?
101        .instantiate_identity()
102        .normalize_projections(&mut infcx.at(impl_span))?;
103
104    let trait_sort = infcx.genv.sort_of_assoc_reft(trait_assoc_id)?;
105    let trait_sort = trait_sort.instantiate(infcx.tcx(), &impl_trait_ref.args, &[]);
106    let trait_sort = trait_sort.normalize_projections(&mut infcx.at(impl_span))?;
107
108    if impl_sort != trait_sort {
109        Err(infcx.genv.emit(errors::IncompatibleSort::new(
110            impl_span,
111            impl_assoc_id.name(),
112            trait_sort,
113            impl_sort,
114        )))?;
115    }
116
117    Ok(())
118}
119
120pub(crate) mod errors {
121    use flux_errors::E0999;
122    use flux_macros::Diagnostic;
123    use flux_middle::rty;
124    use rustc_span::{Span, Symbol};
125
126    #[derive(Diagnostic)]
127    #[diag(refineck_incompatible_sort, code = E0999)]
128    pub(super) struct IncompatibleSort {
129        #[primary_span]
130        #[label]
131        span: Span,
132        name: Symbol,
133        expected: rty::FuncSort,
134        found: rty::FuncSort,
135    }
136
137    impl IncompatibleSort {
138        pub(super) fn new(
139            span: Span,
140            name: Symbol,
141            expected: rty::FuncSort,
142            found: rty::FuncSort,
143        ) -> Self {
144            Self { span, name, expected, found }
145        }
146    }
147
148    #[derive(Diagnostic)]
149    #[diag(refineck_missing_assoc_reft, code = E0999)]
150    pub struct MissingAssocReft {
151        #[primary_span]
152        span: Span,
153        name: Symbol,
154    }
155
156    impl MissingAssocReft {
157        pub(crate) fn new(span: Span, name: Symbol) -> Self {
158            Self { span, name }
159        }
160    }
161
162    #[derive(Diagnostic)]
163    #[diag(refineck_impl_assoc_reft_final, code = E0999)]
164    pub struct ImplAssocReftOnFinal {
165        #[primary_span]
166        span: Span,
167        name: Symbol,
168    }
169
170    impl ImplAssocReftOnFinal {
171        pub(crate) fn new(span: Span, name: Symbol) -> Self {
172            Self { span, name }
173        }
174    }
175
176    #[derive(Diagnostic)]
177    #[diag(refineck_invalid_assoc_reft, code = E0999)]
178    pub struct InvalidAssocReft {
179        #[primary_span]
180        span: Span,
181        trait_: String,
182        name: Symbol,
183    }
184
185    impl InvalidAssocReft {
186        pub(crate) fn new(span: Span, name: Symbol, trait_: String) -> Self {
187            Self { span, trait_, name }
188        }
189    }
190}
flux_refineck/compare_impl_item.rs

flux_refineck/
compare_impl_item.rs
