Fix a subtype unification bug

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",

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)

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

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| {

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

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]