Skip to main content

aver/types/checker/
mod.rs

1/// Aver static type checker.
2///
3/// Two-phase analysis:
4///   Phase 1 — build a signature table from all FnDef nodes and builtins.
5///   Phase 2 — check top-level statements, then each FnDef for call-site
6///              argument types, return type, BinOp compatibility, and effects.
7///
8/// The checker keeps gradual typing for nested placeholders, but applies
9/// stricter rules for checker constraints: a bare `Unknown` does not satisfy
10/// a concrete expected type in argument/return/ascription checks.
11use std::collections::{HashMap, HashSet};
12
13use super::{Type, parse_type_str_strict};
14use crate::ast::{
15    BinOp, Expr, FnDef, Literal, Module, Pattern, Spanned, Stmt, TailCallData, TopLevel, TypeDef,
16};
17
18mod builtins;
19pub mod effect_classification;
20pub mod effect_lifting;
21mod exhaustiveness;
22mod flow;
23pub mod hostile_effects;
24pub mod hostile_values;
25mod infer;
26mod memo;
27mod modules;
28pub mod oracle_subtypes;
29pub mod proof_trust_header;
30
31#[cfg(test)]
32mod tests;
33
34// ---------------------------------------------------------------------------
35// Public API
36// ---------------------------------------------------------------------------
37
38#[derive(Debug, Clone)]
39pub struct TypeError {
40    pub message: String,
41    pub line: usize,
42    pub col: usize,
43    /// Optional secondary span for multi-region diagnostics (e.g. declared type vs actual return).
44    pub secondary: Option<TypeErrorSpan>,
45}
46
47#[derive(Debug, Clone)]
48pub struct TypeErrorSpan {
49    pub line: usize,
50    pub col: usize,
51    pub label: String,
52}
53
54/// Result of type-checking that also carries memo-safety metadata.
55#[derive(Debug)]
56pub struct TypeCheckResult {
57    pub errors: Vec<TypeError>,
58    /// For each user-defined fn: (param_types, return_type, effects).
59    /// Used by the memo system to decide which fns qualify.
60    pub fn_sigs: HashMap<String, (Vec<Type>, Type, Vec<String>)>,
61    /// Set of type names whose values are memo-safe (hashable scalars / records of scalars).
62    pub memo_safe_types: HashSet<String>,
63    /// Unused binding warnings: (binding_name, fn_name, line).
64    pub unused_bindings: Vec<(String, String, usize)>,
65}
66
67pub fn run_type_check(items: &[TopLevel]) -> Vec<TypeError> {
68    run_type_check_with_base(items, None)
69}
70
71pub fn run_type_check_with_base(items: &[TopLevel], base_dir: Option<&str>) -> Vec<TypeError> {
72    run_type_check_full(items, base_dir).errors
73}
74
75pub fn run_type_check_full(items: &[TopLevel], base_dir: Option<&str>) -> TypeCheckResult {
76    let mut checker = TypeChecker::new();
77    checker.check(items, base_dir);
78    finalize_check_result(checker, items)
79}
80
81/// Variant of [`run_type_check_full`] that uses pre-loaded dependency
82/// modules instead of resolving them from disk. The playground feeds
83/// this from its in-memory virtual fs so multi-file projects type-
84/// check without any filesystem access.
85pub fn run_type_check_with_loaded(
86    items: &[TopLevel],
87    loaded: &[crate::source::LoadedModule],
88) -> TypeCheckResult {
89    let mut checker = TypeChecker::new();
90    checker.check_with_loaded(items, loaded);
91    finalize_check_result(checker, items)
92}
93
94fn finalize_check_result(mut checker: TypeChecker, items: &[TopLevel]) -> TypeCheckResult {
95    let fn_sigs: HashMap<String, (Vec<Type>, Type, Vec<String>)> = checker
96        .fn_sigs
97        .iter()
98        .map(|(k, v)| {
99            (
100                k.clone(),
101                (v.params.clone(), v.ret.clone(), v.effects.clone()),
102            )
103        })
104        .collect();
105
106    let memo_safe_types = checker.compute_memo_safe_types(items);
107
108    check_module_effect_boundary(items, &mut checker.errors);
109
110    TypeCheckResult {
111        errors: checker.errors,
112        fn_sigs,
113        memo_safe_types,
114        unused_bindings: checker.unused_warnings,
115    }
116}
117
118/// Enforce module-level `effects [...]` declaration against per-fn effect
119/// usage. The rule:
120///
121/// - Module without `effects [...]` → legacy/mixed, no enforcement (0.13
122///   migration shim; 0.14+ may upgrade to soft warning).
123/// - Module with `effects [...]` (including `effects []` for explicit pure)
124///   → every function's `! [...]` must be covered by the module's declared
125///   surface. A namespace-level entry like `Disk` admits any `Disk.*`
126///   method; a method-level entry like `Time.now` admits only that one.
127fn check_module_effect_boundary(items: &[TopLevel], errors: &mut Vec<TypeError>) {
128    let Some(allowed) = items.iter().find_map(|i| match i {
129        TopLevel::Module(m) => m.effects.as_ref().map(|e| (e, m)),
130        _ => None,
131    }) else {
132        return;
133    };
134    let (allowed_list, module) = allowed;
135
136    let allowed_namespaces: HashSet<&str> = allowed_list
137        .iter()
138        .filter(|e| !e.contains('.'))
139        .map(|e| e.as_str())
140        .collect();
141    let allowed_methods: HashSet<&str> = allowed_list.iter().map(|e| e.as_str()).collect();
142
143    for item in items {
144        let TopLevel::FnDef(fd) = item else { continue };
145        for eff in &fd.effects {
146            let method = eff.node.as_str();
147            if allowed_methods.contains(method) {
148                continue;
149            }
150            if let Some((ns, _)) = method.split_once('.')
151                && allowed_namespaces.contains(ns)
152            {
153                continue;
154            }
155            errors.push(TypeError {
156                message: format!(
157                    "module '{}' declared `effects [{}]` but '{}' uses '{}' which is not in the declared boundary",
158                    module.name,
159                    allowed_list.join(", "),
160                    fd.name,
161                    method
162                ),
163                line: eff.line,
164                col: 1,
165                secondary: module.effects_line.map(|l| TypeErrorSpan {
166                    line: l,
167                    col: 1,
168                    label: "module effects declared here".to_string(),
169                }),
170            });
171        }
172    }
173}
174
175// ---------------------------------------------------------------------------
176// Internal structures
177// ---------------------------------------------------------------------------
178
179#[derive(Debug, Clone)]
180struct FnSig {
181    params: Vec<Type>,
182    ret: Type,
183    effects: Vec<String>,
184}
185
186struct TypeChecker {
187    fn_sigs: HashMap<String, FnSig>,
188    value_members: HashMap<String, Type>,
189    /// Field types for record types: "TypeName.fieldName" → Type.
190    /// Populated for both user-defined `record` types and built-in records
191    /// (HttpResponse, Header). Enables checked dot-access on Named types.
192    record_field_types: HashMap<String, Type>,
193    /// Unqualified → qualified aliases for cross-module lookups.
194    /// E.g. "Shape.Circle" → "Data.Shape.Circle".
195    sig_aliases: HashMap<String, String>,
196    /// Variant names for sum types: "Shape" → ["Circle", "Rect", "Point"].
197    /// Pre-populated for Result and Option; extended by user-defined sum types.
198    type_variants: HashMap<String, Vec<String>>,
199    /// Top-level bindings visible from function bodies.
200    globals: HashMap<String, Type>,
201    /// Local bindings in the current function/scope.
202    locals: HashMap<String, Type>,
203    errors: Vec<TypeError>,
204    /// Return type of the function currently being checked; None at top level.
205    current_fn_ret: Option<Type>,
206    /// Line number of the function currently being checked; None at top level.
207    current_fn_line: Option<usize>,
208    /// Type names that are opaque in this module's context (imported via `exposes opaque`).
209    opaque_types: HashSet<String>,
210    /// Names referenced during type checking of current function body (for unused detection).
211    used_names: HashSet<String>,
212    /// Bindings defined in the current function body: (name, line).
213    fn_bindings: Vec<(String, usize)>,
214    /// Unused binding warnings collected during checking: (binding_name, fn_name, line).
215    unused_warnings: Vec<(String, String, usize)>,
216    /// Oracle v1: `.result` / `.trace` / `.trace.*` projections are
217    /// only meaningful inside `verify <fn> trace` cases. This flag is
218    /// set true while checking such a case's LHS / RHS, false
219    /// otherwise. Outside verify-trace the projections are rejected at
220    /// check time — otherwise user code would type-check then crash
221    /// at runtime with "namespace has no member 'trace'".
222    in_verify_trace_context: bool,
223}
224
225impl TypeChecker {
226    fn new() -> Self {
227        let mut type_variants = HashMap::new();
228        type_variants.insert(
229            "Result".to_string(),
230            vec!["Ok".to_string(), "Err".to_string()],
231        );
232        type_variants.insert(
233            "Option".to_string(),
234            vec!["Some".to_string(), "None".to_string()],
235        );
236
237        let mut tc = TypeChecker {
238            fn_sigs: HashMap::new(),
239            value_members: HashMap::new(),
240            record_field_types: HashMap::new(),
241            sig_aliases: HashMap::new(),
242            type_variants,
243            globals: HashMap::new(),
244            locals: HashMap::new(),
245            errors: Vec::new(),
246            current_fn_ret: None,
247            current_fn_line: None,
248            opaque_types: HashSet::new(),
249            used_names: HashSet::new(),
250            fn_bindings: Vec::new(),
251            unused_warnings: Vec::new(),
252            in_verify_trace_context: false,
253        };
254        tc.register_builtins();
255        tc
256    }
257
258    // -- Alias-aware lookups ------------------------------------------------
259
260    fn find_fn_sig(&self, key: &str) -> Option<&FnSig> {
261        self.fn_sigs
262            .get(key)
263            .or_else(|| self.sig_aliases.get(key).and_then(|c| self.fn_sigs.get(c)))
264    }
265
266    fn find_value_member(&self, key: &str) -> Option<&Type> {
267        self.value_members.get(key).or_else(|| {
268            self.sig_aliases
269                .get(key)
270                .and_then(|c| self.value_members.get(c))
271        })
272    }
273
274    fn find_record_field_type(&self, key: &str) -> Option<&Type> {
275        self.record_field_types.get(key).or_else(|| {
276            self.sig_aliases
277                .get(key)
278                .and_then(|c| self.record_field_types.get(c))
279        })
280    }
281
282    // -- Helpers -----------------------------------------------------------
283
284    /// Check whether `required_effect` is satisfied by `caller_effects`.
285    fn caller_has_effect(&self, caller_effects: &[String], required_effect: &str) -> bool {
286        caller_effects
287            .iter()
288            .any(|declared| crate::effects::effect_satisfies(declared, required_effect))
289    }
290
291    fn error(&mut self, msg: impl Into<String>) {
292        let line = self.current_fn_line.unwrap_or(1);
293        self.errors.push(TypeError {
294            message: msg.into(),
295            line,
296            col: 0,
297            secondary: None,
298        });
299    }
300
301    fn error_at_line(&mut self, line: usize, msg: impl Into<String>) {
302        self.errors.push(TypeError {
303            message: msg.into(),
304            line,
305            col: 0,
306            secondary: None,
307        });
308    }
309
310    fn insert_sig(&mut self, name: &str, params: &[Type], ret: Type, effects: &[&str]) {
311        self.fn_sigs.insert(
312            name.to_string(),
313            FnSig {
314                params: params.to_vec(),
315                ret,
316                effects: effects.iter().map(|s| s.to_string()).collect(),
317            },
318        );
319    }
320
321    fn fn_type_from_sig(sig: &FnSig) -> Type {
322        Type::Fn(
323            sig.params.clone(),
324            Box::new(sig.ret.clone()),
325            sig.effects.clone(),
326        )
327    }
328
329    fn sig_from_callable_type(ty: &Type) -> Option<FnSig> {
330        match ty {
331            Type::Fn(params, ret, effects) => Some(FnSig {
332                params: params.clone(),
333                ret: *ret.clone(),
334                effects: effects.clone(),
335            }),
336            _ => None,
337        }
338    }
339
340    fn binding_type(&self, name: &str) -> Option<Type> {
341        self.locals
342            .get(name)
343            .or_else(|| self.globals.get(name))
344            .cloned()
345    }
346
347    /// Compatibility used for checker constraints (call args, returns, ascriptions).
348    ///
349    /// We keep gradual typing for nested placeholders (`Result<Int, Unknown>` can
350    /// still fit `Result<Int, String>`), but reject *bare* `Unknown` when a
351    /// concrete type is required. This closes common false negatives where an
352    /// unresolved expression silently passes a concrete signature.
353    pub(super) fn constraint_compatible(actual: &Type, expected: &Type) -> bool {
354        if matches!(actual, Type::Unknown) && !matches!(expected, Type::Unknown) {
355            return false;
356        }
357        actual.compatible(expected)
358    }
359}