diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index fbec8cdf..b2743416 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -262,7 +262,7 @@ impl Context {
         if !self.is_class(lhs) || !self.is_class(rhs) {
             return (Maybe, false);
         }
-        if let Some(ty_ctx) = self.get_nominal_type_ctx(rhs) {
+        if let Some((_, ty_ctx)) = self.get_nominal_type_ctx(rhs) {
             for rhs_sup in ty_ctx.super_classes.iter() {
                 let rhs_sup = if rhs_sup.has_qvar() {
                     let rhs = match rhs {
@@ -300,7 +300,7 @@ impl Context {
         if !self.is_trait(lhs) {
             return (Maybe, false);
         }
-        if let Some(rhs_ctx) = self.get_nominal_type_ctx(rhs) {
+        if let Some((_, rhs_ctx)) = self.get_nominal_type_ctx(rhs) {
             for rhs_sup in rhs_ctx.super_traits.iter() {
                 // Not `supertype_of` (only structures are compared)
                 match self.cheap_supertype_of(lhs, rhs_sup) {
@@ -644,7 +644,7 @@ impl Context {
             erg_common::fmt_vec(lparams),
             erg_common::fmt_vec(rparams)
         );
-        let ctx = self
+        let (_, ctx) = self
             .get_nominal_type_ctx(typ)
             .unwrap_or_else(|| panic!("{typ} is not found"));
         let variances = ctx.type_params_variance();
@@ -846,9 +846,13 @@ impl Context {
             }
             (Refinement(l), Refinement(r)) => Type::Refinement(self.union_refinement(l, r)),
             (t, Type::Never) | (Type::Never, t) => t.clone(),
-            (t, Refinement(r)) | (Refinement(r), t) => {
-                let t = self.into_refinement(t.clone());
-                Type::Refinement(self.union_refinement(&t, r))
+            // ?T or {"b"} cannot be {I: (?T or Str) | I == "b"} because ?T may be {"a"} etc.
+            // (if so, {I: ?T or Str | I == "b"} == {I: {"a"} or Str | I == "b"} == {I: Str | I == "b"})
+            (other, Refinement(refine)) | (Refinement(refine), other)
+                if !other.is_unbound_var() =>
+            {
+                let other = self.into_refinement(other.clone());
+                Type::Refinement(self.union_refinement(&other, refine))
             }
             // Array({1, 2}, 2), Array({3, 4}, 2) ==> Array({1, 2, 3, 4}, 2)
             (
diff --git a/compiler/erg_compiler/context/hint.rs b/compiler/erg_compiler/context/hint.rs
index 5f1aef6e..a3d5db94 100644
--- a/compiler/erg_compiler/context/hint.rs
+++ b/compiler/erg_compiler/context/hint.rs
@@ -21,7 +21,7 @@ enum Sequence {
 
 // TODO: these should not be in Context
 impl Context {
-    fn readable_type(typ: &Type) -> Type {
+    pub(crate) fn readable_type(typ: &Type) -> Type {
         match typ {
             Type::FreeVar(fv) if fv.constraint_is_sandwiched() => {
                 let (sub, sup) = fv.get_subsup().unwrap();
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index b8b09ce6..47370acd 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -551,7 +551,7 @@ impl Context {
                 self.get_attr_info_from_attributive(&fv.crack(), ident, namespace)
             }
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
+                let sup = fv.get_super().unwrap();
                 self.get_attr_info_from_attributive(&sup, ident, namespace)
             }
             Type::Ref(t) => self.get_attr_info_from_attributive(t, ident, namespace),
@@ -1573,7 +1573,7 @@ impl Context {
         match t {
             Type::FreeVar(fv) if fv.is_linked() => self.get_nominal_super_type_ctxs(&fv.crack()),
             Type::FreeVar(fv) => {
-                if let Some(sup) = fv.get_sup() {
+                if let Some(sup) = fv.get_super() {
                     self.get_nominal_super_type_ctxs(&sup)
                 } else {
                     self.get_nominal_super_type_ctxs(&Type)
@@ -1614,7 +1614,7 @@ impl Context {
         &'a self,
         t: &Type,
     ) -> Option<impl Iterator<Item = &'a Context>> {
-        let ctx = self.get_nominal_type_ctx(t)?;
+        let (_, ctx) = self.get_nominal_type_ctx(t)?;
         let sups = ctx
             .super_classes
             .iter()
@@ -1622,18 +1622,19 @@ impl Context {
             .map(|sup| {
                 self.get_nominal_type_ctx(sup)
                     .unwrap_or_else(|| todo!("compiler bug: {sup} not found"))
+                    .1
             });
         Some(vec![ctx].into_iter().chain(sups))
     }
 
     pub(crate) fn _get_super_traits(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
         self.get_nominal_type_ctx(typ)
-            .map(|ctx| ctx.super_traits.clone().into_iter())
+            .map(|(_, ctx)| ctx.super_traits.clone().into_iter())
     }
 
     /// if `typ` is a refinement type, include the base type (refine.t)
     pub(crate) fn _get_super_classes(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
-        self.get_nominal_type_ctx(typ).map(|ctx| {
+        self.get_nominal_type_ctx(typ).map(|(_, ctx)| {
             let super_classes = ctx.super_classes.clone();
             let derefined = typ.derefine();
             if typ != &derefined {
@@ -1645,7 +1646,10 @@ impl Context {
     }
 
     // TODO: Never
-    pub(crate) fn get_nominal_type_ctx<'a>(&'a self, typ: &Type) -> Option<&'a Context> {
+    pub(crate) fn get_nominal_type_ctx<'a>(
+        &'a self,
+        typ: &Type,
+    ) -> Option<(&'a Type, &'a Context)> {
         match typ {
             Type::FreeVar(fv) if fv.is_linked() => {
                 if let Some(res) = self.get_nominal_type_ctx(&fv.crack()) {
@@ -1653,7 +1657,7 @@ impl Context {
                 }
             }
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
+                let sup = fv.get_super().unwrap();
                 if let Some(res) = self.get_nominal_type_ctx(&sup) {
                     return Some(res);
                 }
@@ -1664,37 +1668,37 @@ impl Context {
                 }
             }
             Type::Quantified(_) => {
-                if let Some((_t, ctx)) = self
+                if let Some((t, ctx)) = self
                     .get_builtins()
                     .unwrap_or(self)
                     .rec_get_mono_type("QuantifiedFunc")
                 {
-                    return Some(ctx);
+                    return Some((t, ctx));
                 }
             }
             Type::Subr(subr) => match subr.kind {
                 SubrKind::Func => {
-                    if let Some((_, ctx)) = self
+                    if let Some((t, ctx)) = self
                         .get_builtins()
                         .unwrap_or(self)
                         .rec_get_mono_type("Func")
                     {
-                        return Some(ctx);
+                        return Some((t, ctx));
                     }
                 }
                 SubrKind::Proc => {
-                    if let Some((_, ctx)) = self
+                    if let Some((t, ctx)) = self
                         .get_builtins()
                         .unwrap_or(self)
                         .rec_get_mono_type("Proc")
                     {
-                        return Some(ctx);
+                        return Some((t, ctx));
                     }
                 }
             },
             Type::Mono(name) => {
-                if let Some((_, ctx)) = self.rec_get_mono_type(&typ.local_name()) {
-                    return Some(ctx);
+                if let Some((t, ctx)) = self.rec_get_mono_type(&typ.local_name()) {
+                    return Some((t, ctx));
                 }
                 // e.g. http.client.Response -> http.client
                 let mut namespaces = name.split_with(&[".", "::"]);
@@ -1717,14 +1721,14 @@ impl Context {
                             .and_then(|cache| cache.ref_ctx(path.as_path()))
                     })
                 {
-                    if let Some((_, ctx)) = ctx.rec_get_mono_type(type_name) {
-                        return Some(ctx);
+                    if let Some((t, ctx)) = ctx.rec_get_mono_type(type_name) {
+                        return Some((t, ctx));
                     }
                 }
             }
             Type::Poly { name, .. } => {
-                if let Some((_, ctx)) = self.rec_get_poly_type(&typ.local_name()) {
-                    return Some(ctx);
+                if let Some((t, ctx)) = self.rec_get_poly_type(&typ.local_name()) {
+                    return Some((t, ctx));
                 }
                 // NOTE: This needs to be changed if we want to be able to define classes/traits outside of the top level
                 let mut namespaces = name.split_with(&[".", "::"]);
@@ -1747,8 +1751,8 @@ impl Context {
                             .and_then(|cache| cache.ref_ctx(path.as_path()))
                     })
                 {
-                    if let Some((_, ctx)) = ctx.rec_get_poly_type(type_name) {
-                        return Some(ctx);
+                    if let Some((t, ctx)) = ctx.rec_get_poly_type(type_name) {
+                        return Some((t, ctx));
                     }
                 }
             }
@@ -1756,15 +1760,13 @@ impl Context {
                 return self
                     .get_builtins()
                     .unwrap_or(self)
-                    .rec_get_mono_type("RecordType")
-                    .map(|(_, ctx)| ctx);
+                    .rec_get_mono_type("RecordType");
             }
             Type::Record(_) => {
                 return self
                     .get_builtins()
                     .unwrap_or(self)
-                    .rec_get_mono_type("Record")
-                    .map(|(_, ctx)| ctx);
+                    .rec_get_mono_type("Record");
             }
             Type::Or(_l, _r) => {
                 if let Some(ctx) = self.get_nominal_type_ctx(&poly("Or", vec![])) {
@@ -1773,8 +1775,8 @@ impl Context {
             }
             // FIXME: `F()`などの場合、実際は引数が省略されていてもmonomorphicになる
             other if other.is_monomorphic() => {
-                if let Some((_t, ctx)) = self.rec_get_mono_type(&other.local_name()) {
-                    return Some(ctx);
+                if let Some((t, ctx)) = self.rec_get_mono_type(&other.local_name()) {
+                    return Some((t, ctx));
                 }
             }
             Type::Ref(t) | Type::RefMut { before: t, .. } => {
@@ -1801,7 +1803,7 @@ impl Context {
                 }
             }
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
+                let sup = fv.get_super().unwrap();
                 if let Some(res) = self.get_mut_nominal_type_ctx(&sup) {
                     return Some(res);
                 }
@@ -2184,7 +2186,7 @@ impl Context {
         #[allow(clippy::single_match)]
         match lhs {
             Type::FreeVar(fv) => {
-                if let Some(sup) = fv.get_sup() {
+                if let Some(sup) = fv.get_super() {
                     let insts = self.get_trait_impls(&sup);
                     let candidates = insts.into_iter().filter_map(move |inst| {
                         if self.supertype_of(&inst.sup_trait, &sup) {
@@ -2220,7 +2222,7 @@ impl Context {
             Type::Refinement(refine) => self.is_class(&refine.t),
             Type::Ref(t) | Type::RefMut { before: t, .. } => self.is_class(t),
             _ => {
-                if let Some(ctx) = self.get_nominal_type_ctx(typ) {
+                if let Some((_, ctx)) = self.get_nominal_type_ctx(typ) {
                     ctx.kind.is_class()
                 } else {
                     // TODO: unknown types
@@ -2243,7 +2245,7 @@ impl Context {
             Type::Refinement(refine) => self.is_trait(&refine.t),
             Type::Ref(t) | Type::RefMut { before: t, .. } => self.is_trait(t),
             _ => {
-                if let Some(ctx) = self.get_nominal_type_ctx(typ) {
+                if let Some((_, ctx)) = self.get_nominal_type_ctx(typ) {
                     ctx.kind.is_trait()
                 } else {
                     false
diff --git a/compiler/erg_compiler/context/mod.rs b/compiler/erg_compiler/context/mod.rs
index 23a1f1bd..a4e40f67 100644
--- a/compiler/erg_compiler/context/mod.rs
+++ b/compiler/erg_compiler/context/mod.rs
@@ -416,7 +416,7 @@ impl ContextProvider for Context {
             .chain(self.methods_list.iter().flat_map(|(_, ctx)| ctx.dir()))
             .collect();
         for sup in self.super_classes.iter() {
-            if let Some(sup_ctx) = self.get_nominal_type_ctx(sup) {
+            if let Some((_, sup_ctx)) = self.get_nominal_type_ctx(sup) {
                 vars.extend(sup_ctx.type_dir());
             }
         }
@@ -432,7 +432,7 @@ impl ContextProvider for Context {
         self.get_mod(receiver_name)
             .or_else(|| {
                 let (_, vi) = self.get_var_info(receiver_name)?;
-                self.get_nominal_type_ctx(&vi.t)
+                self.get_nominal_type_ctx(&vi.t).map(|(_, ctx)| ctx)
             })
             .or_else(|| self.rec_get_type(receiver_name).map(|(_, ctx)| ctx))
     }
diff --git a/compiler/erg_compiler/context/register.rs b/compiler/erg_compiler/context/register.rs
index 23874fa8..0b7eaf5a 100644
--- a/compiler/erg_compiler/context/register.rs
+++ b/compiler/erg_compiler/context/register.rs
@@ -824,7 +824,7 @@ impl Context {
                         self.level,
                     );
                     for sup in super_classes.into_iter() {
-                        let sup_ctx = self
+                        let (_, sup_ctx) = self
                             .get_nominal_type_ctx(&sup)
                             .unwrap_or_else(|| todo!("{sup} not found"));
                         ctx.register_superclass(sup, sup_ctx);
@@ -942,7 +942,7 @@ impl Context {
                         }
                     }
                     for sup in super_classes.into_iter() {
-                        let sup_ctx = self.get_nominal_type_ctx(&sup).unwrap();
+                        let (_, sup_ctx) = self.get_nominal_type_ctx(&sup).unwrap();
                         ctx.register_supertrait(sup, sup_ctx);
                     }
                     self.register_gen_mono_type(ident, gen, ctx, Const);
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index 86757a8a..9ae8c4df 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -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) {
diff --git a/compiler/erg_compiler/hir.rs b/compiler/erg_compiler/hir.rs
index 1f5a37ef..a3c3129d 100644
--- a/compiler/erg_compiler/hir.rs
+++ b/compiler/erg_compiler/hir.rs
@@ -1914,6 +1914,11 @@ impl Expr {
         }
     }
 
+    pub fn to_string_notype(&self) -> String {
+        let s = self.to_string();
+        s.split("(:").next().unwrap_or("?").trim_end().to_string()
+    }
+
     /// 参照するオブジェクト自体が持っている名前(e.g. Int.qual_name == Some("int"), Socket!.qual_name == Some("io.Socket!"))
     pub fn qual_name(&self) -> Option<&str> {
         match self {
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index 7a23b6a1..b01a884d 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -302,6 +302,31 @@ impl ASTLowerer {
         }
     }
 
+    fn elem_err(&self, l: &Type, r: &Type, elem: &hir::Expr) -> LowerErrors {
+        let elem_disp_notype = elem.to_string_notype();
+        let l = Context::readable_type(l);
+        let r = Context::readable_type(r);
+        LowerErrors::from(LowerError::syntax_error(
+            self.cfg.input.clone(),
+            line!() as usize,
+            elem.loc(),
+            String::from(&self.ctx.name[..]),
+            switch_lang!(
+                "japanese" => "配列の要素は全て同じ型である必要があります",
+                "simplified_chinese" => "数组元素必须全部是相同类型",
+                "traditional_chinese" => "數組元素必須全部是相同類型",
+                "english" => "all elements of an array must be of the same type",
+            )
+            .to_owned(),
+            Some(switch_lang!(
+                "japanese" => format!("[..., {elem_disp_notype}: {l} or {r}]など明示的に型を指定してください"),
+                "simplified_chinese" => format!("请明确指定类型，例如: [..., {elem_disp_notype}: {l} or {r}]"),
+                "traditional_chinese" => format!("請明確指定類型，例如: [..., {elem_disp_notype}: {l} or {r}]"),
+                "english" => format!("please specify the type explicitly, e.g. [..., {elem_disp_notype}: {l} or {r}]"),
+            )),
+        ))
+    }
+
     fn lower_normal_array(&mut self, array: ast::NormalArray) -> LowerResult<hir::NormalArray> {
         log!(info "entered {}({array})", fn_name!());
         let mut new_array = vec![];
@@ -310,29 +335,16 @@ impl ASTLowerer {
         for elem in elems {
             let elem = self.lower_expr(elem.expr)?;
             union = self.ctx.union(&union, elem.ref_t());
-            if matches!(union, Type::Or(_, _)) {
-                return Err(LowerErrors::from(LowerError::syntax_error(
-                    self.cfg.input.clone(),
-                    line!() as usize,
-                    elem.loc(),
-                    String::from(&self.ctx.name[..]),
-                    switch_lang!(
-                        "japanese" => "配列の要素は全て同じ型である必要があります",
-                        "simplified_chinese" => "数组元素必须全部是相同类型",
-                        "traditional_chinese" => "數組元素必須全部是相同類型",
-                        "english" => "all elements of an array must be of the same type",
-                    )
-                    .to_owned(),
-                    Some(
-                        switch_lang!(
-                            "japanese" => "Int or Strなど明示的に型を指定してください",
-                            "simplified_chinese" => "请明确指定类型，例如: Int or Str",
-                            "traditional_chinese" => "請明確指定類型，例如: Int or Str",
-                            "english" => "please specify the type explicitly, e.g. Int or Str",
-                        )
-                        .to_owned(),
-                    ),
-                )));
+            if let Some((l, r)) = union.union_types() {
+                match (l.is_unbound_var(), r.is_unbound_var()) {
+                    (false, false) => {
+                        return Err(self.elem_err(&l, &r, &elem));
+                    }
+                    // TODO: check if the type is compatible with the other type
+                    (true, false) => {}
+                    (false, true) => {}
+                    (true, true) => {}
+                }
             }
             new_array.push(elem);
         }
@@ -1202,7 +1214,7 @@ impl ASTLowerer {
             if let Some((trait_, trait_loc)) = &impl_trait {
                 self.register_trait_impl(&class, trait_, *trait_loc)?;
             }
-            if let Some(class_root) = self.ctx.get_nominal_type_ctx(&class) {
+            if let Some((_, class_root)) = self.ctx.get_nominal_type_ctx(&class) {
                 if !class_root.kind.is_class() {
                     return Err(LowerErrors::from(LowerError::method_definition_error(
                         self.cfg.input.clone(),
@@ -1271,7 +1283,7 @@ impl ASTLowerer {
             self.check_collision_and_push(class);
         }
         let class = mono(hir_def.sig.ident().inspect());
-        let class_ctx = self.ctx.get_nominal_type_ctx(&class).unwrap();
+        let (_, class_ctx) = self.ctx.get_nominal_type_ctx(&class).unwrap();
         let type_obj = enum_unwrap!(self.ctx.rec_get_const_obj(hir_def.sig.ident().inspect()).unwrap(), ValueObj::Type:(TypeObj::Generated:(_)));
         let sup_type = enum_unwrap!(&hir_def.body.block.first().unwrap(), hir::Expr::Call)
             .args
@@ -1313,7 +1325,7 @@ impl ASTLowerer {
                 set! {TypeRelationInstance::new(class.clone(), trait_.clone())},
             );
         }
-        let trait_ctx = if let Some(trait_ctx) = self.ctx.get_nominal_type_ctx(trait_) {
+        let trait_ctx = if let Some((_, trait_ctx)) = self.ctx.get_nominal_type_ctx(trait_) {
             trait_ctx.clone()
         } else {
             // TODO: maybe parameters are wrong
@@ -1451,7 +1463,7 @@ impl ASTLowerer {
                             other => todo!("{other}"),
                         },
                         TypeObj::Builtin(_typ) => {
-                            let ctx = self.ctx.get_nominal_type_ctx(_typ).unwrap();
+                            let (_, ctx) = self.ctx.get_nominal_type_ctx(_typ).unwrap();
                             for (decl_name, decl_vi) in ctx.decls.iter() {
                                 if let Some((name, vi)) = self.ctx.get_local_kv(decl_name.inspect())
                                 {
diff --git a/compiler/erg_compiler/ty/free.rs b/compiler/erg_compiler/ty/free.rs
index c1aaf2ac..cc7da214 100644
--- a/compiler/erg_compiler/ty/free.rs
+++ b/compiler/erg_compiler/ty/free.rs
@@ -152,6 +152,7 @@ impl Constraint {
         }
     }
 
+    /// :> Sub
     pub fn get_sub(&self) -> Option<&Type> {
         match self {
             Self::Sandwiched { sub, .. } => Some(sub),
@@ -159,6 +160,7 @@ impl Constraint {
         }
     }
 
+    /// <: Sup
     pub fn get_super(&self) -> Option<&Type> {
         match self {
             Self::Sandwiched { sup, .. } => Some(sup),
@@ -567,10 +569,12 @@ impl<T: CanbeFree> Free<T> {
         self.constraint().and_then(|c| c.get_type().cloned())
     }
 
-    pub fn get_sup(&self) -> Option<Type> {
+    /// <: Super
+    pub fn get_super(&self) -> Option<Type> {
         self.constraint().and_then(|c| c.get_super().cloned())
     }
 
+    /// :> Sub
     pub fn get_sub(&self) -> Option<Type> {
         self.constraint().and_then(|c| c.get_sub().cloned())
     }
diff --git a/tests/bug/infer_union_array.er b/tests/bug/infer_union_array.er
deleted file mode 100644
index 7e01ecd3..00000000
--- a/tests/bug/infer_union_array.er
+++ /dev/null
@@ -1,7 +0,0 @@
-f x: [{""}; _] = None
-
-arr = ["aaa"]
-for! arr, elem =>
-    # elem: Never
-    a = ["", elem] # [{"", "aaa"}; 2]
-    f a
diff --git a/tests/should_err/infer_union_array.er b/tests/should_err/infer_union_array.er
new file mode 100644
index 00000000..0cae4c02
--- /dev/null
+++ b/tests/should_err/infer_union_array.er
@@ -0,0 +1,6 @@
+f x: [{""}; _] = None
+
+arr = ["aaa"]
+for! arr, elem =>
+    a = ["", "aaa"] # [{"", "aaa"}; 2]
+    f a # ERR: type mismatched
diff --git a/tests/test.rs b/tests/test.rs
index 270dd023..c441f8c4 100644
--- a/tests/test.rs
+++ b/tests/test.rs
@@ -144,6 +144,11 @@ fn exec_args() -> Result<(), ()> {
     expect_failure("tests/should_err/args.er", 16)
 }
 
+#[test]
+fn exec_infer_union_array() -> Result<(), ()> {
+    expect_failure("tests/should_err/infer_union_array.er", 1)
+}
+
 #[test]
 fn exec_invalid_param() -> Result<(), ()> {
     expect_failure("tests/should_err/invalid_param.er", 3)