diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index f426ac81..6e4f86f2 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -391,6 +391,7 @@ impl Context {
                 // () -> Never <: () -> Int <: () -> Object
                 // (Object) -> Int <: (Int) -> Int <: (Never) -> Int
                 ls.non_default_params.len() == rs.non_default_params.len()
+                // REVIEW:
                 && ls.default_params.len() == rs.default_params.len()
                 && self.supertype_of(&ls.return_t, &rs.return_t) // covariant
                 && ls.non_default_params.iter()
@@ -579,6 +580,7 @@ impl Context {
                 self.structural_supertype_of(&q_callable, r)
             }
             // (Int or Str) :> Nat == Int :> Nat || Str :> Nat == true
+            // (Num or Show) :> Show == Num :> Show || Show :> Num == true
             (Or(l_or, r_or), rhs) => self.supertype_of(l_or, rhs) || self.supertype_of(r_or, rhs),
             // Int :> (Nat or Str) == Int :> Nat && Int :> Str == false
             (lhs, Or(l_or, r_or)) => self.supertype_of(lhs, l_or) && self.supertype_of(lhs, r_or),
diff --git a/compiler/erg_compiler/context/eval.rs b/compiler/erg_compiler/context/eval.rs
index 3fff4fc5..2d9539b9 100644
--- a/compiler/erg_compiler/context/eval.rs
+++ b/compiler/erg_compiler/context/eval.rs
@@ -1,3 +1,4 @@
+use std::fmt;
 use std::mem;
 
 use erg_common::dict::Dict;
@@ -77,14 +78,24 @@ pub(crate) fn eval_lit(lit: &Literal) -> ValueObj {
     ValueObj::from_str(t, lit.token.content.clone())
 }
 
-/// SubstContext::new([?T; 0], Context(Array('T, 'N))) => SubstContext{ params: { 'T: ?T; 'N: 0 } } => ctx
-/// ctx.substitute(['T; !'N]): [?T; !0]
+/// SubstContext::new(Array(?T, 0), Context(Array('T, 'N))) => SubstContext{ params: { 'T: ?T; 'N: 0 } } => ctx
+/// ctx.substitute(Array!('T; !'N)): Array(?T, !0)
 #[derive(Debug)]
 pub struct SubstContext {
     bounds: Set<TyBound>,
     params: Dict<Str, TyParam>,
 }
 
+impl fmt::Display for SubstContext {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            f,
+            "SubstContext{{ bounds: {}, params: {} }}",
+            self.bounds, self.params
+        )
+    }
+}
+
 impl SubstContext {
     pub fn new(substituted: &Type, ty_ctx: &Context) -> Self {
         let bounds = ty_ctx.type_params_bounds();
@@ -116,8 +127,8 @@ impl SubstContext {
         match param {
             TyParam::FreeVar(fv) => {
                 if let Some(name) = fv.unbound_name() {
-                    if let Some(v) = self.params.get(&name) {
-                        ctx.sub_unify_tp(param, v, None, false)?;
+                    if let Some(tp) = self.params.get(&name) {
+                        ctx.sub_unify_tp(param, tp, None, Location::Unknown, false)?;
                     }
                 } else if fv.is_unbound() {
                     panic!()
@@ -151,9 +162,9 @@ impl SubstContext {
         match param_t {
             Type::FreeVar(fv) => {
                 if let Some(name) = fv.unbound_name() {
-                    if let Some(v) = self.params.get(&name) {
-                        if let TyParam::Type(v) = v {
-                            ctx.sub_unify(param_t, v, None, None, None)?;
+                    if let Some(tp) = self.params.get(&name) {
+                        if let TyParam::Type(t) = tp {
+                            ctx.sub_unify(param_t, t, Location::Unknown, None)?;
                         } else {
                             panic!()
                         }
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index 8aeea04f..8abde6c5 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -41,10 +41,7 @@ impl Context {
         mode: RegistrationMode,
     ) -> TyCheckResult<()> {
         let spec_t = self.instantiate_var_sig_t(t_spec, None, mode)?;
-        if self
-            .sub_unify(body_t, &spec_t, None, Some(ident.loc()), None)
-            .is_err()
-        {
+        if self.sub_unify(body_t, &spec_t, ident.loc(), None).is_err() {
             return Err(TyCheckErrors::from(TyCheckError::type_mismatch_error(
                 self.cfg.input.clone(),
                 line!() as usize,
@@ -220,7 +217,7 @@ impl Context {
         // NG: expr_t: Nat, union_pat_t: {1, 2}
         // OK: expr_t: Int, union_pat_t: {1} or 'T
         if self
-            .sub_unify(match_target_expr_t, &union_pat_t, None, None, None)
+            .sub_unify(match_target_expr_t, &union_pat_t, pos_args[0].loc(), None)
             .is_err()
         {
             return Err(TyCheckErrors::from(TyCheckError::match_error(
@@ -457,7 +454,7 @@ impl Context {
         }
     }
 
-    /// 戻り値ではなく、call全体の型を返す
+    // returns callee's type, not the return type
     fn search_callee_t(
         &self,
         obj: &hir::Expr,
@@ -676,7 +673,7 @@ impl Context {
                     None
                 }
             }) {
-                self.reunify(callee.ref_t(), after, Some(callee.loc()), None)?;
+                self.reunify(callee.ref_t(), after, callee.loc())?;
             }
         }
         Ok(())
@@ -746,13 +743,7 @@ impl Context {
                     {
                         let mut non_default_params = subr.non_default_params.iter();
                         let self_pt = non_default_params.next().unwrap();
-                        self.sub_unify(
-                            obj.ref_t(),
-                            self_pt.typ(),
-                            Some(obj.loc()),
-                            None,
-                            self_pt.name(),
-                        )?;
+                        self.sub_unify(obj.ref_t(), self_pt.typ(), obj.loc(), self_pt.name())?;
                         non_default_params
                     } else {
                         subr.non_default_params.iter()
@@ -843,7 +834,7 @@ impl Context {
     ) -> TyCheckResult<()> {
         let arg_t = arg.ref_t();
         let param_t = &param.typ();
-        self.sub_unify(arg_t, param_t, Some(arg.loc()), None, param.name())
+        self.sub_unify(arg_t, param_t, arg.loc(), param.name())
             .map_err(|errs| {
                 log!(err "semi-unification failed with {callee}\n{arg_t} !<: {param_t}");
                 // REVIEW:
@@ -892,7 +883,7 @@ impl Context {
     ) -> TyCheckResult<()> {
         let arg_t = arg.ref_t();
         let param_t = &param.typ();
-        self.sub_unify(arg_t, param_t, Some(arg.loc()), None, param.name())
+        self.sub_unify(arg_t, param_t, arg.loc(), param.name())
             .map_err(|errs| {
                 log!(err "semi-unification failed with {callee}\n{arg_t} !<: {param_t}");
                 // REVIEW:
@@ -943,7 +934,7 @@ impl Context {
             .iter()
             .find(|pt| pt.name().unwrap() == kw_name)
         {
-            self.sub_unify(arg_t, pt.typ(), Some(arg.loc()), None, Some(kw_name))
+            self.sub_unify(arg_t, pt.typ(), arg.loc(), Some(kw_name))
                 .map_err(|errs| {
                     log!(err "semi-unification failed with {callee}\n{arg_t} !<: {}", pt.typ());
                     // REVIEW:
@@ -1251,6 +1242,39 @@ impl Context {
         }))
     }
 
+    /*pub(crate) fn get_nominal_super_type_ctxs<'a>(
+        &'a self,
+        t: &Type,
+    ) -> Option<Vec<(&'a Type, &'a Context)>> {
+        match t {
+            Type::And(l, r) => {
+                match (self.get_nominal_super_type_ctxs(l), self.get_nominal_super_type_ctxs(r)) {
+                    // TODO: sort
+                    (Some(l), Some(r)) => Some([l, r].concat()),
+                    (Some(l), None) => Some(l),
+                    (None, Some(r)) => Some(r),
+                    (None, None) => None,
+                }
+            }
+            // TODO
+            Type::Or(_l, _r) => None,
+            _ => self.get_simple_nominal_super_type_ctxs(t).map(|ctxs| ctxs.collect()),
+        }
+    }
+
+    fn get_simple_nominal_super_type_ctxs<'a>(
+        &'a self,
+        t: &Type,
+    ) -> Option<impl Iterator<Item = (&'a Type, &'a Context)>> {
+        let (t, ctx) = self.get_nominal_type_ctx(t)?;
+        let sups = ctx
+            .super_classes
+            .iter()
+            .chain(ctx.super_traits.iter())
+            .map(|sup| self.get_nominal_type_ctx(sup).unwrap());
+        Some(vec![(t, ctx)].into_iter().chain(sups))
+    }*/
+
     pub(crate) fn get_nominal_super_type_ctxs<'a>(
         &'a self,
         t: &Type,
diff --git a/compiler/erg_compiler/context/instantiate.rs b/compiler/erg_compiler/context/instantiate.rs
index 7ff103c4..1085c467 100644
--- a/compiler/erg_compiler/context/instantiate.rs
+++ b/compiler/erg_compiler/context/instantiate.rs
@@ -432,7 +432,12 @@ impl Context {
             free_var(self.level, Constraint::new_type_of(Type))
         };
         if let Some(eval_t) = opt_eval_t {
-            self.sub_unify(&eval_t, &spec_t, None, t_spec.map(|s| s.loc()), None)?;
+            self.sub_unify(
+                &eval_t,
+                &spec_t,
+                t_spec.map(|s| s.loc()).unwrap_or(Location::Unknown),
+                None,
+            )?;
         }
         Ok(spec_t)
     }
@@ -527,8 +532,10 @@ impl Context {
             self.sub_unify(
                 decl_pt.typ(),
                 &spec_t,
-                None,
-                sig.t_spec.as_ref().map(|s| s.loc()),
+                sig.t_spec
+                    .as_ref()
+                    .map(|s| s.loc())
+                    .unwrap_or_else(|| sig.loc()),
                 None,
             )?;
         }
@@ -1016,8 +1023,7 @@ impl Context {
                             self.sub_unify(
                                 callee.ref_t(),
                                 self_t,
-                                None,
-                                Some(callee.loc()),
+                                callee.loc(),
                                 Some(&Str::ever("self")),
                             )?;
                         }
diff --git a/compiler/erg_compiler/context/register.rs b/compiler/erg_compiler/context/register.rs
index a59a95bf..781931ba 100644
--- a/compiler/erg_compiler/context/register.rs
+++ b/compiler/erg_compiler/context/register.rs
@@ -191,13 +191,7 @@ impl Context {
                     let spec_t = self.instantiate_param_sig_t(sig, opt_decl_t, None, Normal)?;
                     if &name.inspect()[..] == "self" {
                         let self_t = self.rec_get_self_t().unwrap();
-                        self.sub_unify(
-                            &spec_t,
-                            &self_t,
-                            Some(name.loc()),
-                            None,
-                            Some(name.inspect()),
-                        )?;
+                        self.sub_unify(&spec_t, &self_t, name.loc(), Some(name.inspect()))?;
                     }
                     let idx = if let Some(outer) = outer {
                         ParamIdx::nested(outer, nth)
@@ -236,13 +230,7 @@ impl Context {
                     let spec_t = self.instantiate_param_sig_t(sig, opt_decl_t, None, Normal)?;
                     if &name.inspect()[..] == "self" {
                         let self_t = self.rec_get_self_t().unwrap();
-                        self.sub_unify(
-                            &spec_t,
-                            &self_t,
-                            Some(name.loc()),
-                            None,
-                            Some(name.inspect()),
-                        )?;
+                        self.sub_unify(&spec_t, &self_t, name.loc(), Some(name.inspect()))?;
                     }
                     let spec_t = ref_(spec_t);
                     let idx = if let Some(outer) = outer {
@@ -281,13 +269,7 @@ impl Context {
                     let spec_t = self.instantiate_param_sig_t(sig, opt_decl_t, None, Normal)?;
                     if &name.inspect()[..] == "self" {
                         let self_t = self.rec_get_self_t().unwrap();
-                        self.sub_unify(
-                            &spec_t,
-                            &self_t,
-                            Some(name.loc()),
-                            None,
-                            Some(name.inspect()),
-                        )?;
+                        self.sub_unify(&spec_t, &self_t, name.loc(), Some(name.inspect()))?;
                     }
                     let spec_t = ref_mut(spec_t.clone(), Some(spec_t));
                     let idx = if let Some(outer) = outer {
@@ -387,7 +369,7 @@ impl Context {
         let var_args = t.var_args();
         let default_params = t.default_params().unwrap();
         if let Some(spec_ret_t) = t.return_t() {
-            self.sub_unify(body_t, spec_ret_t, None, Some(sig.loc()), None)
+            self.sub_unify(body_t, spec_ret_t, sig.loc(), None)
                 .map_err(|errs| {
                     TyCheckErrors::new(
                         errs.into_iter()
@@ -544,7 +526,7 @@ impl Context {
                         };
                     if let Some(spec) = sig.return_t_spec.as_ref() {
                         let spec_t = self.instantiate_typespec(spec, None, None, PreRegister)?;
-                        self.sub_unify(&const_t, &spec_t, Some(def.body.loc()), None, None)?;
+                        self.sub_unify(&const_t, &spec_t, def.body.loc(), None)?;
                     }
                     self.pop();
                     self.register_gen_const(def.sig.ident().unwrap(), obj)?;
@@ -561,7 +543,7 @@ impl Context {
                 };
                 if let Some(spec) = sig.t_spec.as_ref() {
                     let spec_t = self.instantiate_typespec(spec, None, None, PreRegister)?;
-                    self.sub_unify(&const_t, &spec_t, Some(def.body.loc()), None, None)?;
+                    self.sub_unify(&const_t, &spec_t, def.body.loc(), None)?;
                 }
                 self.register_gen_const(sig.ident().unwrap(), obj)?;
             }
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index 7366f29e..c96e8b4a 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -326,8 +326,7 @@ impl Context {
                                         line!() as usize,
                                         &self.deref_tyvar(sub_t.clone(), variance, loc)?,
                                         &self.deref_tyvar(super_t.clone(), variance, loc)?,
-                                        None,
-                                        Some(loc),
+                                        loc,
                                         self.caused_by(),
                                     ))
                                 }
@@ -339,8 +338,7 @@ impl Context {
                             line!() as usize,
                             &self.deref_tyvar(sub_t.clone(), variance, loc)?,
                             &self.deref_tyvar(super_t.clone(), variance, loc)?,
-                            None,
-                            Some(loc),
+                            loc,
                             self.caused_by(),
                         ))
                     }
@@ -638,13 +636,7 @@ impl Context {
     // occur(X -> ?T, ?T) ==> Error
     // occur(?T, ?T -> X) ==> Error
     // occur(?T, Option(?T)) ==> Error
-    fn occur(
-        &self,
-        maybe_sub: &Type,
-        maybe_sup: &Type,
-        sub_loc: Option<Location>,
-        sup_loc: Option<Location>,
-    ) -> TyCheckResult<()> {
+    fn occur(&self, maybe_sub: &Type, maybe_sup: &Type, loc: Location) -> TyCheckResult<()> {
         match (maybe_sub, maybe_sup) {
             (Type::FreeVar(sub), Type::FreeVar(sup)) => {
                 if sub.is_unbound() && sup.is_unbound() && sub == sup {
@@ -653,8 +645,7 @@ impl Context {
                         line!() as usize,
                         maybe_sub,
                         maybe_sup,
-                        sub_loc,
-                        sup_loc,
+                        loc,
                         self.caused_by(),
                     )))
                 } else {
@@ -663,28 +654,28 @@ impl Context {
             }
             (Type::Subr(subr), Type::FreeVar(fv)) if fv.is_unbound() => {
                 for default_t in subr.default_params.iter().map(|pt| pt.typ()) {
-                    self.occur(default_t, maybe_sup, sub_loc, sup_loc)?;
+                    self.occur(default_t, maybe_sup, loc)?;
                 }
                 if let Some(var_params) = subr.var_params.as_ref() {
-                    self.occur(var_params.typ(), maybe_sup, sub_loc, sup_loc)?;
+                    self.occur(var_params.typ(), maybe_sup, loc)?;
                 }
                 for non_default_t in subr.non_default_params.iter().map(|pt| pt.typ()) {
-                    self.occur(non_default_t, maybe_sup, sub_loc, sup_loc)?;
+                    self.occur(non_default_t, maybe_sup, loc)?;
                 }
-                self.occur(&subr.return_t, maybe_sup, sub_loc, sup_loc)?;
+                self.occur(&subr.return_t, maybe_sup, loc)?;
                 Ok(())
             }
             (Type::FreeVar(fv), Type::Subr(subr)) if fv.is_unbound() => {
                 for default_t in subr.default_params.iter().map(|pt| pt.typ()) {
-                    self.occur(maybe_sub, default_t, sub_loc, sup_loc)?;
+                    self.occur(maybe_sub, default_t, loc)?;
                 }
                 if let Some(var_params) = subr.var_params.as_ref() {
-                    self.occur(maybe_sub, var_params.typ(), sub_loc, sup_loc)?;
+                    self.occur(maybe_sub, var_params.typ(), loc)?;
                 }
                 for non_default_t in subr.non_default_params.iter().map(|pt| pt.typ()) {
-                    self.occur(maybe_sub, non_default_t, sub_loc, sup_loc)?;
+                    self.occur(maybe_sub, non_default_t, loc)?;
                 }
-                self.occur(maybe_sub, &subr.return_t, sub_loc, sup_loc)?;
+                self.occur(maybe_sub, &subr.return_t, loc)?;
                 Ok(())
             }
             (
@@ -700,7 +691,7 @@ impl Context {
                         None
                     }
                 }) {
-                    self.occur(param, maybe_sup, sub_loc, sup_loc)?;
+                    self.occur(param, maybe_sup, loc)?;
                 }
                 Ok(())
             }
@@ -717,7 +708,7 @@ impl Context {
                         None
                     }
                 }) {
-                    self.occur(maybe_sub, param, sub_loc, sup_loc)?;
+                    self.occur(maybe_sub, param, loc)?;
                 }
                 Ok(())
             }
@@ -728,30 +719,37 @@ impl Context {
     /// allow_divergence = trueにすると、Num型変数と±Infの単一化を許す
     pub(crate) fn sub_unify_tp(
         &self,
-        lhs: &TyParam,
-        rhs: &TyParam,
-        lhs_variance: Option<&Vec<Variance>>,
+        maybe_sub: &TyParam,
+        maybe_sup: &TyParam,
+        variance: Option<Variance>,
+        loc: Location,
         allow_divergence: bool,
     ) -> TyCheckResult<()> {
-        if lhs.has_no_unbound_var() && rhs.has_no_unbound_var() && lhs == rhs {
+        if maybe_sub.has_no_unbound_var()
+            && maybe_sup.has_no_unbound_var()
+            && maybe_sub == maybe_sup
+        {
             return Ok(());
         }
-        match (lhs, rhs) {
-            (TyParam::Type(l), TyParam::Type(r)) => self.sub_unify(l, r, None, None, None),
-            (ltp @ TyParam::FreeVar(lfv), rtp @ TyParam::FreeVar(rfv))
+        match (maybe_sub, maybe_sup) {
+            (TyParam::Type(maybe_sub), TyParam::Type(maybe_sup)) => {
+                self.sub_unify(maybe_sub, maybe_sup, loc, None)
+            }
+            (TyParam::FreeVar(lfv), TyParam::FreeVar(rfv))
                 if lfv.is_unbound() && rfv.is_unbound() =>
             {
                 if lfv.level().unwrap() > rfv.level().unwrap() {
-                    lfv.link(rtp);
+                    lfv.link(maybe_sup);
                 } else {
-                    rfv.link(ltp);
+                    rfv.link(maybe_sub);
                 }
                 Ok(())
             }
+            // REVIEW: 反転しても同じ？
             (TyParam::FreeVar(fv), tp) | (tp, TyParam::FreeVar(fv)) => {
                 match &*fv.borrow() {
                     FreeKind::Linked(l) | FreeKind::UndoableLinked { t: l, .. } => {
-                        return self.sub_unify_tp(l, tp, lhs_variance, allow_divergence);
+                        return self.sub_unify_tp(l, tp, variance, loc, allow_divergence);
                     }
                     FreeKind::Unbound { .. } | FreeKind::NamedUnbound { .. } => {}
                 } // &fv is dropped
@@ -796,7 +794,7 @@ impl Context {
             (TyParam::UnaryOp { op: lop, val: lval }, TyParam::UnaryOp { op: rop, val: rval })
                 if lop == rop =>
             {
-                self.sub_unify_tp(lval, rval, lhs_variance, allow_divergence)
+                self.sub_unify_tp(lval, rval, variance, loc, allow_divergence)
             }
             (
                 TyParam::BinOp { op: lop, lhs, rhs },
@@ -806,14 +804,19 @@ impl Context {
                     rhs: rhs2,
                 },
             ) if lop == rop => {
-                self.sub_unify_tp(lhs, lhs2, lhs_variance, allow_divergence)?;
-                self.sub_unify_tp(rhs, rhs2, lhs_variance, allow_divergence)
+                self.sub_unify_tp(lhs, lhs2, variance, loc, allow_divergence)?;
+                self.sub_unify_tp(rhs, rhs2, variance, loc, allow_divergence)
             }
             (l, r) => panic!("type-parameter unification failed:\nl:{l}\nr: {r}"),
         }
     }
 
-    fn reunify_tp(&self, before: &TyParam, after: &TyParam) -> SingleTyCheckResult<()> {
+    fn reunify_tp(
+        &self,
+        before: &TyParam,
+        after: &TyParam,
+        loc: Location,
+    ) -> SingleTyCheckResult<()> {
         match (before, after) {
             (TyParam::Value(ValueObj::Mut(l)), TyParam::Value(ValueObj::Mut(r))) => {
                 *l.borrow_mut() = r.borrow().clone();
@@ -823,11 +826,11 @@ impl Context {
                 *l.borrow_mut() = r.clone();
                 Ok(())
             }
-            (TyParam::Type(l), TyParam::Type(r)) => self.reunify(l, r, None, None),
+            (TyParam::Type(l), TyParam::Type(r)) => self.reunify(l, r, loc),
             (TyParam::UnaryOp { op: lop, val: lval }, TyParam::UnaryOp { op: rop, val: rval })
                 if lop == rop =>
             {
-                self.reunify_tp(lval, rval)
+                self.reunify_tp(lval, rval, loc)
             }
             (
                 TyParam::BinOp { op: lop, lhs, rhs },
@@ -837,8 +840,8 @@ impl Context {
                     rhs: rhs2,
                 },
             ) if lop == rop => {
-                self.reunify_tp(lhs, lhs2)?;
-                self.reunify_tp(rhs, rhs2)
+                self.reunify_tp(lhs, lhs2, loc)?;
+                self.reunify_tp(rhs, rhs2, loc)
             }
             (l, r) if self.eq_tp(l, r) => Ok(()),
             (l, r) => panic!("type-parameter re-unification failed:\nl: {l}\nr: {r}"),
@@ -846,19 +849,27 @@ impl Context {
     }
 
     /// predは正規化されているとする
-    fn _sub_unify_pred(&self, l_pred: &Predicate, r_pred: &Predicate) -> TyCheckResult<()> {
+    fn _sub_unify_pred(
+        &self,
+        l_pred: &Predicate,
+        r_pred: &Predicate,
+        loc: Location,
+    ) -> TyCheckResult<()> {
         match (l_pred, r_pred) {
             (Pred::Value(_), Pred::Value(_)) | (Pred::Const(_), Pred::Const(_)) => Ok(()),
             (Pred::Equal { rhs, .. }, Pred::Equal { rhs: rhs2, .. })
             | (Pred::GreaterEqual { rhs, .. }, Pred::GreaterEqual { rhs: rhs2, .. })
             | (Pred::LessEqual { rhs, .. }, Pred::LessEqual { rhs: rhs2, .. })
             | (Pred::NotEqual { rhs, .. }, Pred::NotEqual { rhs: rhs2, .. }) => {
-                self.sub_unify_tp(rhs, rhs2, None, false)
+                self.sub_unify_tp(rhs, rhs2, None, loc, false)
             }
             (Pred::And(l1, r1), Pred::And(l2, r2))
             | (Pred::Or(l1, r1), Pred::Or(l2, r2))
             | (Pred::Not(l1, r1), Pred::Not(l2, r2)) => {
-                match (self._sub_unify_pred(l1, l2), self._sub_unify_pred(r1, r2)) {
+                match (
+                    self._sub_unify_pred(l1, l2, loc),
+                    self._sub_unify_pred(r1, r2, loc),
+                ) {
                     (Ok(()), Ok(())) => Ok(()),
                     (Ok(()), Err(e)) | (Err(e), Ok(())) | (Err(e), Err(_)) => Err(e),
                 }
@@ -875,8 +886,8 @@ impl Context {
                         Pred::LessEqual { rhs: le_rhs, .. },
                         Pred::GreaterEqual { rhs: ge_rhs, .. },
                     ) => {
-                        self.sub_unify_tp(rhs, ge_rhs, None, false)?;
-                        self.sub_unify_tp(le_rhs, &TyParam::value(Inf), None, true)
+                        self.sub_unify_tp(rhs, ge_rhs, None, loc, false)?;
+                        self.sub_unify_tp(le_rhs, &TyParam::value(Inf), None, loc, true)
                     }
                     _ => Err(TyCheckErrors::from(TyCheckError::pred_unification_error(
                         self.cfg.input.clone(),
@@ -891,8 +902,8 @@ impl Context {
             | (Pred::And(l, r), Pred::LessEqual { rhs, .. }) => match (l.as_ref(), r.as_ref()) {
                 (Pred::GreaterEqual { rhs: ge_rhs, .. }, Pred::LessEqual { rhs: le_rhs, .. })
                 | (Pred::LessEqual { rhs: le_rhs, .. }, Pred::GreaterEqual { rhs: ge_rhs, .. }) => {
-                    self.sub_unify_tp(rhs, le_rhs, None, false)?;
-                    self.sub_unify_tp(ge_rhs, &TyParam::value(NegInf), None, true)
+                    self.sub_unify_tp(rhs, le_rhs, None, loc, false)?;
+                    self.sub_unify_tp(ge_rhs, &TyParam::value(NegInf), None, loc, true)
                 }
                 _ => Err(TyCheckErrors::from(TyCheckError::pred_unification_error(
                     self.cfg.input.clone(),
@@ -906,8 +917,8 @@ impl Context {
             | (Pred::And(l, r), Pred::Equal { rhs, .. }) => match (l.as_ref(), r.as_ref()) {
                 (Pred::GreaterEqual { rhs: ge_rhs, .. }, Pred::LessEqual { rhs: le_rhs, .. })
                 | (Pred::LessEqual { rhs: le_rhs, .. }, Pred::GreaterEqual { rhs: ge_rhs, .. }) => {
-                    self.sub_unify_tp(rhs, le_rhs, None, false)?;
-                    self.sub_unify_tp(rhs, ge_rhs, None, false)
+                    self.sub_unify_tp(rhs, le_rhs, None, loc, false)?;
+                    self.sub_unify_tp(rhs, ge_rhs, None, loc, false)
                 }
                 _ => Err(TyCheckErrors::from(TyCheckError::pred_unification_error(
                     self.cfg.input.clone(),
@@ -934,17 +945,12 @@ impl Context {
         &self,
         before_t: &Type,
         after_t: &Type,
-        bef_loc: Option<Location>,
-        aft_loc: Option<Location>,
+        loc: Location,
     ) -> SingleTyCheckResult<()> {
         match (before_t, after_t) {
-            (Type::FreeVar(fv), r) if fv.is_linked() => {
-                self.reunify(&fv.crack(), r, bef_loc, aft_loc)
-            }
-            (l, Type::FreeVar(fv)) if fv.is_linked() => {
-                self.reunify(l, &fv.crack(), bef_loc, aft_loc)
-            }
-            (Type::Ref(l), Type::Ref(r)) => self.reunify(l, r, bef_loc, aft_loc),
+            (Type::FreeVar(fv), r) if fv.is_linked() => self.reunify(&fv.crack(), r, loc),
+            (l, Type::FreeVar(fv)) if fv.is_linked() => self.reunify(l, &fv.crack(), loc),
+            (Type::Ref(l), Type::Ref(r)) => self.reunify(l, r, loc),
             (
                 Type::RefMut {
                     before: lbefore,
@@ -955,21 +961,21 @@ impl Context {
                     after: rafter,
                 },
             ) => {
-                self.reunify(lbefore, rbefore, bef_loc, aft_loc)?;
+                self.reunify(lbefore, rbefore, loc)?;
                 match (lafter, rafter) {
                     (Some(lafter), Some(rafter)) => {
-                        self.reunify(lafter, rafter, bef_loc, aft_loc)?;
+                        self.reunify(lafter, rafter, loc)?;
                     }
                     (None, None) => {}
                     _ => todo!(),
                 }
                 Ok(())
             }
-            (Type::Ref(l), r) => self.reunify(l, r, bef_loc, aft_loc),
+            (Type::Ref(l), r) => self.reunify(l, r, loc),
             // REVIEW:
-            (Type::RefMut { before, .. }, r) => self.reunify(before, r, bef_loc, aft_loc),
-            (l, Type::Ref(r)) => self.reunify(l, r, bef_loc, aft_loc),
-            (l, Type::RefMut { before, .. }) => self.reunify(l, before, bef_loc, aft_loc),
+            (Type::RefMut { before, .. }, r) => self.reunify(before, r, loc),
+            (l, Type::Ref(r)) => self.reunify(l, r, loc),
+            (l, Type::RefMut { before, .. }) => self.reunify(l, before, loc),
             (
                 Type::BuiltinPoly {
                     name: ln,
@@ -987,13 +993,12 @@ impl Context {
                         line!() as usize,
                         &before_t,
                         after_t,
-                        bef_loc,
-                        aft_loc,
+                        loc,
                         self.caused_by(),
                     ));
                 }
                 for (l, r) in lps.iter().zip(rps.iter()) {
-                    self.reunify_tp(l, r)?;
+                    self.reunify_tp(l, r, loc)?;
                 }
                 Ok(())
             }
@@ -1016,13 +1021,12 @@ impl Context {
                         line!() as usize,
                         &before_t,
                         after_t,
-                        bef_loc,
-                        aft_loc,
+                        loc,
                         self.caused_by(),
                     ));
                 }
                 for (l, r) in lps.iter().zip(rps.iter()) {
-                    self.reunify_tp(l, r)?;
+                    self.reunify_tp(l, r, loc)?;
                 }
                 Ok(())
             }
@@ -1032,8 +1036,7 @@ impl Context {
                 line!() as usize,
                 l,
                 r,
-                bef_loc,
-                aft_loc,
+                loc,
                 self.caused_by(),
             )),
         }
@@ -1055,8 +1058,7 @@ impl Context {
         &self,
         maybe_sub: &Type,
         maybe_sup: &Type,
-        sub_loc: Option<Location>,
-        sup_loc: Option<Location>,
+        loc: Location,
         param_name: Option<&Str>,
     ) -> TyCheckResult<()> {
         log!(info "trying sub_unify:\nmaybe_sub: {maybe_sub}\nmaybe_sup: {maybe_sup}");
@@ -1065,13 +1067,12 @@ impl Context {
         if maybe_sub == &Type::Never || maybe_sup == &Type::Obj || maybe_sup == maybe_sub {
             return Ok(());
         }
-        self.occur(maybe_sub, maybe_sup, sub_loc, sup_loc)?;
+        self.occur(maybe_sub, maybe_sup, loc)?;
         let maybe_sub_is_sub = self.subtype_of(maybe_sub, maybe_sup);
         if maybe_sub.has_no_unbound_var() && maybe_sup.has_no_unbound_var() && maybe_sub_is_sub {
             return Ok(());
         }
         if !maybe_sub_is_sub {
-            let loc = sub_loc.or(sup_loc).unwrap_or(Location::Unknown);
             return Err(TyCheckErrors::from(TyCheckError::type_mismatch_error(
                 self.cfg.input.clone(),
                 line!() as usize,
@@ -1086,9 +1087,9 @@ impl Context {
         }
         match (maybe_sub, maybe_sup) {
             (Type::FreeVar(lfv), _) if lfv.is_linked() =>
-                self.sub_unify(&lfv.crack(), maybe_sup, sub_loc, sup_loc, param_name),
+                self.sub_unify(&lfv.crack(), maybe_sup, loc, param_name),
             (_, Type::FreeVar(rfv)) if rfv.is_linked() =>
-                self.sub_unify(maybe_sub, &rfv.crack(), sub_loc, sup_loc, param_name),
+                self.sub_unify(maybe_sub, &rfv.crack(), loc, param_name),
             // 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))
@@ -1113,8 +1114,7 @@ impl Context {
                         line!() as usize,
                         maybe_sub,
                         maybe_sup,
-                        sub_loc,
-                        sup_loc,
+                        loc,
                         self.caused_by(),
                     )));
                 };
@@ -1146,7 +1146,7 @@ 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 {
+                            /*let judge = match cyclicity {
                                 Cyclicity::Super => self.cyclic_supertype_of(rfv, maybe_sub),
                                 Cyclicity::Not => self.supertype_of(sup, maybe_sub),
                                 _ => todo!(),
@@ -1161,7 +1161,7 @@ impl Context {
                                     sup_loc,
                                     self.caused_by(),
                                 )));
-                            }
+                            }*/
                             if let Some(new_sub) = self.max(maybe_sub, sub) {
                                 *constraint =
                                     Constraint::new_sandwiched(new_sub.clone(), mem::take(sup), *cyclicity);
@@ -1200,7 +1200,8 @@ 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 } => {
-                            if !self.subtype_of(sub, maybe_sup) || !self.supertype_of(sup, maybe_sup) {
+                            // 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,
@@ -1210,7 +1211,7 @@ impl Context {
                                     sup_loc,
                                     self.caused_by(),
                                 )));
-                            }
+                            }*/
                             if let Some(new_sup) = self.min(sup, maybe_sup) {
                                 *constraint =
                                     Constraint::new_sandwiched(mem::take(sub), new_sup.clone(), *cyclicity);
@@ -1237,15 +1238,14 @@ impl Context {
             (Type::Record(lrec), Type::Record(rrec)) => {
                 for (k, l) in lrec.iter() {
                     if let Some(r) = rrec.get(k) {
-                        self.sub_unify(l, r, sub_loc, sup_loc, param_name)?;
+                        self.sub_unify(l, r, loc, param_name)?;
                     } else {
                         return Err(TyCheckErrors::from(TyCheckError::subtyping_error(
                             self.cfg.input.clone(),
                             line!() as usize,
                             maybe_sub,
                             maybe_sup,
-                            sub_loc,
-                            sup_loc,
+                            loc,
                             self.caused_by(),
                         )));
                     }
@@ -1256,15 +1256,15 @@ impl Context {
                 for lpt in lsub.default_params.iter() {
                     if let Some(rpt) = rsub.default_params.iter().find(|rpt| rpt.name() == lpt.name()) {
                         // contravariant
-                        self.sub_unify(rpt.typ(), lpt.typ(), sup_loc, sub_loc, param_name)?;
+                        self.sub_unify(rpt.typ(), lpt.typ(), loc, param_name)?;
                     } else { todo!() }
                 }
                 lsub.non_default_params.iter().zip(rsub.non_default_params.iter()).try_for_each(
                     // contravariant
-                    |(l, r)| self.sub_unify(r.typ(), l.typ(), sup_loc, sub_loc, param_name),
+                    |(l, r)| self.sub_unify(r.typ(), l.typ(), loc, param_name),
                 )?;
                 // covariant
-                self.sub_unify(&lsub.return_t, &rsub.return_t, sub_loc, sup_loc, param_name)?;
+                self.sub_unify(&lsub.return_t, &rsub.return_t, loc, param_name)?;
                 Ok(())
             }
             (
@@ -1283,13 +1283,12 @@ impl Context {
                         line!() as usize,
                         maybe_sub,
                         maybe_sup,
-                        sub_loc,
-                        sup_loc,
+                        loc,
                         self.caused_by(),
                     )));
                 }
                 for (l, r) in lps.iter().zip(rps.iter()) {
-                    self.sub_unify_tp(l, r, None, false)?;
+                    self.sub_unify_tp(l, r, None, loc, false)?;
                 }
                 Ok(())
             }
@@ -1311,22 +1310,21 @@ impl Context {
                         line!() as usize,
                         maybe_sub,
                         maybe_sup,
-                        sub_loc,
-                        sup_loc,
+                        loc,
                         self.caused_by(),
                     )));
                 }
-                for (l, r) in lps.iter().zip(rps.iter()) {
-                    self.sub_unify_tp(l, r, None, false)?;
+                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::Ref(t)) => {
-                self.sub_unify(maybe_sub, t, sub_loc, sup_loc, param_name)?;
+                self.sub_unify(maybe_sub, t, loc, param_name)?;
                 Ok(())
             }
             (_, Type::RefMut{ before, .. }) => {
-                self.sub_unify(maybe_sub, before, sub_loc, sup_loc, param_name)?;
+                self.sub_unify(maybe_sub, before, loc, param_name)?;
                 Ok(())
             }
             (Type::MonoProj { .. }, _) => todo!(),
diff --git a/compiler/erg_compiler/error.rs b/compiler/erg_compiler/error.rs
index 50adb5b8..28de3cab 100644
--- a/compiler/erg_compiler/error.rs
+++ b/compiler/erg_compiler/error.rs
@@ -631,16 +631,9 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         errno: usize,
         lhs_t: &Type,
         rhs_t: &Type,
-        lhs_loc: Option<Location>,
-        rhs_loc: Option<Location>,
+        loc: Location,
         caused_by: AtomicStr,
     ) -> Self {
-        let loc = match (lhs_loc, rhs_loc) {
-            (Some(l), Some(r)) => Location::pair(l, r),
-            (Some(l), None) => l,
-            (None, Some(r)) => r,
-            (None, None) => Location::Unknown,
-        };
         Self::new(
             ErrorCore::new(
                 errno,
@@ -664,16 +657,9 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         errno: usize,
         lhs_t: &Type,
         rhs_t: &Type,
-        lhs_loc: Option<Location>,
-        rhs_loc: Option<Location>,
+        loc: Location,
         caused_by: AtomicStr,
     ) -> Self {
-        let loc = match (lhs_loc, rhs_loc) {
-            (Some(l), Some(r)) => Location::pair(l, r),
-            (Some(l), None) => l,
-            (None, Some(r)) => r,
-            (None, None) => Location::Unknown,
-        };
         Self::new(
             ErrorCore::new(
                 errno,
@@ -697,16 +683,9 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         errno: usize,
         sub_t: &Type,
         sup_t: &Type,
-        sub_loc: Option<Location>,
-        sup_loc: Option<Location>,
+        loc: Location,
         caused_by: AtomicStr,
     ) -> Self {
-        let loc = match (sub_loc, sup_loc) {
-            (Some(l), Some(r)) => Location::pair(l, r),
-            (Some(l), None) => l,
-            (None, Some(r)) => r,
-            (None, None) => Location::Unknown,
-        };
         Self::new(
             ErrorCore::new(
                 errno,
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index 73c77f68..ef0f8f2e 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -125,7 +125,7 @@ impl ASTLowerer {
         found: &Type,
     ) -> SingleLowerResult<()> {
         self.ctx
-            .sub_unify(found, expect, None, Some(loc), Some(name))
+            .sub_unify(found, expect, loc, Some(name))
             .map_err(|_| {
                 LowerError::type_mismatch_error(
                     self.cfg.input.clone(),
@@ -887,7 +887,7 @@ impl ASTLowerer {
 
     fn check_override(&mut self, class: &Type, ctx: &Context) {
         if let Some(sups) = self.ctx.get_nominal_super_type_ctxs(class) {
-            for (sup_t, sup) in sups.skip(1) {
+            for (sup_t, sup) in sups.into_iter().skip(1) {
                 for (method_name, vi) in ctx.locals.iter() {
                     if let Some(_sup_vi) = sup.get_current_scope_var(method_name.inspect()) {
                         // must `@Override`
@@ -1058,8 +1058,7 @@ impl ASTLowerer {
         self.ctx.sub_unify(
             expr.ref_t(),
             &t,
-            Some(expr.loc()),
-            None,
+            expr.loc(),
             Some(&Str::from(expr.to_string())),
         )?;
         Ok(hir::TypeAscription::new(expr, tasc.t_spec))