diff --git a/Cargo.lock b/Cargo.lock
index ff99242a..b82dc801 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -15,7 +15,7 @@ dependencies = [
 
 [[package]]
 name = "erg"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 dependencies = [
  "erg_common",
  "erg_compiler",
@@ -25,14 +25,14 @@ dependencies = [
 
 [[package]]
 name = "erg_common"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 dependencies = [
  "atty",
 ]
 
 [[package]]
 name = "erg_compiler"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 dependencies = [
  "erg_common",
  "erg_parser",
@@ -41,14 +41,14 @@ dependencies = [
 
 [[package]]
 name = "erg_parser"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 dependencies = [
  "erg_common",
 ]
 
 [[package]]
 name = "erg_type"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 dependencies = [
  "erg_common",
  "erg_parser",
diff --git a/Cargo.toml b/Cargo.toml
index 05bcfb4a..ff0fd2ca 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 description = "The Erg programming language"
 authors = ["erg-lang team <moderation.erglang@gmail.com>"]
 license = "MIT OR Apache-2.0"
@@ -47,10 +47,10 @@ traditional_chinese = [
 pre-commit = []
 
 [dependencies]
-erg_common = { version = "0.5.6", path = "./compiler/erg_common" }
-erg_parser = { version = "0.5.6", path = "./compiler/erg_parser" }
-erg_compiler = { version = "0.5.6", path = "./compiler/erg_compiler" }
-erg_type = { version = "0.5.6", path = "./compiler/erg_type" }
+erg_common = { version = "0.5.7-nightly.1", path = "./compiler/erg_common" }
+erg_parser = { version = "0.5.7-nightly.1", path = "./compiler/erg_parser" }
+erg_compiler = { version = "0.5.7-nightly.1", path = "./compiler/erg_compiler" }
+erg_type = { version = "0.5.7-nightly.1", path = "./compiler/erg_type" }
 
 # [workspace]
 # member = ["cm", "dyne"]
diff --git a/compiler/erg_common/Cargo.toml b/compiler/erg_common/Cargo.toml
index 775cc64f..58df4a4a 100644
--- a/compiler/erg_common/Cargo.toml
+++ b/compiler/erg_common/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_common"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 description = "A common components library of Erg"
 authors = ["erg-lang team <moderation.erglang@gmail.com>"]
 license = "MIT OR Apache-2.0"
diff --git a/compiler/erg_common/config.rs b/compiler/erg_common/config.rs
index c0ca3fe4..a83a9869 100644
--- a/compiler/erg_common/config.rs
+++ b/compiler/erg_common/config.rs
@@ -93,7 +93,7 @@ impl Input {
                     let mut codes = vec![];
                     let mut lines = BufReader::new(file).lines().skip(ln_begin - 1);
                     for _ in ln_begin..=ln_end {
-                        codes.push(lines.next().unwrap().unwrap());
+                        codes.push(lines.next().unwrap_or_else(|| Ok("".to_string())).unwrap());
                     }
                     codes
                 }
diff --git a/compiler/erg_common/error.rs b/compiler/erg_common/error.rs
index 61fee15b..f2b5b200 100644
--- a/compiler/erg_common/error.rs
+++ b/compiler/erg_common/error.rs
@@ -114,6 +114,20 @@ use ErrorKind::*;
 
 impl_display_from_debug!(ErrorKind);
 
+impl ErrorKind {
+    pub fn is_warning(&self) -> bool {
+        (60..=100).contains(&(*self as u8)) || (180..=200).contains(&(*self as u8))
+    }
+
+    pub fn is_error(&self) -> bool {
+        (0..=59).contains(&(*self as u8)) || (100..=179).contains(&(*self as u8))
+    }
+
+    pub fn is_exception(&self) -> bool {
+        (200..=255).contains(&(*self as u8))
+    }
+}
+
 impl From<&str> for ErrorKind {
     fn from(s: &str) -> ErrorKind {
         match s {
@@ -467,10 +481,9 @@ pub trait ErrorDisplay {
     }
 
     fn format_header(&self) -> String {
-        let kind = self.core().kind as u8;
-        let (color, err_or_warn) = if (60..=100).contains(&kind) || (180..=200).contains(&kind) {
+        let (color, err_or_warn) = if self.core().kind.is_warning() {
             (YELLOW, "Warning")
-        } else if kind >= 200 {
+        } else if self.core().kind.is_exception() {
             ("", "Exception")
         } else {
             (RED, "Error")
diff --git a/compiler/erg_common/set.rs b/compiler/erg_common/set.rs
index 315b9571..55c3b61f 100644
--- a/compiler/erg_common/set.rs
+++ b/compiler/erg_common/set.rs
@@ -177,6 +177,10 @@ impl<T: Hash + Eq> Set<T> {
 }
 
 impl<T: Hash + Eq + Clone> Set<T> {
+    /// ```
+    /// # use erg_common::set;
+    /// assert_eq!(set!{1, 2, 3}.union(&set!{2, 3, 4}), set!{1, 2, 3, 4});
+    /// ```
     #[inline]
     pub fn union(&self, other: &Set<T>) -> Set<T> {
         let u = self.elems.union(&other.elems);
@@ -185,6 +189,10 @@ impl<T: Hash + Eq + Clone> Set<T> {
         }
     }
 
+    /// ```
+    /// # use erg_common::set;
+    /// assert_eq!(set!{1, 2, 3}.intersection(&set!{2, 3, 4}), set!{2, 3});
+    /// ```
     #[inline]
     pub fn intersection(&self, other: &Set<T>) -> Set<T> {
         let u = self.elems.intersection(&other.elems);
diff --git a/compiler/erg_compiler/Cargo.toml b/compiler/erg_compiler/Cargo.toml
index 59262159..5cf4c729 100644
--- a/compiler/erg_compiler/Cargo.toml
+++ b/compiler/erg_compiler/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_compiler"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 description = "Centimetre: the Erg compiler"
 authors = ["erg-lang team <moderation.erglang@gmail.com>"]
 license = "MIT OR Apache-2.0"
@@ -17,9 +17,9 @@ simplified_chinese = [ "erg_common/simplified_chinese", "erg_parser/simplified_c
 traditional_chinese = [ "erg_common/traditional_chinese", "erg_parser/traditional_chinese", "erg_type/traditional_chinese" ]
 
 [dependencies]
-erg_common = { version = "0.5.6", path = "../erg_common" }
-erg_parser = { version = "0.5.6", path = "../erg_parser" }
-erg_type = { version = "0.5.6", path = "../erg_type" }
+erg_common = { version = "0.5.7-nightly.1", path = "../erg_common" }
+erg_parser = { version = "0.5.7-nightly.1", path = "../erg_parser" }
+erg_type = { version = "0.5.7-nightly.1", path = "../erg_type" }
 
 [lib]
 path = "lib.rs"
diff --git a/compiler/erg_compiler/codegen.rs b/compiler/erg_compiler/codegen.rs
index 0c96d110..63e6c064 100644
--- a/compiler/erg_compiler/codegen.rs
+++ b/compiler/erg_compiler/codegen.rs
@@ -207,7 +207,7 @@ fn is_fake_method(class: &str, name: &str) -> bool {
     matches!(
         (class, name),
         (
-            "Complex" | "Float" | "Ratio" | "Int" | "Nat" | "Bool",
+            _, // "Complex" | "Float" | "Ratio" | "Int" | "Nat" | "Bool",
             "abs"
         ) | (_, "iter")
             | (_, "map")
@@ -1205,6 +1205,17 @@ impl CodeGenerator {
         }
     }
 
+    fn emit_del_instr(&mut self, mut args: Args) {
+        let ident = enum_unwrap!(args.remove_left_or_key("obj").unwrap(), Expr::Accessor:(Accessor::Ident:(_)));
+        log!(info "entered {} ({ident})", fn_name!());
+        let escaped = escape_name(ident);
+        let name = self
+            .local_search(&escaped, Name)
+            .unwrap_or_else(|| self.register_name(escaped));
+        self.write_instr(DELETE_NAME);
+        self.write_arg(name.idx as u8);
+    }
+
     fn emit_discard_instr(&mut self, mut args: Args) {
         log!(info "entered {}", fn_name!());
         while let Some(arg) = args.try_remove(0) {
@@ -1448,6 +1459,7 @@ impl CodeGenerator {
         log!(info "entered {}", fn_name!());
         match &local.inspect()[..] {
             "assert" => self.emit_assert_instr(args),
+            "Del" => self.emit_del_instr(args),
             "discard" => self.emit_discard_instr(args),
             "for" | "for!" => self.emit_for_instr(args),
             "if" | "if!" => self.emit_if_instr(args),
diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index 6e4f86f2..705ee5b3 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -278,6 +278,11 @@ impl Context {
         if let Some((_, ty_ctx)) = self.get_nominal_type_ctx(rhs) {
             for rhs_sup in ty_ctx.super_classes.iter() {
                 let rhs_sup = if rhs_sup.has_qvar() {
+                    let rhs = match rhs {
+                        Type::Ref(t) => t,
+                        Type::RefMut { before, .. } => before,
+                        other => other,
+                    };
                     let subst_ctx = SubstContext::new(rhs, ty_ctx);
                     subst_ctx
                         .substitute(rhs_sup.clone(), self, Location::Unknown)
@@ -311,6 +316,11 @@ impl Context {
         if let Some((_, rhs_ctx)) = self.get_nominal_type_ctx(rhs) {
             for rhs_sup in rhs_ctx.super_traits.iter() {
                 let rhs_sup = if rhs_sup.has_qvar() {
+                    let rhs = match rhs {
+                        Type::Ref(t) => t,
+                        Type::RefMut { before, .. } => before,
+                        other => other,
+                    };
                     let subst_ctx = SubstContext::new(rhs, rhs_ctx);
                     subst_ctx
                         .substitute(rhs_sup.clone(), self, Location::Unknown)
@@ -638,8 +648,26 @@ impl Context {
             (l, MonoQVar(name)) | (l, PolyQVar { name, .. }) => {
                 panic!("internal error: not instantiated type variable: '{name}, l: {l}")
             }
-            (MonoProj { .. }, _) => todo!(),
-            (_, MonoProj { .. }) => todo!(),
+            (MonoProj { .. }, _) => {
+                if let Some(cands) = self.get_candidates(lhs) {
+                    for cand in cands.into_iter() {
+                        if self.supertype_of(&cand, rhs) {
+                            return true;
+                        }
+                    }
+                }
+                false
+            }
+            (_, MonoProj { .. }) => {
+                if let Some(cands) = self.get_candidates(rhs) {
+                    for cand in cands.into_iter() {
+                        if self.supertype_of(lhs, &cand) {
+                            return true;
+                        }
+                    }
+                }
+                false
+            }
             (_l, _r) => false,
         }
     }
@@ -810,13 +838,19 @@ impl Context {
 
     /// returns union of two types (A or B)
     pub(crate) fn union(&self, lhs: &Type, rhs: &Type) -> Type {
-        match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
-            (true, true) => return lhs.clone(),  // lhs = rhs
-            (true, false) => return lhs.clone(), // lhs :> rhs
-            (false, true) => return rhs.clone(),
-            (false, false) => {}
+        // ?T or ?U will not be unified
+        if lhs.has_no_unbound_var() && rhs.has_no_unbound_var() {
+            match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
+                (true, true) => return lhs.clone(),  // lhs = rhs
+                (true, false) => return lhs.clone(), // lhs :> rhs
+                (false, true) => return rhs.clone(),
+                (false, false) => {}
+            }
         }
         match (lhs, rhs) {
+            (FreeVar(lfv), FreeVar(rfv)) if lfv.is_linked() && rfv.is_linked() => {
+                self.union(&lfv.crack(), &rfv.crack())
+            }
             (Refinement(l), Refinement(r)) => Type::Refinement(self.union_refinement(l, r)),
             (t, Type::Never) | (Type::Never, t) => t.clone(),
             (t, Refinement(r)) | (Refinement(r), t) => {
@@ -842,16 +876,19 @@ impl Context {
 
     /// returns intersection of two types (A and B)
     pub(crate) fn intersection(&self, lhs: &Type, rhs: &Type) -> Type {
-        match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
-            (true, true) => return lhs.clone(),  // lhs = rhs
-            (true, false) => return rhs.clone(), // lhs :> rhs
-            (false, true) => return lhs.clone(),
-            (false, false) => {}
+        // ?T and ?U will not be unified
+        if !lhs.is_unbound_var() && !rhs.is_unbound_var() {
+            match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
+                (true, true) => return lhs.clone(),  // lhs = rhs
+                (true, false) => return rhs.clone(), // lhs :> rhs
+                (false, true) => return lhs.clone(),
+                (false, false) => {}
+            }
         }
         match (lhs, rhs) {
-            /*(Type::FreeVar(_), _) | (_, Type::FreeVar(_)) => {
-                todo!()
-            }*/
+            (FreeVar(lfv), FreeVar(rfv)) if lfv.is_linked() && rfv.is_linked() => {
+                self.intersection(&lfv.crack(), &rfv.crack())
+            }
             // {.i = Int} and {.s = Str} == {.i = Int; .s = Str}
             (Type::Record(l), Type::Record(r)) => Type::Record(l.clone().concat(r.clone())),
             (l, r) if self.is_trait(l) && self.is_trait(r) => and(l.clone(), r.clone()),
@@ -1008,7 +1045,7 @@ impl Context {
         }
     }
 
-    pub(crate) fn max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
+    pub(crate) fn _max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
         // 同じならどちらを返しても良い
         match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
             (true, true) | (true, false) => Some(lhs),
diff --git a/compiler/erg_compiler/context/eval.rs b/compiler/erg_compiler/context/eval.rs
index 5ca813ad..cae8d3e7 100644
--- a/compiler/erg_compiler/context/eval.rs
+++ b/compiler/erg_compiler/context/eval.rs
@@ -2,6 +2,7 @@ use std::fmt;
 use std::mem;
 
 use erg_common::dict::Dict;
+use erg_common::enum_unwrap;
 use erg_common::error::Location;
 use erg_common::set::Set;
 use erg_common::shared::Shared;
@@ -15,19 +16,18 @@ use erg_parser::ast::*;
 use erg_parser::token::{Token, TokenKind};
 
 use erg_type::constructors::{
-    and, builtin_mono, builtin_poly, mono_proj, not, or, poly, ref_, ref_mut, refinement, subr_t,
-    v_enum,
+    builtin_mono, builtin_poly, mono_proj, not, poly, ref_, ref_mut, refinement, subr_t, v_enum,
 };
 use erg_type::typaram::{OpKind, TyParam};
 use erg_type::value::ValueObj;
-use erg_type::{
-    ConstSubr, HasType, ParamTy, Predicate, SubrKind, TyBound, Type, UserConstSubr, ValueArgs,
-};
+use erg_type::{ConstSubr, HasType, Predicate, SubrKind, TyBound, Type, UserConstSubr, ValueArgs};
 
 use crate::context::instantiate::TyVarContext;
 use crate::context::{ClassDefType, Context, ContextKind, RegistrationMode};
 use crate::error::{EvalError, EvalErrors, EvalResult, SingleEvalResult, TyCheckResult};
 
+use super::Variance;
+
 #[inline]
 pub fn type_from_token_kind(kind: TokenKind) -> Type {
     use TokenKind::*;
@@ -72,6 +72,34 @@ fn try_get_op_kind_from_token(kind: TokenKind) -> EvalResult<OpKind> {
     }
 }
 
+fn op_to_name(op: OpKind) -> &'static str {
+    match op {
+        OpKind::Add => "__add__",
+        OpKind::Sub => "__sub__",
+        OpKind::Mul => "__mul__",
+        OpKind::Div => "__div__",
+        OpKind::Mod => "__mod__",
+        OpKind::Pow => "__pow__",
+        OpKind::Pos => "__pos__",
+        OpKind::Neg => "__neg__",
+        OpKind::Eq => "__eq__",
+        OpKind::Ne => "__ne__",
+        OpKind::Lt => "__lt__",
+        OpKind::Le => "__le__",
+        OpKind::Gt => "__gt__",
+        OpKind::Ge => "__ge__",
+        OpKind::And => "__and__",
+        OpKind::Or => "__or__",
+        OpKind::Invert => "__invert__",
+        OpKind::BitAnd => "__bitand__",
+        OpKind::BitOr => "__bitor__",
+        OpKind::BitXor => "__bitxor__",
+        OpKind::Shl => "__shl__",
+        OpKind::Shr => "__shr__",
+        OpKind::Mutate => "__mutate__",
+    }
+}
+
 #[inline]
 pub(crate) fn eval_lit(lit: &Literal) -> ValueObj {
     let t = type_from_token_kind(lit.token.kind);
@@ -104,7 +132,13 @@ impl SubstContext {
                 .as_ref()
                 .map_or_else(|| Str::ever("_"), |n| n.inspect().clone())
         });
-        assert_eq!(param_names.len(), substituted.typarams().len());
+        if param_names.len() != substituted.typarams().len() {
+            let param_names = param_names.collect::<Vec<_>>();
+            panic!(
+                "{param_names:?} != {}",
+                erg_common::fmt_vec(&substituted.typarams())
+            );
+        }
         // REVIEW: 順番は保証されるか? 引数がunnamed_paramsに入る可能性は?
         SubstContext {
             bounds,
@@ -464,36 +498,20 @@ impl Context {
         let tv_ctx = TyVarContext::new(self.level, bounds, self);
         let mut non_default_params = Vec::with_capacity(lambda.sig.params.non_defaults.len());
         for sig in lambda.sig.params.non_defaults.iter() {
-            let t =
-                self.instantiate_param_sig_t(sig, None, Some(&tv_ctx), RegistrationMode::Normal)?;
-            let pt = if let Some(name) = sig.inspect() {
-                ParamTy::kw(name.clone(), t)
-            } else {
-                ParamTy::anonymous(t)
-            };
+            let pt =
+                self.instantiate_param_ty(sig, None, Some(&tv_ctx), RegistrationMode::Normal)?;
             non_default_params.push(pt);
         }
         let var_params = if let Some(p) = lambda.sig.params.var_args.as_ref() {
-            let t =
-                self.instantiate_param_sig_t(p, None, Some(&tv_ctx), RegistrationMode::Normal)?;
-            let pt = if let Some(name) = p.inspect() {
-                ParamTy::kw(name.clone(), t)
-            } else {
-                ParamTy::anonymous(t)
-            };
+            let pt = self.instantiate_param_ty(p, None, Some(&tv_ctx), RegistrationMode::Normal)?;
             Some(pt)
         } else {
             None
         };
         let mut default_params = Vec::with_capacity(lambda.sig.params.defaults.len());
         for sig in lambda.sig.params.defaults.iter() {
-            let t =
-                self.instantiate_param_sig_t(sig, None, Some(&tv_ctx), RegistrationMode::Normal)?;
-            let pt = if let Some(name) = sig.inspect() {
-                ParamTy::kw(name.clone(), t)
-            } else {
-                ParamTy::anonymous(t)
-            };
+            let pt =
+                self.instantiate_param_ty(sig, None, Some(&tv_ctx), RegistrationMode::Normal)?;
             default_params.push(pt);
         }
         // HACK: should avoid cloning
@@ -661,28 +679,10 @@ impl Context {
             (TyParam::Value(lhs), TyParam::Value(rhs)) => self
                 .eval_bin(op, lhs.clone(), rhs.clone())
                 .map(TyParam::value),
-            (TyParam::FreeVar(fv), r) => {
-                if fv.is_linked() {
-                    self.eval_bin_tp(op, &*fv.crack(), r)
-                } else {
-                    Err(EvalErrors::from(EvalError::unreachable(
-                        self.cfg.input.clone(),
-                        fn_name!(),
-                        line!(),
-                    )))
-                }
-            }
-            (l, TyParam::FreeVar(fv)) => {
-                if fv.is_linked() {
-                    self.eval_bin_tp(op, l, &*fv.crack())
-                } else {
-                    Err(EvalErrors::from(EvalError::unreachable(
-                        self.cfg.input.clone(),
-                        fn_name!(),
-                        line!(),
-                    )))
-                }
-            }
+            (TyParam::FreeVar(fv), r) if fv.is_linked() => self.eval_bin_tp(op, &*fv.crack(), r),
+            (TyParam::FreeVar(_), _) => Ok(TyParam::bin(op, lhs.clone(), rhs.clone())),
+            (l, TyParam::FreeVar(fv)) if fv.is_linked() => self.eval_bin_tp(op, l, &*fv.crack()),
+            (_, TyParam::FreeVar(_)) => Ok(TyParam::bin(op, lhs.clone(), rhs.clone())),
             (e @ TyParam::Erased(_), _) | (_, e @ TyParam::Erased(_)) => Ok(e.clone()),
             (l, r) => todo!("{l} {op} {r}"),
         }
@@ -845,15 +845,42 @@ impl Context {
                         }
                     }
                 }
-                let proj = mono_proj(*lhs, rhs);
-                Err(EvalErrors::from(EvalError::no_candidate_error(
-                    self.cfg.input.clone(),
-                    line!() as usize,
-                    &proj,
-                    t_loc,
-                    self.caused_by(),
-                    self.get_no_candidate_hint(&proj),
-                )))
+                if lhs.is_unbound_var() {
+                    let (sub, sup) = enum_unwrap!(lhs.as_ref(), Type::FreeVar)
+                        .get_bound_types()
+                        .unwrap();
+                    if self.is_trait(&sup) && !self.trait_impl_exists(&sub, &sup) {
+                        return Err(EvalErrors::from(EvalError::no_trait_impl_error(
+                            self.cfg.input.clone(),
+                            line!() as usize,
+                            &sub,
+                            &sup,
+                            t_loc,
+                            self.caused_by(),
+                            None,
+                        )));
+                    }
+                }
+                // if the target can't be found in the supertype, the type will be dereferenced.
+                // In many cases, it is still better to determine the type variable than if the target is not found.
+                let coerced = self.deref_tyvar(*lhs.clone(), Variance::Covariant, t_loc)?;
+                if lhs.as_ref() != &coerced {
+                    let proj = mono_proj(coerced, rhs);
+                    self.eval_t_params(proj, level, t_loc).map(|t| {
+                        self.coerce(&lhs);
+                        t
+                    })
+                } else {
+                    let proj = mono_proj(*lhs, rhs);
+                    Err(EvalErrors::from(EvalError::no_candidate_error(
+                        self.cfg.input.clone(),
+                        line!() as usize,
+                        &proj,
+                        t_loc,
+                        self.caused_by(),
+                        self.get_no_candidate_hint(&proj),
+                    )))
+                }
             }
             Type::Ref(l) => Ok(ref_(self.eval_t_params(*l, level, t_loc)?)),
             Type::RefMut { before, after } => {
@@ -884,12 +911,12 @@ impl Context {
             Type::And(l, r) => {
                 let l = self.eval_t_params(*l, level, t_loc)?;
                 let r = self.eval_t_params(*r, level, t_loc)?;
-                Ok(and(l, r))
+                Ok(self.intersection(&l, &r))
             }
             Type::Or(l, r) => {
                 let l = self.eval_t_params(*l, level, t_loc)?;
                 let r = self.eval_t_params(*r, level, t_loc)?;
-                Ok(or(l, r))
+                Ok(self.union(&l, &r))
             }
             Type::Not(l, r) => {
                 let l = self.eval_t_params(*l, level, t_loc)?;
@@ -971,6 +998,10 @@ impl Context {
                 OpKind::Mutate => Ok(self.get_tp_t(&val)?.mutate()),
                 _ => todo!(),
             },
+            TyParam::BinOp { op, lhs, rhs } => {
+                let op_name = op_to_name(op);
+                todo!("get type: {op_name}({lhs}, {rhs})")
+            }
             other => todo!("{other}"),
         }
     }
diff --git a/compiler/erg_compiler/context/initialize/mod.rs b/compiler/erg_compiler/context/initialize/mod.rs
index f8515f25..e17e4f11 100644
--- a/compiler/erg_compiler/context/initialize/mod.rs
+++ b/compiler/erg_compiler/context/initialize/mod.rs
@@ -23,7 +23,9 @@ use erg_parser::ast::VarName;
 
 use crate::context::initialize::const_func::*;
 use crate::context::instantiate::{ConstTemplate, TyVarContext};
-use crate::context::{ClassDefType, Context, ContextKind, DefaultInfo, ParamSpec, TraitInstance};
+use crate::context::{
+    ClassDefType, Context, ContextKind, DefaultInfo, MethodType, ParamSpec, TraitInstance,
+};
 use crate::mod_cache::SharedModuleCache;
 use crate::varinfo::{Mutability, VarInfo, VarKind};
 use DefaultInfo::*;
@@ -77,6 +79,7 @@ impl Context {
         }
     }
 
+    /// FIXME: トレイトの汎化型を指定するのにも使っているので、この名前は適当でない
     pub(crate) fn register_superclass(&mut self, sup: Type, sup_ctx: &Context) {
         self.super_classes.push(sup);
         self.super_classes.extend(sup_ctx.super_classes.clone());
@@ -114,22 +117,32 @@ impl Context {
                 .insert(name.clone(), ValueObj::builtin_t(t.clone()));
             for impl_trait in ctx.super_traits.iter() {
                 if let Some(impls) = self.trait_impls.get_mut(&impl_trait.name()) {
-                    impls.push(TraitInstance::new(t.clone(), impl_trait.clone()));
+                    impls.insert(TraitInstance::new(t.clone(), impl_trait.clone()));
                 } else {
                     self.trait_impls.insert(
                         impl_trait.name(),
-                        vec![TraitInstance::new(t.clone(), impl_trait.clone())],
+                        set![TraitInstance::new(t.clone(), impl_trait.clone())],
                     );
                 }
             }
-            if ctx.kind == ContextKind::Trait {
-                for method in ctx.decls.keys() {
-                    if let Some(traits) = self.method_traits.get_mut(method.inspect()) {
-                        traits.push(t.clone());
-                    } else {
-                        self.method_traits
-                            .insert(method.inspect().clone(), vec![t.clone()]);
-                    }
+            for (trait_method, vi) in ctx.decls.iter() {
+                if let Some(types) = self.method_to_traits.get_mut(trait_method.inspect()) {
+                    types.push(MethodType::new(t.clone(), vi.t.clone()));
+                } else {
+                    self.method_to_traits.insert(
+                        trait_method.inspect().clone(),
+                        vec![MethodType::new(t.clone(), vi.t.clone())],
+                    );
+                }
+            }
+            for (class_method, vi) in ctx.locals.iter() {
+                if let Some(types) = self.method_to_classes.get_mut(class_method.inspect()) {
+                    types.push(MethodType::new(t.clone(), vi.t.clone()));
+                } else {
+                    self.method_to_classes.insert(
+                        class_method.inspect().clone(),
+                        vec![MethodType::new(t.clone(), vi.t.clone())],
+                    );
                 }
             }
             self.mono_types.insert(name, (t, ctx));
@@ -155,22 +168,32 @@ impl Context {
                 .insert(name.clone(), ValueObj::builtin_t(t.clone()));
             for impl_trait in ctx.super_traits.iter() {
                 if let Some(impls) = self.trait_impls.get_mut(&impl_trait.name()) {
-                    impls.push(TraitInstance::new(t.clone(), impl_trait.clone()));
+                    impls.insert(TraitInstance::new(t.clone(), impl_trait.clone()));
                 } else {
                     self.trait_impls.insert(
                         impl_trait.name(),
-                        vec![TraitInstance::new(t.clone(), impl_trait.clone())],
+                        set![TraitInstance::new(t.clone(), impl_trait.clone())],
                     );
                 }
             }
-            if ctx.kind == ContextKind::Trait {
-                for method in ctx.decls.keys() {
-                    if let Some(traits) = self.method_traits.get_mut(method.inspect()) {
-                        traits.push(t.clone());
-                    } else {
-                        self.method_traits
-                            .insert(method.inspect().clone(), vec![t.clone()]);
-                    }
+            for (trait_method, vi) in ctx.decls.iter() {
+                if let Some(traits) = self.method_to_traits.get_mut(trait_method.inspect()) {
+                    traits.push(MethodType::new(t.clone(), vi.t.clone()));
+                } else {
+                    self.method_to_traits.insert(
+                        trait_method.inspect().clone(),
+                        vec![MethodType::new(t.clone(), vi.t.clone())],
+                    );
+                }
+            }
+            for (class_method, vi) in ctx.locals.iter() {
+                if let Some(types) = self.method_to_classes.get_mut(class_method.inspect()) {
+                    types.push(MethodType::new(t.clone(), vi.t.clone()));
+                } else {
+                    self.method_to_classes.insert(
+                        class_method.inspect().clone(),
+                        vec![MethodType::new(t.clone(), vi.t.clone())],
+                    );
                 }
             }
             self.poly_types.insert(name, (t, ctx));
@@ -209,7 +232,7 @@ impl Context {
         let named = Self::builtin_mono_trait("Named", 2);
         let mut mutable = Self::builtin_mono_trait("Mutable", 2);
         let proj = mono_proj(mono_q("Self"), "ImmutType");
-        let f_t = func(vec![param_t("old", proj.clone())], None, vec![], proj);
+        let f_t = func(vec![kw("old", proj.clone())], None, vec![], proj);
         let t = pr1_met(ref_mut(mono_q("Self"), None), f_t, NoneType);
         let t = quant(
             t,
@@ -229,7 +252,7 @@ impl Context {
             ref_mut(mono_q("Self"), None),
             vec![],
             None,
-            vec![param_t("n", Int)],
+            vec![kw("n", Int)],
             Str,
         );
         let t_read = quant(
@@ -540,7 +563,6 @@ impl Context {
         ratio.register_trait(Ratio, builtin_mono("Show"), ratio_show);
         let mut int = Self::builtin_mono_class("Int", 2);
         int.register_superclass(Float, &float); // TODO: Float -> Ratio
-        int.register_superclass(Obj, &obj);
         int.register_marker_trait(builtin_mono("Num"));
         int.register_marker_trait(builtin_mono("Ord"));
         int.register_marker_trait(builtin_poly("Eq", vec![ty_tp(Int)]));
@@ -588,15 +610,13 @@ impl Context {
         int.register_builtin_impl("Imag", Int, Const, Public);
         let mut nat = Self::builtin_mono_class("Nat", 10);
         nat.register_superclass(Int, &int);
-        nat.register_superclass(Float, &float); // TODO: Float -> Ratio
-        nat.register_superclass(Obj, &obj);
         // class("Rational"),
         // class("Integral"),
         nat.register_builtin_impl(
             "times!",
             pr_met(
                 Nat,
-                vec![param_t("p", nd_proc(vec![], None, NoneType))],
+                vec![kw("p", nd_proc(vec![], None, NoneType))],
                 None,
                 vec![],
                 NoneType,
@@ -638,9 +658,6 @@ impl Context {
         nat.register_builtin_impl("Imag", Nat, Const, Public);
         let mut bool_ = Self::builtin_mono_class("Bool", 10);
         bool_.register_superclass(Nat, &nat);
-        bool_.register_superclass(Int, &int);
-        bool_.register_superclass(Float, &float); // TODO: Float -> Ratio
-        bool_.register_superclass(Obj, &obj);
         // class("Rational"),
         // class("Integral"),
         // TODO: And, Or trait
@@ -671,6 +688,9 @@ impl Context {
         bool_mutizable
             .register_builtin_const("MutType!", ValueObj::builtin_t(builtin_mono("Bool!")));
         bool_.register_trait(Bool, builtin_mono("Mutizable"), bool_mutizable);
+        let mut bool_show = Self::builtin_methods("Show", 1);
+        bool_show.register_builtin_impl("to_str", fn0_met(Bool, Str), Immutable, Public);
+        bool_.register_trait(Bool, builtin_mono("Show"), bool_show);
         let mut str_ = Self::builtin_mono_class("Str", 10);
         str_.register_superclass(Obj, &obj);
         str_.register_marker_trait(builtin_mono("Ord"));
@@ -679,7 +699,7 @@ impl Context {
             "replace",
             fn_met(
                 Str,
-                vec![param_t("pat", Str), param_t("into", Str)],
+                vec![kw("pat", Str), kw("into", Str)],
                 None,
                 vec![],
                 Str,
@@ -693,7 +713,7 @@ impl Context {
                 Str,
                 vec![],
                 None,
-                vec![param_t("encoding", Str), param_t("errors", Str)],
+                vec![kw("encoding", Str), kw("errors", Str)],
                 builtin_mono("Bytes"),
             ),
             Immutable,
@@ -717,6 +737,9 @@ impl Context {
         let mut str_mutizable = Self::builtin_methods("Mutizable", 2);
         str_mutizable.register_builtin_const("MutType!", ValueObj::builtin_t(builtin_mono("Str!")));
         str_.register_trait(Str, builtin_mono("Mutizable"), str_mutizable);
+        let mut str_show = Self::builtin_methods("Show", 1);
+        str_show.register_builtin_impl("to_str", fn0_met(Str, Str), Immutable, Public);
+        str_.register_trait(Str, builtin_mono("Show"), str_show);
         let mut type_ = Self::builtin_mono_class("Type", 2);
         type_.register_superclass(Obj, &obj);
         type_.register_builtin_impl("mro", array(Type, TyParam::erased(Nat)), Immutable, Public);
@@ -726,7 +749,6 @@ impl Context {
         type_.register_trait(Type, builtin_poly("Eq", vec![ty_tp(Type)]), type_eq);
         let mut class_type = Self::builtin_mono_class("ClassType", 2);
         class_type.register_superclass(Type, &type_);
-        class_type.register_superclass(Obj, &obj);
         class_type.register_marker_trait(builtin_mono("Named"));
         let mut class_eq = Self::builtin_methods("Eq", 2);
         class_eq.register_builtin_impl("__eq__", fn1_met(Class, Class, Bool), Const, Public);
@@ -759,7 +781,7 @@ impl Context {
         let array_t = array(mono_q("T"), n.clone());
         let t = fn_met(
             array_t.clone(),
-            vec![param_t("rhs", array(mono_q("T"), m.clone()))],
+            vec![kw("rhs", array(mono_q("T"), m.clone()))],
             None,
             vec![],
             array(mono_q("T"), n + m),
@@ -784,14 +806,22 @@ impl Context {
         );
         array_.register_trait(
             array_t.clone(),
-            builtin_poly("Eq", vec![ty_tp(array_t)]),
+            builtin_poly("Eq", vec![ty_tp(array_t.clone())]),
             array_eq,
         );
         array_.register_marker_trait(builtin_mono("Mutizable"));
         array_.register_marker_trait(builtin_poly("Seq", vec![ty_tp(mono_q("T"))]));
+        let mut array_show = Self::builtin_methods("Show", 1);
+        array_show.register_builtin_impl(
+            "to_str",
+            fn0_met(array_t.clone(), Str),
+            Immutable,
+            Public,
+        );
+        array_.register_trait(array_t, builtin_mono("Show"), array_show);
         let mut bytes = Self::builtin_mono_class("Bytes", 2);
         bytes.register_superclass(Obj, &obj);
-        // TODO: make Tuple6, Tuple7, ... etc.
+        // FIXME: replace to Tuple Ts (e.g. Tuple [Int, Str])
         let mut tuple_ = Self::builtin_mono_class("Tuple", 2);
         tuple_.register_superclass(Obj, &obj);
         let mut tuple_eq = Self::builtin_methods("Eq", 2);
@@ -808,7 +838,6 @@ impl Context {
         );
         let mut tuple1 = Self::builtin_poly_class("Tuple1", vec![PS::t_nd("A")], 2);
         tuple1.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple1.register_superclass(Obj, &obj);
         let mut tuple1_eq = Self::builtin_methods("Eq", 2);
         tuple1_eq.register_builtin_impl(
             "__eq__",
@@ -830,7 +859,6 @@ impl Context {
         );
         let mut tuple2 = Self::builtin_poly_class("Tuple2", vec![PS::t_nd("A"), PS::t_nd("B")], 2);
         tuple2.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple2.register_superclass(Obj, &obj);
         let mut tuple2_eq = Self::builtin_methods("Eq", 2);
         tuple2_eq.register_builtin_impl(
             "__eq__",
@@ -859,7 +887,6 @@ impl Context {
             2,
         );
         tuple3.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple3.register_superclass(Obj, &obj);
         let mut tuple3_eq = Self::builtin_methods("Eq", 2);
         tuple3_eq.register_builtin_impl(
             "__eq__",
@@ -897,7 +924,6 @@ impl Context {
             2,
         );
         tuple4.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple4.register_superclass(Obj, &obj);
         let mut tuple4_eq = Self::builtin_methods("Eq", 2);
         tuple4_eq.register_builtin_impl(
             "__eq__",
@@ -961,7 +987,6 @@ impl Context {
             2,
         );
         tuple5.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple5.register_superclass(Obj, &obj);
         let mut tuple5_eq = Self::builtin_methods("Eq", 2);
         tuple5_eq.register_builtin_impl(
             "__eq__",
@@ -1030,7 +1055,6 @@ impl Context {
             2,
         );
         tuple6.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple6.register_superclass(Obj, &obj);
         let mut tuple6_eq = Self::builtin_methods("Eq", 2);
         tuple6_eq.register_builtin_impl(
             "__eq__",
@@ -1104,7 +1128,6 @@ impl Context {
             2,
         );
         tuple7.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple7.register_superclass(Obj, &obj);
         let mut tuple7_eq = Self::builtin_methods("Eq", 2);
         tuple7_eq.register_builtin_impl(
             "__eq__",
@@ -1183,7 +1206,6 @@ impl Context {
             2,
         );
         tuple8.register_superclass(builtin_mono("Tuple"), &tuple_);
-        tuple8.register_superclass(Obj, &obj);
         let mut tuple8_eq = Self::builtin_methods("Eq", 2);
         tuple8_eq.register_builtin_impl(
             "__eq__",
@@ -1256,13 +1278,11 @@ impl Context {
         let mut record_type = Self::builtin_mono_class("RecordType", 2);
         record_type.register_superclass(builtin_mono("Record"), &record);
         record_type.register_superclass(builtin_mono("Type"), &type_);
-        record_type.register_superclass(Obj, &obj);
         let mut float_mut = Self::builtin_mono_class("Float!", 2);
         float_mut.register_superclass(Float, &float);
-        float_mut.register_superclass(Obj, &obj);
         let mut float_mut_mutable = Self::builtin_methods("Mutable", 2);
         float_mut_mutable.register_builtin_const("ImmutType", ValueObj::builtin_t(Float));
-        let f_t = param_t("f", func(vec![param_t("old", Float)], None, vec![], Float));
+        let f_t = kw("f", func(vec![kw("old", Float)], None, vec![], Float));
         let t = pr_met(
             ref_mut(builtin_mono("Float!"), None),
             vec![f_t],
@@ -1278,13 +1298,12 @@ impl Context {
         );
         let mut ratio_mut = Self::builtin_mono_class("Ratio!", 2);
         ratio_mut.register_superclass(Ratio, &ratio);
-        ratio_mut.register_superclass(Obj, &obj);
         let mut ratio_mut_mutable = Self::builtin_methods("Mutable", 2);
         ratio_mut_mutable.register_builtin_const("ImmutType", ValueObj::builtin_t(Ratio));
-        let f_t = param_t(
+        let f_t = kw(
             "f",
             func(
-                vec![param_t("old", builtin_mono("Ratio"))],
+                vec![kw("old", builtin_mono("Ratio"))],
                 None,
                 vec![],
                 builtin_mono("Ratio"),
@@ -1306,10 +1325,9 @@ impl Context {
         let mut int_mut = Self::builtin_mono_class("Int!", 2);
         int_mut.register_superclass(Int, &int);
         int_mut.register_superclass(builtin_mono("Float!"), &float_mut);
-        int_mut.register_superclass(Obj, &obj);
         let mut int_mut_mutable = Self::builtin_methods("Mutable", 2);
         int_mut_mutable.register_builtin_const("ImmutType", ValueObj::builtin_t(Int));
-        let f_t = param_t("f", func(vec![param_t("old", Int)], None, vec![], Int));
+        let f_t = kw("f", func(vec![kw("old", Int)], None, vec![], Int));
         let t = pr_met(
             ref_mut(builtin_mono("Int!"), None),
             vec![f_t],
@@ -1326,11 +1344,9 @@ impl Context {
         let mut nat_mut = Self::builtin_mono_class("Nat!", 2);
         nat_mut.register_superclass(Nat, &nat);
         nat_mut.register_superclass(builtin_mono("Int!"), &int_mut);
-        nat_mut.register_superclass(builtin_mono("Float!"), &float_mut);
-        nat_mut.register_superclass(Obj, &obj);
         let mut nat_mut_mutable = Self::builtin_methods("Mutable", 2);
         nat_mut_mutable.register_builtin_const("ImmutType", ValueObj::builtin_t(Nat));
-        let f_t = param_t("f", func(vec![param_t("old", Nat)], None, vec![], Nat));
+        let f_t = kw("f", func(vec![kw("old", Nat)], None, vec![], Nat));
         let t = pr_met(
             ref_mut(builtin_mono("Nat!"), None),
             vec![f_t],
@@ -1347,12 +1363,9 @@ impl Context {
         let mut bool_mut = Self::builtin_mono_class("Bool!", 2);
         bool_mut.register_superclass(Bool, &bool_);
         bool_mut.register_superclass(builtin_mono("Nat!"), &nat_mut);
-        bool_mut.register_superclass(builtin_mono("Int!"), &int_mut);
-        bool_mut.register_superclass(builtin_mono("Float!"), &float_mut);
-        bool_mut.register_superclass(Obj, &obj);
         let mut bool_mut_mutable = Self::builtin_methods("Mutable", 2);
         bool_mut_mutable.register_builtin_const("ImmutType", ValueObj::builtin_t(Bool));
-        let f_t = param_t("f", func(vec![param_t("old", Bool)], None, vec![], Bool));
+        let f_t = kw("f", func(vec![kw("old", Bool)], None, vec![], Bool));
         let t = pr_met(
             ref_mut(builtin_mono("Bool!"), None),
             vec![f_t],
@@ -1368,10 +1381,9 @@ impl Context {
         );
         let mut str_mut = Self::builtin_mono_class("Str!", 2);
         str_mut.register_superclass(Str, &str_);
-        str_mut.register_superclass(Obj, &obj);
         let mut str_mut_mutable = Self::builtin_methods("Mutable", 2);
         str_mut_mutable.register_builtin_const("ImmutType", ValueObj::builtin_t(Str));
-        let f_t = param_t("f", func(vec![param_t("old", Str)], None, vec![], Str));
+        let f_t = kw("f", func(vec![kw("old", Str)], None, vec![], Str));
         let t = pr_met(
             ref_mut(builtin_mono("Str!"), None),
             vec![f_t],
@@ -1393,7 +1405,7 @@ impl Context {
                 ref_mut(builtin_mono("File!"), None),
                 vec![],
                 None,
-                vec![param_t("n", Int)],
+                vec![kw("n", Int)],
                 Str,
             ),
             Immutable,
@@ -1412,7 +1424,6 @@ impl Context {
             2,
         );
         array_mut_.register_superclass(array_t.clone(), &array_);
-        array_mut_.register_superclass(Obj, &obj);
         let t = pr_met(
             ref_mut(
                 array_mut_t.clone(),
@@ -1421,7 +1432,7 @@ impl Context {
                     vec![ty_tp(mono_q("T")), mono_q_tp("N") + value(1)],
                 )),
             ),
-            vec![param_t("elem", mono_q("T"))],
+            vec![kw("elem", mono_q("T"))],
             None,
             vec![],
             NoneType,
@@ -1433,10 +1444,7 @@ impl Context {
         array_mut_.register_builtin_impl("push!", t, Immutable, Public);
         let t = pr_met(
             array_mut_t.clone(),
-            vec![param_t(
-                "f",
-                nd_func(vec![anon(mono_q("T"))], None, mono_q("T")),
-            )],
+            vec![kw("f", nd_func(vec![anon(mono_q("T"))], None, mono_q("T")))],
             None,
             vec![],
             NoneType,
@@ -1446,10 +1454,10 @@ impl Context {
             set! {static_instance("T", Type), static_instance("N", builtin_mono("Nat!"))},
         );
         array_mut_.register_builtin_impl("strict_map!", t, Immutable, Public);
-        let f_t = param_t(
+        let f_t = kw(
             "f",
             func(
-                vec![param_t("old", array_t.clone())],
+                vec![kw("old", array_t.clone())],
                 None,
                 vec![],
                 array_t.clone(),
@@ -1487,16 +1495,16 @@ impl Context {
         );
         let mut proc = Self::builtin_mono_class("Proc", 2);
         proc.register_superclass(Obj, &obj);
-        // TODO: lambda
-        proc.register_marker_trait(builtin_mono("Named"));
+        let mut named_proc = Self::builtin_mono_class("NamedProc", 2);
+        named_proc.register_superclass(Obj, &obj);
+        named_proc.register_marker_trait(builtin_mono("Named"));
         let mut func = Self::builtin_mono_class("Func", 2);
         func.register_superclass(builtin_mono("Proc"), &proc);
-        func.register_superclass(Obj, &obj);
-        // TODO: lambda
-        func.register_marker_trait(builtin_mono("Named"));
+        let mut named_func = Self::builtin_mono_class("NamedFunc", 2);
+        named_func.register_superclass(builtin_mono("Func"), &func);
+        named_func.register_marker_trait(builtin_mono("Named"));
         let mut qfunc = Self::builtin_mono_class("QuantifiedFunc", 2);
         qfunc.register_superclass(builtin_mono("Func"), &func);
-        qfunc.register_superclass(Obj, &obj);
         self.register_builtin_type(Obj, obj, Const);
         // self.register_type(mono("Record"), vec![], record, Const);
         self.register_builtin_type(Int, int, Const);
@@ -1586,42 +1594,50 @@ impl Context {
         self.register_builtin_type(range_t, range, Const);
         self.register_builtin_type(builtin_mono("Tuple"), tuple_, Const);
         self.register_builtin_type(builtin_mono("Proc"), proc, Const);
+        self.register_builtin_type(builtin_mono("NamedProc"), named_proc, Const);
         self.register_builtin_type(builtin_mono("Func"), func, Const);
+        self.register_builtin_type(builtin_mono("NamedFunc"), named_func, Const);
         self.register_builtin_type(builtin_mono("QuantifiedFunc"), qfunc, Const);
     }
 
     fn init_builtin_funcs(&mut self) {
-        let t_abs = nd_func(vec![param_t("n", builtin_mono("Num"))], None, Nat);
+        let t_abs = nd_func(vec![kw("n", builtin_mono("Num"))], None, Nat);
         let t_assert = func(
-            vec![param_t("condition", Bool)],
+            vec![kw("condition", Bool)],
             None,
-            vec![param_t("err_message", Str)],
+            vec![kw("err_message", Str)],
             NoneType,
         );
-        let t_classof = nd_func(vec![param_t("old", Obj)], None, Class);
-        let t_compile = nd_func(vec![param_t("src", Str)], None, Code);
+        let t_classof = nd_func(vec![kw("old", Obj)], None, Class);
+        let t_compile = nd_func(vec![kw("src", Str)], None, Code);
         let t_cond = nd_func(
             vec![
-                param_t("condition", Bool),
-                param_t("then", mono_q("T")),
-                param_t("else", mono_q("T")),
+                kw("condition", Bool),
+                kw("then", mono_q("T")),
+                kw("else", mono_q("T")),
             ],
             None,
             mono_q("T"),
         );
         let t_cond = quant(t_cond, set! {static_instance("T", Type)});
-        let t_discard = nd_func(vec![param_t("old", Obj)], None, NoneType);
-        // FIXME: quantify
+        let t_discard = nd_func(vec![kw("obj", Obj)], None, NoneType);
         let t_if = func(
             vec![
-                param_t("cond", Bool),
-                param_t("then", nd_func(vec![], None, mono_q("T"))),
+                kw("cond", Bool),
+                kw("then", nd_func(vec![], None, mono_q("T"))),
             ],
             None,
-            vec![param_t("else", nd_func(vec![], None, mono_q("T")))],
-            or(mono_q("T"), NoneType),
+            vec![kw_default(
+                "else",
+                nd_func(vec![], None, mono_q("U")),
+                nd_func(vec![], None, NoneType),
+            )],
+            or(mono_q("T"), mono_q("U")),
+        );
+        let t_if = quant(
+            t_if,
+            set! {static_instance("T", Type), static_instance("U", Type)},
         );
-        let t_if = quant(t_if, set! {static_instance("T", Type)});
         let t_import = nd_func(
             vec![anon(tp_enum(Str, set! {mono_q_tp("Path")}))],
             None,
@@ -1630,12 +1646,12 @@ impl Context {
         let t_import = quant(t_import, set! {static_instance("Path", Str)});
         let t_log = func(
             vec![],
-            Some(param_t("objects", ref_(Obj))),
+            Some(kw("objects", ref_(Obj))),
             vec![
-                param_t("sep", Str),
-                param_t("end", Str),
-                param_t("file", builtin_mono("Write")),
-                param_t("flush", Bool),
+                kw("sep", Str),
+                kw("end", Str),
+                kw("file", builtin_mono("Write")),
+                kw("flush", Bool),
             ],
             NoneType,
         );
@@ -1644,9 +1660,9 @@ impl Context {
             None,
             module(mono_q_tp("Path")),
         );
-        let t_panic = nd_func(vec![param_t("err_message", Str)], None, NoneType);
+        let t_panic = nd_func(vec![kw("err_message", Str)], None, NoneType);
         let t_pyimport = quant(t_pyimport, set! {static_instance("Path", Str)});
-        let t_quit = func(vec![], None, vec![param_t("code", Int)], NoneType);
+        let t_quit = func(vec![], None, vec![kw("code", Int)], NoneType);
         let t_exit = t_quit.clone();
         self.register_builtin_impl("abs", t_abs, Immutable, Private);
         self.register_builtin_impl("assert", t_assert, Const, Private); // assert casting に悪影響が出る可能性があるため、Constとしておく
@@ -1668,17 +1684,17 @@ impl Context {
 
     fn init_builtin_const_funcs(&mut self) {
         let class_t = func(
-            vec![param_t("Requirement", Type)],
+            vec![kw("Requirement", Type)],
             None,
-            vec![param_t("Impl", Type)],
+            vec![kw("Impl", Type)],
             Class,
         );
         let class = ConstSubr::Builtin(BuiltinConstSubr::new("Class", class_func, class_t, None));
         self.register_builtin_const("Class", ValueObj::Subr(class));
         let inherit_t = func(
-            vec![param_t("Super", Class)],
+            vec![kw("Super", Class)],
             None,
-            vec![param_t("Impl", Type), param_t("Additional", Type)],
+            vec![kw("Impl", Type), kw("Additional", Type)],
             Class,
         );
         let inherit = ConstSubr::Builtin(BuiltinConstSubr::new(
@@ -1689,17 +1705,17 @@ impl Context {
         ));
         self.register_builtin_const("Inherit", ValueObj::Subr(inherit));
         let trait_t = func(
-            vec![param_t("Requirement", Type)],
+            vec![kw("Requirement", Type)],
             None,
-            vec![param_t("Impl", Type)],
+            vec![kw("Impl", Type)],
             Trait,
         );
         let trait_ = ConstSubr::Builtin(BuiltinConstSubr::new("Trait", trait_func, trait_t, None));
         self.register_builtin_const("Trait", ValueObj::Subr(trait_));
         let subsume_t = func(
-            vec![param_t("Super", Trait)],
+            vec![kw("Super", Trait)],
             None,
-            vec![param_t("Impl", Type), param_t("Additional", Type)],
+            vec![kw("Impl", Type), kw("Additional", Type)],
             Trait,
         );
         let subsume = ConstSubr::Builtin(BuiltinConstSubr::new(
@@ -1718,42 +1734,45 @@ impl Context {
             None,
         ));
         self.register_builtin_const("Inheritable", ValueObj::Subr(inheritable));
+        // TODO: register Del function object
+        let t_del = nd_func(vec![kw("obj", Obj)], None, NoneType);
+        self.register_builtin_impl("Del", t_del, Immutable, Private);
     }
 
     fn init_builtin_procs(&mut self) {
         let t_dir = proc(
-            vec![param_t("obj", ref_(Obj))],
+            vec![kw("obj", ref_(Obj))],
             None,
             vec![],
             array(Str, TyParam::erased(Nat)),
         );
         let t_print = proc(
             vec![],
-            Some(param_t("objects", ref_(Obj))),
+            Some(kw("objects", ref_(Obj))),
             vec![
-                param_t("sep", Str),
-                param_t("end", Str),
-                param_t("file", builtin_mono("Write")),
-                param_t("flush", Bool),
+                kw("sep", Str),
+                kw("end", Str),
+                kw("file", builtin_mono("Write")),
+                kw("flush", Bool),
             ],
             NoneType,
         );
-        let t_id = nd_func(vec![param_t("old", Obj)], None, Nat);
-        let t_input = proc(vec![], None, vec![param_t("msg", Str)], Str);
+        let t_id = nd_func(vec![kw("old", Obj)], None, Nat);
+        let t_input = proc(vec![], None, vec![kw("msg", Str)], Str);
         let t_if = proc(
             vec![
-                param_t("cond", Bool),
-                param_t("then", nd_proc(vec![], None, mono_q("T"))),
+                kw("cond", Bool),
+                kw("then", nd_proc(vec![], None, mono_q("T"))),
             ],
             None,
-            vec![param_t("else", nd_proc(vec![], None, mono_q("T")))],
+            vec![kw("else", nd_proc(vec![], None, mono_q("T")))],
             or(mono_q("T"), NoneType),
         );
         let t_if = quant(t_if, set! {static_instance("T", Type)});
         let t_for = nd_proc(
             vec![
-                param_t("iter", iter(mono_q("T"))),
-                param_t("p", nd_proc(vec![anon(mono_q("T"))], None, NoneType)),
+                kw("iter", iter(mono_q("T"))),
+                kw("p", nd_proc(vec![anon(mono_q("T"))], None, NoneType)),
             ],
             None,
             NoneType,
@@ -1761,22 +1780,22 @@ impl Context {
         let t_for = quant(t_for, set! {static_instance("T", Type)});
         let t_while = nd_proc(
             vec![
-                param_t("cond", builtin_mono("Bool!")),
-                param_t("p", nd_proc(vec![], None, NoneType)),
+                kw("cond", builtin_mono("Bool!")),
+                kw("p", nd_proc(vec![], None, NoneType)),
             ],
             None,
             NoneType,
         );
         let t_open = proc(
-            vec![param_t("file", mono_q("P"))],
+            vec![kw("file", mono_q("P"))],
             None,
             vec![
-                param_t("mode", Str),
-                param_t("buffering", Int),
-                param_t("encoding", or(Str, NoneType)),
-                param_t("errors", or(Str, NoneType)),
-                param_t("newline", or(Str, NoneType)),
-                param_t("closefd", Bool),
+                kw("mode", Str),
+                kw("buffering", Int),
+                kw("encoding", or(Str, NoneType)),
+                kw("errors", or(Str, NoneType)),
+                kw("newline", or(Str, NoneType)),
+                kw("closefd", Bool),
                 // param_t("opener", option),
             ],
             builtin_mono("File!"),
@@ -1788,8 +1807,8 @@ impl Context {
         // TODO: T <: With
         let t_with = nd_proc(
             vec![
-                param_t("obj", mono_q("T")),
-                param_t("p!", nd_proc(vec![anon(mono_q("T"))], None, mono_q("U"))),
+                kw("obj", mono_q("T")),
+                kw("p!", nd_proc(vec![anon(mono_q("T"))], None, mono_q("U"))),
             ],
             None,
             mono_q("U"),
@@ -1815,7 +1834,7 @@ impl Context {
         let r = mono_q("R");
         let params = vec![ty_tp(mono_q("R"))];
         let op_t = nd_func(
-            vec![param_t("lhs", l.clone()), param_t("rhs", r.clone())],
+            vec![kw("lhs", l.clone()), kw("rhs", r.clone())],
             None,
             mono_proj(mono_q("L"), "Output"),
         );
diff --git a/compiler/erg_compiler/context/initialize/py_mods/random.rs b/compiler/erg_compiler/context/initialize/py_mods/random.rs
index 2c2c1914..0fa876bf 100644
--- a/compiler/erg_compiler/context/initialize/py_mods/random.rs
+++ b/compiler/erg_compiler/context/initialize/py_mods/random.rs
@@ -2,7 +2,7 @@ use erg_common::set;
 use erg_common::vis::Visibility;
 
 use erg_type::constructors::{
-    builtin_mono, builtin_poly, mono_q, nd_proc, param_t, proc, quant, static_instance, ty_tp,
+    builtin_mono, builtin_poly, kw, mono_q, nd_proc, proc, quant, static_instance, ty_tp,
 };
 use erg_type::Type;
 use Type::*;
@@ -21,8 +21,8 @@ impl Context {
                 vec![],
                 None,
                 vec![
-                    param_t("a", builtin_mono("Num")), // TODO: NoneType, int, float, str, bytes, bytearray
-                    param_t("version", Int),
+                    kw("a", builtin_mono("Num")), // TODO: NoneType, int, float, str, bytes, bytearray
+                    kw("version", Int),
                 ],
                 NoneType,
             ),
@@ -31,15 +31,12 @@ impl Context {
         );
         random.register_builtin_impl(
             "randint!",
-            nd_proc(vec![param_t("a", Int), param_t("b", Int)], None, Int),
+            nd_proc(vec![kw("a", Int), kw("b", Int)], None, Int),
             Immutable,
             Public,
         );
         let t = nd_proc(
-            vec![param_t(
-                "seq",
-                builtin_poly("Seq", vec![ty_tp(mono_q("T"))]),
-            )],
+            vec![kw("seq", builtin_poly("Seq", vec![ty_tp(mono_q("T"))]))],
             None,
             mono_q("T"),
         );
diff --git a/compiler/erg_compiler/context/initialize/py_mods/socket.rs b/compiler/erg_compiler/context/initialize/py_mods/socket.rs
index 9839f70e..586b3487 100644
--- a/compiler/erg_compiler/context/initialize/py_mods/socket.rs
+++ b/compiler/erg_compiler/context/initialize/py_mods/socket.rs
@@ -1,6 +1,6 @@
 use erg_common::vis::Visibility;
 
-use erg_type::constructors::{builtin_mono, func, or, param_t};
+use erg_type::constructors::{builtin_mono, func, kw, or};
 use erg_type::Type;
 use Type::*;
 
@@ -21,10 +21,10 @@ impl Context {
                 vec![],
                 None,
                 vec![
-                    param_t("family", Int),
-                    param_t("type", Int),
-                    param_t("proto", Int),
-                    param_t("fileno", or(Int, NoneType)),
+                    kw("family", Int),
+                    kw("type", Int),
+                    kw("proto", Int),
+                    kw("fileno", or(Int, NoneType)),
                 ],
                 builtin_mono("Socket!"),
             ),
diff --git a/compiler/erg_compiler/context/initialize/py_mods/urllib.rs b/compiler/erg_compiler/context/initialize/py_mods/urllib.rs
index bb864e65..b9383040 100644
--- a/compiler/erg_compiler/context/initialize/py_mods/urllib.rs
+++ b/compiler/erg_compiler/context/initialize/py_mods/urllib.rs
@@ -2,7 +2,7 @@ use std::path::PathBuf;
 
 use erg_common::vis::Visibility;
 
-use erg_type::constructors::{builtin_mono, module_from_path, mono, or, param_t, proc};
+use erg_type::constructors::{builtin_mono, kw, module_from_path, mono, or, proc};
 use erg_type::Type;
 use Type::*;
 
@@ -22,11 +22,11 @@ impl Context {
         urllib.register_builtin_impl("request", module_from_path("request"), Immutable, Public);
         let mut request = Context::builtin_module("urllib.request", 15);
         let t = proc(
-            vec![param_t("url", or(Str, mono("urllib.request", "Request")))],
+            vec![kw("url", or(Str, mono("urllib.request", "Request")))],
             None,
             vec![
-                param_t("data", or(builtin_mono("Bytes"), NoneType)),
-                param_t("timeout", or(Nat, NoneType)),
+                kw("data", or(builtin_mono("Bytes"), NoneType)),
+                kw("timeout", or(Nat, NoneType)),
             ],
             mono("http.client", "HTTPResponse"),
         );
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index 12326f7e..dfc137af 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -16,7 +16,10 @@ use ast::VarName;
 use erg_parser::ast::{self, Identifier};
 use erg_parser::token::Token;
 
-use erg_type::constructors::{builtin_mono, func, module, mono, mono_proj, v_enum};
+use erg_type::constructors::{
+    anon, builtin_mono, free_var, func, module, mono, mono_proj, subr_t, v_enum,
+};
+use erg_type::free::Constraint;
 use erg_type::typaram::TyParam;
 use erg_type::value::{GenTypeObj, TypeObj, ValueObj};
 use erg_type::{HasType, ParamTy, SubrKind, SubrType, TyBound, Type};
@@ -32,6 +35,8 @@ use crate::varinfo::VarInfo;
 use RegistrationMode::*;
 use Visibility::*;
 
+use super::MethodType;
+
 impl Context {
     pub(crate) fn validate_var_sig_t(
         &self,
@@ -93,7 +98,7 @@ impl Context {
     ) -> SingleTyCheckResult<&Context> {
         match obj {
             hir::Expr::Accessor(hir::Accessor::Ident(ident)) => {
-                self.get_singular_ctx_from_ident(&ident.clone().downcast(), namespace)
+                self.get_singular_ctx_by_ident(&ident.clone().downcast(), namespace)
             }
             hir::Expr::Accessor(hir::Accessor::Attr(attr)) => {
                 // REVIEW: 両方singularとは限らない?
@@ -113,12 +118,12 @@ impl Context {
         }
     }
 
-    pub fn get_singular_ctx_from_ident(
+    pub fn get_singular_ctx_by_ident(
         &self,
         ident: &ast::Identifier,
         namespace: &Str,
     ) -> SingleTyCheckResult<&Context> {
-        self.get_mod(ident)
+        self.get_mod(ident.inspect())
             .or_else(|| self.rec_get_type(ident.inspect()).map(|(_, ctx)| ctx))
             .ok_or_else(|| {
                 TyCheckError::no_var_error(
@@ -132,7 +137,7 @@ impl Context {
             })
     }
 
-    pub fn get_mut_singular_ctx_from_ident(
+    pub fn get_mut_singular_ctx_by_ident(
         &mut self,
         ident: &ast::Identifier,
         namespace: &Str,
@@ -157,7 +162,7 @@ impl Context {
     ) -> SingleTyCheckResult<&mut Context> {
         match obj {
             ast::Expr::Accessor(ast::Accessor::Ident(ident)) => {
-                self.get_mut_singular_ctx_from_ident(ident, namespace)
+                self.get_mut_singular_ctx_by_ident(ident, namespace)
             }
             ast::Expr::Accessor(ast::Accessor::Attr(attr)) => {
                 // REVIEW: 両方singularとは限らない?
@@ -335,6 +340,30 @@ impl Context {
         }
     }
 
+    pub(crate) fn rec_get_decl_t(
+        &self,
+        ident: &Identifier,
+        input: &Input,
+        namespace: &Str,
+    ) -> SingleTyCheckResult<Type> {
+        if let Some(vi) = self.decls.get(&ident.inspect()[..]) {
+            self.validate_visibility(ident, vi, input, namespace)?;
+            Ok(vi.t())
+        } else {
+            if let Some(parent) = self.get_outer().or_else(|| self.get_builtins()) {
+                return parent.rec_get_decl_t(ident, input, namespace);
+            }
+            Err(TyCheckError::no_var_error(
+                input.clone(),
+                line!() as usize,
+                ident.loc(),
+                namespace.into(),
+                ident.inspect(),
+                self.get_similar_name(ident.inspect()),
+            ))
+        }
+    }
+
     pub(crate) fn rec_get_attr_t(
         &self,
         obj: &hir::Expr,
@@ -540,10 +569,12 @@ impl Context {
                     self.get_similar_attr_from_singular(obj, method_name.inspect()),
                 ));
             }
-            match self.rec_get_method_traits(method_name) {
-                Ok(trait_) => {
-                    let (_, ctx) = self.get_nominal_type_ctx(trait_).unwrap();
-                    return ctx.rec_get_var_t(method_name, input, namespace);
+            match self.get_method_type_by_name(method_name) {
+                Ok(t) => {
+                    self.sub_unify(obj.ref_t(), &t.definition_type, obj.loc(), None)
+                        // HACK: change this func's return type to TyCheckResult<Type>
+                        .map_err(|mut errs| errs.remove(0))?;
+                    return Ok(t.method_type.clone());
                 }
                 Err(err) if err.core.kind == ErrorKind::TypeError => {
                     return Err(err);
@@ -700,6 +731,7 @@ impl Context {
     /// substitute_call(instance: ((?T, Int) -> ?T), [Int, Nat], []) => instance: (Int, Int) -> Str
     /// substitute_call(instance: ((?M(: Nat)..?N(: Nat)) -> ?M+?N), [1..2], []) => instance: (1..2) -> {3}
     /// substitute_call(instance: ((?L(: Add(?R, ?O)), ?R) -> ?O), [1, 2], []) => instance: (Nat, Nat) -> Nat
+    /// substitute_call(instance: ?T, [Int, Str], []) => instance: (Int, Str) -> Int
     /// ```
     fn substitute_call(
         &self,
@@ -713,6 +745,26 @@ impl Context {
             Type::FreeVar(fv) if fv.is_linked() => {
                 self.substitute_call(obj, method_name, &fv.crack(), pos_args, kw_args)
             }
+            Type::FreeVar(fv) => {
+                if let Some(_method_name) = method_name {
+                    todo!()
+                } else {
+                    let is_procedural = obj
+                        .show_acc()
+                        .map(|acc| acc.ends_with('!'))
+                        .unwrap_or(false);
+                    let kind = if is_procedural {
+                        SubrKind::Proc
+                    } else {
+                        SubrKind::Func
+                    };
+                    let ret_t = free_var(self.level, Constraint::new_type_of(Type));
+                    let non_default_params = pos_args.iter().map(|a| anon(a.expr.t())).collect();
+                    let subr_t = subr_t(kind, non_default_params, None, vec![], ret_t);
+                    fv.link(&subr_t);
+                    Ok(())
+                }
+            }
             Type::Refinement(refine) => {
                 self.substitute_call(obj, method_name, &refine.t, pos_args, kw_args)
             }
@@ -788,6 +840,15 @@ impl Context {
                             &mut passed_params,
                         )?;
                     }
+                    for not_passed in subr
+                        .default_params
+                        .iter()
+                        .filter(|pt| !passed_params.contains(pt.name().unwrap()))
+                    {
+                        if let ParamTy::KwWithDefault { ty, default, .. } = not_passed {
+                            self.sub_unify(default, ty, obj.loc(), not_passed.name())?;
+                        }
+                    }
                 } else {
                     let missing_len = subr.non_default_params.len() - pos_args.len();
                     let missing_params = subr
@@ -1152,13 +1213,19 @@ impl Context {
             .iter()
             .map(|(opt_name, _)| {
                 if let Some(name) = opt_name {
-                    if let Some(t) = self.super_traits.iter().find(|t| {
-                        (&t.name()[..] == "Input" || &t.name()[..] == "Output")
-                            && t.inner_ts()
-                                .first()
-                                .map(|t| &t.name() == name.inspect())
-                                .unwrap_or(false)
-                    }) {
+                    // トレイトの変性を調べるときはsuper_classesも見る必要がある
+                    if let Some(t) = self
+                        .super_traits
+                        .iter()
+                        .chain(self.super_classes.iter())
+                        .find(|t| {
+                            (&t.name()[..] == "Input" || &t.name()[..] == "Output")
+                                && t.inner_ts()
+                                    .first()
+                                    .map(|t| &t.name() == name.inspect())
+                                    .unwrap_or(false)
+                        })
+                    {
                         match &t.name()[..] {
                             "Output" => Variance::Covariant,
                             "Input" => Variance::Contravariant,
@@ -1280,7 +1347,17 @@ impl Context {
                 }
             }
             // TODO
-            Type::Or(_l, _r) => None,
+            Type::Or(l, r) => match (l.as_ref(), r.as_ref()) {
+                (Type::FreeVar(l), Type::FreeVar(r)) if l.is_unbound() && r.is_unbound() => {
+                    let (_lsub, lsup) = l.get_bound_types().unwrap();
+                    let (_rsub, rsup) = r.get_bound_types().unwrap();
+                    self.get_nominal_super_type_ctxs(&self.union(&lsup, &rsup))
+                }
+                (Type::Refinement(l), Type::Refinement(r)) if l.t == r.t => {
+                    self.get_nominal_super_type_ctxs(&l.t)
+                }
+                _ => None,
+            },
             _ => self
                 .get_simple_nominal_super_type_ctxs(t)
                 .map(|ctxs| ctxs.collect()),
@@ -1417,6 +1494,17 @@ impl Context {
                     return Some(res);
                 }
             }
+            Type::Or(l, r) => {
+                let (lt, lctx) = self.get_nominal_type_ctx(l)?;
+                let (rt, rctx) = self.get_nominal_type_ctx(r)?;
+                // use smaller context
+                return match (self.supertype_of(lt, rt), self.supertype_of(rt, lt)) {
+                    (true, true) => Some((rt, lctx)),
+                    (true, false) => Some((rt, lctx)),
+                    (false, true) => Some((lt, rctx)),
+                    (false, false) => None,
+                };
+            }
             // FIXME: `F()`などの場合、実際は引数が省略されていてもmonomorphicになる
             other if other.is_monomorphic() => {
                 if let Some((t, ctx)) = self.rec_get_mono_type(&other.name()) {
@@ -1491,14 +1579,43 @@ impl Context {
         None
     }
 
-    pub(crate) fn rec_get_trait_impls(&self, name: &Str) -> Vec<TraitInstance> {
-        let current = if let Some(impls) = self.trait_impls.get(name) {
+    pub(crate) fn get_trait_impls(&self, t: &Type) -> Set<TraitInstance> {
+        match t {
+            // And(Add, Sub) == intersection({Int <: Add(Int), Bool <: Add(Bool) ...}, {Int <: Sub(Int), ...})
+            // == {Int <: Add(Int) and Sub(Int), ...}
+            Type::And(l, r) => {
+                let l_impls = self.get_trait_impls(l);
+                let l_base = Set::from_iter(l_impls.iter().map(|ti| &ti.sub_type));
+                let r_impls = self.get_trait_impls(r);
+                let r_base = Set::from_iter(r_impls.iter().map(|ti| &ti.sub_type));
+                let bases = l_base.intersection(&r_base);
+                let mut isec = set! {};
+                for base in bases.into_iter() {
+                    let lti = l_impls.iter().find(|ti| &ti.sub_type == base).unwrap();
+                    let rti = r_impls.iter().find(|ti| &ti.sub_type == base).unwrap();
+                    let sup_trait = self.intersection(&lti.sup_trait, &rti.sup_trait);
+                    isec.insert(TraitInstance::new(lti.sub_type.clone(), sup_trait));
+                }
+                isec
+            }
+            Type::Or(l, r) => {
+                let l_impls = self.get_trait_impls(l);
+                let r_impls = self.get_trait_impls(r);
+                // FIXME:
+                l_impls.union(&r_impls)
+            }
+            _ => self.get_simple_trait_impls(t),
+        }
+    }
+
+    pub(crate) fn get_simple_trait_impls(&self, t: &Type) -> Set<TraitInstance> {
+        let current = if let Some(impls) = self.trait_impls.get(&t.name()) {
             impls.clone()
         } else {
-            vec![]
+            set! {}
         };
         if let Some(outer) = self.get_outer().or_else(|| self.get_builtins()) {
-            [current, outer.rec_get_trait_impls(name)].concat()
+            current.union(&outer.get_simple_trait_impls(t))
         } else {
             current
         }
@@ -1515,10 +1632,8 @@ impl Context {
     }
 
     // FIXME: 現在の実装だとimportしたモジュールはどこからでも見れる
-    fn get_mod(&self, ident: &ast::Identifier) -> Option<&Context> {
-        let t = self
-            .rec_get_var_t(ident, &self.cfg.input, &self.name)
-            .ok()?;
+    pub(crate) fn get_mod(&self, name: &str) -> Option<&Context> {
+        let t = self.get_var_info(name).map(|(_, vi)| vi.t.clone()).ok()?;
         match t {
             Type::BuiltinPoly { name, mut params } if &name[..] == "Module" => {
                 let path =
@@ -1624,7 +1739,7 @@ impl Context {
         }
     }
 
-    fn rec_get_type(&self, name: &str) -> Option<(&Type, &Context)> {
+    pub(crate) fn rec_get_type(&self, name: &str) -> Option<(&Type, &Context)> {
         if let Some((t, ctx)) = self.mono_types.get(name) {
             Some((t, ctx))
         } else if let Some((t, ctx)) = self.poly_types.get(name) {
@@ -1646,22 +1761,52 @@ impl Context {
         }
     }
 
-    fn rec_get_method_traits(&self, name: &Identifier) -> SingleTyCheckResult<&Type> {
-        if let Some(candidates) = self.method_traits.get(name.inspect()) {
-            let first_t = candidates.first().unwrap();
-            if candidates.iter().skip(1).all(|t| t == first_t) {
-                Ok(&candidates[0])
+    fn get_method_type_by_name(&self, name: &Identifier) -> SingleTyCheckResult<&MethodType> {
+        // TODO: min_by
+        if let Some(candidates) = self.method_to_traits.get(name.inspect()) {
+            let first_method_type = &candidates.first().unwrap().method_type;
+            if candidates
+                .iter()
+                .skip(1)
+                .all(|t| &t.method_type == first_method_type)
+            {
+                return Ok(&candidates[0]);
             } else {
-                Err(TyCheckError::ambiguous_type_error(
+                return Err(TyCheckError::ambiguous_type_error(
                     self.cfg.input.clone(),
                     line!() as usize,
                     name,
-                    candidates,
+                    &candidates
+                        .iter()
+                        .map(|t| t.definition_type.clone())
+                        .collect::<Vec<_>>(),
                     self.caused_by(),
-                ))
+                ));
             }
-        } else if let Some(outer) = self.get_outer().or_else(|| self.get_builtins()) {
-            outer.rec_get_method_traits(name)
+        }
+        if let Some(candidates) = self.method_to_classes.get(name.inspect()) {
+            let first_method_type = &candidates.first().unwrap().method_type;
+            if candidates
+                .iter()
+                .skip(1)
+                .all(|t| &t.method_type == first_method_type)
+            {
+                return Ok(&candidates[0]);
+            } else {
+                return Err(TyCheckError::ambiguous_type_error(
+                    self.cfg.input.clone(),
+                    line!() as usize,
+                    name,
+                    &candidates
+                        .iter()
+                        .map(|t| t.definition_type.clone())
+                        .collect::<Vec<_>>(),
+                    self.caused_by(),
+                ));
+            }
+        }
+        if let Some(outer) = self.get_outer().or_else(|| self.get_builtins()) {
+            outer.get_method_type_by_name(name)
         } else {
             Err(TyCheckError::no_attr_error(
                 self.cfg.input.clone(),
@@ -1731,7 +1876,7 @@ impl Context {
         match lhs {
             Type::FreeVar(fv) => {
                 if let Some(sup) = fv.get_sup() {
-                    let insts = self.rec_get_trait_impls(&sup.name());
+                    let insts = self.get_trait_impls(&sup);
                     let candidates = insts.into_iter().filter_map(move |inst| {
                         if self.supertype_of(&inst.sup_trait, &sup) {
                             self.eval_t_params(
diff --git a/compiler/erg_compiler/context/instantiate.rs b/compiler/erg_compiler/context/instantiate.rs
index 5142099a..921da50e 100644
--- a/compiler/erg_compiler/context/instantiate.rs
+++ b/compiler/erg_compiler/context/instantiate.rs
@@ -168,6 +168,62 @@ impl TyVarContext {
                 };
                 mono_proj(lhs, rhs)
             }
+            Type::Ref(t) if t.has_qvar() => ref_(self.instantiate_qvar(*t)),
+            Type::RefMut { before, after } => {
+                let before = if before.has_qvar() {
+                    self.instantiate_qvar(*before)
+                } else {
+                    *before
+                };
+                let after = after.map(|t| {
+                    if t.has_qvar() {
+                        self.instantiate_qvar(*t)
+                    } else {
+                        *t
+                    }
+                });
+                ref_mut(before, after)
+            }
+            Type::And(l, r) => {
+                let l = if l.has_qvar() {
+                    self.instantiate_qvar(*l)
+                } else {
+                    *l
+                };
+                let r = if r.has_qvar() {
+                    self.instantiate_qvar(*r)
+                } else {
+                    *r
+                };
+                and(l, r)
+            }
+            Type::Or(l, r) => {
+                let l = if l.has_qvar() {
+                    self.instantiate_qvar(*l)
+                } else {
+                    *l
+                };
+                let r = if r.has_qvar() {
+                    self.instantiate_qvar(*r)
+                } else {
+                    *r
+                };
+                or(l, r)
+            }
+            Type::Not(l, r) => {
+                let l = if l.has_qvar() {
+                    self.instantiate_qvar(*l)
+                } else {
+                    *l
+                };
+                let r = if r.has_qvar() {
+                    self.instantiate_qvar(*r)
+                } else {
+                    *r
+                };
+                not(l, r)
+            }
+            Type::MonoQVar(_) => self.instantiate_qvar(sub_or_sup),
             other => other,
         }
     }
@@ -461,7 +517,7 @@ impl Context {
     ) -> TyCheckResult<Type> {
         // -> Result<Type, (Type, TyCheckErrors)> {
         let opt_decl_sig_t = self
-            .rec_get_var_t(&sig.ident, &self.cfg.input, &self.name)
+            .rec_get_decl_t(&sig.ident, &self.cfg.input, &self.name)
             .ok()
             .map(|t| enum_unwrap!(t, Type::Subr));
         let bounds = self.instantiate_ty_bounds(&sig.bounds, PreRegister)?;
@@ -471,17 +527,13 @@ impl Context {
             let opt_decl_t = opt_decl_sig_t
                 .as_ref()
                 .and_then(|subr| subr.non_default_params.get(n));
-            non_defaults.push(ParamTy::pos(
-                p.inspect().cloned(),
-                self.instantiate_param_sig_t(p, opt_decl_t, Some(&tv_ctx), mode)?,
-            ));
+            non_defaults.push(self.instantiate_param_ty(p, opt_decl_t, Some(&tv_ctx), mode)?);
         }
         let var_args = if let Some(var_args) = sig.params.var_args.as_ref() {
             let opt_decl_t = opt_decl_sig_t
                 .as_ref()
                 .and_then(|subr| subr.var_params.as_ref().map(|v| v.as_ref()));
-            let va_t = self.instantiate_param_sig_t(var_args, opt_decl_t, Some(&tv_ctx), mode)?;
-            Some(ParamTy::pos(var_args.inspect().cloned(), va_t))
+            Some(self.instantiate_param_ty(var_args, opt_decl_t, Some(&tv_ctx), mode)?)
         } else {
             None
         };
@@ -490,10 +542,7 @@ impl Context {
             let opt_decl_t = opt_decl_sig_t
                 .as_ref()
                 .and_then(|subr| subr.default_params.get(n));
-            defaults.push(ParamTy::kw(
-                p.inspect().unwrap().clone(),
-                self.instantiate_param_sig_t(p, opt_decl_t, Some(&tv_ctx), mode)?,
-            ));
+            defaults.push(self.instantiate_param_ty(p, opt_decl_t, Some(&tv_ctx), mode)?);
         }
         let spec_return_t = if let Some(s) = sig.return_t_spec.as_ref() {
             let opt_decl_t = opt_decl_sig_t
@@ -554,6 +603,29 @@ impl Context {
         Ok(spec_t)
     }
 
+    pub(crate) fn instantiate_param_ty(
+        &self,
+        sig: &ParamSignature,
+        opt_decl_t: Option<&ParamTy>,
+        tmp_tv_ctx: Option<&TyVarContext>,
+        mode: RegistrationMode,
+    ) -> TyCheckResult<ParamTy> {
+        let t = self.instantiate_param_sig_t(sig, opt_decl_t, tmp_tv_ctx, mode)?;
+        match (sig.inspect(), &sig.opt_default_val) {
+            (Some(name), Some(default)) => {
+                let default = self.instantiate_const_expr(default);
+                Ok(ParamTy::kw_default(
+                    name.clone(),
+                    t,
+                    self.get_tp_t(&default)?,
+                ))
+            }
+            (Some(name), None) => Ok(ParamTy::kw(name.clone(), t)),
+            (None, None) => Ok(ParamTy::anonymous(t)),
+            _ => unreachable!(),
+        }
+    }
+
     pub(crate) fn instantiate_predecl_t(
         &self,
         predecl: &PreDeclTypeSpec,
@@ -695,19 +767,18 @@ impl Context {
             TypeSpec::PreDeclTy(predecl) => {
                 Ok(self.instantiate_predecl_t(predecl, opt_decl_t, tmp_tv_ctx)?)
             }
-            // TODO: Flatten
-            TypeSpec::And(lhs, rhs) => Ok(and(
-                self.instantiate_typespec(lhs, opt_decl_t, tmp_tv_ctx, mode)?,
-                self.instantiate_typespec(rhs, opt_decl_t, tmp_tv_ctx, mode)?,
+            TypeSpec::And(lhs, rhs) => Ok(self.union(
+                &self.instantiate_typespec(lhs, opt_decl_t, tmp_tv_ctx, mode)?,
+                &self.instantiate_typespec(rhs, opt_decl_t, tmp_tv_ctx, mode)?,
+            )),
+            TypeSpec::Or(lhs, rhs) => Ok(self.intersection(
+                &self.instantiate_typespec(lhs, opt_decl_t, tmp_tv_ctx, mode)?,
+                &self.instantiate_typespec(rhs, opt_decl_t, tmp_tv_ctx, mode)?,
             )),
             TypeSpec::Not(lhs, rhs) => Ok(not(
                 self.instantiate_typespec(lhs, opt_decl_t, tmp_tv_ctx, mode)?,
                 self.instantiate_typespec(rhs, opt_decl_t, tmp_tv_ctx, mode)?,
             )),
-            TypeSpec::Or(lhs, rhs) => Ok(or(
-                self.instantiate_typespec(lhs, opt_decl_t, tmp_tv_ctx, mode)?,
-                self.instantiate_typespec(rhs, opt_decl_t, tmp_tv_ctx, mode)?,
-            )),
             TypeSpec::Array(arr) => {
                 let elem_t = self.instantiate_typespec(&arr.ty, opt_decl_t, tmp_tv_ctx, mode)?;
                 let len = self.instantiate_const_expr(&arr.len);
@@ -945,13 +1016,14 @@ impl Context {
                     *pt.typ_mut() = self.instantiate_t(mem::take(pt.typ_mut()), tmp_tv_ctx, loc)?;
                 }
                 let return_t = self.instantiate_t(*subr.return_t, tmp_tv_ctx, loc)?;
-                Ok(subr_t(
+                let res = subr_t(
                     subr.kind,
                     subr.non_default_params,
                     subr.var_params.map(|p| *p),
                     subr.default_params,
                     return_t,
-                ))
+                );
+                Ok(res)
             }
             Record(mut dict) => {
                 for v in dict.values_mut() {
@@ -1007,12 +1079,12 @@ impl Context {
             And(l, r) => {
                 let l = self.instantiate_t(*l, tmp_tv_ctx, loc)?;
                 let r = self.instantiate_t(*r, tmp_tv_ctx, loc)?;
-                Ok(and(l, r))
+                Ok(self.intersection(&l, &r))
             }
             Or(l, r) => {
                 let l = self.instantiate_t(*l, tmp_tv_ctx, loc)?;
                 let r = self.instantiate_t(*r, tmp_tv_ctx, loc)?;
-                Ok(or(l, r))
+                Ok(self.union(&l, &r))
             }
             Not(l, r) => {
                 let l = self.instantiate_t(*l, tmp_tv_ctx, loc)?;
diff --git a/compiler/erg_compiler/context/mod.rs b/compiler/erg_compiler/context/mod.rs
index aba208b1..19519c76 100644
--- a/compiler/erg_compiler/context/mod.rs
+++ b/compiler/erg_compiler/context/mod.rs
@@ -23,6 +23,7 @@ use erg_common::config::ErgConfig;
 use erg_common::dict::Dict;
 use erg_common::error::Location;
 use erg_common::impl_display_from_debug;
+use erg_common::set::Set;
 use erg_common::traits::{Locational, Stream};
 use erg_common::vis::Visibility;
 use erg_common::Str;
@@ -274,15 +275,17 @@ pub enum RegistrationMode {
     Normal,
 }
 
+/// Some Erg functions require additional operation by the compiler.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub enum ImportKind {
-    ErgImport,
+pub enum OperationKind {
+    Import,
     PyImport,
+    Del,
 }
 
-impl ImportKind {
+impl OperationKind {
     pub const fn is_erg_import(&self) -> bool {
-        matches!(self, Self::ErgImport)
+        matches!(self, Self::Import)
     }
     pub const fn is_py_import(&self) -> bool {
         matches!(self, Self::PyImport)
@@ -294,6 +297,31 @@ pub struct ContextInfo {
     mod_id: usize,
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct MethodType {
+    definition_type: Type,
+    method_type: Type,
+}
+
+impl fmt::Display for MethodType {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            f,
+            "{{ def: {} t: {} }}",
+            self.definition_type, self.method_type
+        )
+    }
+}
+
+impl MethodType {
+    pub const fn new(definition_type: Type, method_type: Type) -> Self {
+        Self {
+            definition_type,
+            method_type,
+        }
+    }
+}
+
 /// Represents the context of the current scope
 ///
 /// Recursive functions/methods are highlighted with the prefix `rec_`, as performance may be significantly degraded.
@@ -317,8 +345,10 @@ pub struct Context {
     // method definitions, if the context is a type
     // specializations are included and needs to be separated out
     pub(crate) methods_list: Vec<(ClassDefType, Context)>,
-    // K: method name, V: trait defines the method
-    pub(crate) method_traits: Dict<Str, Vec<Type>>,
+    // K: method name, V: types defines the method
+    // If it is declared in a trait, it takes precedence over the class.
+    pub(crate) method_to_traits: Dict<Str, Vec<MethodType>>,
+    pub(crate) method_to_classes: Dict<Str, Vec<MethodType>>,
     /// K: method name, V: impl patch
     /// Provided methods can switch implementations on a scope-by-scope basis
     /// K: メソッド名, V: それを実装するパッチたち
@@ -327,7 +357,7 @@ pub struct Context {
     /// K: name of a trait, V: (type, monomorphised trait that the type implements)
     /// K: トレイトの名前, V: (型, その型が実装する単相化トレイト)
     /// e.g. { "Named": [(Type, Named), (Func, Named), ...], "Add": [(Nat, Add(Nat)), (Int, Add(Int)), ...], ... }
-    pub(crate) trait_impls: Dict<Str, Vec<TraitInstance>>,
+    pub(crate) trait_impls: Dict<Str, Set<TraitInstance>>,
     /// stores declared names (not initialized)
     pub(crate) decls: Dict<VarName, VarInfo>,
     // stores defined names
@@ -456,7 +486,8 @@ impl Context {
             super_traits: vec![],
             methods_list: vec![],
             const_param_defaults: Dict::default(),
-            method_traits: Dict::default(),
+            method_to_traits: Dict::default(),
+            method_to_classes: Dict::default(),
             method_impl_patches: Dict::default(),
             trait_impls: Dict::default(),
             params: params_,
@@ -871,15 +902,28 @@ impl Context {
 /// for language server
 impl Context {
     pub fn dir(&self) -> Vec<(&VarName, &VarInfo)> {
-        let mut vars: Vec<_> = self.locals.iter().collect();
+        let mut vars: Vec<_> = self
+            .locals
+            .iter()
+            .chain(self.methods_list.iter().flat_map(|(_, ctx)| ctx.dir()))
+            .collect();
         if let Some(outer) = self.get_outer() {
             vars.extend(outer.dir());
-        } else {
-            vars.extend(self.get_builtins().unwrap().locals.iter());
+        } else if let Some(builtins) = self.get_builtins() {
+            vars.extend(builtins.locals.iter());
         }
         vars
     }
 
+    pub fn get_receiver_ctx(&self, receiver_name: &str) -> Option<&Context> {
+        self.get_mod(receiver_name)
+            .or_else(|| {
+                let (_, vi) = self.get_var_info(receiver_name).ok()?;
+                self.get_nominal_type_ctx(&vi.t).map(|(_, ctx)| ctx)
+            })
+            .or_else(|| self.rec_get_type(receiver_name).map(|(_, ctx)| ctx))
+    }
+
     pub fn get_var_info(&self, name: &str) -> SingleTyCheckResult<(&VarName, &VarInfo)> {
         if let Some(info) = self.get_local_kv(name) {
             Ok(info)
diff --git a/compiler/erg_compiler/context/register.rs b/compiler/erg_compiler/context/register.rs
index 781931ba..9d9ff432 100644
--- a/compiler/erg_compiler/context/register.rs
+++ b/compiler/erg_compiler/context/register.rs
@@ -15,16 +15,17 @@ use erg_parser::ast;
 
 use erg_type::constructors::{func, func1, proc, ref_, ref_mut, v_enum};
 use erg_type::value::{GenTypeObj, TypeKind, TypeObj, ValueObj};
-use erg_type::{ParamTy, SubrType, TyBound, Type};
+use erg_type::{ParamTy, SubrType, Type};
 
 use crate::build_hir::HIRBuilder;
 use crate::context::{
-    ClassDefType, Context, ContextKind, DefaultInfo, RegistrationMode, TraitInstance,
+    ClassDefType, Context, ContextKind, DefaultInfo, MethodType, RegistrationMode, TraitInstance,
 };
 use crate::error::readable_name;
 use crate::error::{
     CompileResult, SingleTyCheckResult, TyCheckError, TyCheckErrors, TyCheckResult,
 };
+use crate::hir;
 use crate::hir::Literal;
 use crate::mod_cache::SharedModuleCache;
 use crate::varinfo::{Mutability, ParamIdx, VarInfo, VarKind};
@@ -33,7 +34,7 @@ use RegistrationMode::*;
 use Visibility::*;
 
 use super::instantiate::TyVarContext;
-use super::ImportKind;
+use super::OperationKind;
 
 impl Context {
     /// If it is a constant that is defined, there must be no variable of the same name defined across all scopes
@@ -347,12 +348,13 @@ impl Context {
         sig: &ast::SubrSignature,
         id: DefId,
         body_t: &Type,
-    ) -> TyCheckResult<()> {
+    ) -> TyCheckResult<Type> {
         // already defined as const
         if sig.is_const() {
             let vi = self.decls.remove(sig.ident.inspect()).unwrap();
+            let t = vi.t.clone();
             self.locals.insert(sig.ident.name.clone(), vi);
-            return Ok(());
+            return Ok(t);
         }
         let muty = if sig.ident.is_const() {
             Mutability::Const
@@ -442,9 +444,10 @@ impl Context {
             VarKind::Defined(id),
             Some(comptime_decos),
         );
-        log!(info "Registered {}::{name}: {}", self.name, &vi.t);
+        let t = vi.t.clone();
+        log!(info "Registered {}::{name}: {}", self.name, t);
         self.locals.insert(name.clone(), vi);
-        Ok(())
+        Ok(t)
     }
 
     pub(crate) fn fake_subr_assign(&mut self, sig: &ast::SubrSignature, failure_t: Type) {
@@ -632,10 +635,12 @@ impl Context {
             ))
         } else {
             match obj {
-                ValueObj::Type(t) => {
-                    let gen = enum_unwrap!(t, TypeObj::Generated);
-                    self.register_gen_type(ident, gen);
-                }
+                ValueObj::Type(t) => match t {
+                    TypeObj::Generated(gen) => {
+                        self.register_gen_type(ident, gen);
+                    }
+                    TypeObj::Builtin(_t) => panic!("aliasing bug"),
+                },
                 // TODO: not all value objects are comparable
                 other => {
                     let id = DefId(get_hash(ident));
@@ -834,20 +839,32 @@ impl Context {
                 .insert(name.clone(), ValueObj::Type(TypeObj::Generated(gen)));
             for impl_trait in ctx.super_traits.iter() {
                 if let Some(impls) = self.trait_impls.get_mut(&impl_trait.name()) {
-                    impls.push(TraitInstance::new(t.clone(), impl_trait.clone()));
+                    impls.insert(TraitInstance::new(t.clone(), impl_trait.clone()));
                 } else {
                     self.trait_impls.insert(
                         impl_trait.name(),
-                        vec![TraitInstance::new(t.clone(), impl_trait.clone())],
+                        set![TraitInstance::new(t.clone(), impl_trait.clone())],
                     );
                 }
             }
-            for method in ctx.decls.keys() {
-                if let Some(impls) = self.method_traits.get_mut(method.inspect()) {
-                    impls.push(t.clone());
+            for (trait_method, vi) in ctx.decls.iter() {
+                if let Some(types) = self.method_to_traits.get_mut(trait_method.inspect()) {
+                    types.push(MethodType::new(t.clone(), vi.t.clone()));
                 } else {
-                    self.method_traits
-                        .insert(method.inspect().clone(), vec![t.clone()]);
+                    self.method_to_traits.insert(
+                        trait_method.inspect().clone(),
+                        vec![MethodType::new(t.clone(), vi.t.clone())],
+                    );
+                }
+            }
+            for (class_method, vi) in ctx.locals.iter() {
+                if let Some(types) = self.method_to_classes.get_mut(class_method.inspect()) {
+                    types.push(MethodType::new(t.clone(), vi.t.clone()));
+                } else {
+                    self.method_to_classes.insert(
+                        class_method.inspect().clone(),
+                        vec![MethodType::new(t.clone(), vi.t.clone())],
+                    );
                 }
             }
             self.mono_types.insert(name.clone(), (t, ctx));
@@ -856,7 +873,7 @@ impl Context {
 
     pub(crate) fn import_mod(
         &mut self,
-        kind: ImportKind,
+        kind: OperationKind,
         mod_name: &Literal,
     ) -> CompileResult<PathBuf> {
         if kind.is_erg_import() {
@@ -1031,11 +1048,32 @@ impl Context {
         Ok(path)
     }
 
-    pub(crate) fn _push_subtype_bound(&mut self, sub: Type, sup: Type) {
-        self.bounds.push(TyBound::subtype_of(sub, sup));
-    }
-
-    pub(crate) fn _push_instance_bound(&mut self, name: Str, t: Type) {
-        self.bounds.push(TyBound::instance(name, t));
+    pub fn del(&mut self, ident: &hir::Identifier) -> CompileResult<()> {
+        if self.rec_get_const_obj(ident.inspect()).is_some()
+            || self
+                .get_builtins()
+                .unwrap()
+                .get_local_kv(ident.inspect())
+                .is_some()
+        {
+            Err(TyCheckErrors::from(TyCheckError::del_error(
+                self.cfg.input.clone(),
+                line!() as usize,
+                ident,
+                self.caused_by(),
+            )))
+        } else if self.locals.get(ident.inspect()).is_some() {
+            self.locals.remove(ident.inspect());
+            Ok(())
+        } else {
+            Err(TyCheckErrors::from(TyCheckError::no_var_error(
+                self.cfg.input.clone(),
+                line!() as usize,
+                ident.loc(),
+                self.caused_by(),
+                ident.inspect(),
+                self.get_similar_name(ident.inspect()),
+            )))
+        }
     }
 }
diff --git a/compiler/erg_compiler/context/test.rs b/compiler/erg_compiler/context/test.rs
index fa4fe312..8626ef90 100644
--- a/compiler/erg_compiler/context/test.rs
+++ b/compiler/erg_compiler/context/test.rs
@@ -32,9 +32,9 @@ impl Context {
     pub fn test_resolve_trait_inner1(&self) -> Result<(), ()> {
         let name = Str::ever("Add");
         let params = vec![TyParam::t(Nat)];
-        let maybe_trait = builtin_poly(name.clone(), params);
+        let maybe_trait = builtin_poly(name, params);
         let mut min = Type::Obj;
-        for pair in self.rec_get_trait_impls(&name) {
+        for pair in self.get_trait_impls(&maybe_trait) {
             if self.supertype_of(&pair.sup_trait, &maybe_trait) {
                 min = self.min(&min, &pair.sub_type).unwrap_or(&min).clone();
             }
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index b4f42aa7..1ebe98fa 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -120,15 +120,31 @@ impl Context {
             // TODO: Polymorphic generalization
             FreeVar(fv) if fv.level().unwrap() > self.level => match &*fv.borrow() {
                 FreeKind::Unbound { id, constraint, .. } => {
-                    let name = format!("%{id}");
-                    self.generalize_constraint(&name, constraint, bounds, lazy_inits);
-                    mono_q(name)
+                    // |Int <: T <: Int| T -> T ==> Int -> Int
+                    let (l, r) = constraint.get_sub_sup().unwrap();
+                    if l == r {
+                        fv.forced_link(&l.clone());
+                        FreeVar(fv.clone())
+                    } else if r != &Obj && self.is_class(r) {
+                        // x: T <: Bool ==> x: Bool
+                        r.clone()
+                    } else {
+                        let name = format!("%{id}");
+                        self.generalize_constraint(&name, constraint, bounds, lazy_inits);
+                        mono_q(name)
+                    }
                 }
                 FreeKind::NamedUnbound {
                     name, constraint, ..
                 } => {
-                    self.generalize_constraint(name, constraint, bounds, lazy_inits);
-                    mono_q(name)
+                    let (l, r) = constraint.get_sub_sup().unwrap();
+                    if l == r {
+                        fv.forced_link(l);
+                        FreeVar(fv.clone())
+                    } else {
+                        self.generalize_constraint(name, constraint, bounds, lazy_inits);
+                        mono_q(name)
+                    }
                 }
                 _ => assume_unreachable!(),
             },
@@ -182,6 +198,23 @@ impl Context {
                 let lhs = self.generalize_t_inner(*lhs, bounds, lazy_inits);
                 mono_proj(lhs, rhs)
             }
+            And(l, r) => {
+                let l = self.generalize_t_inner(*l, bounds, lazy_inits);
+                let r = self.generalize_t_inner(*r, bounds, lazy_inits);
+                // not `self.intersection` because types are generalized
+                and(l, r)
+            }
+            Or(l, r) => {
+                let l = self.generalize_t_inner(*l, bounds, lazy_inits);
+                let r = self.generalize_t_inner(*r, bounds, lazy_inits);
+                // not `self.union` because types are generalized
+                or(l, r)
+            }
+            Not(l, r) => {
+                let l = self.generalize_t_inner(*l, bounds, lazy_inits);
+                let r = self.generalize_t_inner(*r, bounds, lazy_inits);
+                not(l, r)
+            }
             // REVIEW: その他何でもそのまま通していいのか?
             other => other,
         }
@@ -312,6 +345,12 @@ impl Context {
                 let constraint = fv.crack_constraint();
                 let (sub_t, super_t) = constraint.get_sub_sup().unwrap();
                 if self.level <= fv.level().unwrap() {
+                    /*if self.is_trait(sub_t) {
+                        self.check_trait_exists(sub_t, loc)?;
+                    }*/
+                    if self.is_trait(super_t) {
+                        self.check_trait_impl(sub_t, super_t, loc)?;
+                    }
                     // REVIEW: Even if type constraints can be satisfied, implementation may not exist
                     if self.subtype_of(sub_t, super_t) {
                         match variance {
@@ -472,6 +511,58 @@ impl Context {
         }
     }
 
+    pub(crate) fn trait_impl_exists(&self, class: &Type, trait_: &Type) -> bool {
+        let mut super_exists = false;
+        for inst in self.get_trait_impls(trait_).into_iter() {
+            if self.supertype_of(&inst.sub_type, class)
+                && self.supertype_of(&inst.sup_trait, trait_)
+            {
+                super_exists = true;
+                break;
+            }
+        }
+        super_exists
+    }
+
+    fn check_trait_impl(
+        &self,
+        class: &Type,
+        trait_: &Type,
+        loc: Location,
+    ) -> SingleTyCheckResult<()> {
+        if !self.trait_impl_exists(class, trait_) {
+            Err(TyCheckError::no_trait_impl_error(
+                self.cfg.input.clone(),
+                line!() as usize,
+                class,
+                trait_,
+                loc,
+                self.caused_by(),
+                None,
+            ))
+        } else {
+            Ok(())
+        }
+    }
+
+    /// Fix type variables at their lower bound
+    pub(crate) fn coerce(&self, t: &Type) {
+        match t {
+            Type::FreeVar(fv) if fv.is_linked() => {
+                self.coerce(&fv.crack());
+            }
+            Type::FreeVar(fv) if fv.is_unbound() => {
+                let (sub, _sup) = fv.get_bound_types().unwrap();
+                fv.link(&sub);
+            }
+            Type::And(l, r) | Type::Or(l, r) | Type::Not(l, r) => {
+                self.coerce(l);
+                self.coerce(r);
+            }
+            _ => {}
+        }
+    }
+
     /// Check if all types are resolvable (if traits, check if an implementation exists)
     /// And replace them if resolvable
     pub(crate) fn resolve(
@@ -602,17 +693,23 @@ impl Context {
                 Ok(())
             }
             hir::Expr::Def(def) => {
-                match &mut def.sig {
-                    hir::Signature::Var(var) => {
-                        var.t = self.deref_tyvar(mem::take(&mut var.t), Covariant, var.loc())?;
+                // It is not possible to further dereference the quantified type.
+                // TODO: However, it is possible that there are external type variables within the quantified type.
+                if !def.sig.ref_t().is_quantified() {
+                    match &mut def.sig {
+                        hir::Signature::Var(var) => {
+                            var.t =
+                                self.deref_tyvar(mem::take(&mut var.t), Covariant, var.loc())?;
+                        }
+                        hir::Signature::Subr(subr) => {
+                            subr.t =
+                                self.deref_tyvar(mem::take(&mut subr.t), Covariant, subr.loc())?;
+                        }
                     }
-                    hir::Signature::Subr(subr) => {
-                        subr.t = self.deref_tyvar(mem::take(&mut subr.t), Covariant, subr.loc())?;
+                    for chunk in def.body.block.iter_mut() {
+                        self.resolve_expr_t(chunk)?;
                     }
                 }
-                for chunk in def.body.block.iter_mut() {
-                    self.resolve_expr_t(chunk)?;
-                }
                 Ok(())
             }
             hir::Expr::Lambda(lambda) => {
@@ -1158,29 +1255,15 @@ 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 {
-                                Cyclicity::Super => self.cyclic_supertype_of(rfv, maybe_sub),
-                                Cyclicity::Not => self.supertype_of(sup, maybe_sub),
-                                _ => todo!(),
-                            };
-                            if !judge {
-                                return Err(TyCheckErrors::from(TyCheckError::subtyping_error(
-                                    self.cfg.input.clone(),
-                                    line!() as usize,
-                                    maybe_sub,
-                                    sup, // TODO: this?
-                                    sub_loc,
-                                    sup_loc,
-                                    self.caused_by(),
-                                )));
-                            }*/
-                            if let Some(new_sub) = self.max(maybe_sub, sub) {
+                            /*if let Some(new_sub) = self.max(maybe_sub, sub) {
                                 *constraint =
                                     Constraint::new_sandwiched(new_sub.clone(), mem::take(sup), *cyclicity);
-                            } else {
-                                let new_sub = self.union(maybe_sub, sub);
-                                *constraint = Constraint::new_sandwiched(new_sub, mem::take(sup), *cyclicity);
-                            }
+                            } else {*/
+                            erg_common::log!(err "{maybe_sub}, {sub}");
+                            let new_sub = self.union(maybe_sub, sub);
+                            erg_common::log!(err "{new_sub}");
+                            *constraint = Constraint::new_sandwiched(new_sub, mem::take(sup), *cyclicity);
+                            // }
                         }
                         // sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
                         Constraint::TypeOf(ty) => {
@@ -1212,18 +1295,7 @@ 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 } => {
-                            // 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,
-                                    sub,
-                                    maybe_sup,
-                                    sub_loc,
-                                    sup_loc,
-                                    self.caused_by(),
-                                )));
-                            }*/
+                            // REVIEW: correct?
                             if let Some(new_sup) = self.min(sup, maybe_sup) {
                                 *constraint =
                                     Constraint::new_sandwiched(mem::take(sub), new_sup.clone(), *cyclicity);
@@ -1331,6 +1403,20 @@ impl Context {
                 }
                 Ok(())
             }
+            (Type::And(l, r), _)
+            | (Type::Or(l, r), _)
+            | (Type::Not(l, r), _) => {
+                self.sub_unify(l, maybe_sup, loc, param_name)?;
+                self.sub_unify(r, maybe_sup, loc, param_name)?;
+                Ok(())
+            }
+            (_, Type::And(l, r))
+            | (_, Type::Or(l, r))
+            | (_, Type::Not(l, r)) => {
+                self.sub_unify(maybe_sub, l, loc, param_name)?;
+                self.sub_unify(maybe_sub, r, loc, param_name)?;
+                Ok(())
+            }
             (_, Type::Ref(t)) => {
                 self.sub_unify(maybe_sub, t, loc, param_name)?;
                 Ok(())
diff --git a/compiler/erg_compiler/effectcheck.rs b/compiler/erg_compiler/effectcheck.rs
index d29166d3..0a8c96ab 100644
--- a/compiler/erg_compiler/effectcheck.rs
+++ b/compiler/erg_compiler/effectcheck.rs
@@ -9,8 +9,10 @@ use erg_common::vis::Visibility;
 use erg_common::Str;
 use Visibility::*;
 
+use erg_type::HasType;
+
 use crate::error::{EffectError, EffectErrors};
-use crate::hir::{Accessor, Array, Def, Expr, Signature, Tuple, HIR};
+use crate::hir::{Array, Def, Expr, Signature, Tuple, HIR};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 enum BlockKind {
@@ -208,8 +210,22 @@ impl SideEffectChecker {
                 self.block_stack.push(ConstInstant);
             }
         }
-        for chunk in def.body.block.iter() {
+        let last_idx = def.body.block.len() - 1;
+        for (i, chunk) in def.body.block.iter().enumerate() {
             self.check_expr(chunk);
+            // e.g. `echo = print!`
+            if i == last_idx
+                && self.block_stack.last().unwrap() == &Instant
+                && !def.sig.is_procedural()
+                && chunk.t().is_procedural()
+            {
+                self.errs.push(EffectError::proc_assign_error(
+                    self.cfg.input.clone(),
+                    line!() as usize,
+                    &def.sig,
+                    self.full_path(),
+                ));
+            }
         }
         self.path_stack.pop();
         self.block_stack.pop();
@@ -290,7 +306,7 @@ impl SideEffectChecker {
             },
             // 引数がproceduralでも関数呼び出しなら副作用なし
             Expr::Call(call) => {
-                if (self.is_procedural(&call.obj)
+                if (call.obj.t().is_procedural()
                     || call
                         .method_name
                         .as_ref()
@@ -340,19 +356,4 @@ impl SideEffectChecker {
             _ => {}
         }
     }
-
-    fn is_procedural(&self, expr: &Expr) -> bool {
-        match expr {
-            Expr::Lambda(lambda) => lambda.is_procedural(),
-            // 引数がproceduralでも関数呼び出しなら副作用なし
-            Expr::Call(call) => self.is_procedural(&call.obj),
-            Expr::Accessor(Accessor::Ident(ident)) => ident.name.is_procedural(),
-            // procedural: x.y! (e.g. Array.sample!)
-            // !procedural: !x.y
-            Expr::Accessor(Accessor::Attr(attr)) => attr.ident.is_procedural(),
-            Expr::Accessor(_) => todo!(),
-            Expr::TypeAsc(tasc) => self.is_procedural(&tasc.expr),
-            _ => false,
-        }
-    }
 }
diff --git a/compiler/erg_compiler/error.rs b/compiler/erg_compiler/error.rs
index 28de3cab..023449ad 100644
--- a/compiler/erg_compiler/error.rs
+++ b/compiler/erg_compiler/error.rs
@@ -16,7 +16,7 @@ use erg_parser::error::{ParserRunnerError, ParserRunnerErrors};
 
 use erg_type::{Predicate, Type};
 
-use crate::hir::Expr;
+use crate::hir::{Expr, Identifier, Signature};
 
 /// dname is for "double under name"
 pub fn binop_to_dname(op: &str) -> &str {
@@ -755,6 +755,33 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"
         )
     }
 
+    pub fn no_trait_impl_error(
+        input: Input,
+        errno: usize,
+        class: &Type,
+        trait_: &Type,
+        loc: Location,
+        caused_by: AtomicStr,
+        hint: Option<AtomicStr>,
+    ) -> Self {
+        Self::new(
+            ErrorCore::new(
+                errno,
+                TypeError,
+                loc,
+                switch_lang!(
+                    "japanese" => format!("{class}は{trait_}を実装していません"),
+                    "simplified_chinese" => format!("{class}没有实现{trait_}"),
+                    "traditional_chinese" => format!("{class}沒有實現{trait_}"),
+                    "english" => format!("{class} does not implement {trait_}"),
+                ),
+                hint,
+            ),
+            input,
+            caused_by,
+        )
+    }
+
     pub fn method_definition_error(
         input: Input,
         errno: usize,
@@ -992,6 +1019,38 @@ impl EffectError {
             caused_by.into(),
         )
     }
+
+    pub fn proc_assign_error<S: Into<AtomicStr>>(
+        input: Input,
+        errno: usize,
+        sig: &Signature,
+        caused_by: S,
+    ) -> Self {
+        Self::new(
+            ErrorCore::new(
+                errno,
+                HasEffect,
+                sig.loc(),
+                switch_lang!(
+                    "japanese" => "プロシージャを通常の変数に代入することはできません",
+                    "simplified_chinese" => "不能将过程赋值给普通变量",
+                    "traditional_chinese" => "不能將過程賦值給普通變量",
+                    "english" => "cannot assign a procedure to a normal variable",
+                ),
+                Some(
+                    switch_lang!(
+                        "japanese" => "変数の末尾に`!`をつけてください",
+                        "simplified_chinese" => "请在变量名后加上`!`",
+                        "traditional_chinese" => "請在變量名後加上`!`",
+                        "english" => "add `!` to the end of the variable name",
+                    )
+                    .into(),
+                ),
+            ),
+            input,
+            caused_by.into(),
+        )
+    }
 }
 
 pub type OwnershipError = TyCheckError;
@@ -1305,6 +1364,26 @@ impl LowerError {
         )
     }
 
+    pub fn del_error(input: Input, errno: usize, ident: &Identifier, caused_by: AtomicStr) -> Self {
+        let name = readable_name(ident.inspect());
+        Self::new(
+            ErrorCore::new(
+                errno,
+                NameError,
+                ident.loc(),
+                switch_lang!(
+                    "japanese" => format!("{YELLOW}{name}{RESET}は削除できません"),
+                    "simplified_chinese" => format!("{YELLOW}{name}{RESET}不能删除"),
+                    "traditional_chinese" => format!("{YELLOW}{name}{RESET}不能刪除"),
+                    "english" => format!("{YELLOW}{name}{RESET} cannot be deleted"),
+                ),
+                None,
+            ),
+            input,
+            caused_by,
+        )
+    }
+
     pub fn visibility_error(
         input: Input,
         errno: usize,
diff --git a/compiler/erg_compiler/hir.rs b/compiler/erg_compiler/hir.rs
index 2ce5059c..b14541a4 100644
--- a/compiler/erg_compiler/hir.rs
+++ b/compiler/erg_compiler/hir.rs
@@ -20,7 +20,7 @@ use erg_type::value::{TypeKind, ValueObj};
 use erg_type::{impl_t, impl_t_for_enum, HasType, Type};
 
 use crate::context::eval::type_from_token_kind;
-use crate::context::ImportKind;
+use crate::context::OperationKind;
 use crate::error::readable_name;
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
@@ -1085,10 +1085,11 @@ impl Call {
         }
     }
 
-    pub fn import_kind(&self) -> Option<ImportKind> {
+    pub fn additional_operation(&self) -> Option<OperationKind> {
         self.obj.show_acc().and_then(|s| match &s[..] {
-            "import" => Some(ImportKind::ErgImport),
-            "pyimport" | "py" => Some(ImportKind::PyImport),
+            "import" => Some(OperationKind::Import),
+            "pyimport" | "py" => Some(OperationKind::PyImport),
+            "Del" => Some(OperationKind::Del),
             _ => None,
         })
     }
diff --git a/compiler/erg_compiler/link.rs b/compiler/erg_compiler/link.rs
index ceae6667..98ac3ed3 100644
--- a/compiler/erg_compiler/link.rs
+++ b/compiler/erg_compiler/link.rs
@@ -14,7 +14,7 @@ use erg_type::typaram::TyParam;
 use erg_type::value::ValueObj;
 use erg_type::{HasType, Type};
 
-use crate::context::ImportKind;
+use crate::context::OperationKind;
 use crate::hir::*;
 use crate::mod_cache::SharedModuleCache;
 
@@ -94,14 +94,14 @@ impl<'a> Linker<'a> {
             Expr::UnaryOp(unaryop) => {
                 self.replace_import(&mut unaryop.expr);
             }
-            Expr::Call(call) => match call.import_kind() {
-                Some(ImportKind::ErgImport) => {
+            Expr::Call(call) => match call.additional_operation() {
+                Some(OperationKind::Import) => {
                     self.replace_erg_import(expr);
                 }
-                Some(ImportKind::PyImport) => {
+                Some(OperationKind::PyImport) => {
                     self.replace_py_import(expr);
                 }
-                None => {
+                _ => {
                     for arg in call.args.pos_args.iter_mut() {
                         self.replace_import(&mut arg.expr);
                     }
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index 73935f64..4d97c83c 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -5,6 +5,7 @@
 use erg_common::astr::AtomicStr;
 use erg_common::config::ErgConfig;
 use erg_common::error::{Location, MultiErrorDisplay};
+use erg_common::set;
 use erg_common::set::Set;
 use erg_common::traits::{Locational, Runnable, Stream};
 use erg_common::vis::Visibility;
@@ -24,7 +25,9 @@ use erg_type::value::{GenTypeObj, TypeKind, TypeObj, ValueObj};
 use erg_type::{HasType, ParamTy, Type};
 
 use crate::context::instantiate::TyVarContext;
-use crate::context::{ClassDefType, Context, ContextKind, RegistrationMode};
+use crate::context::{
+    ClassDefType, Context, ContextKind, OperationKind, RegistrationMode, TraitInstance,
+};
 use crate::error::{
     CompileError, CompileErrors, LowerError, LowerErrors, LowerResult, LowerWarning, LowerWarnings,
     SingleLowerResult,
@@ -252,7 +255,7 @@ impl ASTLowerer {
         let maybe_len = self.ctx.eval_const_expr(len, None);
         match maybe_len {
             Ok(v @ ValueObj::Nat(_)) => {
-                if elem.ref_t().is_mut() {
+                if elem.ref_t().is_mut_type() {
                     builtin_poly(
                         "ArrayWithMutType!",
                         vec![TyParam::t(elem.t()), TyParam::Value(v)],
@@ -262,7 +265,7 @@ impl ASTLowerer {
                 }
             }
             Ok(v @ ValueObj::Mut(_)) if v.class() == builtin_mono("Nat!") => {
-                if elem.ref_t().is_mut() {
+                if elem.ref_t().is_mut_type() {
                     builtin_poly(
                         "ArrayWithMutTypeAndLength!",
                         vec![TyParam::t(elem.t()), TyParam::Value(v)],
@@ -274,7 +277,7 @@ impl ASTLowerer {
             Ok(other) => todo!("{other} is not a Nat object"),
             // REVIEW: is it ok to ignore the error?
             Err(_e) => {
-                if elem.ref_t().is_mut() {
+                if elem.ref_t().is_mut_type() {
                     builtin_poly(
                         "ArrayWithMutType!",
                         vec![TyParam::t(elem.t()), TyParam::erased(Type::Nat)],
@@ -508,7 +511,7 @@ impl ASTLowerer {
                 self.ctx
                     .rec_get_var_t(&ident, &self.cfg.input, &self.ctx.name)?,
                 self.ctx
-                    .get_singular_ctx_from_ident(&ident, &self.ctx.name)
+                    .get_singular_ctx_by_ident(&ident, &self.ctx.name)
                     .ok()
                     .map(|ctx| ctx.name.clone()),
             )
@@ -581,11 +584,30 @@ impl ASTLowerer {
             None
         };
         let call = hir::Call::new(obj, method_name, hir_args, sig_t);
-        if let Some(kind) = call.import_kind() {
-            let mod_name = enum_unwrap!(call.args.get_left_or_key("Path").unwrap(), hir::Expr::Lit);
-            if let Err(errs) = self.ctx.import_mod(kind, mod_name) {
-                self.errs.extend(errs.into_iter());
-            };
+        match call.additional_operation() {
+            Some(kind @ (OperationKind::Import | OperationKind::PyImport)) => {
+                let mod_name =
+                    enum_unwrap!(call.args.get_left_or_key("Path").unwrap(), hir::Expr::Lit);
+                if let Err(errs) = self.ctx.import_mod(kind, mod_name) {
+                    self.errs.extend(errs.into_iter());
+                };
+            }
+            Some(OperationKind::Del) => match call.args.get_left_or_key("obj").unwrap() {
+                hir::Expr::Accessor(hir::Accessor::Ident(ident)) => {
+                    self.ctx.del(ident)?;
+                }
+                other => {
+                    return Err(LowerErrors::from(LowerError::syntax_error(
+                        self.input().clone(),
+                        line!() as usize,
+                        other.loc(),
+                        self.ctx.caused_by(),
+                        "",
+                        None,
+                    )))
+                }
+            },
+            _ => {}
         }
         Ok(call)
     }
@@ -824,13 +846,14 @@ impl ASTLowerer {
                     }
                 }
                 let id = body.id;
-                self.ctx
+                let t = self
+                    .ctx
                     .outer
                     .as_mut()
                     .unwrap()
                     .assign_subr(&sig, id, found_body_t)?;
                 let ident = hir::Identifier::bare(sig.ident.dot, sig.ident.name);
-                let sig = hir::SubrSignature::new(ident, sig.params, Type::Subr(t));
+                let sig = hir::SubrSignature::new(ident, sig.params, t);
                 let body = hir::DefBody::new(body.op, block, body.id);
                 Ok(hir::Def::new(hir::Signature::Subr(sig), body))
             }
@@ -939,6 +962,9 @@ impl ASTLowerer {
             match self.ctx.check_decls_and_pop() {
                 Ok(methods) => {
                     self.check_override(&class, &methods);
+                    if let Some((trait_, _)) = &impl_trait {
+                        self.register_trait_impl(&class, trait_);
+                    }
                     self.check_trait_impl(impl_trait, &class, &methods)?;
                     self.push_methods(class, methods);
                 }
@@ -1033,6 +1059,8 @@ impl ASTLowerer {
         }
     }
 
+    /// Inspect the Trait implementation for correctness,
+    /// i.e., check that all required attributes are defined and that no extra attributes are defined
     fn check_trait_impl(
         &mut self,
         impl_trait: Option<(Type, Location)>,
@@ -1127,6 +1155,18 @@ impl ASTLowerer {
         Ok(())
     }
 
+    fn register_trait_impl(&mut self, class: &Type, trait_: &Type) {
+        // TODO: polymorphic trait
+        if let Some(impls) = self.ctx.trait_impls.get_mut(&trait_.name()) {
+            impls.insert(TraitInstance::new(class.clone(), trait_.clone()));
+        } else {
+            self.ctx.trait_impls.insert(
+                trait_.name(),
+                set! {TraitInstance::new(class.clone(), trait_.clone())},
+            );
+        }
+    }
+
     fn push_methods(&mut self, class: Type, methods: Context) {
         let (_, class_root) = self.ctx.get_mut_nominal_type_ctx(&class).unwrap();
         for (newly_defined_name, _vi) in methods.locals.iter() {
diff --git a/compiler/erg_compiler/ownercheck.rs b/compiler/erg_compiler/ownercheck.rs
index 3c217267..b8637dec 100644
--- a/compiler/erg_compiler/ownercheck.rs
+++ b/compiler/erg_compiler/ownercheck.rs
@@ -212,7 +212,7 @@ impl OwnershipChecker {
                     self.errs.push(e);
                     return;
                 }
-                if acc.ref_t().is_mut() && ownership.is_owned() && !chunk {
+                if acc.ref_t().is_mut_type() && ownership.is_owned() && !chunk {
                     self.drop(ident);
                 }
             }
diff --git a/compiler/erg_parser/Cargo.toml b/compiler/erg_parser/Cargo.toml
index f4a08302..34d5be76 100644
--- a/compiler/erg_parser/Cargo.toml
+++ b/compiler/erg_parser/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_parser"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 description = "The Erg parser"
 authors = ["erg-lang team <moderation.erglang@gmail.com>"]
 license = "MIT OR Apache-2.0"
@@ -16,7 +16,7 @@ simplified_chinese = [ "erg_common/simplified_chinese" ]
 traditional_chinese = [ "erg_common/traditional_chinese" ]
 
 [dependencies]
-erg_common = { version = "0.5.6", path = "../erg_common" }
+erg_common = { version = "0.5.7-nightly.1", path = "../erg_common" }
 
 [lib]
 path = "lib.rs"
diff --git a/compiler/erg_type/Cargo.toml b/compiler/erg_type/Cargo.toml
index 7a4fb5e4..beda3039 100644
--- a/compiler/erg_type/Cargo.toml
+++ b/compiler/erg_type/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_type"
-version = "0.5.6"
+version = "0.5.7-nightly.1"
 description = "APIs for Erg types"
 authors = ["erg-lang team <moderation.erglang@gmail.com>"]
 license = "MIT OR Apache-2.0"
@@ -18,8 +18,8 @@ simplified_chinese = [ "erg_common/simplified_chinese" ]
 traditional_chinese = [ "erg_common/traditional_chinese" ]
 
 [dependencies]
-erg_common = { version = "0.5.6", path = "../erg_common" }
-erg_parser = { version = "0.5.6", path = "../erg_parser" }
+erg_common = { version = "0.5.7-nightly.1", path = "../erg_common" }
+erg_parser = { version = "0.5.7-nightly.1", path = "../erg_parser" }
 
 [lib]
 path = "lib.rs"
diff --git a/compiler/erg_type/constructors.rs b/compiler/erg_type/constructors.rs
index 71ffb440..9ddeeee4 100644
--- a/compiler/erg_type/constructors.rs
+++ b/compiler/erg_type/constructors.rs
@@ -3,10 +3,15 @@ use std::convert::TryInto;
 use crate::*;
 
 #[inline]
-pub const fn param_t(name: &'static str, ty: Type) -> ParamTy {
+pub const fn kw(name: &'static str, ty: Type) -> ParamTy {
     ParamTy::kw(Str::ever(name), ty)
 }
 
+#[inline]
+pub const fn kw_default(name: &'static str, ty: Type, default: Type) -> ParamTy {
+    ParamTy::kw_default(Str::ever(name), ty, default)
+}
+
 #[inline]
 pub const fn anon(ty: Type) -> ParamTy {
     ParamTy::anonymous(ty)
diff --git a/compiler/erg_type/free.rs b/compiler/erg_type/free.rs
index de2d57e3..eefc9e47 100644
--- a/compiler/erg_type/free.rs
+++ b/compiler/erg_type/free.rs
@@ -436,6 +436,16 @@ impl<T: Clone + HasLevel> Free<T> {
         *self.borrow_mut() = FreeKind::Linked(to.clone());
     }
 
+    pub fn forced_link(&self, to: &T) {
+        // prevent linking to self
+        if self.is_linked() && addr_eq!(*self.crack(), *to) {
+            return;
+        }
+        unsafe {
+            *self.as_ptr() = FreeKind::Linked(to.clone());
+        }
+    }
+
     pub fn undoable_link(&self, to: &T) {
         if self.is_linked() && addr_eq!(*self.crack(), *to) {
             panic!("link to self");
diff --git a/compiler/erg_type/lib.rs b/compiler/erg_type/lib.rs
index b9cf4495..3293ab55 100644
--- a/compiler/erg_type/lib.rs
+++ b/compiler/erg_type/lib.rs
@@ -724,6 +724,7 @@ impl Predicate {
 pub enum ParamTy {
     Pos { name: Option<Str>, ty: Type },
     Kw { name: Str, ty: Type },
+    KwWithDefault { name: Str, ty: Type, default: Type },
 }
 
 impl fmt::Display for ParamTy {
@@ -736,6 +737,9 @@ impl fmt::Display for ParamTy {
                 write!(f, ": {}", ty)
             }
             Self::Kw { name, ty } => write!(f, "{}: {}", name, ty),
+            Self::KwWithDefault { name, ty, default } => {
+                write!(f, "{}: {} := {}", name, ty, default)
+            }
         }
     }
 }
@@ -749,6 +753,10 @@ impl ParamTy {
         Self::Kw { name, ty }
     }
 
+    pub const fn kw_default(name: Str, ty: Type, default: Type) -> Self {
+        Self::KwWithDefault { name, ty, default }
+    }
+
     pub const fn anonymous(ty: Type) -> Self {
         Self::pos(None, ty)
     }
@@ -756,26 +764,27 @@ impl ParamTy {
     pub fn name(&self) -> Option<&Str> {
         match self {
             Self::Pos { name, .. } => name.as_ref(),
-            Self::Kw { name, .. } => Some(name),
+            Self::Kw { name, .. } | Self::KwWithDefault { name, .. } => Some(name),
         }
     }
 
     pub const fn typ(&self) -> &Type {
         match self {
-            Self::Pos { ty, .. } | Self::Kw { ty, .. } => ty,
+            Self::Pos { ty, .. } | Self::Kw { ty, .. } | Self::KwWithDefault { ty, .. } => ty,
         }
     }
 
     pub fn typ_mut(&mut self) -> &mut Type {
         match self {
-            Self::Pos { ty, .. } | Self::Kw { ty, .. } => ty,
+            Self::Pos { ty, .. } | Self::Kw { ty, .. } | Self::KwWithDefault { ty, .. } => ty,
         }
     }
 
-    pub fn deconstruct(self) -> (Option<Str>, Type) {
+    pub fn deconstruct(self) -> (Option<Str>, Type, Option<Type>) {
         match self {
-            Self::Pos { name, ty } => (name, ty),
-            Self::Kw { name, ty } => (Some(name), ty),
+            Self::Pos { name, ty } => (name, ty, None),
+            Self::Kw { name, ty } => (Some(name), ty, None),
+            Self::KwWithDefault { name, ty, default } => (Some(name), ty, Some(default)),
         }
     }
 }
@@ -931,11 +940,12 @@ impl LimitedDisplay for RefinementType {
             return write!(f, "...");
         }
         let first_subj = self.preds.iter().next().and_then(|p| p.subject());
-        if self
+        let is_simple_type = self.t.is_simple_class();
+        let is_simple_preds = self
             .preds
             .iter()
-            .all(|p| p.is_equal() && p.subject() == first_subj)
-        {
+            .all(|p| p.is_equal() && p.subject() == first_subj);
+        if is_simple_type && is_simple_preds {
             write!(f, "{{")?;
             for pred in self.preds.iter() {
                 let (_, rhs) = enum_unwrap!(pred, Predicate::Equal { lhs, rhs });
@@ -1684,11 +1694,25 @@ impl Type {
         }
     }
 
-    pub fn is_mut(&self) -> bool {
+    /// Procedure or MutType?
+    pub fn is_procedural(&self) -> bool {
+        match self {
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_procedural(),
+            Self::Callable { .. } => true,
+            Self::Subr(subr) if subr.kind == SubrKind::Proc => true,
+            Self::Refinement(refine) =>
+                refine.t.is_procedural() || refine.preds.iter().any(|pred|
+                    matches!(pred, Predicate::Equal{ rhs, .. } if pred.mentions(&refine.var) && rhs.name().map(|n| n.ends_with('!')).unwrap_or(false))
+                ),
+            _ => false,
+        }
+    }
+
+    pub fn is_mut_type(&self) -> bool {
         match self {
             Self::FreeVar(fv) => {
                 if fv.is_linked() {
-                    fv.crack().is_mut()
+                    fv.crack().is_mut_type()
                 } else {
                     fv.unbound_name().unwrap().ends_with('!')
                 }
@@ -1700,7 +1724,7 @@ impl Type {
             | Self::BuiltinPoly { name, .. }
             | Self::PolyQVar { name, .. }
             | Self::MonoProj { rhs: name, .. } => name.ends_with('!'),
-            Self::Refinement(refine) => refine.t.is_mut(),
+            Self::Refinement(refine) => refine.t.is_mut_type(),
             _ => false,
         }
     }
@@ -1730,6 +1754,14 @@ impl Type {
         }
     }
 
+    pub fn is_quantified(&self) -> bool {
+        match self {
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_quantified(),
+            Self::Quantified(_) => true,
+            _ => false,
+        }
+    }
+
     pub fn contains_tvar(&self, name: &str) -> bool {
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_tvar(name),
diff --git a/doc/EN/dev_guide/env.md b/doc/EN/dev_guide/env.md
index fe337e00..f0d1b348 100644
--- a/doc/EN/dev_guide/env.md
+++ b/doc/EN/dev_guide/env.md
@@ -9,6 +9,9 @@
 
 * [pre-commit](https://pre-commit.com/)
 
+We use pre-commit to have clippy check and test automatically.
+The checks may fail on the first run even if there are no bugs, in which case you should try committing again.
+
 * Python3 interpreter
 
 ## Recommendation
diff --git a/doc/JA/dev_guide/env.md b/doc/JA/dev_guide/env.md
index 6d69e356..a4537b6b 100644
--- a/doc/JA/dev_guide/env.md
+++ b/doc/JA/dev_guide/env.md
@@ -1,6 +1,6 @@
 # 開発環境
 
-[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3Ddoc/EN/dev_guide/env.md%26commit_hash%3D61d72afbbfdba8c2ca994499c7ec9f8fc01440cb)](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=doc/EN/dev_guide/env.md&commit_hash=61d72afbbfdba8c2ca994499c7ec9f8fc01440cb)
+[![badge](https://img.shields.io/endpoint.svg?url=https%3A%2F%2Fgezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com%2Fdefault%2Fsource_up_to_date%3Fowner%3Derg-lang%26repos%3Derg%26ref%3Dmain%26path%3Ddoc/EN/dev_guide/env.md%26commit_hash%3D735c840e681ad106795654212680696a2be29eee)](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=doc/EN/dev_guide/env.md&commit_hash=735c840e681ad106795654212680696a2be29eee)
 
 ## インストールが必要なもの
 
@@ -11,6 +11,9 @@
 
 * [pre-commit](https://pre-commit.com/)
 
+pre-commitを使ってclippyのチェックやテストを自動で行わせています。
+バグがなくても最初の実行でチェックが失敗する場合があります。その場合はもう一度コミットを試みてください。
+
 * Python3インタープリタ
 
 ## 推奨
diff --git a/doc/JA/syntax/12_dict.md b/doc/JA/syntax/12_dict.md
index 900ac84e..7b9f4231 100644
--- a/doc/JA/syntax/12_dict.md
+++ b/doc/JA/syntax/12_dict.md
@@ -5,7 +5,7 @@
 Dictはキーと値のペアを持つコレクションです。
 
 ```python
-ids = {"Alice": 145, "Bob": 214, "Charlie": 301}
+ids = {"Alice" >: 145, "Bob": 214, "Charlie": 301}
 assert ids["Alice"] == 145
 ```
 
diff --git a/doc/JA/syntax/type/advanced/default_param.md b/doc/JA/syntax/type/advanced/default_param.md
index 33309674..5bee3f0f 100644
--- a/doc/JA/syntax/type/advanced/default_param.md
+++ b/doc/JA/syntax/type/advanced/default_param.md
@@ -28,3 +28,12 @@ assert fold(g, [1, 2, 3]) == 8
 
 1番目は、デフォルト引数のある関数は、ない関数と同一視できる、という意味である。
 2番目は、任意のデフォルト引数は省略できる、という意味である。
+
+デフォルト引数の型は、引数を渡した場合と渡さなかった場合で変えることができる。
+具体的には、`if`関数の型などが良い例である。
+
+```python
+if: |T: Type, U: Type|(then: () -> T, else: () -> U := () -> NoneType) -> T or U
+```
+
+`if`関数は、`else`引数が与えられなければ`T or NoneType`を返す。
diff --git a/examples/side_effect.er b/examples/side_effect.er
index 237edf0a..4aaf9e43 100644
--- a/examples/side_effect.er
+++ b/examples/side_effect.er
@@ -7,3 +7,8 @@ if True, do:
 
 f x: Int = log x
 g x: Int = print! x # this should cause an effect error
+
+echo = print! # this should be an effect error
+_echo = # this is OK
+    print! 1
+    log
diff --git a/library/std/_prelude.er b/library/std/_prelude.er
new file mode 100644
index 00000000..0f8386ee
--- /dev/null
+++ b/library/std/_prelude.er
@@ -0,0 +1,82 @@
+@Attach NeImpl
+Eq(R := Self) = Trait {
+    .`==` = (self: Self, R) -> Bool
+}
+
+NeImpl R = Patch Eq R
+NeImpl(R).
+    `!=`(self, other: R): Bool = not(self == other)
+
+@Attach EqImpl, LeImpl, LtImpl, GeImpl, GtImpl
+PartialOrd(R := Self) = Trait {
+    .cmp = (self: Self, R) -> Option Ordering
+}
+Ord = Subsume PartialOrd()
+
+EqForOrd R = Patch Ord, Impl := Eq()
+EqForOrd(R).
+    `==`(self, other: R): Bool = self.cmp(other) == Ordering.Equal
+
+LeForOrd = Patch Ord
+LeForOrd.
+    `<=`(self, other: Self): Bool = self.cmp(other) == Ordering.Less or self == other
+LtForOrd = Patch Ord
+LtForOrd.
+    `<`(self, other: Self): Bool = self.cmp(other) == Ordering.Less
+GeForOrd = Patch Ord
+GeForOrd.
+    `>=`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater or self == other
+GtForOrd = Patch Ord
+GtForOrd.
+    `>`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater
+
+Add(R := Self) = Trait {
+    .Output = Type
+    .`_+_` = (self: Self, R) -> Self.Output
+}
+Sub(R := Self) = Trait {
+    .Output = Type
+    .`_-_` = (self: Self, R) -> Self.Output
+}
+Mul(R := Self()) = Trait {
+    .Output = Type
+    .`*` = (self: Self, R) -> Self.Output
+}
+Div(R := Self) = Trait {
+    .Output = Type
+    .`/` = (self: Self, R) -> Self.Output or Panic
+}
+Num: (R := Type) -> Type
+Num = Add and Sub and Mul
+
+Seq T = Trait {
+    .__len__ = (self: Ref(Self)) -> Nat
+    .get = (self: Ref(Self), Nat) -> T
+}
+
+`_+_`: |R: Type, A <: Add(R)| (A, R) -> A.AddO
+`_-_`: |R: Type, S <: Add(R)| (S, R) -> S.SubO
+`*`: |R, O: Type, M <: Add(R)| (M, R) -> M.MulO
+`/`: |R, O: Type, D <: Add(R)| (D, R) -> D.DivO
+
+AddForInt = Patch Int, Impl := Add()
+AddForInt.AddO = Int
+AddForInt.
+    `_+_`: (self: Self, other: Int) -> Int = magic("Add.`_+_`")
+
+# TODO: Mul and Div
+NumForInterval M, N, O, P: Int =
+    Patch M..N, Impl := Add(R := O..P) and Sub(R := O..P)
+NumForInterval(M, N, O, P).
+    `_+_`: (self: Self, other: O..P) -> M+O..N+P = magic("NumForInterval.`_+_`")
+    `_-_`: (self: Self, other: O..P) -> M-P..N-O = magic("NumForInterval.`_-_`")
+
+Read = Trait {
+    .read = (self: Ref(Self)) -> Str
+}
+Read! = Trait {
+    .read! = (self: Ref!(Self)) => Str
+}
+Write! = Trait {
+    .write! = (self: Ref!(Self), Str) => ()
+}
diff --git a/library/std/prelude.er b/library/std/prelude.er
index 0f8386ee..b0c0df8f 100644
--- a/library/std/prelude.er
+++ b/library/std/prelude.er
@@ -1,82 +1,12 @@
-@Attach NeImpl
-Eq(R := Self) = Trait {
-    .`==` = (self: Self, R) -> Bool
-}
+discard _x = None
 
-NeImpl R = Patch Eq R
-NeImpl(R).
-    `!=`(self, other: R): Bool = not(self == other)
+discard 1
 
-@Attach EqImpl, LeImpl, LtImpl, GeImpl, GtImpl
-PartialOrd(R := Self) = Trait {
-    .cmp = (self: Self, R) -> Option Ordering
-}
-Ord = Subsume PartialOrd()
+cond c, then, else =
+    if c:
+        do then
+        do else
 
-EqForOrd R = Patch Ord, Impl := Eq()
-EqForOrd(R).
-    `==`(self, other: R): Bool = self.cmp(other) == Ordering.Equal
-
-LeForOrd = Patch Ord
-LeForOrd.
-    `<=`(self, other: Self): Bool = self.cmp(other) == Ordering.Less or self == other
-LtForOrd = Patch Ord
-LtForOrd.
-    `<`(self, other: Self): Bool = self.cmp(other) == Ordering.Less
-GeForOrd = Patch Ord
-GeForOrd.
-    `>=`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater or self == other
-GtForOrd = Patch Ord
-GtForOrd.
-    `>`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater
-
-Add(R := Self) = Trait {
-    .Output = Type
-    .`_+_` = (self: Self, R) -> Self.Output
-}
-Sub(R := Self) = Trait {
-    .Output = Type
-    .`_-_` = (self: Self, R) -> Self.Output
-}
-Mul(R := Self()) = Trait {
-    .Output = Type
-    .`*` = (self: Self, R) -> Self.Output
-}
-Div(R := Self) = Trait {
-    .Output = Type
-    .`/` = (self: Self, R) -> Self.Output or Panic
-}
-Num: (R := Type) -> Type
-Num = Add and Sub and Mul
-
-Seq T = Trait {
-    .__len__ = (self: Ref(Self)) -> Nat
-    .get = (self: Ref(Self), Nat) -> T
-}
-
-`_+_`: |R: Type, A <: Add(R)| (A, R) -> A.AddO
-`_-_`: |R: Type, S <: Add(R)| (S, R) -> S.SubO
-`*`: |R, O: Type, M <: Add(R)| (M, R) -> M.MulO
-`/`: |R, O: Type, D <: Add(R)| (D, R) -> D.DivO
-
-AddForInt = Patch Int, Impl := Add()
-AddForInt.AddO = Int
-AddForInt.
-    `_+_`: (self: Self, other: Int) -> Int = magic("Add.`_+_`")
-
-# TODO: Mul and Div
-NumForInterval M, N, O, P: Int =
-    Patch M..N, Impl := Add(R := O..P) and Sub(R := O..P)
-NumForInterval(M, N, O, P).
-    `_+_`: (self: Self, other: O..P) -> M+O..N+P = magic("NumForInterval.`_+_`")
-    `_-_`: (self: Self, other: O..P) -> M-P..N-O = magic("NumForInterval.`_-_`")
-
-Read = Trait {
-    .read = (self: Ref(Self)) -> Str
-}
-Read! = Trait {
-    .read! = (self: Ref!(Self)) => Str
-}
-Write! = Trait {
-    .write! = (self: Ref!(Self), Str) => ()
-}
+assert cond(False, 1, 2) == 2
+# assert cond(True, 1, 3) == "a"
+# assert "a" == cond(True, 1, 3)
diff --git a/tests/add.er b/tests/add.er
deleted file mode 100644
index d939d349..00000000
--- a/tests/add.er
+++ /dev/null
@@ -1,5 +0,0 @@
-add x, y =
-    x + y
-
-print! 1 + 1
-print! 1.0 + 1
\ No newline at end of file
diff --git a/tests/addition.er b/tests/addition.er
new file mode 100644
index 00000000..60543168
--- /dev/null
+++ b/tests/addition.er
@@ -0,0 +1,7 @@
+add x, y =
+    x + y
+
+print! add(1, 1)
+print! add(1.0, 1)
+print! add("a", "b")
+print! add("a", 1) # this will be an error
diff --git a/tests/fizzbuzz.er b/tests/fizzbuzz.er
index 2368ddba..afcf9b73 100644
--- a/tests/fizzbuzz.er
+++ b/tests/fizzbuzz.er
@@ -1,6 +1,6 @@
-for! 1..100, i =>
+for! 1..<100, i =>
     match (i % 3, i % 5):
-        0, 0 => print! "FizzBuzz"
-        0, _ => print! "Fizz"
-        _, 0 => print! "Buzz"
-        _ => print! i
+        (0, 0) => print! "FizzBuzz"
+        (0, _) => print! "Fizz"
+        (_, 0) => print! "Buzz"
+        (_, _) => print! i
diff --git a/tests/infer_class.er b/tests/infer_class.er
new file mode 100644
index 00000000..513afe7e
--- /dev/null
+++ b/tests/infer_class.er
@@ -0,0 +1,14 @@
+_abs x =
+    x.abs() # currently this method only implemented for integers
+
+assert _abs(-1) == 1
+
+#[
+push! a, elem =
+    a.push!(elem)
+    a
+
+a = ![]
+b = push! a, 1
+print! b
+]#
diff --git a/tests/infer_trait.er b/tests/infer_trait.er
new file mode 100644
index 00000000..84afebab
--- /dev/null
+++ b/tests/infer_trait.er
@@ -0,0 +1,6 @@
+show s =
+    s.to_str()
+
+assert show(1) == "1"
+assert show(True) == "True"
+# discard show((x,) -> x)
diff --git a/tests/mut_array.er b/tests/mut_array.er
index 4e637175..9707ec7c 100644
--- a/tests/mut_array.er
+++ b/tests/mut_array.er
@@ -1,5 +1,5 @@
 v = ![]
-for! 0..10, i =>
+for! 0..<10, i =>
     v.push! i
 
 log v.sum()
diff --git a/tests/rec.er b/tests/rec.er
new file mode 100644
index 00000000..6e143cb4
--- /dev/null
+++ b/tests/rec.er
@@ -0,0 +1,10 @@
+stop_or_call n, f: (Nat -> Nat), g: (Nat -> Nat) =
+    cond n <= 0:
+        1
+        g (f (n - 1))
+
+fact(n: Nat): Nat =
+    stop_or_call n, fact, (r, ) -> r * n
+
+print! fact
+print! fact 5
diff --git a/tests/subtyping.er b/tests/subtyping.er
new file mode 100644
index 00000000..205c2577
--- /dev/null
+++ b/tests/subtyping.er
@@ -0,0 +1,6 @@
+f(x: Nat): Int = x
+y: Ratio = f 1
+# Erg's type checking does not necessarily enlarge the type. So this is OK.
+z: Int = y
+# But this is invalid.
+invalid: 10..<20 = z
diff --git a/tests/test.rs b/tests/test.rs
index c206cb21..2c53ef11 100644
--- a/tests/test.rs
+++ b/tests/test.rs
@@ -6,6 +6,11 @@ use erg_common::traits::Runnable;
 
 use erg::dummy::DummyVM;
 
+#[test]
+fn exec_addition() -> Result<(), ()> {
+    expect_failure("tests/addition.er")
+}
+
 #[test]
 fn exec_class() -> Result<(), ()> {
     expect_success("examples/class.er")
@@ -31,6 +36,16 @@ fn exec_import() -> Result<(), ()> {
     expect_success("examples/import.er")
 }
 
+#[test]
+fn exec_infer_class() -> Result<(), ()> {
+    expect_success("tests/infer_class.er")
+}
+
+#[test]
+fn exec_infer_trait() -> Result<(), ()> {
+    expect_success("tests/infer_trait.er")
+}
+
 #[test]
 fn exec_move_check() -> Result<(), ()> {
     expect_failure("examples/move_check.er")
@@ -41,6 +56,12 @@ fn exec_quantified() -> Result<(), ()> {
     expect_success("examples/quantified.er")
 }
 
+#[test]
+fn exec_rec() -> Result<(), ()> {
+    // this script is valid but the current code generating process has a bug.
+    expect_end_with("tests/rec.er", 1)
+}
+
 #[test]
 fn exec_record() -> Result<(), ()> {
     expect_success("examples/record.er")
@@ -51,6 +72,11 @@ fn exec_side_effect() -> Result<(), ()> {
     expect_failure("examples/side_effect.er")
 }
 
+#[test]
+fn exec_subtyping() -> Result<(), ()> {
+    expect_failure("tests/subtyping.er")
+}
+
 #[test]
 fn exec_trait() -> Result<(), ()> {
     expect_success("examples/trait.er")