language-servers/erg
1
0
Fork 0
mirror of https://github.com/erg-lang/erg.git synced 2025-09-30 21:01:10 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix subtyping bugs

Browse source
This commit is contained in:
Shunsuke Shibayama 2022-10-05 11:53:29 +09:00
parent 4d7181f2f0
commit 85c6057d7c
15 changed files with 224 additions and 152 deletions
Download patch file Download diff file Expand all files Collapse all files

4
compiler/erg_compiler/context/compare.rs
View file

@ -829,7 +829,7 @@ impl Context {
/// returns union of two types (A or B)
pub(crate) fn union(&self, lhs: &Type, rhs: &Type) -> Type {
// ?T or ?U will not be unified
if !lhs.is_unbound_var() && !rhs.is_unbound_var() {
if lhs.has_no_unbound_var() && rhs.has_no_unbound_var() {
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) => return lhs.clone(), // lhs = rhs
(true, false) => return lhs.clone(), // lhs :> rhs
@ -1035,7 +1035,7 @@ impl Context {
}
}
pub(crate) fn max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
pub(crate) fn _max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
// 同じならどちらを返しても良い
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) | (true, false) => Some(lhs),

17
compiler/erg_compiler/context/eval.rs
View file

@ -2,6 +2,7 @@ use std::fmt;
use std::mem;
use erg_common::dict::Dict;
use erg_common::enum_unwrap;
use erg_common::error::Location;
use erg_common::set::Set;
use erg_common::shared::Shared;
@ -828,6 +829,22 @@ impl Context {
}
}
}
if lhs.is_unbound_var() {
let (sub, sup) = enum_unwrap!(lhs.as_ref(), Type::FreeVar)
.get_bound_types()
.unwrap();
if self.is_trait(&sup) && !self.trait_impl_exists(&sub, &sup) {
return Err(EvalErrors::from(EvalError::no_trait_impl_error(
self.cfg.input.clone(),
line!() as usize,
&sub,
&sup,
t_loc,
self.caused_by(),
None,
)));
}
}
// if the target can't be found in the supertype, the type will be dereferenced.
// In many cases, it is still better to determine the type variable than if the target is not found.
let coerced = self.deref_tyvar(*lhs.clone(), Variance::Covariant, t_loc)?;

10
compiler/erg_compiler/context/register.rs
View file

@ -348,12 +348,13 @@ impl Context {
sig: &ast::SubrSignature,
id: DefId,
body_t: &Type,
) -> TyCheckResult<()> {
) -> TyCheckResult<Type> {
// already defined as const
if sig.is_const() {
let vi = self.decls.remove(sig.ident.inspect()).unwrap();
let t = vi.t.clone();
self.locals.insert(sig.ident.name.clone(), vi);
return Ok(());
return Ok(t);
}
let muty = if sig.ident.is_const() {
Mutability::Const
@ -443,9 +444,10 @@ impl Context {
VarKind::Defined(id),
Some(comptime_decos),
);
log!(info "Registered {}::{name}: {}", self.name, &vi.t);
let t = vi.t.clone();
log!(info "Registered {}::{name}: {}", self.name, t);
self.locals.insert(name.clone(), vi);
Ok(())
Ok(t)
}
pub(crate) fn fake_subr_assign(&mut self, sig: &ast::SubrSignature, failure_t: Type) {

99
compiler/erg_compiler/context/tyvar.rs
View file

@ -125,6 +125,9 @@ impl Context {
if l == r {
fv.forced_link(&l.clone());
FreeVar(fv.clone())
} else if r != &Obj && self.is_class(r) {
// x: T <: Bool ==> x: Bool
r.clone()
} else {
let name = format!("%{id}");
self.generalize_constraint(&name, constraint, bounds, lazy_inits);
@ -346,7 +349,7 @@ impl Context {
self.check_trait_exists(sub_t, loc)?;
}*/
if self.is_trait(super_t) {
self.check_trait_exists(sub_t, super_t, loc)?;
self.check_trait_impl(sub_t, super_t, loc)?;
}
// REVIEW: Even if type constraints can be satisfied, implementation may not exist
if self.subtype_of(sub_t, super_t) {
@ -508,20 +511,26 @@ impl Context {
}
}
fn check_trait_exists(
pub(crate) fn trait_impl_exists(&self, class: &Type, trait_: &Type) -> bool {
let mut super_exists = false;
for inst in self.get_trait_impls(trait_).into_iter() {
if self.supertype_of(&inst.sub_type, class)
&& self.supertype_of(&inst.sup_trait, trait_)
{
super_exists = true;
break;
}
}
super_exists
}
fn check_trait_impl(
&self,
class: &Type,
trait_: &Type,
loc: Location,
) -> SingleTyCheckResult<()> {
let mut super_exists = false;
for inst in self.get_trait_impls(trait_).into_iter() {
if self.supertype_of(&inst.sup_trait, trait_) {
super_exists = true;
break;
}
}
if !super_exists {
if !self.trait_impl_exists(class, trait_) {
Err(TyCheckError::no_trait_impl_error(
self.cfg.input.clone(),
line!() as usize,
@ -675,17 +684,23 @@ impl Context {
Ok(())
}
hir::Expr::Def(def) => {
match &mut def.sig {
hir::Signature::Var(var) => {
var.t = self.deref_tyvar(mem::take(&mut var.t), Covariant, var.loc())?;
// It is not possible to further dereference the quantified type.
// TODO: However, it is possible that there are external type variables within the quantified type.
if !def.sig.ref_t().is_quantified() {
match &mut def.sig {
hir::Signature::Var(var) => {
var.t =
self.deref_tyvar(mem::take(&mut var.t), Covariant, var.loc())?;
}
hir::Signature::Subr(subr) => {
subr.t =
self.deref_tyvar(mem::take(&mut subr.t), Covariant, subr.loc())?;
}
}
hir::Signature::Subr(subr) => {
subr.t = self.deref_tyvar(mem::take(&mut subr.t), Covariant, subr.loc())?;
for chunk in def.body.block.iter_mut() {
self.resolve_expr_t(chunk)?;
}
}
for chunk in def.body.block.iter_mut() {
self.resolve_expr_t(chunk)?;
}
Ok(())
}
hir::Expr::Lambda(lambda) => {
@ -1231,29 +1246,15 @@ impl Context {
// * sub_unify(Str, ?T(:> Int, <: Obj)): (?T(:> Str or Int, <: Obj))
// * sub_unify({0}, ?T(:> {1}, <: Nat)): (?T(:> {0, 1}, <: Nat))
Constraint::Sandwiched { sub, sup, cyclicity } => {
/*let judge = match cyclicity {
Cyclicity::Super => self.cyclic_supertype_of(rfv, maybe_sub),
Cyclicity::Not => self.supertype_of(sup, maybe_sub),
_ => todo!(),
};
if !judge {
return Err(TyCheckErrors::from(TyCheckError::subtyping_error(
self.cfg.input.clone(),
line!() as usize,
maybe_sub,
sup, // TODO: this?
sub_loc,
sup_loc,
self.caused_by(),
)));
}*/
if let Some(new_sub) = self.max(maybe_sub, sub) {
/*if let Some(new_sub) = self.max(maybe_sub, sub) {
*constraint =
Constraint::new_sandwiched(new_sub.clone(), mem::take(sup), *cyclicity);
} else {
let new_sub = self.union(maybe_sub, sub);
*constraint = Constraint::new_sandwiched(new_sub, mem::take(sup), *cyclicity);
}
} else {*/
erg_common::log!(err "{maybe_sub}, {sub}");
let new_sub = self.union(maybe_sub, sub);
erg_common::log!(err "{new_sub}");
*constraint = Constraint::new_sandwiched(new_sub, mem::take(sup), *cyclicity);
// }
}
// sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
Constraint::TypeOf(ty) => {
@ -1285,18 +1286,7 @@ impl Context {
// sup = union(sup, r) if min does not exist
// * sub_unify(?T(:> Never, <: {1}), {0}): (?T(:> Never, <: {0, 1}))
Constraint::Sandwiched { sub, sup, cyclicity } => {
// maybe_sup: Ref(Obj), sub: Never, sup: Show and Obj
/*if !self.subtype_of(sub, maybe_sup) || !self.supertype_of(sup, maybe_sup) {
return Err(TyCheckErrors::from(TyCheckError::subtyping_error(
self.cfg.input.clone(),
line!() as usize,
sub,
maybe_sup,
sub_loc,
sup_loc,
self.caused_by(),
)));
}*/
// REVIEW: correct?
if let Some(new_sup) = self.min(sup, maybe_sup) {
*constraint =
Constraint::new_sandwiched(mem::take(sub), new_sup.clone(), *cyclicity);
@ -1411,6 +1401,13 @@ impl Context {
self.sub_unify(r, maybe_sup, loc, param_name)?;
Ok(())
}
(_, Type::And(l, r))
| (_, Type::Or(l, r))
| (_, Type::Not(l, r)) => {
self.sub_unify(maybe_sub, l, loc, param_name)?;
self.sub_unify(maybe_sub, r, loc, param_name)?;
Ok(())
}
(_, Type::Ref(t)) => {
self.sub_unify(maybe_sub, t, loc, param_name)?;
Ok(())

5
compiler/erg_compiler/lower.rs
View file

@ -722,13 +722,14 @@ impl ASTLowerer {
}
}
let id = body.id;
self.ctx
let t = self
.ctx
.outer
.as_mut()
.unwrap()
.assign_subr(&sig, id, found_body_t)?;
let ident = hir::Identifier::bare(sig.ident.dot, sig.ident.name);
let sig = hir::SubrSignature::new(ident, sig.params, Type::Subr(t));
let sig = hir::SubrSignature::new(ident, sig.params, t);
let body = hir::DefBody::new(body.op, block, body.id);
Ok(hir::Def::new(hir::Signature::Subr(sig), body))
}

15
compiler/erg_type/lib.rs
View file

@ -940,11 +940,12 @@ impl LimitedDisplay for RefinementType {
return write!(f, "...");
}
let first_subj = self.preds.iter().next().and_then(|p| p.subject());
if self
let is_simple_type = self.t.is_simple_class();
let is_simple_preds = self
.preds
.iter()
.all(|p| p.is_equal() && p.subject() == first_subj)
{
.all(|p| p.is_equal() && p.subject() == first_subj);
if is_simple_type && is_simple_preds {
write!(f, "{{")?;
for pred in self.preds.iter() {
let (_, rhs) = enum_unwrap!(pred, Predicate::Equal { lhs, rhs });
@ -1753,6 +1754,14 @@ impl Type {
}
}
pub fn is_quantified(&self) -> bool {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_quantified(),
Self::Quantified(_) => true,
_ => false,
}
}
pub fn contains_tvar(&self, name: &str) -> bool {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_tvar(name),

82
library/std/_prelude.er Normal file
View file

@ -0,0 +1,82 @@
@Attach NeImpl
Eq(R := Self) = Trait {
.`==` = (self: Self, R) -> Bool
}
NeImpl R = Patch Eq R
NeImpl(R).
`!=`(self, other: R): Bool = not(self == other)
@Attach EqImpl, LeImpl, LtImpl, GeImpl, GtImpl
PartialOrd(R := Self) = Trait {
.cmp = (self: Self, R) -> Option Ordering
}
Ord = Subsume PartialOrd()
EqForOrd R = Patch Ord, Impl := Eq()
EqForOrd(R).
`==`(self, other: R): Bool = self.cmp(other) == Ordering.Equal
LeForOrd = Patch Ord
LeForOrd.
`<=`(self, other: Self): Bool = self.cmp(other) == Ordering.Less or self == other
LtForOrd = Patch Ord
LtForOrd.
`<`(self, other: Self): Bool = self.cmp(other) == Ordering.Less
GeForOrd = Patch Ord
GeForOrd.
`>=`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater or self == other
GtForOrd = Patch Ord
GtForOrd.
`>`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater
Add(R := Self) = Trait {
.Output = Type
.`_+_` = (self: Self, R) -> Self.Output
}
Sub(R := Self) = Trait {
.Output = Type
.`_-_` = (self: Self, R) -> Self.Output
}
Mul(R := Self()) = Trait {
.Output = Type
.`*` = (self: Self, R) -> Self.Output
}
Div(R := Self) = Trait {
.Output = Type
.`/` = (self: Self, R) -> Self.Output or Panic
}
Num: (R := Type) -> Type
Num = Add and Sub and Mul
Seq T = Trait {
.__len__ = (self: Ref(Self)) -> Nat
.get = (self: Ref(Self), Nat) -> T
}
`_+_`: |R: Type, A <: Add(R)| (A, R) -> A.AddO
`_-_`: |R: Type, S <: Add(R)| (S, R) -> S.SubO
`*`: |R, O: Type, M <: Add(R)| (M, R) -> M.MulO
`/`: |R, O: Type, D <: Add(R)| (D, R) -> D.DivO
AddForInt = Patch Int, Impl := Add()
AddForInt.AddO = Int
AddForInt.
`_+_`: (self: Self, other: Int) -> Int = magic("Add.`_+_`")
# TODO: Mul and Div
NumForInterval M, N, O, P: Int =
Patch M..N, Impl := Add(R := O..P) and Sub(R := O..P)
NumForInterval(M, N, O, P).
`_+_`: (self: Self, other: O..P) -> M+O..N+P = magic("NumForInterval.`_+_`")
`_-_`: (self: Self, other: O..P) -> M-P..N-O = magic("NumForInterval.`_-_`")
Read = Trait {
.read = (self: Ref(Self)) -> Str
}
Read! = Trait {
.read! = (self: Ref!(Self)) => Str
}
Write! = Trait {
.write! = (self: Ref!(Self), Str) => ()
}

88
library/std/prelude.er
View file

@ -1,82 +1,12 @@
@Attach NeImpl
Eq(R := Self) = Trait {
.`==` = (self: Self, R) -> Bool
}
discard _x = None
NeImpl R = Patch Eq R
NeImpl(R).
`!=`(self, other: R): Bool = not(self == other)
discard 1
@Attach EqImpl, LeImpl, LtImpl, GeImpl, GtImpl
PartialOrd(R := Self) = Trait {
.cmp = (self: Self, R) -> Option Ordering
}
Ord = Subsume PartialOrd()
cond c, then, else =
if c:
do then
do else
EqForOrd R = Patch Ord, Impl := Eq()
EqForOrd(R).
`==`(self, other: R): Bool = self.cmp(other) == Ordering.Equal
LeForOrd = Patch Ord
LeForOrd.
`<=`(self, other: Self): Bool = self.cmp(other) == Ordering.Less or self == other
LtForOrd = Patch Ord
LtForOrd.
`<`(self, other: Self): Bool = self.cmp(other) == Ordering.Less
GeForOrd = Patch Ord
GeForOrd.
`>=`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater or self == other
GtForOrd = Patch Ord
GtForOrd.
`>`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater
Add(R := Self) = Trait {
.Output = Type
.`_+_` = (self: Self, R) -> Self.Output
}
Sub(R := Self) = Trait {
.Output = Type
.`_-_` = (self: Self, R) -> Self.Output
}
Mul(R := Self()) = Trait {
.Output = Type
.`*` = (self: Self, R) -> Self.Output
}
Div(R := Self) = Trait {
.Output = Type
.`/` = (self: Self, R) -> Self.Output or Panic
}
Num: (R := Type) -> Type
Num = Add and Sub and Mul
Seq T = Trait {
.__len__ = (self: Ref(Self)) -> Nat
.get = (self: Ref(Self), Nat) -> T
}
`_+_`: |R: Type, A <: Add(R)| (A, R) -> A.AddO
`_-_`: |R: Type, S <: Add(R)| (S, R) -> S.SubO
`*`: |R, O: Type, M <: Add(R)| (M, R) -> M.MulO
`/`: |R, O: Type, D <: Add(R)| (D, R) -> D.DivO
AddForInt = Patch Int, Impl := Add()
AddForInt.AddO = Int
AddForInt.
`_+_`: (self: Self, other: Int) -> Int = magic("Add.`_+_`")
# TODO: Mul and Div
NumForInterval M, N, O, P: Int =
Patch M..N, Impl := Add(R := O..P) and Sub(R := O..P)
NumForInterval(M, N, O, P).
`_+_`: (self: Self, other: O..P) -> M+O..N+P = magic("NumForInterval.`_+_`")
`_-_`: (self: Self, other: O..P) -> M-P..N-O = magic("NumForInterval.`_-_`")
Read = Trait {
.read = (self: Ref(Self)) -> Str
}
Read! = Trait {
.read! = (self: Ref!(Self)) => Str
}
Write! = Trait {
.write! = (self: Ref!(Self), Str) => ()
}
assert cond(False, 1, 2) == 2
# assert cond(True, 1, 3) == "a"
# assert "a" == cond(True, 1, 3)

5
tests/add.er
View file

@ -1,5 +0,0 @@
add x, y =
x + y
print! 1 + 1
print! 1.0 + 1

7
tests/addition.er Normal file
View file

@ -0,0 +1,7 @@
add x, y =
x + y
print! add(1, 1)
print! add(1.0, 1)
print! add("a", "b")
print! add("a", 1) # this will be an error

10
tests/fizzbuzz.er
View file

@ -1,6 +1,6 @@
for! 1..100, i =>
for! 1..<100, i =>
match (i % 3, i % 5):
0, 0 => print! "FizzBuzz"
0, _ => print! "Fizz"
_, 0 => print! "Buzz"
_ => print! i
(0, 0) => print! "FizzBuzz"
(0, _) => print! "Fizz"
(_, 0) => print! "Buzz"
(_, _) => print! i

2
tests/mut_array.er
View file

@ -1,5 +1,5 @@
v = ![]
for! 0..10, i =>
for! 0..<10, i =>
v.push! i
log v.sum()

10
tests/rec.er Normal file
View file

@ -0,0 +1,10 @@
stop_or_call n, f: (Nat -> Nat), g: (Nat -> Nat) =
cond n <= 0:
1
g (f (n - 1))
fact(n: Nat): Nat =
stop_or_call n, fact, (r, ) -> r * n
print! fact
print! fact 5

6
tests/subtyping.er Normal file
View file

@ -0,0 +1,6 @@
f(x: Nat): Int = x
y: Ratio = f 1
# Erg's type checking does not necessarily enlarge the type. So this is OK.
z: Int = y
# But this is invalid.
invalid: 10..<20 = z

16
tests/test.rs
View file

@ -6,6 +6,11 @@ use erg_common::traits::Runnable;
use erg::dummy::DummyVM;
#[test]
fn exec_addition() -> Result<(), ()> {
expect_failure("tests/addition.er")
}
#[test]
fn exec_class() -> Result<(), ()> {
expect_success("examples/class.er")
@ -41,6 +46,12 @@ fn exec_quantified() -> Result<(), ()> {
expect_success("examples/quantified.er")
}
#[test]
fn exec_rec() -> Result<(), ()> {
// this script is valid but the current code generating process has a bug.
expect_end_with("tests/rec.er", 1)
}
#[test]
fn exec_record() -> Result<(), ()> {
expect_success("examples/record.er")
@ -51,6 +62,11 @@ fn exec_side_effect() -> Result<(), ()> {
expect_failure("examples/side_effect.er")
}
#[test]
fn exec_subtyping() -> Result<(), ()> {
expect_failure("tests/subtyping.er")
}
#[test]
fn exec_trait() -> Result<(), ()> {
expect_success("examples/trait.er")