fix: sub-unification bugs

This commit is contained in:
Shunsuke Shibayama 2023-03-22 15:38:47 +09:00
parent b318395a32
commit 0079aed860
10 changed files with 190 additions and 153 deletions

View file

@ -587,6 +587,25 @@ impl<T> Free<T> {
}
}
impl Free<Type> {
pub fn deep_clone(&self) -> Self {
Self::new_named_unbound(
self.unbound_name().unwrap(),
self.level().unwrap(),
self.constraint().unwrap(),
)
}
}
impl Free<TyParam> {
pub fn deep_clone(&self) -> Self {
Self::new_named_unbound(
self.unbound_name().unwrap(),
self.level().unwrap(),
self.constraint().unwrap(),
)
}
}
impl<T: StructuralEq + CanbeFree + Clone + Default> StructuralEq for Free<T> {
fn structural_eq(&self, other: &Self) -> bool {
if let (Some((l, r)), Some((l2, r2))) = (self.get_subsup(), other.get_subsup()) {

View file

@ -990,7 +990,7 @@ impl LimitedDisplay for Type {
impl CanbeFree for Type {
fn unbound_name(&self) -> Option<Str> {
if let Type::FreeVar(fv) = self {
if let Some(fv) = self.as_free() {
fv.unbound_name()
} else {
None
@ -998,7 +998,7 @@ impl CanbeFree for Type {
}
fn constraint(&self) -> Option<Constraint> {
if let Type::FreeVar(fv) = self {
if let Some(fv) = self.as_free() {
fv.constraint()
} else {
None
@ -1006,7 +1006,7 @@ impl CanbeFree for Type {
}
fn update_constraint(&self, new_constraint: Constraint, in_instantiation: bool) {
if let Self::FreeVar(fv) = self {
if let Some(fv) = self.as_free() {
fv.update_constraint(new_constraint, in_instantiation);
}
}
@ -1048,6 +1048,17 @@ impl From<Dict<Type, Type>> for Type {
}
}
impl<'t> TryFrom<&'t Type> for &'t FreeTyVar {
type Error = ();
fn try_from(t: &'t Type) -> Result<&'t FreeTyVar, ()> {
match t {
Type::FreeVar(fv) => Ok(fv),
Type::Refinement(refine) => Self::try_from(refine.t.as_ref()),
_ => Err(()),
}
}
}
impl From<Dict<Field, Type>> for Type {
fn from(rec: Dict<Field, Type>) -> Self {
Type::Record(rec)
@ -1582,6 +1593,10 @@ impl Type {
matches!(self, Self::Structural(_))
}
pub fn as_free(&self) -> Option<&FreeTyVar> {
<&FreeTyVar>::try_from(self).ok()
}
pub fn contains_tvar(&self, target: &FreeTyVar) -> bool {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_tvar(target),
@ -2331,6 +2346,7 @@ impl Type {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().clone()._replace(target, to),
Self::FreeVar(fv) => {
let fv = fv.deep_clone();
if let Some((sub, sup)) = fv.get_subsup() {
fv.forced_undoable_link(&sub);
let sub = sub._replace(target, to);