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

flux_refineck/
compare_impl_item.rs
