logicaffeine_compile/analysis/
unify.rs

1//! Unification engine for the bidirectional type checker.
2//!
3//! Provides Robinson unification for [`InferType`], which extends [`LogosType`]
4//! with type variables for the inference pass. After inference, [`UnificationTable::zonk`]
5//! converts `InferType → LogosType`. Unsolved variables become `LogosType::Unknown`,
6//! preserving the existing codegen safety net.
7//!
8//! # Architecture
9//!
10//! ```text
11//! InferType  ←  inference pass (this module + check.rs)
12//!     │
13//!     │  zonk (after inference)
14//!     ▼
15//! LogosType  →  codegen (unchanged)
16//! ```
17
18use std::collections::HashMap;
19
20use crate::intern::{Interner, Symbol};
21use crate::analysis::{FieldType, LogosType};
22
23// ============================================================================
24// Core types
25// ============================================================================
26
27/// A type variable used during inference.
28#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
29pub struct TyVar(pub u32);
30
31/// Inference-time type representation.
32///
33/// Extends [`LogosType`] with:
34/// - [`InferType::Var`] — an unbound type variable
35/// - [`InferType::Function`] — a function type (not needed in codegen)
36/// - [`InferType::Unknown`] — propagated uncertainty (unifies with anything)
37#[derive(Clone, PartialEq, Debug)]
38pub enum InferType {
39    // Ground types mirroring LogosType
40    Int,
41    Float,
42    Bool,
43    Char,
44    Byte,
45    String,
46    Unit,
47    Nat,
48    Rational,
49    Duration,
50    Date,
51    Moment,
52    Time,
53    Span,
54    Seq(Box<InferType>),
55    Map(Box<InferType>, Box<InferType>),
56    Set(Box<InferType>),
57    Option(Box<InferType>),
58    UserDefined(Symbol),
59    // Inference-only types
60    Var(TyVar),
61    Function(Vec<InferType>, Box<InferType>),
62    Unknown,
63}
64
65/// A type error detected during unification or checking.
66#[derive(Debug, Clone)]
67pub enum TypeError {
68    Mismatch { expected: InferType, found: InferType },
69    InfiniteType { var: TyVar, ty: InferType },
70    ArityMismatch { expected: usize, found: usize },
71    FieldNotFound { type_name: Symbol, field_name: Symbol },
72    NotAFunction { found: InferType },
73    /// Dimension-incoherent quantity arithmetic (`2 meters + 1 gram`) caught statically by the
74    /// [`crate::analysis::dimension_check::DimensionChecker`]. Carries its own ready message.
75    DimensionMismatch { message: std::string::String },
76}
77
78impl TypeError {
79    pub fn expected_str(&self) -> std::string::String {
80        match self {
81            TypeError::Mismatch { expected, .. } => expected.to_logos_name(),
82            TypeError::ArityMismatch { expected, .. } => format!("{} arguments", expected),
83            TypeError::FieldNotFound { .. } => "a known field".to_string(),
84            TypeError::NotAFunction { .. } => "a function".to_string(),
85            TypeError::InfiniteType { .. } => "a finite type".to_string(),
86            TypeError::DimensionMismatch { .. } => "a matching dimension".to_string(),
87        }
88    }
89
90    pub fn found_str(&self) -> std::string::String {
91        match self {
92            TypeError::Mismatch { found, .. } => found.to_logos_name(),
93            TypeError::ArityMismatch { found, .. } => format!("{} arguments", found),
94            TypeError::FieldNotFound { field_name, .. } => format!("{:?}", field_name),
95            TypeError::NotAFunction { found } => found.to_logos_name(),
96            TypeError::InfiniteType { ty, .. } => ty.to_logos_name(),
97            TypeError::DimensionMismatch { message } => message.clone(),
98        }
99    }
100
101    /// Convert this TypeError into a `ParseErrorKind` for user-facing reporting.
102    ///
103    /// Uses `interner` to resolve symbol names (field names, type names) into strings.
104    pub fn to_parse_error_kind(
105        &self,
106        interner: &crate::intern::Interner,
107    ) -> crate::error::ParseErrorKind {
108        use crate::error::ParseErrorKind;
109        match self {
110            TypeError::Mismatch { expected, found } => ParseErrorKind::TypeMismatchDetailed {
111                expected: expected.to_logos_name(),
112                found: found.to_logos_name(),
113                context: String::new(),
114            },
115            TypeError::InfiniteType { var, ty } => ParseErrorKind::InfiniteType {
116                var_description: format!("type variable α{}", var.0),
117                type_description: ty.to_logos_name(),
118            },
119            TypeError::ArityMismatch { expected, found } => ParseErrorKind::ArityMismatch {
120                function: String::from("function"),
121                expected: *expected,
122                found: *found,
123            },
124            TypeError::FieldNotFound { type_name, field_name } => ParseErrorKind::FieldNotFound {
125                type_name: interner.resolve(*type_name).to_string(),
126                field_name: interner.resolve(*field_name).to_string(),
127                available: vec![],
128            },
129            TypeError::NotAFunction { found } => ParseErrorKind::NotAFunction {
130                found_type: found.to_logos_name(),
131            },
132            TypeError::DimensionMismatch { message } => ParseErrorKind::Custom(message.clone()),
133        }
134    }
135}
136
137// ============================================================================
138// Unification table
139// ============================================================================
140
141/// A quantified polymorphic type.
142///
143/// Stores a set of bound type variables and a body type that may reference them.
144/// Used for generic function signatures: `forall [T]. T -> T`.
145#[derive(Clone, Debug)]
146pub struct TypeScheme {
147    /// The bound type variables (one per generic type parameter).
148    pub vars: Vec<TyVar>,
149    /// The body type, which may contain `InferType::Var(tv)` for each `tv` in `vars`.
150    pub body: InferType,
151}
152
153/// Union-Find table implementing Robinson unification with occurs check.
154///
155/// Type variables are allocated by `fresh` and resolved by `find`.
156/// `zonk` fully resolves a type after inference, converting remaining
157/// unbound variables to [`InferType::Unknown`] (which maps to `LogosType::Unknown`).
158pub struct UnificationTable {
159    bindings: Vec<Option<InferType>>,
160    next_id: u32,
161}
162
163impl UnificationTable {
164    pub fn new() -> Self {
165        Self {
166            bindings: Vec::new(),
167            next_id: 0,
168        }
169    }
170
171    /// Allocate a fresh unbound type variable, returning the wrapped `InferType`.
172    pub fn fresh(&mut self) -> InferType {
173        let id = self.next_id;
174        self.next_id += 1;
175        self.bindings.push(None);
176        InferType::Var(TyVar(id))
177    }
178
179    /// Allocate a fresh unbound type variable, returning the raw `TyVar`.
180    pub fn fresh_var(&mut self) -> TyVar {
181        let id = self.next_id;
182        self.next_id += 1;
183        self.bindings.push(None);
184        TyVar(id)
185    }
186
187    /// Instantiate a `TypeScheme` by replacing each quantified variable with a fresh one.
188    ///
189    /// Each call site of a generic function gets independent fresh variables so that
190    /// two calls to `identity(42)` and `identity(true)` do not interfere.
191    pub fn instantiate(&mut self, scheme: &TypeScheme) -> InferType {
192        if scheme.vars.is_empty() {
193            return scheme.body.clone();
194        }
195        let subst: HashMap<TyVar, TyVar> = scheme.vars.iter()
196            .map(|&old_tv| (old_tv, self.fresh_var()))
197            .collect();
198        self.substitute_vars(&scheme.body, &subst)
199    }
200
201    /// Substitute type variables according to `subst`, walking the type recursively.
202    fn substitute_vars(&self, ty: &InferType, subst: &HashMap<TyVar, TyVar>) -> InferType {
203        match ty {
204            InferType::Var(tv) => {
205                let resolved = self.find(*tv);
206                match &resolved {
207                    InferType::Var(rtv) => {
208                        if let Some(&new_tv) = subst.get(rtv) {
209                            InferType::Var(new_tv)
210                        } else {
211                            InferType::Var(*rtv)
212                        }
213                    }
214                    other => self.substitute_vars(&other.clone(), subst),
215                }
216            }
217            InferType::Seq(inner) => InferType::Seq(Box::new(self.substitute_vars(inner, subst))),
218            InferType::Map(k, v) => InferType::Map(
219                Box::new(self.substitute_vars(k, subst)),
220                Box::new(self.substitute_vars(v, subst)),
221            ),
222            InferType::Set(inner) => InferType::Set(Box::new(self.substitute_vars(inner, subst))),
223            InferType::Option(inner) => InferType::Option(Box::new(self.substitute_vars(inner, subst))),
224            InferType::Function(params, ret) => InferType::Function(
225                params.iter().map(|p| self.substitute_vars(p, subst)).collect(),
226                Box::new(self.substitute_vars(ret, subst)),
227            ),
228            other => other.clone(),
229        }
230    }
231
232    /// Follow the binding chain for a type variable (iterative, no path compression).
233    pub fn find(&self, tv: TyVar) -> InferType {
234        let mut current = tv;
235        loop {
236            match &self.bindings[current.0 as usize] {
237                None => return InferType::Var(current),
238                Some(InferType::Var(tv2)) => current = *tv2,
239                Some(ty) => return ty.clone(),
240            }
241        }
242    }
243
244    /// Walk the top level of a type: if it's a bound variable, resolve one step.
245    fn walk(&self, ty: &InferType) -> InferType {
246        match ty {
247            InferType::Var(tv) => self.find(*tv),
248            other => other.clone(),
249        }
250    }
251
252    /// Resolve type variables, keeping unbound variables as `Var(tv)`.
253    ///
254    /// Unlike `zonk`, this does not convert unbound variables to `Unknown`.
255    /// Use this during inference to preserve generic type params as `Var(tv)`
256    /// so they can be unified at call sites.
257    pub fn resolve(&self, ty: &InferType) -> InferType {
258        match ty {
259            InferType::Var(tv) => {
260                let resolved = self.find(*tv);
261                match &resolved {
262                    InferType::Var(_) => resolved, // keep as Var — intentionally unbound
263                    other => self.resolve(&other.clone()),
264                }
265            }
266            InferType::Seq(inner) => InferType::Seq(Box::new(self.resolve(inner))),
267            InferType::Map(k, v) => {
268                InferType::Map(Box::new(self.resolve(k)), Box::new(self.resolve(v)))
269            }
270            InferType::Set(inner) => InferType::Set(Box::new(self.resolve(inner))),
271            InferType::Option(inner) => InferType::Option(Box::new(self.resolve(inner))),
272            InferType::Function(params, ret) => {
273                let params = params.iter().map(|p| self.resolve(p)).collect();
274                InferType::Function(params, Box::new(self.resolve(ret)))
275            }
276            other => other.clone(),
277        }
278    }
279
280    /// Fully resolve all type variables in a type.
281    ///
282    /// Unbound variables become [`InferType::Unknown`], which maps to
283    /// `LogosType::Unknown` when converted by `to_logos_type`.
284    pub fn zonk(&self, ty: &InferType) -> InferType {
285        match ty {
286            InferType::Var(tv) => {
287                let resolved = self.find(*tv);
288                match &resolved {
289                    InferType::Var(_) => InferType::Unknown,
290                    other => self.zonk(other),
291                }
292            }
293            InferType::Seq(inner) => InferType::Seq(Box::new(self.zonk(inner))),
294            InferType::Map(k, v) => {
295                InferType::Map(Box::new(self.zonk(k)), Box::new(self.zonk(v)))
296            }
297            InferType::Set(inner) => InferType::Set(Box::new(self.zonk(inner))),
298            InferType::Option(inner) => InferType::Option(Box::new(self.zonk(inner))),
299            InferType::Function(params, ret) => {
300                let params = params.iter().map(|p| self.zonk(p)).collect();
301                InferType::Function(params, Box::new(self.zonk(ret)))
302            }
303            other => other.clone(),
304        }
305    }
306
307    /// Zonk then convert to `LogosType`. Unsolved variables become `Unknown`.
308    pub fn to_logos_type(&self, ty: &InferType) -> LogosType {
309        let zonked = self.zonk(ty);
310        infer_to_logos(&zonked)
311    }
312
313    /// Unify two types, binding type variables as needed.
314    ///
315    /// Returns `Ok(())` if unification succeeds (bindings may be updated).
316    /// Returns `Err(TypeError)` on a genuine type contradiction.
317    pub fn unify(&mut self, a: &InferType, b: &InferType) -> Result<(), TypeError> {
318        let a = self.walk(a);
319        let b = self.walk(b);
320        self.unify_walked(&a, &b)
321    }
322
323    fn unify_walked(&mut self, a: &InferType, b: &InferType) -> Result<(), TypeError> {
324        match (a, b) {
325            // Same variable: trivially unified
326            (InferType::Var(va), InferType::Var(vb)) if va == vb => Ok(()),
327
328            // Bind a variable to a type
329            (InferType::Var(tv), ty) => {
330                let tv = *tv;
331                let ty = ty.clone();
332                self.occurs_check(tv, &ty)?;
333                self.bindings[tv.0 as usize] = Some(ty);
334                Ok(())
335            }
336            (ty, InferType::Var(tv)) => {
337                let tv = *tv;
338                let ty = ty.clone();
339                self.occurs_check(tv, &ty)?;
340                self.bindings[tv.0 as usize] = Some(ty);
341                Ok(())
342            }
343
344            // Unknown unifies with anything (propagated uncertainty)
345            (InferType::Unknown, _) | (_, InferType::Unknown) => Ok(()),
346
347            // Ground type equality
348            (InferType::Int, InferType::Int) => Ok(()),
349            (InferType::Float, InferType::Float) => Ok(()),
350            (InferType::Bool, InferType::Bool) => Ok(()),
351            (InferType::Char, InferType::Char) => Ok(()),
352            (InferType::Byte, InferType::Byte) => Ok(()),
353            (InferType::String, InferType::String) => Ok(()),
354            (InferType::Unit, InferType::Unit) => Ok(()),
355            (InferType::Nat, InferType::Nat) => Ok(()),
356            (InferType::Duration, InferType::Duration) => Ok(()),
357            (InferType::Date, InferType::Date) => Ok(()),
358            (InferType::Moment, InferType::Moment) => Ok(()),
359            (InferType::Time, InferType::Time) => Ok(()),
360            (InferType::Span, InferType::Span) => Ok(()),
361
362            // Nat embeds into Int for numeric contexts
363            (InferType::Nat, InferType::Int) | (InferType::Int, InferType::Nat) => Ok(()),
364
365            // Byte ↔ Int promotion (numeric literals infer as Int, adapt to Byte in context)
366            (InferType::Byte, InferType::Int) | (InferType::Int, InferType::Byte) => Ok(()),
367
368            // Rational equality + integer embedding: an integer IS an exact rational, so a
369            // `Let x: Rational be 5` (or `… be 7 / 2`, whose `ExactDivide` infers numeric)
370            // unifies against the `Rational` annotation. Mirrors Nat/Byte embedding into Int.
371            (InferType::Rational, InferType::Rational) => Ok(()),
372            (InferType::Rational, InferType::Int | InferType::Nat)
373            | (InferType::Int | InferType::Nat, InferType::Rational) => Ok(()),
374
375            // User-defined types unify if same name
376            (InferType::UserDefined(a), InferType::UserDefined(b)) if a == b => Ok(()),
377
378            // Structural recursion
379            (InferType::Seq(a_inner), InferType::Seq(b_inner)) => {
380                let a_inner = (**a_inner).clone();
381                let b_inner = (**b_inner).clone();
382                self.unify(&a_inner, &b_inner)
383            }
384            (InferType::Set(a_inner), InferType::Set(b_inner)) => {
385                let a_inner = (**a_inner).clone();
386                let b_inner = (**b_inner).clone();
387                self.unify(&a_inner, &b_inner)
388            }
389            (InferType::Option(a_inner), InferType::Option(b_inner)) => {
390                let a_inner = (**a_inner).clone();
391                let b_inner = (**b_inner).clone();
392                self.unify(&a_inner, &b_inner)
393            }
394            (InferType::Map(ak, av), InferType::Map(bk, bv)) => {
395                let ak = (**ak).clone();
396                let bk = (**bk).clone();
397                let av = (**av).clone();
398                let bv = (**bv).clone();
399                self.unify(&ak, &bk)?;
400                self.unify(&av, &bv)
401            }
402            (InferType::Function(a_params, a_ret), InferType::Function(b_params, b_ret)) => {
403                if a_params.len() != b_params.len() {
404                    return Err(TypeError::ArityMismatch {
405                        expected: a_params.len(),
406                        found: b_params.len(),
407                    });
408                }
409                let a_params = a_params.clone();
410                let b_params = b_params.clone();
411                let a_ret = (**a_ret).clone();
412                let b_ret = (**b_ret).clone();
413                for (ap, bp) in a_params.iter().zip(b_params.iter()) {
414                    self.unify(ap, bp)?;
415                }
416                self.unify(&a_ret, &b_ret)
417            }
418
419            // Type mismatch
420            (a, b) => Err(TypeError::Mismatch {
421                expected: a.clone(),
422                found: b.clone(),
423            }),
424        }
425    }
426
427    /// Check that `tv` does not appear in `ty`.
428    ///
429    /// Prevents infinite types like `α = List<α>`.
430    fn occurs_check(&self, tv: TyVar, ty: &InferType) -> Result<(), TypeError> {
431        match ty {
432            InferType::Var(tv2) => {
433                let resolved = self.find(*tv2);
434                match &resolved {
435                    InferType::Var(rtv) => {
436                        if *rtv == tv {
437                            Err(TypeError::InfiniteType { var: tv, ty: ty.clone() })
438                        } else {
439                            Ok(())
440                        }
441                    }
442                    other => self.occurs_check(tv, &other.clone()),
443                }
444            }
445            InferType::Seq(inner) | InferType::Set(inner) | InferType::Option(inner) => {
446                self.occurs_check(tv, inner)
447            }
448            InferType::Map(k, v) => {
449                self.occurs_check(tv, k)?;
450                self.occurs_check(tv, v)
451            }
452            InferType::Function(params, ret) => {
453                for p in params {
454                    self.occurs_check(tv, p)?;
455                }
456                self.occurs_check(tv, ret)
457            }
458            _ => Ok(()),
459        }
460    }
461}
462
463// ============================================================================
464// InferType helpers
465// ============================================================================
466
467impl InferType {
468    /// Convert a `TypeExpr` AST node to `InferType`.
469    ///
470    /// Unlike `LogosType::from_type_expr`, this correctly handles
471    /// `TypeExpr::Function { inputs, output }` by producing
472    /// `InferType::Function(...)` instead of `Unknown`.
473    pub fn from_type_expr(ty: &crate::ast::stmt::TypeExpr, interner: &Interner) -> InferType {
474        Self::from_type_expr_with_params(ty, interner, &HashMap::new())
475    }
476
477    /// Convert a `TypeExpr` to `InferType`, substituting generic type parameters.
478    ///
479    /// When `type_params` maps a name like `T` to a `TyVar`, any `TypeExpr::Primitive(T)`
480    /// or `TypeExpr::Named(T)` in the expression produces `InferType::Var(tv)` instead
481    /// of `Unknown`. This is used for generic function signatures where `T` is a type
482    /// parameter, not a concrete type name.
483    pub fn from_type_expr_with_params(
484        ty: &crate::ast::stmt::TypeExpr,
485        interner: &Interner,
486        type_params: &HashMap<Symbol, TyVar>,
487    ) -> InferType {
488        use crate::ast::stmt::TypeExpr;
489        match ty {
490            // A `mutable` parameter unifies as its underlying type.
491            TypeExpr::Mutable { inner } => {
492                Self::from_type_expr_with_params(inner, interner, type_params)
493            }
494            TypeExpr::Primitive(sym) | TypeExpr::Named(sym) => {
495                // Check if this name is a generic type parameter
496                if let Some(&tv) = type_params.get(sym) {
497                    return InferType::Var(tv);
498                }
499                Self::from_type_name(interner.resolve(*sym))
500            }
501            TypeExpr::Generic { base, params } => {
502                let base_name = interner.resolve(*base);
503                match base_name {
504                    "Seq" | "List" | "Vec" => {
505                        let elem = params
506                            .first()
507                            .map(|p| InferType::from_type_expr_with_params(p, interner, type_params))
508                            .unwrap_or(InferType::Unit);
509                        InferType::Seq(Box::new(elem))
510                    }
511                    "Map" | "HashMap" => {
512                        let key = params
513                            .first()
514                            .map(|p| InferType::from_type_expr_with_params(p, interner, type_params))
515                            .unwrap_or(InferType::String);
516                        let val = params
517                            .get(1)
518                            .map(|p| InferType::from_type_expr_with_params(p, interner, type_params))
519                            .unwrap_or(InferType::String);
520                        InferType::Map(Box::new(key), Box::new(val))
521                    }
522                    "Set" | "HashSet" => {
523                        let elem = params
524                            .first()
525                            .map(|p| InferType::from_type_expr_with_params(p, interner, type_params))
526                            .unwrap_or(InferType::Unit);
527                        InferType::Set(Box::new(elem))
528                    }
529                    "Option" | "Maybe" => {
530                        let inner = params
531                            .first()
532                            .map(|p| InferType::from_type_expr_with_params(p, interner, type_params))
533                            .unwrap_or(InferType::Unit);
534                        InferType::Option(Box::new(inner))
535                    }
536                    _ => InferType::Unknown,
537                }
538            }
539            TypeExpr::Refinement { base, .. } => {
540                InferType::from_type_expr_with_params(base, interner, type_params)
541            }
542            TypeExpr::Persistent { inner } => {
543                InferType::from_type_expr_with_params(inner, interner, type_params)
544            }
545            TypeExpr::Function { inputs, output } => {
546                let param_types: Vec<InferType> = inputs
547                    .iter()
548                    .map(|p| InferType::from_type_expr_with_params(p, interner, type_params))
549                    .collect();
550                let ret_type = InferType::from_type_expr_with_params(output, interner, type_params);
551                InferType::Function(param_types, Box::new(ret_type))
552            }
553        }
554    }
555
556    /// Convert a registry `FieldType` to `InferType`.
557    ///
558    /// `type_params` maps generic type parameter names (e.g., `T`, `U`) to
559    /// type variable indices allocated by [`UnificationTable::fresh`].
560    pub fn from_field_type(
561        ty: &FieldType,
562        interner: &Interner,
563        type_params: &HashMap<Symbol, TyVar>,
564    ) -> InferType {
565        match ty {
566            FieldType::Primitive(sym) => InferType::from_type_name(interner.resolve(*sym)),
567            FieldType::Named(sym) => {
568                let name = interner.resolve(*sym);
569                let primitive = InferType::from_type_name(name);
570                if primitive == InferType::Unknown {
571                    InferType::UserDefined(*sym)
572                } else {
573                    primitive
574                }
575            }
576            FieldType::Generic { base, params } => {
577                let base_name = interner.resolve(*base);
578                let converted: Vec<InferType> = params
579                    .iter()
580                    .map(|p| InferType::from_field_type(p, interner, type_params))
581                    .collect();
582                match base_name {
583                    "Seq" | "List" | "Vec" => {
584                        InferType::Seq(Box::new(
585                            converted.into_iter().next().unwrap_or(InferType::Unit),
586                        ))
587                    }
588                    "Map" | "HashMap" => {
589                        let mut it = converted.into_iter();
590                        let k = it.next().unwrap_or(InferType::String);
591                        let v = it.next().unwrap_or(InferType::String);
592                        InferType::Map(Box::new(k), Box::new(v))
593                    }
594                    "Set" | "HashSet" => {
595                        InferType::Set(Box::new(
596                            converted.into_iter().next().unwrap_or(InferType::Unit),
597                        ))
598                    }
599                    "Option" | "Maybe" => {
600                        InferType::Option(Box::new(
601                            converted.into_iter().next().unwrap_or(InferType::Unit),
602                        ))
603                    }
604                    _ => InferType::Unknown,
605                }
606            }
607            FieldType::TypeParam(sym) => {
608                if let Some(tv) = type_params.get(sym) {
609                    InferType::Var(*tv)
610                } else {
611                    InferType::Unknown
612                }
613            }
614        }
615    }
616
617    /// Infer `InferType` from a literal value.
618    pub fn from_literal(lit: &crate::ast::stmt::Literal) -> InferType {
619        use crate::ast::stmt::Literal;
620        match lit {
621            Literal::Number(_) => InferType::Int,
622            Literal::Float(_) => InferType::Float,
623            Literal::Text(_) => InferType::String,
624            Literal::Boolean(_) => InferType::Bool,
625            Literal::Char(_) => InferType::Char,
626            Literal::Nothing => InferType::Unit,
627            Literal::Duration(_) => InferType::Duration,
628            Literal::Date(_) => InferType::Date,
629            Literal::Moment(_) => InferType::Moment,
630            Literal::Span { .. } => InferType::Span,
631            Literal::Time(_) => InferType::Time,
632        }
633    }
634
635    /// Parse a LOGOS type name into `InferType`.
636    pub fn from_type_name(name: &str) -> InferType {
637        match name {
638            "Int" => InferType::Int,
639            "Nat" => InferType::Nat,
640            "Rational" => InferType::Rational,
641            "Real" | "Float" => InferType::Float,
642            "Bool" | "Boolean" => InferType::Bool,
643            "Text" | "String" => InferType::String,
644            "Char" => InferType::Char,
645            "Byte" => InferType::Byte,
646            "Unit" | "()" => InferType::Unit,
647            "Duration" => InferType::Duration,
648            "Date" => InferType::Date,
649            "Moment" => InferType::Moment,
650            "Time" => InferType::Time,
651            "Span" => InferType::Span,
652            _ => InferType::Unknown,
653        }
654    }
655
656    /// Human-readable type name in Logos terms, for error messages.
657    pub fn to_logos_name(&self) -> std::string::String {
658        match self {
659            InferType::Int => "Int".into(),
660            InferType::Float => "Real".into(),
661            InferType::Bool => "Bool".into(),
662            InferType::Char => "Char".into(),
663            InferType::Byte => "Byte".into(),
664            InferType::String => "Text".into(),
665            InferType::Unit => "Unit".into(),
666            InferType::Nat => "Nat".into(),
667            InferType::Rational => "Rational".into(),
668            InferType::Duration => "Duration".into(),
669            InferType::Date => "Date".into(),
670            InferType::Moment => "Moment".into(),
671            InferType::Time => "Time".into(),
672            InferType::Span => "Span".into(),
673            InferType::Seq(inner) => format!("Seq of {}", inner.to_logos_name()),
674            InferType::Map(k, v) => {
675                format!("Map of {} and {}", k.to_logos_name(), v.to_logos_name())
676            }
677            InferType::Set(inner) => format!("Set of {}", inner.to_logos_name()),
678            InferType::Option(inner) => format!("Option of {}", inner.to_logos_name()),
679            InferType::UserDefined(_) => "a user-defined type".into(),
680            InferType::Var(_) => "an unknown type".into(),
681            InferType::Function(params, ret) => {
682                let params_str = params
683                    .iter()
684                    .map(|p| p.to_logos_name())
685                    .collect::<Vec<_>>()
686                    .join(", ");
687                format!("fn({}) -> {}", params_str, ret.to_logos_name())
688            }
689            InferType::Unknown => "unknown".into(),
690        }
691    }
692
693    /// Convert a known-ground `InferType` to `LogosType`.
694    ///
695    /// # Panics
696    ///
697    /// Panics if called on a `Var`. Callers must `zonk` first.
698    pub fn to_logos_type_ground(&self) -> LogosType {
699        match self {
700            InferType::Int => LogosType::Int,
701            InferType::Float => LogosType::Float,
702            InferType::Bool => LogosType::Bool,
703            InferType::Char => LogosType::Char,
704            InferType::Byte => LogosType::Byte,
705            InferType::String => LogosType::String,
706            InferType::Unit => LogosType::Unit,
707            InferType::Nat => LogosType::Nat,
708            InferType::Rational => LogosType::Rational,
709            InferType::Duration => LogosType::Duration,
710            InferType::Date => LogosType::Date,
711            InferType::Moment => LogosType::Moment,
712            InferType::Time => LogosType::Time,
713            InferType::Span => LogosType::Span,
714            InferType::Seq(inner) => LogosType::Seq(Box::new(inner.to_logos_type_ground())),
715            InferType::Map(k, v) => LogosType::Map(
716                Box::new(k.to_logos_type_ground()),
717                Box::new(v.to_logos_type_ground()),
718            ),
719            InferType::Set(inner) => LogosType::Set(Box::new(inner.to_logos_type_ground())),
720            InferType::Option(inner) => LogosType::Option(Box::new(inner.to_logos_type_ground())),
721            InferType::UserDefined(sym) => LogosType::UserDefined(*sym),
722            InferType::Function(params, ret) => LogosType::Function(
723                params.iter().map(|p| p.to_logos_type_ground()).collect(),
724                Box::new(ret.to_logos_type_ground()),
725            ),
726            InferType::Unknown => LogosType::Unknown,
727            InferType::Var(_) => panic!("to_logos_type_ground called on unresolved Var"),
728        }
729    }
730}
731
732// ============================================================================
733// Helpers
734// ============================================================================
735
736/// Numeric promotion: Float wins; Int + Int = Int; Nat + Nat = Nat; Byte + Byte = Byte;
737/// Byte + Int (literal context) = Byte; otherwise error.
738pub fn unify_numeric(a: &InferType, b: &InferType) -> Result<InferType, TypeError> {
739    match (a, b) {
740        (InferType::Float, _) | (_, InferType::Float) => Ok(InferType::Float),
741        // A Rational operand promotes the result to Rational (the exact type wins over Int).
742        (InferType::Rational, InferType::Rational | InferType::Int | InferType::Nat)
743        | (InferType::Int | InferType::Nat, InferType::Rational) => Ok(InferType::Rational),
744        (InferType::Int, InferType::Int) => Ok(InferType::Int),
745        (InferType::Nat, InferType::Int) | (InferType::Int, InferType::Nat) => Ok(InferType::Int),
746        (InferType::Nat, InferType::Nat) => Ok(InferType::Nat),
747        (InferType::Byte, InferType::Byte) => Ok(InferType::Byte),
748        (InferType::Byte, InferType::Int) | (InferType::Int, InferType::Byte) => Ok(InferType::Byte),
749        _ => Err(TypeError::Mismatch {
750            expected: InferType::Int,
751            found: a.clone(),
752        }),
753    }
754}
755
756/// Convert a zonked `InferType` to `LogosType`.
757pub fn infer_to_logos(ty: &InferType) -> LogosType {
758    match ty {
759        InferType::Int => LogosType::Int,
760        InferType::Float => LogosType::Float,
761        InferType::Bool => LogosType::Bool,
762        InferType::Char => LogosType::Char,
763        InferType::Byte => LogosType::Byte,
764        InferType::String => LogosType::String,
765        InferType::Unit => LogosType::Unit,
766        InferType::Nat => LogosType::Nat,
767        InferType::Rational => LogosType::Rational,
768        InferType::Duration => LogosType::Duration,
769        InferType::Date => LogosType::Date,
770        InferType::Moment => LogosType::Moment,
771        InferType::Time => LogosType::Time,
772        InferType::Span => LogosType::Span,
773        InferType::Seq(inner) => LogosType::Seq(Box::new(infer_to_logos(inner))),
774        InferType::Map(k, v) => {
775            LogosType::Map(Box::new(infer_to_logos(k)), Box::new(infer_to_logos(v)))
776        }
777        InferType::Set(inner) => LogosType::Set(Box::new(infer_to_logos(inner))),
778        InferType::Option(inner) => LogosType::Option(Box::new(infer_to_logos(inner))),
779        InferType::UserDefined(sym) => LogosType::UserDefined(*sym),
780        InferType::Function(params, ret) => LogosType::Function(
781            params.iter().map(infer_to_logos).collect(),
782            Box::new(infer_to_logos(ret)),
783        ),
784        InferType::Unknown | InferType::Var(_) => LogosType::Unknown,
785    }
786}
787
788// ============================================================================
789// Tests
790// ============================================================================
791
792#[cfg(test)]
793mod tests {
794    use super::*;
795    use crate::analysis::{FieldDef, TypeDef};
796
797    // =========================================================================
798    // UnificationTable::fresh / find
799    // =========================================================================
800
801    #[test]
802    fn fresh_produces_distinct_vars() {
803        let mut table = UnificationTable::new();
804        let a = table.fresh();
805        let b = table.fresh();
806        assert_ne!(a, b);
807    }
808
809    #[test]
810    fn unbound_var_finds_itself() {
811        let mut table = UnificationTable::new();
812        let v = table.fresh();
813        if let InferType::Var(tv) = v {
814            assert_eq!(table.find(tv), InferType::Var(tv));
815        } else {
816            panic!("expected Var");
817        }
818    }
819
820    // =========================================================================
821    // Unify ground types
822    // =========================================================================
823
824    #[test]
825    fn unify_identical_ground_types() {
826        let mut table = UnificationTable::new();
827        assert!(table.unify(&InferType::Int, &InferType::Int).is_ok());
828        assert!(table.unify(&InferType::Float, &InferType::Float).is_ok());
829        assert!(table.unify(&InferType::Bool, &InferType::Bool).is_ok());
830        assert!(table.unify(&InferType::String, &InferType::String).is_ok());
831        assert!(table.unify(&InferType::Unit, &InferType::Unit).is_ok());
832    }
833
834    #[test]
835    fn unify_different_ground_types_fails() {
836        let mut table = UnificationTable::new();
837        let result = table.unify(&InferType::Int, &InferType::String);
838        assert!(result.is_err());
839        assert!(matches!(result, Err(TypeError::Mismatch { .. })));
840    }
841
842    #[test]
843    fn unify_int_float_fails() {
844        let mut table = UnificationTable::new();
845        let result = table.unify(&InferType::Int, &InferType::Float);
846        assert!(result.is_err());
847    }
848
849    #[test]
850    fn unify_nat_int_succeeds() {
851        let mut table = UnificationTable::new();
852        assert!(table.unify(&InferType::Nat, &InferType::Int).is_ok());
853        assert!(table.unify(&InferType::Int, &InferType::Nat).is_ok());
854    }
855
856    #[test]
857    fn unify_unknown_with_any_succeeds() {
858        let mut table = UnificationTable::new();
859        assert!(table.unify(&InferType::Unknown, &InferType::Int).is_ok());
860        assert!(table.unify(&InferType::String, &InferType::Unknown).is_ok());
861        assert!(table.unify(&InferType::Unknown, &InferType::Unknown).is_ok());
862    }
863
864    // =========================================================================
865    // Unify variables with ground types
866    // =========================================================================
867
868    #[test]
869    fn var_unifies_with_int() {
870        let mut table = UnificationTable::new();
871        let v = table.fresh();
872        if let InferType::Var(tv) = v {
873            table.unify(&InferType::Var(tv), &InferType::Int).unwrap();
874            assert_eq!(table.find(tv), InferType::Int);
875        }
876    }
877
878    #[test]
879    fn int_unifies_with_var() {
880        let mut table = UnificationTable::new();
881        let v = table.fresh();
882        if let InferType::Var(tv) = v {
883            table.unify(&InferType::Int, &InferType::Var(tv)).unwrap();
884            assert_eq!(table.find(tv), InferType::Int);
885        }
886    }
887
888    #[test]
889    fn two_vars_unify_chain() {
890        let mut table = UnificationTable::new();
891        let va = table.fresh();
892        let vb = table.fresh();
893        let tva = if let InferType::Var(tv) = va { tv } else { panic!() };
894        let tvb = if let InferType::Var(tv) = vb { tv } else { panic!() };
895        table.unify(&InferType::Var(tva), &InferType::Var(tvb)).unwrap();
896        // Bind tvb to Int, then zonk(tva) should follow chain to Int
897        table.unify(&InferType::Var(tvb), &InferType::Int).unwrap();
898        let zonked = table.zonk(&InferType::Var(tva));
899        assert_eq!(zonked, InferType::Int);
900    }
901
902    #[test]
903    fn var_conflicting_types_fails() {
904        let mut table = UnificationTable::new();
905        let v = table.fresh();
906        if let InferType::Var(tv) = v {
907            table.unify(&InferType::Var(tv), &InferType::Int).unwrap();
908            let result = table.unify(&InferType::Var(tv), &InferType::String);
909            // After binding tv → Int, unifying Int with String fails
910            assert!(result.is_err());
911        }
912    }
913
914    // =========================================================================
915    // Occurs check
916    // =========================================================================
917
918    #[test]
919    fn occurs_check_detects_infinite_type() {
920        let mut table = UnificationTable::new();
921        let v = table.fresh();
922        if let InferType::Var(tv) = v {
923            let circular = InferType::Seq(Box::new(InferType::Var(tv)));
924            let result = table.unify(&InferType::Var(tv), &circular);
925            assert!(result.is_err());
926            assert!(matches!(result, Err(TypeError::InfiniteType { .. })));
927        }
928    }
929
930    // =========================================================================
931    // Zonk
932    // =========================================================================
933
934    #[test]
935    fn zonk_resolves_bound_var() {
936        let mut table = UnificationTable::new();
937        let v = table.fresh();
938        if let InferType::Var(tv) = v {
939            table.unify(&InferType::Var(tv), &InferType::Bool).unwrap();
940            let zonked = table.zonk(&InferType::Var(tv));
941            assert_eq!(zonked, InferType::Bool);
942        }
943    }
944
945    #[test]
946    fn zonk_unbound_var_becomes_unknown() {
947        let mut table = UnificationTable::new();
948        let v = table.fresh();
949        if let InferType::Var(tv) = v {
950            let zonked = table.zonk(&InferType::Var(tv));
951            assert_eq!(zonked, InferType::Unknown);
952        }
953    }
954
955    #[test]
956    fn zonk_nested_resolves_inner_var() {
957        let mut table = UnificationTable::new();
958        let v = table.fresh();
959        if let InferType::Var(tv) = v {
960            table.unify(&InferType::Var(tv), &InferType::Int).unwrap();
961            let ty = InferType::Seq(Box::new(InferType::Var(tv)));
962            let zonked = table.zonk(&ty);
963            assert_eq!(zonked, InferType::Seq(Box::new(InferType::Int)));
964        }
965    }
966
967    #[test]
968    fn zonk_chain_of_vars() {
969        let mut table = UnificationTable::new();
970        let tva = if let InferType::Var(tv) = table.fresh() { tv } else { panic!() };
971        let tvb = if let InferType::Var(tv) = table.fresh() { tv } else { panic!() };
972        let tvc = if let InferType::Var(tv) = table.fresh() { tv } else { panic!() };
973        // Chain: tva → tvb → tvc → Float
974        table.unify(&InferType::Var(tva), &InferType::Var(tvb)).unwrap();
975        table.unify(&InferType::Var(tvb), &InferType::Var(tvc)).unwrap();
976        table.unify(&InferType::Var(tvc), &InferType::Float).unwrap();
977        assert_eq!(table.zonk(&InferType::Var(tva)), InferType::Float);
978    }
979
980    // =========================================================================
981    // Nested generic unification
982    // =========================================================================
983
984    #[test]
985    fn unify_seq_of_same_type() {
986        let mut table = UnificationTable::new();
987        let a = InferType::Seq(Box::new(InferType::Int));
988        let b = InferType::Seq(Box::new(InferType::Int));
989        assert!(table.unify(&a, &b).is_ok());
990    }
991
992    #[test]
993    fn unify_seq_of_different_types_fails() {
994        let mut table = UnificationTable::new();
995        let a = InferType::Seq(Box::new(InferType::Int));
996        let b = InferType::Seq(Box::new(InferType::String));
997        assert!(table.unify(&a, &b).is_err());
998    }
999
1000    #[test]
1001    fn unify_seq_with_var_element() {
1002        let mut table = UnificationTable::new();
1003        let v = table.fresh();
1004        if let InferType::Var(tv) = v {
1005            let a = InferType::Seq(Box::new(InferType::Var(tv)));
1006            let b = InferType::Seq(Box::new(InferType::Float));
1007            table.unify(&a, &b).unwrap();
1008            assert_eq!(table.find(tv), InferType::Float);
1009        }
1010    }
1011
1012    #[test]
1013    fn unify_map_types() {
1014        let mut table = UnificationTable::new();
1015        let a = InferType::Map(Box::new(InferType::String), Box::new(InferType::Int));
1016        let b = InferType::Map(Box::new(InferType::String), Box::new(InferType::Int));
1017        assert!(table.unify(&a, &b).is_ok());
1018    }
1019
1020    #[test]
1021    fn unify_function_types_same_arity() {
1022        let mut table = UnificationTable::new();
1023        let a = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1024        let b = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1025        assert!(table.unify(&a, &b).is_ok());
1026    }
1027
1028    #[test]
1029    fn unify_function_arity_mismatch_fails() {
1030        let mut table = UnificationTable::new();
1031        let a = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1032        let b = InferType::Function(
1033            vec![InferType::Int, InferType::Int],
1034            Box::new(InferType::Bool),
1035        );
1036        let result = table.unify(&a, &b);
1037        assert!(matches!(result, Err(TypeError::ArityMismatch { expected: 1, found: 2 })));
1038    }
1039
1040    // =========================================================================
1041    // InferType → LogosType conversion (to_logos_type)
1042    // =========================================================================
1043
1044    #[test]
1045    fn to_logos_type_ground_primitives() {
1046        let table = UnificationTable::new();
1047        assert_eq!(table.to_logos_type(&InferType::Int), LogosType::Int);
1048        assert_eq!(table.to_logos_type(&InferType::Float), LogosType::Float);
1049        assert_eq!(table.to_logos_type(&InferType::Bool), LogosType::Bool);
1050        assert_eq!(table.to_logos_type(&InferType::String), LogosType::String);
1051        assert_eq!(table.to_logos_type(&InferType::Unit), LogosType::Unit);
1052        assert_eq!(table.to_logos_type(&InferType::Nat), LogosType::Nat);
1053    }
1054
1055    #[test]
1056    fn to_logos_type_unbound_var_becomes_unknown() {
1057        let mut table = UnificationTable::new();
1058        let v = table.fresh();
1059        assert_eq!(table.to_logos_type(&v), LogosType::Unknown);
1060    }
1061
1062    #[test]
1063    fn to_logos_type_bound_var_resolves() {
1064        let mut table = UnificationTable::new();
1065        let v = table.fresh();
1066        if let InferType::Var(tv) = v {
1067            table.unify(&InferType::Var(tv), &InferType::Int).unwrap();
1068            assert_eq!(table.to_logos_type(&InferType::Var(tv)), LogosType::Int);
1069        }
1070    }
1071
1072    #[test]
1073    fn to_logos_type_seq_resolves_inner() {
1074        let mut table = UnificationTable::new();
1075        let v = table.fresh();
1076        if let InferType::Var(tv) = v {
1077            table.unify(&InferType::Var(tv), &InferType::String).unwrap();
1078            let ty = InferType::Seq(Box::new(InferType::Var(tv)));
1079            assert_eq!(
1080                table.to_logos_type(&ty),
1081                LogosType::Seq(Box::new(LogosType::String))
1082            );
1083        }
1084    }
1085
1086    #[test]
1087    fn to_logos_type_function_converts_to_logos_function() {
1088        let table = UnificationTable::new();
1089        let ty = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1090        assert_eq!(
1091            table.to_logos_type(&ty),
1092            LogosType::Function(vec![LogosType::Int], Box::new(LogosType::Bool))
1093        );
1094    }
1095
1096    #[test]
1097    fn to_logos_type_function_two_params_converts() {
1098        let table = UnificationTable::new();
1099        let ty = InferType::Function(
1100            vec![InferType::Int, InferType::String],
1101            Box::new(InferType::Bool),
1102        );
1103        assert_eq!(
1104            table.to_logos_type(&ty),
1105            LogosType::Function(
1106                vec![LogosType::Int, LogosType::String],
1107                Box::new(LogosType::Bool)
1108            )
1109        );
1110    }
1111
1112    #[test]
1113    fn to_logos_type_function_zero_params_converts() {
1114        let table = UnificationTable::new();
1115        let ty = InferType::Function(vec![], Box::new(InferType::Unit));
1116        assert_eq!(
1117            table.to_logos_type(&ty),
1118            LogosType::Function(vec![], Box::new(LogosType::Unit))
1119        );
1120    }
1121
1122    #[test]
1123    fn to_logos_type_function_nested_converts() {
1124        // fn(fn(Int) -> Bool) -> String
1125        let table = UnificationTable::new();
1126        let inner = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1127        let outer = InferType::Function(vec![inner], Box::new(InferType::String));
1128        assert_eq!(
1129            table.to_logos_type(&outer),
1130            LogosType::Function(
1131                vec![LogosType::Function(
1132                    vec![LogosType::Int],
1133                    Box::new(LogosType::Bool)
1134                )],
1135                Box::new(LogosType::String)
1136            )
1137        );
1138    }
1139
1140    // =========================================================================
1141    // from_type_expr
1142    // =========================================================================
1143
1144    #[test]
1145    fn from_type_expr_function_produces_function_type() {
1146        use crate::ast::stmt::TypeExpr;
1147        let mut interner = Interner::new();
1148        let int_sym = interner.intern("Int");
1149        let bool_sym = interner.intern("Bool");
1150        let int_ty = TypeExpr::Primitive(int_sym);
1151        let bool_ty = TypeExpr::Primitive(bool_sym);
1152        let fn_ty = TypeExpr::Function {
1153            inputs: std::slice::from_ref(&int_ty),
1154            output: &bool_ty,
1155        };
1156        let result = InferType::from_type_expr(&fn_ty, &interner);
1157        assert_eq!(
1158            result,
1159            InferType::Function(vec![InferType::Int], Box::new(InferType::Bool))
1160        );
1161    }
1162
1163    #[test]
1164    fn from_type_expr_seq_of_int() {
1165        use crate::ast::stmt::TypeExpr;
1166        let mut interner = Interner::new();
1167        let seq_sym = interner.intern("Seq");
1168        let int_sym = interner.intern("Int");
1169        let int_ty = TypeExpr::Primitive(int_sym);
1170        let ty = TypeExpr::Generic {
1171            base: seq_sym,
1172            params: std::slice::from_ref(&int_ty),
1173        };
1174        let result = InferType::from_type_expr(&ty, &interner);
1175        assert_eq!(result, InferType::Seq(Box::new(InferType::Int)));
1176    }
1177
1178    // =========================================================================
1179    // from_field_type with TypeParam
1180    // =========================================================================
1181
1182    #[test]
1183    fn from_field_type_type_param_resolves_to_var() {
1184        let mut interner = Interner::new();
1185        let t_sym = interner.intern("T");
1186        let tv = TyVar(0);
1187        let mut type_params = HashMap::new();
1188        type_params.insert(t_sym, tv);
1189
1190        let field_ty = FieldType::TypeParam(t_sym);
1191        let result = InferType::from_field_type(&field_ty, &interner, &type_params);
1192        assert_eq!(result, InferType::Var(tv));
1193    }
1194
1195    #[test]
1196    fn from_field_type_missing_type_param_becomes_unknown() {
1197        let mut interner = Interner::new();
1198        let t_sym = interner.intern("T");
1199        let type_params = HashMap::new();
1200        let field_ty = FieldType::TypeParam(t_sym);
1201        let result = InferType::from_field_type(&field_ty, &interner, &type_params);
1202        assert_eq!(result, InferType::Unknown);
1203    }
1204
1205    #[test]
1206    fn from_field_type_primitive() {
1207        let mut interner = Interner::new();
1208        let int_sym = interner.intern("Int");
1209        let field_ty = FieldType::Primitive(int_sym);
1210        let result = InferType::from_field_type(&field_ty, &interner, &HashMap::new());
1211        assert_eq!(result, InferType::Int);
1212    }
1213
1214    #[test]
1215    fn from_field_type_generic_seq_of_type_param() {
1216        let mut interner = Interner::new();
1217        let seq_sym = interner.intern("Seq");
1218        let t_sym = interner.intern("T");
1219        let tv = TyVar(0);
1220        let mut type_params = HashMap::new();
1221        type_params.insert(t_sym, tv);
1222
1223        let field_ty = FieldType::Generic {
1224            base: seq_sym,
1225            params: vec![FieldType::TypeParam(t_sym)],
1226        };
1227        let result = InferType::from_field_type(&field_ty, &interner, &type_params);
1228        assert_eq!(result, InferType::Seq(Box::new(InferType::Var(tv))));
1229    }
1230
1231    // =========================================================================
1232    // unify_numeric helper
1233    // =========================================================================
1234
1235    #[test]
1236    fn numeric_float_wins() {
1237        assert_eq!(
1238            unify_numeric(&InferType::Int, &InferType::Float).unwrap(),
1239            InferType::Float
1240        );
1241        assert_eq!(
1242            unify_numeric(&InferType::Float, &InferType::Int).unwrap(),
1243            InferType::Float
1244        );
1245    }
1246
1247    #[test]
1248    fn numeric_int_plus_int_is_int() {
1249        assert_eq!(
1250            unify_numeric(&InferType::Int, &InferType::Int).unwrap(),
1251            InferType::Int
1252        );
1253    }
1254
1255    #[test]
1256    fn numeric_nat_plus_int_is_int() {
1257        assert_eq!(
1258            unify_numeric(&InferType::Nat, &InferType::Int).unwrap(),
1259            InferType::Int
1260        );
1261    }
1262
1263    #[test]
1264    fn numeric_nat_plus_nat_is_nat() {
1265        assert_eq!(
1266            unify_numeric(&InferType::Nat, &InferType::Nat).unwrap(),
1267            InferType::Nat
1268        );
1269    }
1270
1271    #[test]
1272    fn numeric_string_fails() {
1273        let result = unify_numeric(&InferType::String, &InferType::Int);
1274        assert!(result.is_err());
1275    }
1276
1277    // =========================================================================
1278    // to_logos_name
1279    // =========================================================================
1280
1281    #[test]
1282    fn logos_name_primitives() {
1283        assert_eq!(InferType::Int.to_logos_name(), "Int");
1284        assert_eq!(InferType::Float.to_logos_name(), "Real");
1285        assert_eq!(InferType::String.to_logos_name(), "Text");
1286        assert_eq!(InferType::Bool.to_logos_name(), "Bool");
1287    }
1288
1289    #[test]
1290    fn logos_name_seq() {
1291        let ty = InferType::Seq(Box::new(InferType::Int));
1292        assert_eq!(ty.to_logos_name(), "Seq of Int");
1293    }
1294
1295    #[test]
1296    fn logos_name_function() {
1297        let ty = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1298        assert_eq!(ty.to_logos_name(), "fn(Int) -> Bool");
1299    }
1300
1301    // =========================================================================
1302    // TypeError helpers
1303    // =========================================================================
1304
1305    #[test]
1306    fn type_error_mismatch_strings() {
1307        let err = TypeError::Mismatch {
1308            expected: InferType::Int,
1309            found: InferType::String,
1310        };
1311        assert_eq!(err.expected_str(), "Int");
1312        assert_eq!(err.found_str(), "Text");
1313    }
1314
1315    #[test]
1316    fn type_error_arity_mismatch_strings() {
1317        let err = TypeError::ArityMismatch { expected: 2, found: 3 };
1318        assert_eq!(err.expected_str(), "2 arguments");
1319        assert_eq!(err.found_str(), "3 arguments");
1320    }
1321
1322    // =========================================================================
1323    // Phase 5: infer_to_logos for Function types
1324    // =========================================================================
1325
1326    #[test]
1327    fn infer_to_logos_function_single_param() {
1328        let ty = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1329        assert_eq!(
1330            super::infer_to_logos(&ty),
1331            LogosType::Function(vec![LogosType::Int], Box::new(LogosType::Bool))
1332        );
1333    }
1334
1335    #[test]
1336    fn infer_to_logos_function_zero_params() {
1337        let ty = InferType::Function(vec![], Box::new(InferType::Unit));
1338        assert_eq!(
1339            super::infer_to_logos(&ty),
1340            LogosType::Function(vec![], Box::new(LogosType::Unit))
1341        );
1342    }
1343
1344    #[test]
1345    fn infer_to_logos_function_two_params() {
1346        let ty = InferType::Function(
1347            vec![InferType::String, InferType::Float],
1348            Box::new(InferType::Bool),
1349        );
1350        assert_eq!(
1351            super::infer_to_logos(&ty),
1352            LogosType::Function(
1353                vec![LogosType::String, LogosType::Float],
1354                Box::new(LogosType::Bool)
1355            )
1356        );
1357    }
1358
1359    #[test]
1360    fn infer_to_logos_function_nested() {
1361        // fn(fn(Int) -> Bool) -> String
1362        let inner = InferType::Function(vec![InferType::Int], Box::new(InferType::Bool));
1363        let outer = InferType::Function(vec![inner], Box::new(InferType::String));
1364        assert_eq!(
1365            super::infer_to_logos(&outer),
1366            LogosType::Function(
1367                vec![LogosType::Function(
1368                    vec![LogosType::Int],
1369                    Box::new(LogosType::Bool)
1370                )],
1371                Box::new(LogosType::String)
1372            )
1373        );
1374    }
1375}
logicaffeine_compile/analysis/unify.rs

logicaffeine_compile/analysis/
unify.rs
