diff --git a/crates/erg_compiler/context/unify.rs b/crates/erg_compiler/context/unify.rs index 3dc1d5519..cb3987259 100644 --- a/crates/erg_compiler/context/unify.rs +++ b/crates/erg_compiler/context/unify.rs @@ -1022,6 +1022,16 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { } let (lsub, lsup) = sub_fv.get_subsup().unwrap(); let (rsub, rsup) = sup_fv.get_subsup().unwrap(); + // sub: ?T(:> ?U) + // sup: ?U + // => ?T == ?U + if &lsub == maybe_sup { + maybe_sub.link(maybe_sup, self.undoable); + return Ok(()); + } else if &rsup == maybe_sub { + maybe_sup.link(maybe_sub, self.undoable); + return Ok(()); + } // ?T(<: Add(?T)) // ?U(:> {1, 2}, <: Add(?U)) ==> {1, 2} sup_fv.dummy_link(); @@ -1117,6 +1127,40 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { } } } + (FreeVar(sub_fv), FreeVar(sup_fv)) + if sub_fv.constraint_is_sandwiched() && sup_fv.constraint_is_typeof() => + { + if !self.change_generalized && (sub_fv.is_generalized() || sup_fv.is_generalized()) + { + log!(info "generalized:\nmaybe_sub: {maybe_sub}\nmaybe_sup: {maybe_sup}"); + return Ok(()); + } + let (lsub, _lsup) = sub_fv.get_subsup().unwrap(); + // sub: ?T(:> ?U(: {Str, Int})) + // sup: ?U(: {Str, Int}) + // => ?T == ?U + if &lsub == maybe_sup { + maybe_sub.link(maybe_sup, self.undoable); + return Ok(()); + } + let rty = sup_fv.get_type().unwrap(); + let Some(rtys) = rty.refinement_values() else { + todo!("{rty}"); + }; + // sub: ?T(:> Nat) + // sup: ?U(: {Str, Int}) + // => ?T(:> Nat, <: Int) + for tp in rtys { + let Ok(ty) = self.ctx.convert_tp_into_type(tp.clone()) else { + todo!("{tp}"); + }; + if self.ctx.subtype_of(&lsub, &ty) { + sub_fv.update_super(|sup| self.ctx.intersection(&sup, &ty)); + return Ok(()); + } + } + // REVIEW: unreachable? + } ( Bounded { sub: lsub, diff --git a/crates/erg_compiler/ty/free.rs b/crates/erg_compiler/ty/free.rs index 7a68a03dc..4cb6d0cf1 100644 --- a/crates/erg_compiler/ty/free.rs +++ b/crates/erg_compiler/ty/free.rs @@ -800,6 +800,55 @@ impl Free { self.crack().has_unbound_var() } } + + /// interior-mut + /// if `in_inst_or_gen` is true, constraint will be updated forcibly + pub fn update_constraint(&self, new_constraint: Constraint, in_inst_or_gen: bool) { + if new_constraint.get_type() == Some(&Type::Never) { + panic!("{new_constraint}"); + } + // self: T + // new_constraint: (:> T, <: U) => <: U + if new_constraint.get_sub_sup().is_some_and(|(sub, sup)| { + sub.contains_tvar_in_constraint(self) || sup.contains_tvar_in_constraint(self) + }) { + return; + } + match &mut *self.borrow_mut() { + FreeKind::Unbound { + lev, constraint, .. + } + | FreeKind::NamedUnbound { + lev, constraint, .. + } => { + if !in_inst_or_gen && *lev == GENERIC_LEVEL { + log!(err "cannot update the constraint of a generalized type variable"); + return; + } + if addr_eq!(*constraint, new_constraint) { + return; + } + *constraint = new_constraint; + } + FreeKind::Linked(t) | FreeKind::UndoableLinked { t, .. } => { + t.destructive_update_constraint(new_constraint, in_inst_or_gen); + } + } + } + + /// interior-mut + pub fn update_sub(&self, f: impl FnOnce(Type) -> Type) { + let (sub, sup) = self.get_subsup().unwrap(); + let new_constraint = Constraint::new_sandwiched(f(sub), sup); + self.update_constraint(new_constraint, true); + } + + /// interior-mut + pub fn update_super(&self, f: impl FnOnce(Type) -> Type) { + let (sub, sup) = self.get_subsup().unwrap(); + let new_constraint = Constraint::new_sandwiched(sub, f(sup)); + self.update_constraint(new_constraint, true); + } } impl Free { @@ -1219,6 +1268,15 @@ impl Free { pub fn constraint_is_uninited(&self) -> bool { self.constraint().map(|c| c.is_uninited()).unwrap_or(false) } +} + +impl Free { + pub fn map(&self, f: impl Fn(TyParam) -> TyParam) { + if let Some(mut linked) = self.get_linked_refmut() { + let mapped = f(mem::take(&mut *linked)); + *linked = mapped; + } + } /// interior-mut /// if `in_inst_or_gen` is true, constraint will be updated forcibly @@ -1248,20 +1306,6 @@ impl Free { } } - /// interior-mut - pub fn update_sub(&self, f: impl FnOnce(Type) -> Type) { - let (sub, sup) = self.get_subsup().unwrap(); - let new_constraint = Constraint::new_sandwiched(f(sub), sup); - self.update_constraint(new_constraint, true); - } - - /// interior-mut - pub fn update_super(&self, f: impl FnOnce(Type) -> Type) { - let (sub, sup) = self.get_subsup().unwrap(); - let new_constraint = Constraint::new_sandwiched(sub, f(sup)); - self.update_constraint(new_constraint, true); - } - /// interior-mut pub fn update_type(&self, new_type: Type) { let new_constraint = Constraint::new_type_of(new_type); @@ -1269,15 +1313,6 @@ impl Free { } } -impl Free { - pub fn map(&self, f: impl Fn(TyParam) -> TyParam) { - if let Some(mut linked) = self.get_linked_refmut() { - let mapped = f(mem::take(&mut *linked)); - *linked = mapped; - } - } -} - pub type FreeTyVar = Free; pub type FreeTyParam = Free; diff --git a/crates/erg_compiler/ty/mod.rs b/crates/erg_compiler/ty/mod.rs index 7f545ed14..32195de6e 100644 --- a/crates/erg_compiler/ty/mod.rs +++ b/crates/erg_compiler/ty/mod.rs @@ -1773,13 +1773,6 @@ impl CanbeFree for Type { let Some(fv) = self.as_free() else { return; }; - // self: T - // new_constraint: (:> T, <: U) => <: U - if new_constraint.get_sub_sup().is_some_and(|(sub, sup)| { - sub.contains_tvar_in_constraint(fv) || sup.contains_tvar_in_constraint(fv) - }) { - return; - } fv.update_constraint(new_constraint, in_instantiation); } } @@ -2884,6 +2877,13 @@ impl Type { || fv .get_subsup() .map(|(sub, sup)| { + if sub.as_free().is_some_and(|sub_fv| { + ref_addr_eq!(sub_fv.forced_as_ref(), target.forced_as_ref()) + }) || sup.as_free().is_some_and(|sup_fv| { + ref_addr_eq!(sup_fv.forced_as_ref(), target.forced_as_ref()) + }) { + return true; + } fv.do_avoiding_recursion(|| { sub.contains_tvar(target) || sup.contains_tvar(target) }) @@ -2991,6 +2991,13 @@ impl Type { || fv .get_subsup() .map(|(sub, sup)| { + if sub.as_free().is_some_and(|sub_fv| { + ref_addr_eq!(sub_fv.forced_as_ref(), target.forced_as_ref()) + }) || sup.as_free().is_some_and(|sup_fv| { + ref_addr_eq!(sup_fv.forced_as_ref(), target.forced_as_ref()) + }) { + return true; + } fv.do_avoiding_recursion(|| { sub.contains_tvar_in_constraint(target) || sup.contains_tvar_in_constraint(target) @@ -4217,6 +4224,12 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().eliminate_subsup(target), Self::FreeVar(ref fv) if fv.constraint_is_sandwiched() => { let (sub, sup) = fv.get_subsup().unwrap(); + let sub = if sub.addr_eq(target) { + Type::Never + } else { + sub + }; + let sup = if sup.addr_eq(target) { Type::Obj } else { sup }; fv.do_avoiding_recursion(|| { let sub = sub.eliminate_subsup(target); let sup = sup.eliminate_subsup(target); @@ -4901,7 +4914,7 @@ impl Type { } match self { Self::FreeVar(fv) => { - let to = to.clone().eliminate_subsup(self); + let to = to.clone().eliminate_subsup(self); // FIXME: .eliminate_recursion(self) fv.undoable_link(&to); } Self::Refinement(refine) => refine.t.undoable_link(to, list),