diff --git a/compiler/erg_common/ty.rs b/compiler/erg_common/ty.rs
index 53a419f5..64de79f8 100644
--- a/compiler/erg_common/ty.rs
+++ b/compiler/erg_common/ty.rs
@@ -89,10 +89,6 @@ pub trait HasLevel {
 // REVIEW: TyBoundと微妙に役割が被っている
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Constraint {
-    /// :> T
-    SupertypeOf(Type),
-    /// <: T
-    SubtypeOf(Type),
     /// :> Sub, <: Sup
     Sandwiched {
         sub: Type,
@@ -106,9 +102,15 @@ pub enum Constraint {
 impl fmt::Display for Constraint {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Self::SupertypeOf(sub) => write!(f, ":> {sub}"),
-            Self::SubtypeOf(sup) => write!(f, "<: {sup}"),
-            Self::Sandwiched { sub, sup } => write!(f, ":> {sub}, <: {sup}"),
+            Self::Sandwiched { sub, sup } => {
+                if sub.rec_eq(&Type::Never) {
+                    write!(f, "<: {sup}")
+                } else if sup.rec_eq(&Type::Obj) {
+                    write!(f, ":> {sub}")
+                } else {
+                    write!(f, ":> {sub}, <: {sup}")
+                }
+            }
             Self::TypeOf(ty) => write!(f, ": {}", ty),
             Self::Uninited => write!(f, "<uninited>"),
         }
@@ -120,6 +122,14 @@ impl Constraint {
         Self::Sandwiched { sub, sup }
     }
 
+    pub const fn subtype_of(sup: Type) -> Self {
+        Self::sandwiched(Type::Never, sup)
+    }
+
+    pub const fn supertype_of(sub: Type) -> Self {
+        Self::sandwiched(sub, Type::Obj)
+    }
+
     pub const fn is_uninited(&self) -> bool {
         matches!(self, Self::Uninited)
     }
@@ -133,7 +143,6 @@ impl Constraint {
 
     pub fn sub_type(&self) -> Option<&Type> {
         match self {
-            Self::SupertypeOf(ty) => Some(ty),
             Self::Sandwiched { sub, .. } => Some(sub),
             _ => None,
         }
@@ -141,7 +150,6 @@ impl Constraint {
 
     pub fn super_type(&self) -> Option<&Type> {
         match self {
-            Self::SubtypeOf(ty) => Some(ty),
             Self::Sandwiched { sup, .. } => Some(sup),
             _ => None,
         }
@@ -156,7 +164,6 @@ impl Constraint {
 
     pub fn super_type_mut(&mut self) -> Option<&mut Type> {
         match self {
-            Self::SubtypeOf(ty) => Some(ty),
             Self::Sandwiched { sup, .. } => Some(sup),
             _ => None,
         }
@@ -989,21 +996,35 @@ impl TyParamOrdering {
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum TyBound {
-    // e.g. A <: Add => Subtype{sub: A, sup: Add}, A <: {a: Int} => Subtype{sub: A, sup: {a: Int}}
-    Subtype { sub: Type, sup: Type },
-    Supertype { sup: Type, sub: Type },
-    Sandwiched { sub: Type, mid: Type, sup: Type },
+    // e.g.
+    // A :> Int => Sandwiched{sub: Int, mid: A, sup: Obj}
+    // A <: {I: Int | I > 0} => Sandwiched{sub: Never, mid: A, sup: {I: Int | I > 0}}
+    /// Sub <: Mid <: Sup
+    Sandwiched {
+        sub: Type,
+        mid: Type,
+        sup: Type,
+    },
     // TyParam::MonoQuantVarに型の情報が含まれているので、boundsからは除去される
     // e.g. N: Nat => Instance{name: N, t: Nat}
-    Instance { name: Str, t: Type },
+    Instance {
+        name: Str,
+        t: Type,
+    },
 }
 
 impl fmt::Display for TyBound {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Self::Subtype { sub, sup } => write!(f, "{sub} <: {sup}"),
-            Self::Supertype { sup, sub } => write!(f, "{sup} :> {sub}"),
-            Self::Sandwiched { sub, mid, sup } => write!(f, "{sub} <: {mid} <: {sup}"),
+            Self::Sandwiched { sub, mid, sup } => {
+                if sub.rec_eq(&Type::Never) {
+                    write!(f, "{mid} <: {sup}")
+                } else if sup.rec_eq(&Type::Obj) {
+                    write!(f, "{sub} <: {mid}")
+                } else {
+                    write!(f, "{sub} <: {mid} <: {sup}")
+                }
+            }
             Self::Instance { name, t } => write!(f, "'{name}: {t}"),
         }
     }
@@ -1016,10 +1037,6 @@ impl HasLevel for TyBound {
 
     fn update_level(&self, level: usize) {
         match self {
-            Self::Subtype { sub, sup } | Self::Supertype { sup, sub } => {
-                sub.update_level(level);
-                sup.update_level(level);
-            }
             Self::Sandwiched { sub, mid, sup } => {
                 sub.update_level(level);
                 mid.update_level(level);
@@ -1033,10 +1050,6 @@ impl HasLevel for TyBound {
 
     fn lift(&self) {
         match self {
-            Self::Subtype { sub, sup } | Self::Supertype { sup, sub } => {
-                sub.lift();
-                sup.lift();
-            }
             Self::Sandwiched { sub, mid, sup } => {
                 sub.lift();
                 mid.lift();
@@ -1050,16 +1063,14 @@ impl HasLevel for TyBound {
 }
 
 impl TyBound {
-    pub const fn subtype(sub: Type, sup: Type) -> Self {
-        Self::Subtype { sub, sup }
-    }
-    pub const fn supertype(sup: Type, sub: Type) -> Self {
-        Self::Supertype { sup, sub }
-    }
     pub const fn sandwiched(sub: Type, mid: Type, sup: Type) -> Self {
         Self::Sandwiched { sub, mid, sup }
     }
 
+    pub const fn subtype_of(sub: Type, sup: Type) -> Self {
+        Self::sandwiched(Type::Never, sub, sup)
+    }
+
     pub const fn static_instance(name: &'static str, t: Type) -> Self {
         Self::Instance {
             name: Str::ever(name),
@@ -1076,14 +1087,11 @@ impl TyBound {
     }
 
     pub fn mentions_as_subtype(&self, name: &str) -> bool {
-        matches!(self, Self::Subtype{ sub, .. } if sub.name() == name)
+        matches!(self, Self::Sandwiched{ sub, .. } if sub.name() == name)
     }
 
     pub fn has_unbound_var(&self) -> bool {
         match self {
-            Self::Subtype { sub, sup } | Self::Supertype { sub, sup } => {
-                sub.has_unbound_var() || sup.has_unbound_var()
-            }
             Self::Sandwiched { sub, mid, sup } => {
                 sub.has_unbound_var() || mid.has_unbound_var() || sup.has_unbound_var()
             }
@@ -1093,8 +1101,6 @@ impl TyBound {
 
     pub const fn t(&self) -> &Type {
         match self {
-            Self::Subtype { sup, .. } => sup,
-            Self::Supertype { sub, .. } => sub,
             Self::Sandwiched { .. } => todo!(),
             Self::Instance { t, .. } => t,
         }
@@ -1102,8 +1108,6 @@ impl TyBound {
 
     pub fn lhs(&self) -> &str {
         match self {
-            Self::Subtype { sub, .. } => sub.name(),
-            Self::Supertype { sup, .. } => sup.name(),
             Self::Sandwiched { mid, .. } => mid.name(),
             Self::Instance { name, .. } => name,
         }
@@ -1444,26 +1448,15 @@ pub struct SubrType {
 
 impl fmt::Display for SubrType {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        if self.default_params.is_empty() {
-            write!(
-                f,
-                "{}({}) {} {}",
-                self.kind.prefix(),
-                fmt_vec(&self.non_default_params),
-                self.kind.arrow(),
-                self.return_t,
-            )
-        } else {
-            write!(
-                f,
-                "{}({} |= {}) {} {}",
-                self.kind.prefix(),
-                fmt_vec(&self.non_default_params),
-                fmt_vec(&self.default_params),
-                self.kind.arrow(),
-                self.return_t,
-            )
-        }
+        write!(
+            f,
+            "{}({}, {}) {} {}",
+            self.kind.prefix(),
+            fmt_vec(&self.non_default_params),
+            fmt_vec(&self.default_params),
+            self.kind.arrow(),
+            self.return_t,
+        )
     }
 }
 
@@ -2971,9 +2964,10 @@ pub mod type_constrs {
         TyBound::static_instance(name, t)
     }
 
+    /// Sub <: Sup
     #[inline]
-    pub fn subtype(sub: Type, sup: Type) -> TyBound {
-        TyBound::subtype(sub, sup)
+    pub fn subtypeof(sub: Type, sup: Type) -> TyBound {
+        TyBound::sandwiched(Type::Never, sub, sup)
     }
 
     #[inline]
diff --git a/compiler/erg_compiler/context.rs b/compiler/erg_compiler/context.rs
index e79cd02e..07680921 100644
--- a/compiler/erg_compiler/context.rs
+++ b/compiler/erg_compiler/context.rs
@@ -255,48 +255,6 @@ impl TyVarContext {
 
     fn instantiate_bound(&mut self, bound: TyBound, ctx: &Context) {
         match bound {
-            TyBound::Subtype { sub, sup } => {
-                let sup = match sup {
-                    Type::Poly { name, params } => {
-                        self.instantiate_poly(sub.name(), &name, params, ctx)
-                    }
-                    Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
-                    sup => sup,
-                };
-                let constraint = Constraint::SubtypeOf(sup);
-                if let Some(tv) = self.tyvar_instances.get(sub.name()) {
-                    tv.update_constraint(constraint);
-                } else if let Some(tp) = self.typaram_instances.get(sub.name()) {
-                    tp.update_constraint(constraint);
-                } else {
-                    let name = Str::rc(sub.name());
-                    self.push_tyvar(
-                        name.clone(),
-                        Type::named_free_var(name, self.level, constraint),
-                    );
-                }
-            }
-            TyBound::Supertype { sup, sub } => {
-                let sub = match sub {
-                    Type::Poly { name, params } => {
-                        self.instantiate_poly(sup.name(), &name, params, ctx)
-                    }
-                    Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
-                    sub => sub,
-                };
-                let constraint = Constraint::SupertypeOf(sub);
-                if let Some(tv) = self.tyvar_instances.get(sup.name()) {
-                    tv.update_constraint(constraint);
-                } else if let Some(tp) = self.typaram_instances.get(sup.name()) {
-                    tp.update_constraint(constraint);
-                } else {
-                    let name = Str::rc(sup.name());
-                    self.push_tyvar(
-                        name.clone(),
-                        Type::named_free_var(name, self.level, constraint),
-                    );
-                }
-            }
             TyBound::Sandwiched { sub, mid, sup } => {
                 let sub = match sub {
                     Type::Poly { name, params } => {
@@ -803,6 +761,7 @@ impl Context {
             ast::VarPattern::VarName(v) => {
                 if sig.t_spec.is_none() && opt_t.is_none() {
                     Err(TyCheckError::no_type_spec_error(
+                        line!() as usize,
                         sig.loc(),
                         self.caused_by(),
                         v.inspect(),
@@ -810,6 +769,7 @@ impl Context {
                 } else {
                     if self.registered(v.inspect(), v.inspect().is_uppercase()) {
                         return Err(TyCheckError::duplicate_decl_error(
+                            line!() as usize,
                             sig.loc(),
                             self.caused_by(),
                             v.inspect(),
@@ -849,6 +809,7 @@ impl Context {
         let kind = id.map_or(VarKind::Declared, VarKind::Defined);
         if self.registered(name, name.is_uppercase()) {
             return Err(TyCheckError::duplicate_decl_error(
+                line!() as usize,
                 sig.loc(),
                 self.caused_by(),
                 name,
@@ -858,6 +819,7 @@ impl Context {
         let vi = VarInfo::new(t, muty, Private, kind);
         if let Some(_decl) = self.decls.remove(name) {
             return Err(TyCheckError::duplicate_decl_error(
+                line!() as usize,
                 sig.loc(),
                 self.caused_by(),
                 name,
@@ -901,6 +863,7 @@ impl Context {
             ast::VarPattern::VarName(v) => {
                 if self.registered(v.inspect(), v.inspect().is_uppercase()) {
                     Err(TyCheckError::reassign_error(
+                        line!() as usize,
                         v.loc(),
                         self.caused_by(),
                         v.inspect(),
@@ -940,6 +903,7 @@ impl Context {
             ast::ParamPattern::VarName(v) => {
                 if self.registered(v.inspect(), v.inspect().is_uppercase()) {
                     Err(TyCheckError::reassign_error(
+                        line!() as usize,
                         v.loc(),
                         self.caused_by(),
                         v.inspect(),
@@ -1067,6 +1031,7 @@ impl Context {
             self.unify(spec_ret_t, body_t, Some(sig.loc()), None)
                 .map_err(|e| {
                     TyCheckError::return_type_error(
+                        line!() as usize,
                         e.core.loc,
                         e.caused_by,
                         readable_name(name.inspect()),
@@ -1077,6 +1042,7 @@ impl Context {
         }
         if self.registered(name.inspect(), name.inspect().is_uppercase()) {
             Err(TyCheckError::reassign_error(
+                line!() as usize,
                 name.loc(),
                 self.caused_by(),
                 name.inspect(),
@@ -1127,6 +1093,7 @@ impl Context {
             if let Some(vi) = self.decls.remove(name) {
                 if !self.rec_full_supertype_of(&vi.t, &found_t) {
                     return Err(TyCheckError::violate_decl_error(
+                        line!() as usize,
                         sig.loc(),
                         self.caused_by(),
                         name.inspect(),
@@ -1164,6 +1131,7 @@ impl Context {
                     }
                 } else {
                     return Err(TyCheckError::type_mismatch_error(
+                        line!() as usize,
                         mod_name.loc(),
                         self.caused_by(),
                         "import::name",
@@ -1174,6 +1142,7 @@ impl Context {
             }
             _ => {
                 return Err(TyCheckError::feature_error(
+                    line!() as usize,
                     mod_name.loc(),
                     "non-literal importing",
                     self.caused_by(),
@@ -1184,7 +1153,7 @@ impl Context {
     }
 
     pub(crate) fn _push_subtype_bound(&mut self, sub: Type, sup: Type) {
-        self.bounds.push(TyBound::subtype(sub, sup));
+        self.bounds.push(TyBound::subtype_of(sub, sup));
     }
 
     pub(crate) fn _push_instance_bound(&mut self, name: Str, t: Type) {
@@ -1219,12 +1188,6 @@ impl Context {
                 FreeKind::Unbound { id, constraint, .. } => {
                     let name = id.to_string();
                     let bound = match constraint {
-                        Constraint::SubtypeOf(sup) => {
-                            TyBound::subtype(Type::mono(name.clone()), sup.clone())
-                        }
-                        Constraint::SupertypeOf(sub) => {
-                            TyBound::supertype(Type::mono(name.clone()), sub.clone())
-                        }
                         Constraint::Sandwiched { sub, sup } => {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
@@ -1237,12 +1200,6 @@ impl Context {
                     name, constraint, ..
                 } => {
                     let bound = match constraint {
-                        Constraint::SubtypeOf(sup) => {
-                            TyBound::subtype(Type::mono(name.clone()), sup.clone())
-                        }
-                        Constraint::SupertypeOf(sub) => {
-                            TyBound::supertype(Type::mono(name.clone()), sub.clone())
-                        }
                         Constraint::Sandwiched { sub, sup } => {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
@@ -1280,12 +1237,6 @@ impl Context {
                 FreeKind::Unbound { id, constraint, .. } => {
                     let name = id.to_string();
                     let bound = match constraint {
-                        Constraint::SubtypeOf(sup) => {
-                            TyBound::subtype(Type::mono(name.clone()), sup.clone())
-                        }
-                        Constraint::SupertypeOf(sub) => {
-                            TyBound::supertype(Type::mono(name.clone()), sub.clone())
-                        }
                         Constraint::Sandwiched { sub, sup } => {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
@@ -1298,12 +1249,6 @@ impl Context {
                     name, constraint, ..
                 } => {
                     let bound = match constraint {
-                        Constraint::SubtypeOf(sup) => {
-                            TyBound::subtype(Type::mono(name.clone()), sup.clone())
-                        }
-                        Constraint::SupertypeOf(sub) => {
-                            TyBound::supertype(Type::mono(name.clone()), sub.clone())
-                        }
                         Constraint::Sandwiched { sub, sup } => {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
@@ -1581,6 +1526,7 @@ impl Context {
                 let params_len = subr.non_default_params.len() + subr.default_params.len();
                 if params_len < pos_args.len() + kw_args.len() {
                     return Err(TyCheckError::too_many_args_error(
+                        line!() as usize,
                         callee.loc(),
                         &callee.to_string(),
                         self.caused_by(),
@@ -1609,6 +1555,7 @@ impl Context {
                                     .map(|s| readable_name(&s[..]))
                                     .unwrap_or("");
                             TyCheckError::type_mismatch_error(
+                                line!() as usize,
                                 e.core.loc,
                                 e.caused_by,
                                 &name[..],
@@ -1619,6 +1566,7 @@ impl Context {
                     if let Some(name) = &param_ty.name {
                         if passed_params.contains(name) {
                             return Err(TyCheckError::multiple_args_error(
+                                line!() as usize,
                                 callee.loc(),
                                 &callee.to_string(),
                                 self.caused_by(),
@@ -1643,6 +1591,7 @@ impl Context {
                         self.sub_unify(kw_arg.expr.ref_t(), param_ty, None, Some(kw_arg.loc()))?;
                     } else {
                         return Err(TyCheckError::unexpected_kw_arg_error(
+                            line!() as usize,
                             kw_arg.keyword.loc(),
                             &callee.to_string(),
                             self.caused_by(),
@@ -1689,12 +1638,10 @@ impl Context {
 
     fn deref_constraint(&self, constraint: Constraint) -> TyCheckResult<Constraint> {
         match constraint {
-            Constraint::SubtypeOf(sup) => Ok(Constraint::SubtypeOf(self.deref_tyvar(sup)?)),
             Constraint::Sandwiched { sub, sup } => Ok(Constraint::sandwiched(
                 self.deref_tyvar(sub)?,
                 self.deref_tyvar(sup)?,
             )),
-            Constraint::SupertypeOf(sub) => Ok(Constraint::SupertypeOf(self.deref_tyvar(sub)?)),
             Constraint::TypeOf(t) => Ok(Constraint::TypeOf(self.deref_tyvar(t)?)),
             _ => unreachable!(),
         }
@@ -1702,25 +1649,35 @@ impl Context {
 
     /// e.g.
     /// ```
-    /// deref_tyvar(?T(<: Int)[n]): ?T => Int (if self.level <= n)
+    /// deref_tyvar(?T(:> Never, <: Int)[n]): ?T => Int (if self.level <= n)
     /// deref_tyvar((Int)): (Int) => Int
     /// ```
     fn deref_tyvar(&self, t: Type) -> TyCheckResult<Type> {
         match t {
-            // ?T(<: Int)[n] => Int
-            Type::FreeVar(fv) if fv.constraint_is_subtypeof() || fv.constraint_is_sandwiched() => {
-                if self.level <= fv.level().unwrap() {
-                    Ok(fv.crack_constraint().super_type().unwrap().clone())
+            // ?T(:> Nat, <: Int)[n] => Nat (self.level <= n)
+            // ?T(:> Nat, <: Sub ?U(:> {1}))[n] => Nat
+            Type::FreeVar(fv) if fv.constraint_is_sandwiched() => {
+                let constraint = fv.crack_constraint();
+                let (sub, sup) = constraint.sub_sup_type().unwrap();
+                if self.rec_full_same_type_of(sub, sup) {
+                    self.unify(sub, sub, None, None)?;
+                    let t = sub.clone();
+                    drop(constraint);
+                    fv.link(&t);
+                    self.deref_tyvar(Type::FreeVar(fv))
+                } else if self.level == 0 || self.level <= fv.level().unwrap() {
+                    let t = sub.clone();
+                    drop(constraint);
+                    fv.link(&t);
+                    self.deref_tyvar(Type::FreeVar(fv))
                 } else {
+                    drop(constraint);
                     Ok(Type::FreeVar(fv))
                 }
             }
-            // ?T(<: Add(?R(<: T), ?O(<: U)) => ?T(<: Add(T, U))
             Type::FreeVar(fv) if fv.is_unbound() => {
                 if self.level == 0 {
                     match &*fv.crack_constraint() {
-                        Constraint::SupertypeOf(t) | Constraint::SubtypeOf(t) => Ok(t.clone()),
-                        Constraint::Sandwiched { sub, .. } => Ok(sub.clone()),
                         Constraint::TypeOf(_) => {
                             Err(TyCheckError::dummy_infer_error(fn_name!(), line!()))
                         }
@@ -1907,7 +1864,7 @@ impl Context {
                 if self.rec_full_supertype_of(&fv_t, &tp_t) {
                     // 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
                     if fv.level() < Some(self.level) {
-                        let new_constraint = Constraint::SubtypeOf(tp_t);
+                        let new_constraint = Constraint::subtype_of(tp_t);
                         if self.is_sub_constraint_of(
                             fv.borrow().constraint().unwrap(),
                             &new_constraint,
@@ -2025,6 +1982,7 @@ impl Context {
                         self.unify_tp(le_rhs, &TyParam::value(Inf), None, None, true)
                     }
                     _ => Err(TyCheckError::pred_unification_error(
+                        line!() as usize,
                         l_pred,
                         r_pred,
                         self.caused_by(),
@@ -2039,6 +1997,7 @@ impl Context {
                     self.unify_tp(ge_rhs, &TyParam::value(NegInf), None, None, true)
                 }
                 _ => Err(TyCheckError::pred_unification_error(
+                    line!() as usize,
                     l_pred,
                     r_pred,
                     self.caused_by(),
@@ -2052,12 +2011,14 @@ impl Context {
                     self.unify_tp(rhs, ge_rhs, None, None, false)
                 }
                 _ => Err(TyCheckError::pred_unification_error(
+                    line!() as usize,
                     l_pred,
                     r_pred,
                     self.caused_by(),
                 )),
             },
             _ => Err(TyCheckError::pred_unification_error(
+                line!() as usize,
                 l_pred,
                 r_pred,
                 self.caused_by(),
@@ -2123,7 +2084,7 @@ impl Context {
                         }
                     }
                 } // &fv is dropped
-                let new_constraint = Constraint::SubtypeOf(t.clone());
+                let new_constraint = Constraint::subtype_of(t.clone());
                 // 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
                 // fv == ?T(: Type)の場合は?T(<: U)にする
                 if fv.level() < Some(self.level) {
@@ -2142,6 +2103,7 @@ impl Context {
                     && !self.formal_supertype_of(&r.t, &l.t, None, None)
                 {
                     return Err(TyCheckError::unification_error(
+                        line!() as usize,
                         lhs_t,
                         rhs_t,
                         lhs_loc,
@@ -2196,6 +2158,7 @@ impl Context {
             ) => {
                 if ln != rn {
                     return Err(TyCheckError::unification_error(
+                        line!() as usize,
                         lhs_t,
                         rhs_t,
                         lhs_loc,
@@ -2212,6 +2175,7 @@ impl Context {
                 todo!()
             }
             (l, r) => Err(TyCheckError::unification_error(
+                line!() as usize,
                 l,
                 r,
                 lhs_loc,
@@ -2257,6 +2221,7 @@ impl Context {
                 if ln != rn {
                     let before_t = Type::poly(ln.clone(), lps.clone());
                     return Err(TyCheckError::re_unification_error(
+                        line!() as usize,
                         &before_t,
                         after_t,
                         bef_loc,
@@ -2271,6 +2236,7 @@ impl Context {
             }
             (l, r) if self.formal_same_type_of(l, r, None, None) => Ok(()),
             (l, r) => Err(TyCheckError::re_unification_error(
+                line!() as usize,
                 l,
                 r,
                 bef_loc,
@@ -2306,6 +2272,7 @@ impl Context {
         if !maybe_sub_is_sub {
             let loc = sub_loc.or(sup_loc).unwrap_or(Location::Unknown);
             return Err(TyCheckError::type_mismatch_error(
+                line!() as usize,
                 loc,
                 self.caused_by(),
                 "<???>",
@@ -2318,57 +2285,47 @@ impl Context {
                 match &mut *fv.borrow_mut() {
                     FreeKind::NamedUnbound { constraint, .. }
                     | FreeKind::Unbound { constraint, .. } => match constraint {
-                        // sub_unify(Nat, ?T(:> Int)): (/* OK */)
-                        // sub_unify(Int, ?T(:> Nat)): (?T :> Int)
-                        // sub_unify(Str, ?T(:> Int)): (/* ?T = Str or Int */) // TODO:
-                        Constraint::SupertypeOf(sub) => {
-                            if self.rec_full_supertype_of(l, sub) {
-                                *constraint = Constraint::SupertypeOf(l.clone());
-                            } else if self.rec_full_subtype_of(l, sub) {
-                                /* OK */
+                        // sub !<: l => OK (sub will widen)
+                        // sup !:> l => Error
+                        // * sub_unify(Str,   ?T(:> _,     <: Int)): (/* Error */)
+                        // * sub_unify(Ratio, ?T(:> _,     <: Int)): (/* Error */)
+                        // sub = max(l, sub) if max exists
+                        // * sub_unify(Nat,   ?T(:> Int,   <: _)): (/* OK */)
+                        // * sub_unify(Int,   ?T(:> Nat,   <: Obj)): (?T(:> Int, <: Obj))
+                        // * sub_unify(Nat,   ?T(:> Never, <: Add(?R, ?O))): (?T(:> Nat, <: Add(?R, ?O))
+                        // sub = union(l, sub) if max does not exist
+                        // * sub_unify(Str,   ?T(:> Int,   <: Obj)): (?T(:> Str or Int, <: Obj))
+                        // * sub_unify({0},   ?T(:> {1},   <: Nat)): (?T(:> {0, 1}, <: Nat))
+                        // nested variable is prohibited
+                        // ☓ sub_unify({0},  ?T(:> ?U, <: Ord))
+                        Constraint::Sandwiched { sub, sup } => {
+                            if !self.rec_full_supertype_of(sup, l) {
+                                return Err(TyCheckError::subtyping_error(
+                                    line!() as usize,
+                                    l,
+                                    sup, // TODO: this?
+                                    sub_loc,
+                                    sup_loc,
+                                    self.caused_by(),
+                                ));
+                            }
+                            if let Some(new_sub) = self.max(l, sub) {
+                                *constraint =
+                                    Constraint::sandwiched(new_sub.clone(), mem::take(sup));
+                            } else {
+                                let new_sub = self.union(l, sub);
+                                *constraint = Constraint::sandwiched(new_sub, mem::take(sup));
+                            }
+                        }
+                        // sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
+                        Constraint::TypeOf(ty) => {
+                            if self.rec_full_supertype_of(&Type, ty) {
+                                *constraint = Constraint::supertype_of(l.clone());
                             } else {
                                 todo!()
                             }
                         }
-                        // sub_unify(Nat, ?T(<: Int)): (Nat <: ?T <: Int)
-                        // sub_unify(Nat, ?T(<: Add(?R, ?O))): (Nat <: ?T <: Add(?R, ?O))
-                        // sub_unify(Int, ?T(<: Nat)): (/* Error */)
-                        // sub_unify(Str, ?T(<: Int)): (/* Error */)
-                        Constraint::SubtypeOf(sup) => {
-                            if !self.rec_full_subtype_of(l, sup) {
-                                return Err(TyCheckError::subtyping_error(
-                                    l,
-                                    sup,
-                                    sub_loc,
-                                    sup_loc,
-                                    self.caused_by(),
-                                ));
-                            } else {
-                                *constraint = Constraint::sandwiched(l.clone(), mem::take(sup));
-                            }
-                        }
-                        // sub_unify(Nat, (Int <: ?T <: Ratio)): (/* OK */)
-                        // sub_unify(Int, (Nat <: ?T <: Ratio)): (Int <: ?T <: Ratio)
-                        // sub_unify(Str, (Nat <: ?T <: Ratio)): (/* Error */)
-                        // sub_unify({0}, ({1} <: ?T <: Nat)): ({0, 1} <: ?T <: Nat))
-                        Constraint::Sandwiched { sub, sup } => {
-                            if self.rec_full_no_relation_of(l, sup) {
-                                return Err(TyCheckError::subtyping_error(
-                                    l,
-                                    sup, // TODO:
-                                    sub_loc,
-                                    sup_loc,
-                                    self.caused_by(),
-                                ));
-                            } else {
-                                let union = self.union(l, sub);
-                                *constraint = Constraint::sandwiched(union, mem::take(sub));
-                            }
-                        }
-                        Constraint::TypeOf(_t) => {
-                            *constraint = Constraint::SupertypeOf(l.clone());
-                        }
-                        _ => {}
+                        _ => unreachable!(),
                     },
                     _ => {}
                 }
@@ -2378,47 +2335,47 @@ impl Context {
                 match &mut *fv.borrow_mut() {
                     FreeKind::NamedUnbound { constraint, .. }
                     | FreeKind::Unbound { constraint, .. } => match constraint {
-                        // sub_unify(?T(:> Int), Nat): (/* Error */)
-                        // sub_unify(?T(:> Nat), Int): (Nat <: ?T <: Int)
-                        // sub_unify(?T(:> Nat), Str): (/* Error */)
-                        Constraint::SupertypeOf(sub) => {
-                            if !self.rec_full_subtype_of(sub, r) {
+                        // sub !<: r => Error
+                        // * sub_unify(?T(:> Int,   <: _), Nat): (/* Error */)
+                        // * sub_unify(?T(:> Nat,   <: _), Str): (/* Error */)
+                        // sup !:> r => Error
+                        // * sub_unify(?T(:> _, <: Str), Int): (/* Error */)
+                        // * sub_unify(?T(:> _, <: Int), Nat): (/* Error */)
+                        // sub <: r, sup :> r => sup = min(sup, r) if min exists
+                        // * sub_unify(?T(:> Never, <: Nat), Int): (/* OK */)
+                        // * sub_unify(?T(:> Nat,   <: Obj), Int): (?T(:> Nat,   <: Int))
+                        // sup = union(sup, r) if min does not exist
+                        // * sub_unify(?T(:> Never, <: {1}), {0}): (?T(:> Never, <: {0, 1}))
+                        Constraint::Sandwiched { sub, sup } => {
+                            if !self.rec_full_subtype_of(sub, r)
+                                || !self.rec_full_supertype_of(sup, r)
+                            {
                                 return Err(TyCheckError::subtyping_error(
+                                    line!() as usize,
                                     sub,
                                     r,
                                     sub_loc,
                                     sup_loc,
                                     self.caused_by(),
                                 ));
+                            }
+                            if let Some(new_sup) = self.min(sup, r) {
+                                *constraint =
+                                    Constraint::sandwiched(mem::take(sub), new_sup.clone());
                             } else {
-                                *constraint = Constraint::sandwiched(sub.clone(), r.clone());
+                                let new_sup = self.union(sup, r);
+                                *constraint = Constraint::sandwiched(mem::take(sub), new_sup);
                             }
                         }
-                        // sub_unify(?T(<: Int), Nat): (?T(<: Nat))
-                        // sub_unify(?T(<: Nat), Int): (/* OK */)
-                        // sub_unify(?T(<: Str), Int): (/* Error */) // TODO:
-                        Constraint::SubtypeOf(sup) if self.rec_full_supertype_of(sup, r) => {
-                            *constraint = Constraint::SubtypeOf(r.clone());
-                        }
-                        // sub_unify((Int <: ?T <: Ratio), Nat): (/* Error */)
-                        // sub_unify((Nat <: ?T <: Ratio), Int): (/* OK */)
-                        // sub_unify((Nat <: ?T <: Int), Str): (/* Error */)
-                        Constraint::Sandwiched { sub, sup: _ }
-                            if !self.rec_full_subtype_of(sub, r) =>
-                        {
-                            return Err(TyCheckError::subtyping_error(
-                                sub,
-                                r,
-                                sub_loc,
-                                sup_loc,
-                                self.caused_by(),
-                            ))
-                        }
                         // sub_unify(?T(: Type), Int): (?T(<: Int))
-                        Constraint::TypeOf(_t) => {
-                            *constraint = Constraint::SubtypeOf(r.clone());
+                        Constraint::TypeOf(ty) => {
+                            if self.rec_full_supertype_of(&Type, ty) {
+                                *constraint = Constraint::subtype_of(r.clone());
+                            } else {
+                                todo!()
+                            }
                         }
-                        _ => {}
+                        _ => unreachable!(),
                     },
                     _ => {}
                 }
@@ -2502,6 +2459,7 @@ impl Context {
             ast::VarPattern::Discard(token) => {
                 if self.unify(&spec_t, body_t, None, Some(sig.loc())).is_err() {
                     return Err(TyCheckError::type_mismatch_error(
+                        line!() as usize,
                         token.loc(),
                         self.caused_by(),
                         "_",
@@ -2513,6 +2471,7 @@ impl Context {
             ast::VarPattern::VarName(n) => {
                 if self.unify(&spec_t, body_t, None, Some(sig.loc())).is_err() {
                     return Err(TyCheckError::type_mismatch_error(
+                        line!() as usize,
                         n.loc(),
                         self.caused_by(),
                         n.inspect(),
@@ -2804,7 +2763,7 @@ impl Context {
         // REVIEW: 型境界の左辺に来れるのは型変数だけか?
         // TODO: 高階型変数
         match bound {
-            TypeBoundSpec::Subtype { sub, sup } => Ok(TyBound::subtype(
+            TypeBoundSpec::Subtype { sub, sup } => Ok(TyBound::subtype_of(
                 Type::mono_q(sub.inspect().clone()),
                 self.instantiate_typespec(sup, mode)?,
             )),
@@ -2857,6 +2816,7 @@ impl Context {
                         Ok(ctx)
                     } else {
                         Err(TyCheckError::no_var_error(
+                            line!() as usize,
                             obj.loc(),
                             namespace.clone(),
                             name.inspect(),
@@ -2883,6 +2843,7 @@ impl Context {
             let t = pos_arg.expr.ref_t();
             if !matches!(&pos_arg.expr, hir::Expr::Lambda(_)) {
                 return Err(TyCheckError::type_mismatch_error(
+                    line!() as usize,
                     pos_arg.loc(),
                     self.caused_by(),
                     "match",
@@ -2901,6 +2862,7 @@ impl Context {
             }
             if lambda.params.len() != 1 {
                 return Err(TyCheckError::argument_error(
+                    line!() as usize,
                     pos_args[i + 1].loc(),
                     self.caused_by(),
                     1,
@@ -2917,6 +2879,7 @@ impl Context {
             && !self.formal_supertype_of(&union_pat_t, expr_t, None, None)
         {
             return Err(TyCheckError::match_error(
+                line!() as usize,
                 pos_args[0].loc(),
                 self.caused_by(),
                 expr_t,
@@ -2957,6 +2920,7 @@ impl Context {
                 return parent.get_var_t(name, namespace);
             }
             Err(TyCheckError::no_var_error(
+                line!() as usize,
                 name.loc(),
                 namespace.clone(),
                 name.inspect(),
@@ -2993,6 +2957,7 @@ impl Context {
             parent.get_attr_t(obj, name, namespace)
         } else {
             Err(TyCheckError::no_attr_error(
+                line!() as usize,
                 name.loc(),
                 namespace.clone(),
                 &self_t,
@@ -3177,12 +3142,7 @@ impl Context {
         self.rec_full_supertype_of(rhs, lhs)
     }
 
-    /// !(L :> R || L <: R)
-    pub(crate) fn rec_full_no_relation_of(&self, lhs: &Type, rhs: &Type) -> bool {
-        !self.rec_full_supertype_of(lhs, rhs) && !self.rec_full_subtype_of(lhs, rhs)
-    }
-
-    pub(crate) fn _rec_full_same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
+    pub(crate) fn rec_full_same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
         self.rec_full_supertype_of(lhs, rhs) && self.rec_full_subtype_of(lhs, rhs)
     }
 
@@ -3323,12 +3283,8 @@ impl Context {
                     FreeKind::Unbound { constraint, .. }
                     | FreeKind::NamedUnbound { constraint, .. } => match constraint {
                         // `(?T <: Int) :> Nat` can be true, `(?T <: Nat) :> Int` is false
-                        Constraint::SubtypeOf(sup) => {
-                            self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
-                        }
                         // `(?T :> X) :> Y` is true
                         // `(?T :> Str) :> Int` is true (?T :> Str or Int)
-                        Constraint::SupertypeOf(_sub) => true,
                         // `(Nat <: ?T <: Ratio) :> Nat` can be true
                         Constraint::Sandwiched { sup, .. } => {
                             self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
@@ -3356,14 +3312,7 @@ impl Context {
                         // `Nat :> (?T <: Int)` can be true
                         // `Int :> (?T <: Nat)` can be true
                         // `Str :> (?T <: Int)` is false
-                        Constraint::SubtypeOf(sup) => {
-                            self.formal_supertype_of(lhs, sup, bounds, lhs_variance)
-                                || self.formal_subtype_of(lhs, sup, bounds, lhs_variance)
-                        }
                         // `Int :> (?T :> Nat)` can be true, `Nat :> (?T :> Int)` is false
-                        Constraint::SupertypeOf(sub) => {
-                            self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
-                        }
                         // `Int :> (Nat <: ?T <: Ratio)` can be true, `Nat :> (Int <: ?T <: Ratio)` is false
                         Constraint::Sandwiched { sub, sup: _ } => {
                             self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
@@ -3752,17 +3701,14 @@ impl Context {
 
     fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
         match (l, r) {
-            // |T <: Nat| <: |T <: Int|
             // |I: Nat| <: |I: Int|
-            (Constraint::SubtypeOf(lhs), Constraint::SubtypeOf(rhs))
-            | (Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => {
+            (Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => {
                 self.rec_full_subtype_of(lhs, rhs)
             }
+            // |T <: Int| <: |T: Type|
+            (Constraint::Sandwiched { sub: Never, .. }, Constraint::TypeOf(Type)) => true,
             // |Int <: T| <: |Nat <: T|
-            (Constraint::SupertypeOf(lhs), Constraint::SupertypeOf(rhs)) => {
-                self.rec_full_supertype_of(lhs, rhs)
-            }
-            (Constraint::SubtypeOf(_), Constraint::TypeOf(Type)) => true,
+            // |T <: Nat| <: |T <: Int|
             // |Int <: T <: Ratio| <: |Nat <: T <: Complex|
             (
                 Constraint::Sandwiched {
@@ -3853,6 +3799,18 @@ impl Context {
         }
     }
 
+    fn max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
+        // 同じならどちらを返しても良い
+        match (
+            self.rec_full_supertype_of(lhs, rhs),
+            self.rec_full_subtype_of(lhs, rhs),
+        ) {
+            (true, true) | (true, false) => Some(lhs),
+            (false, true) => Some(rhs),
+            (false, false) => None,
+        }
+    }
+
     fn cmp_t<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> TyParamOrdering {
         match self.min(lhs, rhs) {
             Some(l) if l == lhs => TyParamOrdering::Less,
@@ -3886,6 +3844,7 @@ impl Context {
                 return parent.get_local(name, namespace);
             }
             Err(TyCheckError::no_var_error(
+                line!() as usize,
                 name.loc(),
                 namespace.clone(),
                 name.inspect(),
@@ -3911,6 +3870,7 @@ impl Context {
             parent._get_attr(obj, name, namespace)
         } else {
             Err(TyCheckError::no_attr_error(
+                line!() as usize,
                 name.loc(),
                 namespace.clone(),
                 &self_t,
@@ -3973,6 +3933,7 @@ impl Context {
         let mut uninited_errs = TyCheckErrors::empty();
         for (name, vi) in self.decls.iter() {
             uninited_errs.push(TyCheckError::uninitialized_error(
+                line!() as usize,
                 name.loc(),
                 self.caused_by(),
                 name.inspect(),
diff --git a/compiler/erg_compiler/effectcheck.rs b/compiler/erg_compiler/effectcheck.rs
index 4c4fd8b1..2fdd6632 100644
--- a/compiler/erg_compiler/effectcheck.rs
+++ b/compiler/erg_compiler/effectcheck.rs
@@ -97,8 +97,11 @@ impl SideEffectChecker {
             (true, _) => {
                 if !allow_inner_effect {
                     let expr = Expr::Def(def.clone());
-                    self.errs
-                        .push(EffectError::has_effect(&expr, self.full_path()));
+                    self.errs.push(EffectError::has_effect(
+                        line!() as usize,
+                        &expr,
+                        self.full_path(),
+                    ));
                 }
                 for chunk in def.body.block.iter() {
                     self.check_expr(chunk, allow_inner_effect);
@@ -165,8 +168,11 @@ impl SideEffectChecker {
             // 引数がproceduralでも関数呼び出しなら副作用なし
             Expr::Call(call) => {
                 if self.is_procedural(&call.obj) && !allow_self_effect {
-                    self.errs
-                        .push(EffectError::has_effect(expr, self.full_path()));
+                    self.errs.push(EffectError::has_effect(
+                        line!() as usize,
+                        expr,
+                        self.full_path(),
+                    ));
                 }
                 call.args
                     .pos_args
@@ -192,8 +198,11 @@ impl SideEffectChecker {
                     self.path_stack.push((Str::ever("<lambda>"), Private));
                 }
                 if !allow_self_effect && is_proc {
-                    self.errs
-                        .push(EffectError::has_effect(expr, self.full_path()));
+                    self.errs.push(EffectError::has_effect(
+                        line!() as usize,
+                        expr,
+                        self.full_path(),
+                    ));
                 }
                 lambda
                     .body
diff --git a/compiler/erg_compiler/error.rs b/compiler/erg_compiler/error.rs
index 5276c1d8..f04be8e6 100644
--- a/compiler/erg_compiler/error.rs
+++ b/compiler/erg_compiler/error.rs
@@ -248,10 +248,10 @@ impl TyCheckError {
         )
     }
 
-    pub fn feature_error(loc: Location, name: &str, caused_by: Str) -> Self {
+    pub fn feature_error(errno: usize, loc: Location, name: &str, caused_by: Str) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 FeatureError,
                 loc,
                 switch_lang!(
@@ -277,11 +277,11 @@ impl TyCheckError {
         )
     }
 
-    pub fn duplicate_decl_error(loc: Location, caused_by: Str, name: &str) -> Self {
+    pub fn duplicate_decl_error(errno: usize, loc: Location, caused_by: Str, name: &str) -> Self {
         let name = readable_name(name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 NameError,
                 loc,
                 switch_lang!(
@@ -295,6 +295,7 @@ impl TyCheckError {
     }
 
     pub fn violate_decl_error(
+        errno: usize,
         loc: Location,
         caused_by: Str,
         name: &str,
@@ -304,7 +305,7 @@ impl TyCheckError {
         let name = readable_name(name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -317,11 +318,11 @@ impl TyCheckError {
         )
     }
 
-    pub fn no_type_spec_error(loc: Location, caused_by: Str, name: &str) -> Self {
+    pub fn no_type_spec_error(errno: usize, loc: Location, caused_by: Str, name: &str) -> Self {
         let name = readable_name(name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -335,6 +336,7 @@ impl TyCheckError {
     }
 
     pub fn no_var_error(
+        errno: usize,
         loc: Location,
         caused_by: Str,
         name: &str,
@@ -351,7 +353,7 @@ impl TyCheckError {
         });
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 NameError,
                 loc,
                 switch_lang!(
@@ -365,6 +367,7 @@ impl TyCheckError {
     }
 
     pub fn no_attr_error(
+        errno: usize,
         loc: Location,
         caused_by: Str,
         obj_t: &Type,
@@ -381,7 +384,7 @@ impl TyCheckError {
         });
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 AttributeError,
                 loc,
                 switch_lang!(
@@ -395,6 +398,7 @@ impl TyCheckError {
     }
 
     pub fn callable_impl_error<'a, C: Locational + Display>(
+        errno: usize,
         callee: &C,
         param_ts: impl Iterator<Item = &'a Type>,
         caused_by: Str,
@@ -402,7 +406,7 @@ impl TyCheckError {
         let param_ts = fmt_iter(param_ts);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 NotImplementedError,
                 callee.loc(),
                 switch_lang!(
@@ -420,6 +424,7 @@ impl TyCheckError {
     }
 
     pub fn type_mismatch_error(
+        errno: usize,
         loc: Location,
         caused_by: Str,
         name: &str,
@@ -428,7 +433,7 @@ impl TyCheckError {
     ) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -442,6 +447,7 @@ impl TyCheckError {
     }
 
     pub fn return_type_error(
+        errno: usize,
         loc: Location,
         caused_by: Str,
         name: &str,
@@ -450,7 +456,7 @@ impl TyCheckError {
     ) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -463,10 +469,16 @@ impl TyCheckError {
         )
     }
 
-    pub fn uninitialized_error(loc: Location, caused_by: Str, name: &str, t: &Type) -> Self {
+    pub fn uninitialized_error(
+        errno: usize,
+        loc: Location,
+        caused_by: Str,
+        name: &str,
+        t: &Type,
+    ) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 NameError,
                 loc,
                 switch_lang!(
@@ -479,10 +491,16 @@ impl TyCheckError {
         )
     }
 
-    pub fn argument_error(loc: Location, caused_by: Str, expect: usize, found: usize) -> Self {
+    pub fn argument_error(
+        errno: usize,
+        loc: Location,
+        caused_by: Str,
+        expect: usize,
+        found: usize,
+    ) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -495,10 +513,10 @@ impl TyCheckError {
         )
     }
 
-    pub fn match_error(loc: Location, caused_by: Str, expr_t: &Type) -> Self {
+    pub fn match_error(errno: usize, loc: Location, caused_by: Str, expr_t: &Type) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -511,10 +529,10 @@ impl TyCheckError {
         )
     }
 
-    pub fn infer_error(loc: Location, caused_by: Str, expr: &str) -> Self {
+    pub fn infer_error(errno: usize, loc: Location, caused_by: Str, expr: &str) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -535,11 +553,11 @@ impl TyCheckError {
         Self::new(ErrorCore::unreachable(fn_name, line), "".into())
     }
 
-    pub fn reassign_error(loc: Location, caused_by: Str, name: &str) -> Self {
+    pub fn reassign_error(errno: usize, loc: Location, caused_by: Str, name: &str) -> Self {
         let name = readable_name(name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 AssignError,
                 loc,
                 switch_lang!(
@@ -553,6 +571,7 @@ impl TyCheckError {
     }
 
     pub fn too_many_args_error(
+        errno: usize,
         loc: Location,
         callee_name: &str,
         caused_by: Str,
@@ -563,7 +582,7 @@ impl TyCheckError {
         let name = readable_name(callee_name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -587,6 +606,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     }
 
     pub fn multiple_args_error(
+        errno: usize,
         loc: Location,
         callee_name: &str,
         caused_by: Str,
@@ -595,7 +615,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         let name = readable_name(callee_name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -609,6 +629,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     }
 
     pub fn unexpected_kw_arg_error(
+        errno: usize,
         loc: Location,
         callee_name: &str,
         caused_by: Str,
@@ -617,7 +638,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         let name = readable_name(callee_name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -630,11 +651,11 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         )
     }
 
-    pub fn unused_warning(loc: Location, name: &str, caused_by: Str) -> Self {
+    pub fn unused_warning(errno: usize, loc: Location, name: &str, caused_by: Str) -> Self {
         let name = readable_name(name);
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 UnusedWarning,
                 loc,
                 switch_lang!(
@@ -648,6 +669,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     }
 
     pub fn unification_error(
+        errno: usize,
         lhs_t: &Type,
         rhs_t: &Type,
         lhs_loc: Option<Location>,
@@ -662,7 +684,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         };
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -676,6 +698,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     }
 
     pub fn re_unification_error(
+        errno: usize,
         lhs_t: &Type,
         rhs_t: &Type,
         lhs_loc: Option<Location>,
@@ -690,7 +713,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         };
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -704,6 +727,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     }
 
     pub fn subtyping_error(
+        errno: usize,
         sub_t: &Type,
         sup_t: &Type,
         sub_loc: Option<Location>,
@@ -718,7 +742,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         };
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 loc,
                 switch_lang!(
@@ -731,10 +755,15 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         )
     }
 
-    pub fn pred_unification_error(lhs: &Predicate, rhs: &Predicate, caused_by: Str) -> Self {
+    pub fn pred_unification_error(
+        errno: usize,
+        lhs: &Predicate,
+        rhs: &Predicate,
+        caused_by: Str,
+    ) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 TypeError,
                 Location::Unknown,
                 switch_lang!(
@@ -747,10 +776,10 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         )
     }
 
-    pub fn has_effect<S: Into<Str>>(expr: &Expr, caused_by: S) -> Self {
+    pub fn has_effect<S: Into<Str>>(errno: usize, expr: &Expr, caused_by: S) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 HasEffect,
                 expr.loc(),
                 switch_lang!(
@@ -764,6 +793,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     }
 
     pub fn move_error<S: Into<Str>>(
+        errno: usize,
         name: &str,
         name_loc: Location,
         moved_loc: Location,
@@ -771,7 +801,7 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
     ) -> Self {
         Self::new(
             ErrorCore::new(
-                0,
+                errno,
                 MoveError,
                 name_loc,
                 switch_lang!(
diff --git a/compiler/erg_compiler/eval.rs b/compiler/erg_compiler/eval.rs
index da6c9547..777e1eb2 100644
--- a/compiler/erg_compiler/eval.rs
+++ b/compiler/erg_compiler/eval.rs
@@ -399,14 +399,6 @@ impl Evaluator {
         level: usize,
     ) -> EvalResult<TyBound> {
         match bound {
-            TyBound::Subtype { sub, sup } => Ok(TyBound::subtype(
-                self.eval_t_params(sub, ctx, level)?,
-                self.eval_t_params(sup, ctx, level)?,
-            )),
-            TyBound::Supertype { sup, sub } => Ok(TyBound::supertype(
-                self.eval_t_params(sup, ctx, level)?,
-                self.eval_t_params(sub, ctx, level)?,
-            )),
             TyBound::Sandwiched { sub, mid, sup } => {
                 let sub = self.eval_t_params(sub, ctx, level)?;
                 let mid = self.eval_t_params(mid, ctx, level)?;
diff --git a/compiler/erg_compiler/initialize.rs b/compiler/erg_compiler/initialize.rs
index 92c6fc0d..b58e80d1 100644
--- a/compiler/erg_compiler/initialize.rs
+++ b/compiler/erg_compiler/initialize.rs
@@ -122,7 +122,7 @@ impl Context {
         let op_t = quant(
             op_t,
             set! {
-                subtype(mono_q("Self"), poly("Eq", vec![ty_tp(mono_q("R"))])),
+                subtypeof(mono_q("Self"), poly("Eq", vec![ty_tp(mono_q("R"))])),
                 static_instance("R", Type)
             },
         );
@@ -137,7 +137,7 @@ impl Context {
         let op_t = quant(
             op_t,
             set! {
-                subtype(mono_q("Self"), poly("PartialOrd", vec![ty_tp(mono_q("R"))])),
+                subtypeof(mono_q("Self"), poly("PartialOrd", vec![ty_tp(mono_q("R"))])),
                 static_instance("R", Type)
             },
         );
@@ -157,13 +157,13 @@ impl Context {
         let t = fn0_met(self_t.clone(), Nat);
         let t = quant(
             t,
-            set! {subtype(self_t.clone(), poly("Seq", vec![TyParam::erased(Type)]))},
+            set! {subtypeof(self_t.clone(), poly("Seq", vec![TyParam::erased(Type)]))},
         );
         seq.register_decl("__len__", t, Public);
         let t = Type::fn1_met(self_t.clone(), Nat, mono_q("T"));
         let t = quant(
             t,
-            set! {subtype(self_t, poly("Seq", vec![ty_tp(mono_q("T"))])), static_instance("T", Type)},
+            set! {subtypeof(self_t, poly("Seq", vec![ty_tp(mono_q("T"))])), static_instance("T", Type)},
         );
         // Seq.get: |Self <: Seq(T)| Self.(Nat) -> T
         seq.register_decl("get", t, Public);
@@ -180,7 +180,7 @@ impl Context {
             vec![poly("Output", vec![ty_tp(mono_q("R"))])],
             Self::TOP_LEVEL,
         );
-        let self_bound = subtype(mono_q("Self"), poly("Add", ty_params.clone()));
+        let self_bound = subtypeof(mono_q("Self"), poly("Add", ty_params.clone()));
         let op_t = fn1_met(
             poly_q("Self", ty_params.clone()),
             r.clone(),
@@ -195,7 +195,7 @@ impl Context {
             vec![poly("Output", vec![ty_tp(mono_q("R"))])],
             Self::TOP_LEVEL,
         );
-        let self_bound = subtype(mono_q("Self"), poly("Sub", ty_params.clone()));
+        let self_bound = subtypeof(mono_q("Self"), poly("Sub", ty_params.clone()));
         let op_t = fn1_met(
             poly_q("Self", ty_params.clone()),
             r.clone(),
@@ -275,7 +275,7 @@ impl Context {
     fn init_builtin_classes(&mut self) {
         let mut obj = Self::mono_class("Obj", vec![], vec![], Self::TOP_LEVEL);
         let t = fn0_met(mono_q("Self"), mono_q("Self"));
-        let t = quant(t, set! {subtype(mono_q("Self"), mono("Obj"))});
+        let t = quant(t, set! {subtypeof(mono_q("Self"), mono("Obj"))});
         obj.register_impl("clone", t, Const, Public);
         obj.register_impl("__module__", Str, Const, Public);
         obj.register_impl("__sizeof__", fn0_met(Obj, Nat), Const, Public);
@@ -676,7 +676,7 @@ impl Context {
             op_t,
             set! {
                 static_instance("R", Type),
-                subtype(l.clone(), poly("Add", params.clone()))
+                subtypeof(l.clone(), poly("Add", params.clone()))
             },
         );
         self.register_impl("__add__", op_t, Const, Private);
@@ -685,7 +685,7 @@ impl Context {
             op_t,
             set! {
                 static_instance("R", Type),
-                subtype(l.clone(), poly("Sub", params.clone()))
+                subtypeof(l.clone(), poly("Sub", params.clone()))
             },
         );
         self.register_impl("__sub__", op_t, Const, Private);
@@ -694,7 +694,7 @@ impl Context {
             op_t,
             set! {
                 static_instance("R", Type),
-                subtype(l.clone(), poly("Mul", params.clone()))
+                subtypeof(l.clone(), poly("Mul", params.clone()))
             },
         );
         self.register_impl("__mul__", op_t, Const, Private);
@@ -703,27 +703,27 @@ impl Context {
             op_t,
             set! {
                 static_instance("R", Type),
-                subtype(l, poly("Mul", params.clone()))
+                subtypeof(l, poly("Mul", params.clone()))
             },
         );
         self.register_impl("__div__", op_t, Const, Private);
         let m = mono_q("M");
         let op_t = Type::func2(m.clone(), m.clone(), m.clone());
-        let op_t = quant(op_t, set! {subtype(m, poly("Mul", vec![]))});
+        let op_t = quant(op_t, set! {subtypeof(m, poly("Mul", vec![]))});
         // TODO: add bound: M == MulO
         self.register_impl("__pow__", op_t, Const, Private);
         let d = mono_q("D");
         let op_t = Type::func2(d.clone(), d.clone(), d.clone());
-        let op_t = quant(op_t, set! {subtype(d, poly("Div", vec![]))});
+        let op_t = quant(op_t, set! {subtypeof(d, poly("Div", vec![]))});
         self.register_impl("__mod__", op_t, Const, Private);
         let e = mono_q("E");
         let op_t = Type::func2(e.clone(), e.clone(), Bool);
-        let op_t = quant(op_t, set! {subtype(e, poly("Eq", vec![]))});
+        let op_t = quant(op_t, set! {subtypeof(e, poly("Eq", vec![]))});
         self.register_impl("__eq__", op_t.clone(), Const, Private);
         self.register_impl("__ne__", op_t, Const, Private);
         let o = mono_q("O");
         let op_t = Type::func2(o.clone(), o.clone(), Bool);
-        let op_t = quant(op_t, set! {subtype(o, mono("Ord"))});
+        let op_t = quant(op_t, set! {subtypeof(o, mono("Ord"))});
         self.register_impl("__lt__", op_t.clone(), Const, Private);
         self.register_impl("__le__", op_t.clone(), Const, Private);
         self.register_impl("__gt__", op_t.clone(), Const, Private);
@@ -734,18 +734,18 @@ impl Context {
         // TODO: Boolの+/-は警告を出したい
         let n = mono_q("N");
         let op_t = fn0_met(n.clone(), n.clone());
-        let op_t = quant(op_t, set! {subtype(n, mono("Num"))});
+        let op_t = quant(op_t, set! {subtypeof(n, mono("Num"))});
         self.register_decl("__pos__", op_t.clone(), Private);
         self.register_decl("__neg__", op_t, Private);
         let t = mono_q("T");
         let op_t = Type::func2(t.clone(), t.clone(), Type::range(t.clone()));
-        let op_t = quant(op_t, set! {subtype(t.clone(), mono("Ord"))});
+        let op_t = quant(op_t, set! {subtypeof(t.clone(), mono("Ord"))});
         self.register_decl("__rng__", op_t.clone(), Private);
         self.register_decl("__lorng__", op_t.clone(), Private);
         self.register_decl("__rorng__", op_t.clone(), Private);
         self.register_decl("__orng__", op_t, Private);
         let op_t = Type::func1(mono_q("T"), Type::mono_proj(mono_q("T"), "MutType!"));
-        let op_t = quant(op_t, set! {subtype(mono_q("T"), mono("Mutate"))});
+        let op_t = quant(op_t, set! {subtypeof(mono_q("T"), mono("Mutate"))});
         self.register_impl("__mutate__", op_t, Const, Private);
     }
 
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index b204821f..b1d8f3a1 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -51,7 +51,14 @@ impl ASTLowerer {
         found: &Type,
     ) -> LowerResult<()> {
         self.ctx.unify(expect, found, Some(loc), None).map_err(|_| {
-            LowerError::type_mismatch_error(loc, self.ctx.caused_by(), name, expect, found)
+            LowerError::type_mismatch_error(
+                line!() as usize,
+                loc,
+                self.ctx.caused_by(),
+                name,
+                expect,
+                found,
+            )
         })
     }
 
diff --git a/compiler/erg_compiler/ownercheck.rs b/compiler/erg_compiler/ownercheck.rs
index d331906e..b0c51a55 100644
--- a/compiler/erg_compiler/ownercheck.rs
+++ b/compiler/erg_compiler/ownercheck.rs
@@ -109,6 +109,7 @@ impl OwnershipChecker {
                     {
                         let moved_loc = *moved_loc;
                         self.errs.push(OwnershipError::move_error(
+                            line!() as usize,
                             local.inspect(),
                             local.loc(),
                             moved_loc,
diff --git a/compiler/erg_parser/ast.rs b/compiler/erg_parser/ast.rs
index 850b0960..6a4d55da 100644
--- a/compiler/erg_parser/ast.rs
+++ b/compiler/erg_parser/ast.rs
@@ -1261,9 +1261,8 @@ impl TypeSpec {
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub enum TypeBoundSpec {
-    Subtype { sub: VarName, sup: TypeSpec }, // e.g. S <: Show
+    Subtype { sub: VarName, sup: TypeSpec },  // e.g. S <: Show
     Instance { name: VarName, ty: TypeSpec }, // e.g. N: Nat
-                                             // Predicate, // TODO: e.g. N > 5
 }
 
 impl NestedDisplay for TypeBoundSpec {