fix: sub-unification bug

crates/erg_compiler/context/compare.rs

@@ -153,8 +153,8 @@ impl Context {
         }
         match (lhs, rhs) {
             (Obj, _) | (_, Never | Failure) => (Absolutely, true),
-            (_, Obj) if lhs.is_simple_class() => (Absolutely, false),
-            (Never | Failure, _) if rhs.is_simple_class() => (Absolutely, false),
+            (_, Obj) if lhs.is_mono_value_class() => (Absolutely, false),
+            (Never | Failure, _) if rhs.is_mono_value_class() => (Absolutely, false),
             (Complex | Float | Ratio | Int | Nat | Bool, Bool)
             | (Complex | Float | Ratio | Int | Nat, Nat)
             | (Complex | Float | Ratio | Int, Int)
@@ -202,7 +202,9 @@ impl Context {
                 _ => (Maybe, false),
             },
             (Mono(n), Subr(_) | Quantified(_)) if &n[..] == "GenericCallable" => (Absolutely, true),
-            (lhs, rhs) if lhs.is_simple_class() && rhs.is_simple_class() => (Absolutely, false),
+            (lhs, rhs) if lhs.is_mono_value_class() && rhs.is_mono_value_class() => {
+                (Absolutely, false)
+            }
             _ => (Maybe, false),
         }
     }

crates/erg_compiler/context/eval.rs

@@ -1843,7 +1843,7 @@ impl Context {
                 &tp.to_string(),
             )
         })?;
-        if qt.has_undoable_linked_var() && (!st.is_unbound_var() || !st.is_generalized()) {
+        if qt.is_undoable_linked_var() && (!st.is_unbound_var() || !st.is_generalized()) {
             qt.undoable_link(&st);
         }
         if !st.is_unbound_var() || !st.is_generalized() {

crates/erg_compiler/context/register.rs

@@ -2379,7 +2379,6 @@ impl Context {
         tmp_tv_cache: &TyVarCache,
     ) -> bool {
         for arg in poly.args.pos_args() {
-            log!(err "{}", arg.expr);
             self.inc_ref_expr(&arg.expr.clone().downgrade(), namespace, tmp_tv_cache);
         }
         if let Some(arg) = poly.args.var_args.as_ref() {
@@ -2391,7 +2390,7 @@ impl Context {
         self.inc_ref_acc(&poly.acc.clone().downgrade(), namespace, tmp_tv_cache)
     }
 
-    fn inc_ref_local(
+    pub(crate) fn inc_ref_local(
         &self,
         local: &ConstIdentifier,
         namespace: &Context,

crates/erg_compiler/context/unify.rs

@@ -805,6 +805,83 @@ impl Context {
                     }
                 }
             }
+            (
+                Bounded {
+                    sub: lsub,
+                    sup: lsup,
+                },
+                FreeVar(sup_fv),
+            ) if sup_fv.constraint_is_sandwiched() => {
+                if sup_fv.is_generalized() {
+                    log!(info "generalized:\nmaybe_sub: {maybe_sub}\nmaybe_sup: {maybe_sup}");
+                    return Ok(());
+                }
+                let (rsub, rsup) = sup_fv.get_subsup().unwrap();
+                // ?T(<: Add(?T))
+                // ?U(:> {1, 2}, <: Add(?U)) ==> {1, 2}
+                sup_fv.dummy_link();
+                if lsub.qual_name() == rsub.qual_name() {
+                    for (lps, rps) in lsub.typarams().iter().zip(rsub.typarams().iter()) {
+                        self.sub_unify_tp(lps, rps, None, loc, false)
+                            .map_err(|errs| {
+                                sup_fv.undo();
+                                errs
+                            })?;
+                    }
+                }
+                // lsup: Add(?X(:> Int)), rsup: Add(?Y(:> Nat))
+                //   => lsup: Add(?X(:> Int)), rsup: Add((?X(:> Int)))
+                if lsup.qual_name() == rsup.qual_name() {
+                    for (lps, rps) in lsup.typarams().iter().zip(rsup.typarams().iter()) {
+                        self.sub_unify_tp(lps, rps, None, loc, false)
+                            .map_err(|errs| {
+                                sup_fv.undo();
+                                errs
+                            })?;
+                    }
+                }
+                sup_fv.undo();
+                let intersec = self.intersection(lsup, &rsup);
+                if intersec == Type::Never {
+                    return Err(TyCheckErrors::from(TyCheckError::subtyping_error(
+                        self.cfg.input.clone(),
+                        line!() as usize,
+                        maybe_sub,
+                        maybe_sup,
+                        loc.loc(),
+                        self.caused_by(),
+                    )));
+                }
+                let union = self.union(lsub, &rsub);
+                if lsub.union_size().max(rsub.union_size()) < union.union_size() {
+                    let (l, r) = union.union_pair().unwrap_or((*lsub.clone(), rsub.clone()));
+                    let unified = self.unify(&l, &r);
+                    if unified.is_none() {
+                        let maybe_sub = self.readable_type(maybe_sub.clone());
+                        let union = self.readable_type(union);
+                        return Err(TyCheckErrors::from(TyCheckError::implicit_widening_error(
+                            self.cfg.input.clone(),
+                            line!() as usize,
+                            loc.loc(),
+                            self.caused_by(),
+                            &maybe_sub,
+                            &union,
+                        )));
+                    }
+                }
+                // e.g. intersec == Int, rsup == Add(?T)
+                //   => ?T(:> Int)
+                self.sub_unify(&intersec, &rsup, loc, param_name)?;
+                self.sub_unify(&rsub, &union, loc, param_name)?;
+                // self.sub_unify(&intersec, &lsup, loc, param_name)?;
+                // self.sub_unify(&lsub, &union, loc, param_name)?;
+                if union == intersec {
+                    maybe_sup.link(&union);
+                } else {
+                    let new_constraint = Constraint::new_sandwiched(union, intersec);
+                    sup_fv.update_constraint(new_constraint, false);
+                }
+            }
             // (Int or ?T) <: (?U or Int)
             // OK: (Int <: Int); (?T <: ?U)
             // NG: (Int <: ?U); (?T <: Int)

crates/erg_compiler/ty/mod.rs

@@ -43,7 +43,7 @@ pub use value::ValueObj;
 use value::ValueObj::{Inf, NegInf};
 pub use vis::*;
 
-use self::constructors::{proj_call, subr_t};
+use self::constructors::{bounded, proj_call, subr_t};
 
 pub const STR_OMIT_THRESHOLD: usize = 16;
 pub const CONTAINER_OMIT_THRESHOLD: usize = 8;
@@ -594,7 +594,7 @@ impl LimitedDisplay for RefinementType {
             return write!(f, "...");
         }
         let first_subj = self.pred.ors().iter().next().and_then(|p| p.subject());
-        let is_simple_type = self.t.is_simple_class();
+        let is_simple_type = self.t.is_value_class();
         let is_simple_preds = self
             .pred
             .ors()
@@ -1684,9 +1684,9 @@ impl Type {
         Self::Structural(Box::new(self))
     }
 
-    pub fn is_simple_class(&self) -> bool {
+    pub fn is_mono_value_class(&self) -> bool {
         match self {
-            Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_simple_class(),
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_mono_value_class(),
             Self::Obj
             | Self::Int
             | Self::Nat
@@ -1712,6 +1712,23 @@ impl Type {
         }
     }
 
+    /// value class := mono value object class | (Array | Set)(value class)
+    pub fn is_value_class(&self) -> bool {
+        match self {
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_value_class(),
+            Self::Refinement(refine) => refine.t.is_value_class(),
+            Self::Poly { name, params } => {
+                if &name[..] == "Array" || &name[..] == "Set" {
+                    let elem_t = <&Type>::try_from(params.first().unwrap()).unwrap();
+                    elem_t.is_value_class()
+                } else {
+                    false
+                }
+            }
+            _ => self.is_mono_value_class(),
+        }
+    }
+
     /// Procedure
     pub fn is_procedure(&self) -> bool {
         match self {
@@ -2542,6 +2559,14 @@ impl Type {
         }
     }
 
+    pub fn is_undoable_linked_var(&self) -> bool {
+        match self {
+            Self::FreeVar(fv) if fv.is_undoable_linked() => true,
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().has_undoable_linked_var(),
+            _ => false,
+        }
+    }
+
     pub fn has_undoable_linked_var(&self) -> bool {
         match self {
             Self::FreeVar(fv) if fv.is_undoable_linked() => true,
@@ -3157,6 +3182,18 @@ impl Type {
             _ => panic!("{self} is not a free variable"),
         }
     }
+
+    pub fn into_bounded(&self) -> Type {
+        match self {
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().clone().into_bounded(),
+            Self::FreeVar(fv) if fv.constraint_is_sandwiched() => {
+                let (sub, sup) = fv.get_subsup().unwrap();
+                bounded(sub, sup)
+            }
+            Self::Refinement(refine) => refine.t.as_ref().clone().into_bounded(),
+            _ => self.clone(),
+        }
+    }
 }
 
 pub struct ReplaceTable<'t> {