mirror of
https://github.com/erg-lang/erg.git
synced 2025-09-27 11:59:05 +00:00
fix: constraints instantiation bug
This commit is contained in:
parent
5d8506b548
commit
814748a6be
8 changed files with 69 additions and 31 deletions
|
@ -1287,7 +1287,7 @@ impl Context {
|
||||||
t.clone()
|
t.clone()
|
||||||
} else {
|
} else {
|
||||||
let tv = Type::FreeVar(new_fv);
|
let tv = Type::FreeVar(new_fv);
|
||||||
tv_cache.push_or_init_tyvar(&name, &tv);
|
tv_cache.push_or_init_tyvar(&name, &tv, self);
|
||||||
tv
|
tv
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -350,6 +350,7 @@ impl Context {
|
||||||
{
|
{
|
||||||
Ok(TyParam::FreeVar(fv))
|
Ok(TyParam::FreeVar(fv))
|
||||||
}
|
}
|
||||||
|
// REVIEW: most likely the result of an error already made
|
||||||
TyParam::FreeVar(_fv) if self.level == 0 => Err(TyCheckErrors::from(
|
TyParam::FreeVar(_fv) if self.level == 0 => Err(TyCheckErrors::from(
|
||||||
TyCheckError::dummy_infer_error(self.cfg.input.clone(), fn_name!(), line!()),
|
TyCheckError::dummy_infer_error(self.cfg.input.clone(), fn_name!(), line!()),
|
||||||
)),
|
)),
|
||||||
|
@ -629,7 +630,11 @@ impl Context {
|
||||||
let res = self.validate_subsup(sub_t, super_t, variance, qnames, loc);
|
let res = self.validate_subsup(sub_t, super_t, variance, qnames, loc);
|
||||||
fv.undo();
|
fv.undo();
|
||||||
match res {
|
match res {
|
||||||
Ok(ty) => Ok(ty),
|
Ok(ty) => {
|
||||||
|
// TODO: T(:> Nat <: Int) -> T(:> Nat, <: Int) ==> Int -> Nat
|
||||||
|
// fv.link(&ty);
|
||||||
|
Ok(ty)
|
||||||
|
}
|
||||||
Err(errs) => {
|
Err(errs) => {
|
||||||
fv.link(&Never);
|
fv.link(&Never);
|
||||||
Err(errs)
|
Err(errs)
|
||||||
|
@ -637,7 +642,6 @@ impl Context {
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
// no dereference at this point
|
// no dereference at this point
|
||||||
// drop(constraint);
|
|
||||||
Ok(Type::FreeVar(fv))
|
Ok(Type::FreeVar(fv))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -848,6 +848,10 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
let coerced = self
|
||||||
|
.deref_tyvar(obj.t(), Variance::Covariant, &set! {}, obj)
|
||||||
|
.map_err(|mut errs| errs.remove(0))?;
|
||||||
|
if &coerced == obj.ref_t() {
|
||||||
Err(TyCheckError::no_attr_error(
|
Err(TyCheckError::no_attr_error(
|
||||||
self.cfg.input.clone(),
|
self.cfg.input.clone(),
|
||||||
line!() as usize,
|
line!() as usize,
|
||||||
|
@ -857,6 +861,10 @@ impl Context {
|
||||||
attr_name.inspect(),
|
attr_name.inspect(),
|
||||||
self.get_similar_attr(obj.ref_t(), attr_name.inspect()),
|
self.get_similar_attr(obj.ref_t(), attr_name.inspect()),
|
||||||
))
|
))
|
||||||
|
} else {
|
||||||
|
obj.ref_t().coerce();
|
||||||
|
self.search_method_info(obj, attr_name, input, namespace)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn validate_visibility(
|
fn validate_visibility(
|
||||||
|
|
|
@ -121,39 +121,60 @@ impl TyVarCache {
|
||||||
self.already_appeared.insert(name);
|
self.already_appeared.insert(name);
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn push_or_init_tyvar(&mut self, name: &Str, tv: &Type) {
|
pub(crate) fn push_or_init_tyvar(&mut self, name: &Str, tv: &Type, ctx: &Context) {
|
||||||
if let Some(inst) = self.tyvar_instances.get(name) {
|
if let Some(inst) = self.tyvar_instances.get(name) {
|
||||||
// T<tv> <: Eq(T<inst>)
|
self.update_tv(inst, tv, ctx);
|
||||||
// T<inst> is uninitialized
|
|
||||||
// T<inst>.link(T<tv>);
|
|
||||||
// T <: Eq(T <: Eq(T <: ...))
|
|
||||||
let inst = enum_unwrap!(inst, Type::FreeVar);
|
|
||||||
inst.link(tv);
|
|
||||||
} else if let Some(inst) = self.typaram_instances.get(name) {
|
} else if let Some(inst) = self.typaram_instances.get(name) {
|
||||||
if let TyParam::Type(inst) = inst {
|
if let TyParam::Type(inst) = inst {
|
||||||
let fv_inst = enum_unwrap!(inst.as_ref(), Type::FreeVar);
|
self.update_tv(inst, tv, ctx);
|
||||||
fv_inst.link(tv);
|
|
||||||
} else if let TyParam::FreeVar(fv) = inst {
|
} else if let TyParam::FreeVar(fv) = inst {
|
||||||
fv.link(&TyParam::t(tv.clone()));
|
fv.link(&TyParam::t(tv.clone()));
|
||||||
} else {
|
} else {
|
||||||
unreachable!()
|
unreachable!()
|
||||||
}
|
}
|
||||||
}
|
} else {
|
||||||
self.tyvar_instances.insert(name.clone(), tv.clone());
|
self.tyvar_instances.insert(name.clone(), tv.clone());
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn update_tv(&self, inst: &Type, tv: &Type, ctx: &Context) {
|
||||||
|
// T<tv> <: Eq(T<inst>)
|
||||||
|
// T<inst> is uninitialized
|
||||||
|
// T<inst>.link(T<tv>);
|
||||||
|
// T <: Eq(T <: Eq(T <: ...))
|
||||||
|
let inst = enum_unwrap!(inst, Type::FreeVar);
|
||||||
|
if inst.constraint_is_uninited() {
|
||||||
|
inst.link(tv);
|
||||||
|
} else {
|
||||||
|
// inst: ?T(<: Int) => old_sub: Never, old_sup: Int
|
||||||
|
// tv: ?T(:> Nat) => new_sub: Nat, new_sup: Obj
|
||||||
|
// => ?T(:> Nat, <: Int)
|
||||||
|
// inst: ?T(:> Str)
|
||||||
|
// tv: ?T(:> Nat)
|
||||||
|
// => ?T(:> Nat or Str)
|
||||||
|
let (old_sub, old_sup) = inst.get_subsup().unwrap();
|
||||||
|
let tv = enum_unwrap!(tv, Type::FreeVar);
|
||||||
|
let (new_sub, new_sup) = tv.get_subsup().unwrap();
|
||||||
|
let new_constraint = Constraint::new_sandwiched(
|
||||||
|
ctx.union(&old_sub, &new_sub),
|
||||||
|
ctx.intersection(&old_sup, &new_sup),
|
||||||
|
);
|
||||||
|
inst.update_constraint(new_constraint, true);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub(crate) fn push_or_init_typaram(&mut self, name: &Str, tp: &TyParam) {
|
pub(crate) fn push_or_init_typaram(&mut self, name: &Str, tp: &TyParam) {
|
||||||
// FIXME:
|
// FIXME:
|
||||||
if let Some(_tp) = self.typaram_instances.get(name) {
|
if let Some(_tp) = self.typaram_instances.get(name) {
|
||||||
panic!("{_tp} {tp}");
|
panic!("{_tp} {tp}");
|
||||||
// return;
|
// return;
|
||||||
}
|
} else if let Some(_t) = self.tyvar_instances.get(name) {
|
||||||
if let Some(_t) = self.tyvar_instances.get(name) {
|
|
||||||
panic!("{_t} {tp}");
|
panic!("{_t} {tp}");
|
||||||
// return;
|
// return;
|
||||||
}
|
} else {
|
||||||
self.typaram_instances.insert(name.clone(), tp.clone());
|
self.typaram_instances.insert(name.clone(), tp.clone());
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub(crate) fn appeared(&self, name: &Str) -> bool {
|
pub(crate) fn appeared(&self, name: &Str) -> bool {
|
||||||
self.already_appeared.contains(name)
|
self.already_appeared.contains(name)
|
||||||
|
@ -386,7 +407,7 @@ impl Context {
|
||||||
} else {
|
} else {
|
||||||
if tmp_tv_cache.appeared(&name) {
|
if tmp_tv_cache.appeared(&name) {
|
||||||
let tyvar = named_free_var(name.clone(), self.level, Constraint::Uninited);
|
let tyvar = named_free_var(name.clone(), self.level, Constraint::Uninited);
|
||||||
tmp_tv_cache.push_or_init_tyvar(&name, &tyvar);
|
tmp_tv_cache.push_or_init_tyvar(&name, &tyvar, self);
|
||||||
return Ok(tyvar);
|
return Ok(tyvar);
|
||||||
}
|
}
|
||||||
if let Some(tv_ctx) = &self.tv_cache {
|
if let Some(tv_ctx) = &self.tv_cache {
|
||||||
|
@ -407,7 +428,7 @@ impl Context {
|
||||||
tmp_tv_cache.push_appeared(name.clone());
|
tmp_tv_cache.push_appeared(name.clone());
|
||||||
let constr = tmp_tv_cache.instantiate_constraint(constr, self, loc)?;
|
let constr = tmp_tv_cache.instantiate_constraint(constr, self, loc)?;
|
||||||
let tyvar = named_free_var(name.clone(), self.level, constr);
|
let tyvar = named_free_var(name.clone(), self.level, constr);
|
||||||
tmp_tv_cache.push_or_init_tyvar(&name, &tyvar);
|
tmp_tv_cache.push_or_init_tyvar(&name, &tyvar, self);
|
||||||
Ok(tyvar)
|
Ok(tyvar)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -124,7 +124,7 @@ impl Context {
|
||||||
// TODO: other than type `Type`
|
// TODO: other than type `Type`
|
||||||
let constr = Constraint::new_type_of(Type);
|
let constr = Constraint::new_type_of(Type);
|
||||||
let tv = named_free_var(name.inspect().clone(), self.level, constr);
|
let tv = named_free_var(name.inspect().clone(), self.level, constr);
|
||||||
tv_cache.push_or_init_tyvar(name.inspect(), &tv);
|
tv_cache.push_or_init_tyvar(name.inspect(), &tv, self);
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
TypeBoundSpec::NonDefault { lhs, spec } => {
|
TypeBoundSpec::NonDefault { lhs, spec } => {
|
||||||
|
@ -150,7 +150,7 @@ impl Context {
|
||||||
tv_cache.push_or_init_typaram(lhs.inspect(), &tp);
|
tv_cache.push_or_init_typaram(lhs.inspect(), &tp);
|
||||||
} else {
|
} else {
|
||||||
let tv = named_free_var(lhs.inspect().clone(), self.level, constr);
|
let tv = named_free_var(lhs.inspect().clone(), self.level, constr);
|
||||||
tv_cache.push_or_init_tyvar(lhs.inspect(), &tv);
|
tv_cache.push_or_init_tyvar(lhs.inspect(), &tv, self);
|
||||||
}
|
}
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
@ -595,7 +595,7 @@ impl Context {
|
||||||
Ok(typ.clone())
|
Ok(typ.clone())
|
||||||
} else if not_found_is_qvar {
|
} else if not_found_is_qvar {
|
||||||
let tyvar = named_free_var(Str::rc(other), self.level, Constraint::Uninited);
|
let tyvar = named_free_var(Str::rc(other), self.level, Constraint::Uninited);
|
||||||
tmp_tv_cache.push_or_init_tyvar(simple.ident.inspect(), &tyvar);
|
tmp_tv_cache.push_or_init_tyvar(simple.ident.inspect(), &tyvar, self);
|
||||||
Ok(tyvar)
|
Ok(tyvar)
|
||||||
} else {
|
} else {
|
||||||
Err(TyCheckErrors::from(TyCheckError::no_type_error(
|
Err(TyCheckErrors::from(TyCheckError::no_type_error(
|
||||||
|
|
|
@ -838,6 +838,7 @@ impl<T: CanbeFree> Free<T> {
|
||||||
self.constraint().map(|c| c.is_uninited()).unwrap_or(false)
|
self.constraint().map(|c| c.is_uninited()).unwrap_or(false)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// 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) {
|
pub fn update_constraint(&self, new_constraint: Constraint, in_inst_or_gen: bool) {
|
||||||
match unsafe { &mut *self.as_ptr() as &mut FreeKind<T> } {
|
match unsafe { &mut *self.as_ptr() as &mut FreeKind<T> } {
|
||||||
FreeKind::Unbound {
|
FreeKind::Unbound {
|
||||||
|
|
|
@ -33,3 +33,7 @@ for! "aaa", a =>
|
||||||
print! a # OK
|
print! a # OK
|
||||||
for! "aaa", a =>
|
for! "aaa", a =>
|
||||||
print! a + 1 # ERR
|
print! a + 1 # ERR
|
||||||
|
|
||||||
|
inty|T :> Nat, T <: Int|(x: T) = x + x
|
||||||
|
inty 0 # OK
|
||||||
|
inty 1.1 # ERR
|
||||||
|
|
|
@ -278,7 +278,7 @@ fn exec_structural_err() -> Result<(), ()> {
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn exec_subtyping_err() -> Result<(), ()> {
|
fn exec_subtyping_err() -> Result<(), ()> {
|
||||||
expect_failure("tests/should_err/subtyping.er", 6)
|
expect_failure("tests/should_err/subtyping.er", 7)
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue