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

Fix a refinement + union types bug

Browse source
This commit is contained in:
Shunsuke Shibayama 2022-12-05 00:41:37 +09:00
parent 188f8ad965
commit 6cb3231845
12 changed files with 144 additions and 101 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -5,7 +5,9 @@ use std::option::Option;
use erg_common::error::Location;
use erg_common::traits::{Locational, Stream};
use erg_common::Str;
use erg_common::{assume_unreachable, fn_name, log};
use erg_common::{assume_unreachable, fn_name};
#[allow(unused_imports)]
use erg_common::{fmt_vec, log};
use crate::ty::constructors::*;
use crate::ty::free::{Constraint, FreeKind, HasLevel};
@ -421,7 +423,7 @@ impl Context {
}
Type::Poly { name, mut params } => {
let typ = poly(&name, params.clone());
let ctx = self.get_nominal_type_ctx(&typ).unwrap();
let (_, ctx) = self.get_nominal_type_ctx(&typ).unwrap();
let variances = ctx.type_params_variance();
for (param, variance) in params.iter_mut().zip(variances.into_iter()) {
*param = self.deref_tp(mem::take(param), variance, loc)?;
@ -1504,55 +1506,65 @@ impl Context {
},
) => {
// e.g. Set(?T) <: Eq(Set(?T))
// Array(Str) <: Iterable(Str)
if ln != rn {
if let Some(sub_ctx) = self.get_nominal_type_ctx(maybe_sub) {
if let Some((sub_def_t, sub_ctx)) = self.get_nominal_type_ctx(maybe_sub) {
self.substitute_typarams(sub_def_t, maybe_sub);
for sup_trait in sub_ctx.super_traits.iter() {
if self.supertype_of(maybe_sup, sup_trait) {
for (l_maybe_sub, r_maybe_sup) in sup_trait.typarams().iter().zip(rps.iter()) {
self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)
.map_err(|e| { self.undo_substitute_typarams(sub_def_t); e })?;
}
self.undo_substitute_typarams(sub_def_t);
return Ok(());
}
}
}
return Err(TyCheckErrors::from(TyCheckError::unification_error(
Err(TyCheckErrors::from(TyCheckError::unification_error(
self.cfg.input.clone(),
line!() as usize,
maybe_sub,
maybe_sup,
loc,
self.caused_by(),
)));
)))
} else {
for (l_maybe_sub, r_maybe_sup) in lps.iter().zip(rps.iter()) {
self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
}
Ok(())
}
for (l_maybe_sub, r_maybe_sup) in lps.iter().zip(rps.iter()) {
self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
}
Ok(())
}
(Type::And(l, r), _)
| (Type::Or(l, r), _)
| (Type::Not(l, r), _) => {
// (X or Y) <: Z is valid when X <: Z and Y <: Z
(Type::Or(l, r), _) => {
self.sub_unify(l, maybe_sup, loc, param_name)?;
self.sub_unify(r, maybe_sup, loc, param_name)?;
Ok(())
self.sub_unify(r, maybe_sup, loc, param_name)
}
(_, Type::And(l, r))
| (_, Type::Or(l, r))
| (_, Type::Not(l, r)) => {
// X <: (Y and Z) is valid when X <: Y and X <: Z
(_, Type::And(l, r)) => {
self.sub_unify(maybe_sub, l, loc, param_name)?;
self.sub_unify(maybe_sub, r, loc, param_name)?;
Ok(())
self.sub_unify(maybe_sub, r, loc, param_name)
}
// (X and Y) <: Z is valid when X <: Z or Y <: Z
(Type::And(l, r), _) => {
self.sub_unify(l, maybe_sup, loc, param_name)
.or_else(|_e| self.sub_unify(r, maybe_sup, loc, param_name))
}
// X <: (Y or Z) is valid when X <: Y or X <: Z
(_, Type::Or(l, r)) => {
self.sub_unify(maybe_sub, l, loc, param_name)
.or_else(|_e| self.sub_unify(maybe_sub, r, loc, param_name))
}
(_, Type::Ref(t)) => {
self.sub_unify(maybe_sub, t, loc, param_name)?;
Ok(())
self.sub_unify(maybe_sub, t, loc, param_name)
}
(_, Type::RefMut{ before, .. }) => {
self.sub_unify(maybe_sub, before, loc, param_name)?;
Ok(())
self.sub_unify(maybe_sub, before, loc, param_name)
}
(Type::Proj { .. }, _) => todo!(),
(_, Type::Proj { .. }) => todo!(),
// TODO: Judgment for any number of preds
(Refinement(sub), Refinement(sup)) => {
// {I: Int or Str | I == 0} <: {I: Int}
if self.subtype_of(&sub.t, &sup.t) {