|
2 | 2 |
|
3 | 3 | use super::super::{Fql, InferredType}; |
4 | 4 | use super::constraint_gen::infer_expr_hm; |
5 | | -use super::unification::solve_equations; |
6 | | -use super::TypeVarId; |
| 5 | +use super::unification::{solve_equations, Substitution}; |
| 6 | +use super::{annotated_to_mono, TypeVarId}; |
7 | 7 | use super::{HMInferenceContext, MonoType}; |
8 | 8 | use crate::diagnostics::TypeInferenceErrorKind; |
9 | | -use crate::{HirInferDatabase, HirInferredModule}; |
| 9 | +use crate::{DefinitionInferenceResult, HirInferDatabase, TypeInferenceError}; |
10 | 10 | use alloy_hir_def as hir; |
11 | | -use alloy_hir_def::{Name, TypeDefinition}; |
12 | | -use alloy_hir_resolved::{resolve_annotated_type, AnnotatedType, EPTdFql, TypeVarReference}; |
| 11 | +use alloy_hir_resolved::resolve_annotated_type; |
13 | 12 | use alloy_workspace::ModuleId; |
14 | 13 | use non_empty_vec::NonEmpty; |
15 | 14 | use rustc_hash::FxHashMap; |
16 | 15 |
|
17 | | -/// Main Hindley-Milner type inference function for a module |
18 | | -/// |
19 | | -/// Uses a single shared HM context for all same-module definitions and |
20 | | -/// expressions, so that call-site constraints flow back to definitions. |
21 | | -/// |
22 | | -/// Cross-module references and same-module definitions with polymorphic type |
23 | | -/// annotations use `infer_value_signature` (a Salsa tracked query) for |
24 | | -/// caching and proper instantiation. |
25 | | -/// |
26 | | -/// 1. Generate constraints for all expressions in a shared context |
27 | | -/// 2. Solve all type equations |
28 | | -/// 3. Generalize polymorphic-annotated definitions |
29 | | -/// 4. Apply substitution and convert to the module result |
30 | | -pub fn infer_types_hm(db: &dyn HirInferDatabase, module_id: ModuleId) -> HirInferredModule { |
31 | | - let mut ctx = HMInferenceContext::new(db, module_id); |
32 | | - let (hir_module, _) = hir::lower_file(db, module_id); |
33 | | - |
34 | | - // Phase 1: Generate constraints for all top-level definitions and bare expressions. |
35 | | - // Value definitions are inferred via their body expression; sub-expressions |
36 | | - // are recursively handled by the constraint generation. |
37 | | - // Set inferring_expr so that infer_expr_hm resolves the body directly |
38 | | - // instead of going through infer_value_signature (which would lose |
39 | | - // sub-expression types and error reporting). |
40 | | - for (&expr_id, value) in hir_module.values() { |
41 | | - ctx.inferring_expr = Some(Fql::new(module_id, expr_id)); |
42 | | - infer_definition_constraints(&mut ctx, db, module_id, expr_id); |
43 | | - ctx.inferring_expr = None; |
44 | | - |
45 | | - // For definitions with polymorphic annotations, store in poly_env. |
46 | | - // This ensures that subsequent references in the shared context get fresh instantiations, preserving let-polymorphism. |
47 | | - if let Some(type_annotation) = value.type_annotation { |
48 | | - let annotated = resolve_annotated_type(db, module_id, type_annotation); |
49 | | - if annotated.is_polymorphic() { |
50 | | - if let Some(anno_mono) = annotated_to_mono(&annotated, &mut ctx) { |
51 | | - let expr_fql = Fql::new(module_id, expr_id); |
52 | | - let poly_ty = super::PolyType::generalize_all(anno_mono); |
53 | | - ctx.poly_env.insert(expr_fql.into(), poly_ty); |
54 | | - } |
55 | | - } |
56 | | - } |
57 | | - } |
| 16 | +#[salsa::tracked(cycle_initial = infer_body_type_cycle_initial)] |
| 17 | +pub(crate) fn infer_body_type<'db>( |
| 18 | + db: &'db dyn HirInferDatabase, |
| 19 | + value_def: hir::ValueDef<'db>, |
| 20 | +) -> DefinitionInferenceResult { |
| 21 | + let module_id = value_def.module_id(db); |
| 22 | + let expr_idx = value_def.expression_idx(db); |
58 | 23 |
|
59 | | - // Also infer bare top-level expressions (not associated with a value definition) |
60 | | - for (expr_id, _expr, _range, _name_scope) in hir_module.expressions() { |
61 | | - if hir_module.get_value_by_id(&expr_id).is_some() { |
62 | | - continue; |
63 | | - } |
64 | | - let expr_fql = Fql::new(module_id, expr_id); |
65 | | - infer_expr_hm(&mut ctx, expr_fql); |
66 | | - } |
| 24 | + let mut ctx = HMInferenceContext::new(db); |
67 | 25 |
|
68 | | - // Phase 2: Solve all type equations |
69 | | - let (substitution, unification_errors) = solve_equations(db, ctx.equations.clone()); |
| 26 | + let expr_fql = Fql::new(module_id, expr_idx); |
| 27 | + ctx.inferring_expr = Some(expr_fql.clone()); |
70 | 28 |
|
71 | | - // Phase 3: Generalize polymorphic-annotated definitions |
72 | | - // Must read from type_env directly (not maybe_find_type) because poly_env |
73 | | - // may contain pre-solving generalizations from Phase 1 — instantiating those |
74 | | - // would produce fresh variables not present in the substitution. |
75 | | - for (&expr_id, _value) in hir_module.values() { |
76 | | - let expr_fql = Fql::new(module_id, expr_id); |
77 | | - let fql_key: EPTdFql = expr_fql.clone().into(); |
| 29 | + let inferred_mono = infer_expr_hm(&mut ctx, expr_fql.clone()); |
78 | 30 |
|
79 | | - if let Some(mono_ty) = ctx.type_env.get(&fql_key).cloned() { |
80 | | - let resolved_ty = substitution.apply(&mono_ty); |
81 | | - ctx.generalize_to_poly(resolved_ty, fql_key); |
| 31 | + if let Some(type_annotation) = value_def.type_annotation(db) { |
| 32 | + let annotated = resolve_annotated_type(db, module_id, type_annotation); |
| 33 | + if !annotated.is_polymorphic() { |
| 34 | + if let Some(annotated_mono) = annotated_to_mono(&annotated, &mut ctx) { |
| 35 | + ctx.add_equation(inferred_mono, annotated_mono, expr_fql); |
| 36 | + } |
82 | 37 | } |
83 | 38 | } |
84 | 39 |
|
85 | | - // Phase 4: Apply substitution and collect results |
86 | | - let mut result = HirInferredModule::empty(module_id); |
87 | | - |
88 | | - let mut type_var_map: FxHashMap<TypeVarId, usize> = FxHashMap::default(); |
89 | | - let mut next_generic_id = 0; |
90 | | - |
91 | | - for (fql, poly_type) in &ctx.poly_env { |
92 | | - let mono_ty = substitution.apply(&poly_type.body); |
93 | | - let resolved_type = |
94 | | - mono_to_resolved_with_map(&mono_ty, &mut type_var_map, &mut next_generic_id); |
95 | | - result.insert_type(fql.clone(), resolved_type); |
96 | | - } |
97 | | - |
98 | | - for (fql, mono_type) in &ctx.type_env { |
99 | | - let mono_ty = substitution.apply(mono_type); |
100 | | - let resolved_type = |
101 | | - mono_to_resolved_with_map(&mono_ty, &mut type_var_map, &mut next_generic_id); |
102 | | - result.insert_type(fql.clone(), resolved_type); |
103 | | - } |
104 | | - |
105 | | - for err in ctx.resolution_errors { |
106 | | - let range = err.get_range(db); |
107 | | - result.error(TypeInferenceErrorKind::HirResolutionError(err), range); |
108 | | - } |
| 40 | + let (substitution, unification_errors) = solve_equations(db, ctx.equations.clone()); |
109 | 41 |
|
110 | | - for err in unification_errors { |
111 | | - result.push_error(err); |
112 | | - } |
| 42 | + collect_inference_results( |
| 43 | + &mut ctx, |
| 44 | + substitution, |
| 45 | + unification_errors, |
| 46 | + module_id, |
| 47 | + Some(Fql::new(module_id, expr_idx)), |
| 48 | + ) |
| 49 | +} |
113 | 50 |
|
114 | | - result |
| 51 | +fn infer_body_type_cycle_initial( |
| 52 | + _db: &dyn HirInferDatabase, |
| 53 | + _id: salsa::Id, |
| 54 | + _value_def: hir::ValueDef, |
| 55 | +) -> DefinitionInferenceResult { |
| 56 | + DefinitionInferenceResult::empty() |
115 | 57 | } |
116 | 58 |
|
117 | | -/// Run constraint generation for a single value definition. |
118 | | -/// |
119 | | -/// Generates constraints for the body expression and adds annotation |
120 | | -/// constraints if a non-polymorphic type annotation is present. |
121 | | -fn infer_definition_constraints( |
122 | | - ctx: &mut HMInferenceContext, |
| 59 | +pub(crate) fn infer_expressions( |
123 | 60 | db: &dyn HirInferDatabase, |
124 | 61 | module_id: ModuleId, |
125 | | - expr_id: hir::ExpressionIdx, |
126 | | -) { |
127 | | - let expr_fql = Fql::new(module_id, expr_id); |
128 | | - infer_expr_hm(ctx, expr_fql.clone()); |
129 | | - |
130 | | - if let Some(value_def) = hir::module_value_def(db, module_id, expr_id) { |
131 | | - if let Some(type_annotation) = value_def.type_annotation(db) { |
132 | | - if let Some(inferred_mono_ty) = ctx.maybe_find_type(&expr_fql) { |
133 | | - let annotated = resolve_annotated_type(db, module_id, type_annotation); |
134 | | - if !annotated.is_polymorphic() { |
135 | | - if let Some(annotated_mono) = annotated_to_mono(&annotated, ctx) { |
136 | | - ctx.add_equation(inferred_mono_ty, annotated_mono, expr_fql); |
137 | | - } |
138 | | - } |
139 | | - } |
| 62 | +) -> DefinitionInferenceResult { |
| 63 | + let (hir_module, _) = hir::lower_file(db, module_id); |
| 64 | + |
| 65 | + // Handle bare top-level expressions (not bound to a value definition). |
| 66 | + // Use a single shared context so that the `maybe_find_type` cache prevents |
| 67 | + // sub-expressions from being inferred multiple times. |
| 68 | + let mut ctx = HMInferenceContext::new(db); |
| 69 | + for (expr_id, _, _, _) in hir_module.expressions() { |
| 70 | + if hir::module_value_def(db, module_id, expr_id).is_some() { |
| 71 | + continue; |
140 | 72 | } |
| 73 | + let expr_fql = Fql::new(module_id, expr_id); |
| 74 | + infer_expr_hm(&mut ctx, expr_fql); |
141 | 75 | } |
| 76 | + let (bare_substitution, bare_unification_errors) = solve_equations(db, ctx.equations.clone()); |
| 77 | + |
| 78 | + collect_inference_results( |
| 79 | + &mut ctx, |
| 80 | + bare_substitution, |
| 81 | + bare_unification_errors, |
| 82 | + module_id, |
| 83 | + None, |
| 84 | + ) |
142 | 85 | } |
143 | 86 |
|
144 | | -/// Infer the type of a single definition's body in isolation. |
145 | | -/// |
146 | | -/// Creates a fresh HM inference context, runs constraint generation on the body, |
147 | | -/// solves equations, and returns the inferred type. |
| 87 | +/// Collect inference results from a completed inference context. |
148 | 88 | /// |
149 | | -/// This is a Salsa tracked query keyed on ValueDef. Thanks to field-level tracking, |
150 | | -/// it only re-runs when `expression_idx` changes (not when `name` or `type_annotation` change). |
151 | | -#[salsa::tracked(cycle_initial = infer_body_type_cycle_initial)] |
152 | | -pub(super) fn infer_body_type<'db>( |
153 | | - db: &'db dyn HirInferDatabase, |
154 | | - value_def: hir::ValueDef<'db>, |
155 | | -) -> InferredType { |
156 | | - let module_id = value_def.module_id(db); |
157 | | - let expr_idx = value_def.expression_idx(db); |
158 | | - |
159 | | - let mut ctx = HMInferenceContext::new(db, module_id); |
160 | | - |
161 | | - // Mark this expression as the one being inferred to prevent cycles: |
162 | | - // infer_expr_hm will skip the infer_value_signature shortcut for this |
163 | | - // expression and instead resolve it directly from its body. |
164 | | - ctx.inferring_expr = Some(Fql::new(module_id, expr_idx)); |
165 | | - |
166 | | - infer_definition_constraints(&mut ctx, db, module_id, expr_idx); |
167 | | - |
168 | | - let (substitution, _) = solve_equations(db, ctx.equations.clone()); |
| 89 | +/// Applies the substitution to all types in the context, converts MonoTypes |
| 90 | +/// to InferredTypes, and collects errors. |
| 91 | +fn collect_inference_results( |
| 92 | + ctx: &mut HMInferenceContext<'_>, |
| 93 | + substitution: Substitution, |
| 94 | + unification_errors: Vec<TypeInferenceError>, |
| 95 | + module_id: ModuleId, |
| 96 | + definition_fql: Option<Fql<hir::Expression>>, |
| 97 | +) -> DefinitionInferenceResult { |
| 98 | + let db = ctx.db; |
| 99 | + let mut type_var_map: FxHashMap<TypeVarId, usize> = FxHashMap::default(); |
| 100 | + let mut next_generic_id = 0; |
169 | 101 |
|
170 | | - let fql_key: EPTdFql = Fql::new(module_id, expr_idx).into(); |
171 | | - if let Some(mono_ty) = ctx.type_env.get(&fql_key) { |
172 | | - let resolved_ty = substitution.apply(mono_ty); |
173 | | - let mut type_var_map = FxHashMap::default(); |
174 | | - let mut next_id = 0; |
175 | | - mono_to_resolved_with_map(&resolved_ty, &mut type_var_map, &mut next_id) |
176 | | - } else { |
177 | | - InferredType::Unconstrained |
| 102 | + // Get the definition type from type_env |
| 103 | + let definition_type = { |
| 104 | + if let Some(def_fql) = definition_fql { |
| 105 | + if let Some(mono_ty) = ctx.type_env.get(&def_fql.into()) { |
| 106 | + let resolved_ty = substitution.apply(mono_ty); |
| 107 | + mono_to_resolved_with_map(&resolved_ty, &mut type_var_map, &mut next_generic_id) |
| 108 | + } else { |
| 109 | + InferredType::Unconstrained |
| 110 | + } |
| 111 | + } else { |
| 112 | + InferredType::Unconstrained |
| 113 | + } |
| 114 | + }; |
| 115 | + |
| 116 | + let mut result = DefinitionInferenceResult::empty(); |
| 117 | + |
| 118 | + let poly_bodies = ctx.poly_env.iter().map(|(fql, poly)| (fql, &poly.body)); |
| 119 | + let mono_bodies = ctx.type_env.iter().map(|(fql, mono)| (fql, mono)); |
| 120 | + |
| 121 | + poly_bodies |
| 122 | + .chain(mono_bodies) |
| 123 | + .filter(|(fql, _)| fql.module_id() == module_id) |
| 124 | + .map(|(fql, mono)| (fql.clone(), substitution.apply(mono))) |
| 125 | + .map(|(fql, mono)| { |
| 126 | + ( |
| 127 | + fql, |
| 128 | + mono_to_resolved_with_map(&mono, &mut type_var_map, &mut next_generic_id), |
| 129 | + ) |
| 130 | + }) |
| 131 | + .for_each(|(fql, resolved)| result.insert_type(fql, resolved)); |
| 132 | + |
| 133 | + let resolution_errors = ctx |
| 134 | + .resolution_errors |
| 135 | + .iter() |
| 136 | + .map(|err| { |
| 137 | + let range = err.get_range(db); |
| 138 | + TypeInferenceError::new( |
| 139 | + TypeInferenceErrorKind::HirResolutionError(err.clone()), |
| 140 | + range, |
| 141 | + ) |
| 142 | + }) |
| 143 | + .collect::<Vec<_>>(); |
| 144 | + result.extend_errors(&resolution_errors); |
| 145 | + result.extend_errors(&unification_errors); |
| 146 | + |
| 147 | + DefinitionInferenceResult { |
| 148 | + definition_type, |
| 149 | + ..result |
178 | 150 | } |
179 | 151 | } |
180 | 152 |
|
181 | | -fn infer_body_type_cycle_initial( |
182 | | - _db: &dyn HirInferDatabase, |
183 | | - _id: salsa::Id, |
184 | | - _value_def: hir::ValueDef, |
185 | | -) -> InferredType { |
186 | | - InferredType::Unconstrained |
187 | | -} |
188 | | - |
189 | 153 | /// Convert a MonoType to a ResolvedType with a shared type variable mapping |
190 | 154 | /// This ensures that the same TypeVarId gets the same Generic ID across all |
191 | 155 | /// expressions and patterns in a module, preserving polymorphic type structure |
|
0 commit comments