From af3ece6a1becaec735fa1866f379199897f8fc6f Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Thu, 22 Dec 2022 17:56:42 +0900 Subject: [PATCH] Fix a subtype unification bug --- .../erg_compiler/context/initialize/mod.rs | 66 +++++++++++++++---- compiler/erg_compiler/context/inquire.rs | 3 + compiler/erg_compiler/context/instantiate.rs | 2 + compiler/erg_compiler/context/tyvar.rs | 16 +++-- tests/should_err/subtyping.er | 5 +- tests/test.rs | 2 +- 6 files changed, 74 insertions(+), 20 deletions(-) diff --git a/compiler/erg_compiler/context/initialize/mod.rs b/compiler/erg_compiler/context/initialize/mod.rs index 280ef678..c48f0885 100644 --- a/compiler/erg_compiler/context/initialize/mod.rs +++ b/compiler/erg_compiler/context/initialize/mod.rs @@ -41,6 +41,13 @@ use Visibility::*; impl Context { fn register_builtin_decl(&mut self, name: &'static str, t: Type, vis: Visibility) { + if cfg!(feature = "debug") { + if let Type::Subr(subr) = &t { + if subr.has_qvar() { + panic!("not quantified subr: {subr}"); + } + } + } let impl_of = if let ContextKind::MethodDefs(Some(tr)) = &self.kind { Some(tr.clone()) } else { @@ -64,6 +71,13 @@ impl Context { vis: Visibility, py_name: Option<&'static str>, ) { + if cfg!(feature = "debug") { + if let Type::Subr(subr) = &t { + if subr.has_qvar() { + panic!("not quantified subr: {subr}"); + } + } + } let impl_of = if let ContextKind::MethodDefs(Some(tr)) = &self.kind { Some(tr.clone()) } else { @@ -103,6 +117,13 @@ impl Context { muty: Mutability, vis: Visibility, ) { + if cfg!(feature = "debug") { + if let Type::Subr(subr) = &t { + if subr.has_qvar() { + panic!("not quantified subr: {subr}"); + } + } + } let impl_of = if let ContextKind::MethodDefs(Some(tr)) = &self.kind { Some(tr.clone()) } else { @@ -127,6 +148,13 @@ impl Context { vis: Visibility, py_name: Option<&'static str>, ) { + if cfg!(feature = "debug") { + if let Type::Subr(subr) = &t { + if subr.has_qvar() { + panic!("not quantified subr: {subr}"); + } + } + } let impl_of = if let ContextKind::MethodDefs(Some(tr)) = &self.kind { Some(tr.clone()) } else { @@ -1186,7 +1214,7 @@ impl Context { let mut array_eq = Self::builtin_methods(Some(mono("Eq")), 2); array_eq.register_builtin_impl( "__eq__", - fn1_met(arr_t.clone(), arr_t.clone(), Bool), + fn1_met(arr_t.clone(), arr_t.clone(), Bool).quantify(), Const, Public, ); @@ -1196,7 +1224,7 @@ impl Context { let mut array_show = Self::builtin_methods(Some(mono("Show")), 1); array_show.register_builtin_py_impl( "to_str", - fn0_met(arr_t.clone(), Str), + fn0_met(arr_t.clone(), Str).quantify(), Immutable, Public, Some("__str__"), @@ -1234,7 +1262,7 @@ impl Context { let mut set_eq = Self::builtin_methods(Some(mono("Eq")), 2); set_eq.register_builtin_impl( "__eq__", - fn1_met(set_t.clone(), set_t.clone(), Bool), + fn1_met(set_t.clone(), set_t.clone(), Bool).quantify(), Const, Public, ); @@ -1242,7 +1270,12 @@ impl Context { set_.register_marker_trait(mono("Mutizable")); set_.register_marker_trait(poly("Seq", vec![ty_tp(T.clone())])); let mut set_show = Self::builtin_methods(Some(mono("Show")), 1); - set_show.register_builtin_impl("to_str", fn0_met(set_t.clone(), Str), Immutable, Public); + set_show.register_builtin_impl( + "to_str", + fn0_met(set_t.clone(), Str).quantify(), + Immutable, + Public, + ); set_.register_trait(set_t.clone(), set_show); let g_dict_t = mono("GenericDict"); let mut generic_dict = Self::builtin_mono_class("GenericDict", 2); @@ -1250,7 +1283,7 @@ impl Context { let mut generic_dict_eq = Self::builtin_methods(Some(mono("Eq")), 2); generic_dict_eq.register_builtin_impl( "__eq__", - fn1_met(g_dict_t.clone(), g_dict_t.clone(), Bool), + fn1_met(g_dict_t.clone(), g_dict_t.clone(), Bool).quantify(), Const, Public, ); @@ -1547,7 +1580,8 @@ impl Context { None, vec![], NoneType, - ); + ) + .quantify(); let mut array_mut_mutable = Self::builtin_methods(Some(mono("Mutable")), 2); array_mut_mutable.register_builtin_impl("update!", t, Immutable, Public); array_mut_.register_trait(array_mut_t.clone(), array_mut_mutable); @@ -1594,7 +1628,8 @@ impl Context { None, vec![], NoneType, - ); + ) + .quantify(); let mut set_mut_mutable = Self::builtin_methods(Some(mono("Mutable")), 2); set_mut_mutable.register_builtin_impl("update!", t, Immutable, Public); set_mut_.register_trait(set_mut_t.clone(), set_mut_mutable); @@ -1608,7 +1643,7 @@ impl Context { let mut range_eq = Self::builtin_methods(Some(mono("Eq")), 2); range_eq.register_builtin_impl( "__eq__", - fn1_met(range_t.clone(), range_t.clone(), Bool), + fn1_met(range_t.clone(), range_t.clone(), Bool).quantify(), Const, Public, ); @@ -1905,7 +1940,8 @@ impl Context { ], None, poly("Map", vec![ty_tp(T.clone())]), - ); + ) + .quantify(); let t_nat = nd_func(vec![kw("obj", Obj)], None, or(Nat, NoneType)); // e.g. not(b: Bool!): Bool! let B = mono_q("B", subtypeof(Bool)); @@ -1941,7 +1977,8 @@ impl Context { ], None, poly("Zip", vec![ty_tp(T), ty_tp(U)]), - ); + ) + .quantify(); self.register_builtin_py_impl("abs", t_abs, Immutable, vis, Some("abs")); self.register_builtin_py_impl("ascii", t_ascii, Immutable, vis, Some("ascii")); self.register_builtin_impl("assert", t_assert, Const, vis); // assert casting に悪影響が出る可能性があるため、Constとしておく @@ -2147,7 +2184,8 @@ impl Context { )], None, T.clone(), - ); + ) + .quantify(); let t_while = nd_proc( vec![ kw("cond!", nd_proc(vec![], None, Bool)), // not Bool! type because `cond` may be the result of evaluation of a mutable object's method returns Bool. @@ -2305,7 +2343,8 @@ impl Context { class.clone(), Type::from(&o..=&p), Type::from(m.clone() + o.clone()..=n.clone() + p.clone()), - ); + ) + .quantify(); let mut interval_add = Self::builtin_methods(Some(impls), 2); interval_add.register_builtin_impl("__add__", op_t, Const, Public); interval_add.register_builtin_const( @@ -2320,7 +2359,8 @@ impl Context { class.clone(), Type::from(&o..=&p), Type::from(m.clone() - p.clone()..=n.clone() - o.clone()), - ); + ) + .quantify(); interval_sub.register_builtin_impl("__sub__", op_t, Const, Public); interval_sub.register_builtin_const( "Output", diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs index 73279a66..4d0951d3 100644 --- a/compiler/erg_compiler/context/inquire.rs +++ b/compiler/erg_compiler/context/inquire.rs @@ -1153,6 +1153,9 @@ impl Context { } } if errs.is_empty() { + /*if subr.has_qvar() { + panic!("{subr} has qvar"); + }*/ Ok(None) } else { Err(errs) diff --git a/compiler/erg_compiler/context/instantiate.rs b/compiler/erg_compiler/context/instantiate.rs index 7c5eb52f..bcbe24ab 100644 --- a/compiler/erg_compiler/context/instantiate.rs +++ b/compiler/erg_compiler/context/instantiate.rs @@ -37,6 +37,8 @@ use crate::AccessKind; use RegistrationMode::*; /// Context for instantiating a quantified type +/// For example, cloning each type variable of quantified type `?T -> ?T` would result in `?1 -> ?2`. +/// To avoid this, an environment to store type variables is needed, which is `TyVarCache`. /// 量化型をインスタンス化するための文脈 /// e.g. Array -> [("T": ?T(: Type)), ("N": ?N(: Nat))] /// FIXME: current implementation is wrong diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs index b15da51e..73e3a4cd 100644 --- a/compiler/erg_compiler/context/tyvar.rs +++ b/compiler/erg_compiler/context/tyvar.rs @@ -9,6 +9,7 @@ use erg_common::{dict, set, Str}; #[allow(unused_imports)] use erg_common::{fmt_vec, log}; +use crate::context::instantiate::TyVarCache; use crate::ty::constructors::*; use crate::ty::free::{Constraint, FreeKind, HasLevel}; use crate::ty::typaram::TyParam; @@ -1374,10 +1375,6 @@ impl Context { ))); } match (maybe_sub, maybe_sup) { - /* - (Type::FreeVar(fv), _) if fv.is_generalized() => todo!("{maybe_sub}, {maybe_sup}"), - (_, Type::FreeVar(fv)) if fv.is_generalized() => todo!("{maybe_sub}, {maybe_sup}"), - */ // lfv's sup can be shrunk (take min), rfv's sub can be expanded (take union) // lfvのsupは縮小可能(minを取る)、rfvのsubは拡大可能(unionを取る) // sub_unify(?T[0](:> Never, <: Int), ?U[1](:> Never, <: Nat)): (/* ?U[1] --> ?T[0](:> Never, <: Nat)) @@ -1625,15 +1622,24 @@ impl Context { // Zip(T, U) <: Iterable(Tuple([T, U])) if ln != rn { if let Some((sub_def_t, sub_ctx)) = self.get_nominal_type_ctx(maybe_sub) { + let mut tv_cache = TyVarCache::new(self.level, self); + let _sub_def_instance = + self.instantiate_t_inner(sub_def_t.clone(), &mut tv_cache, loc)?; + // e.g. + // maybe_sub: Zip(Int, Str) + // sub_def_t: Zip(T, U) ==> Zip(Int, Str) + // super_traits: [Iterable((T, U)), ...] ==> [Iterable((Int, Str)), ...] self.substitute_typarams(sub_def_t, maybe_sub) .map_err(|errs| { Self::undo_substitute_typarams(sub_def_t); errs })?; for sup_trait in sub_ctx.super_traits.iter() { + let sub_trait_instance = + self.instantiate_t_inner(sup_trait.clone(), &mut tv_cache, loc)?; if self.supertype_of(maybe_sup, sup_trait) { for (l_maybe_sub, r_maybe_sup) in - sup_trait.typarams().iter().zip(rps.iter()) + sub_trait_instance.typarams().iter().zip(rps.iter()) { self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false) .map_err(|errs| { diff --git a/tests/should_err/subtyping.er b/tests/should_err/subtyping.er index 3b902cc3..05c0b844 100644 --- a/tests/should_err/subtyping.er +++ b/tests/should_err/subtyping.er @@ -15,7 +15,10 @@ for! zip([1], ["a"]), ((i: Int, s: Str),) => k = i + 1 l = s + "b" print! k, l -# ERR +# ERR: i should be Int for! zip([1], ["a"]), ((i: Str, s: Str),) => k = i + "a" print! k +for! zip([1], ["a"]), ((i, s),) => + k = i + "a" # ERR + print! k diff --git a/tests/test.rs b/tests/test.rs index d6555a55..5026f1cb 100644 --- a/tests/test.rs +++ b/tests/test.rs @@ -202,7 +202,7 @@ fn exec_side_effect() -> Result<(), ()> { #[test] fn exec_subtyping() -> Result<(), ()> { - expect_failure("tests/should_err/subtyping.er", 3) + expect_failure("tests/should_err/subtyping.er", 4) } #[test]