diff --git a/compiler/erg_common/Cargo.toml b/compiler/erg_common/Cargo.toml
index 509742860..f0b9e884f 100644
--- a/compiler/erg_common/Cargo.toml
+++ b/compiler/erg_common/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_common"
-version = "0.2.2"
+version = "0.2.3"
 description = "A common components library of Erg"
 authors = ["Shunsuke Shibayama <sbym1346@gmail.com>"]
 license = "MIT OR Apache-2.0"
diff --git a/compiler/erg_common/codeobj.rs b/compiler/erg_common/codeobj.rs
index 913581fe7..6abfe5969 100644
--- a/compiler/erg_common/codeobj.rs
+++ b/compiler/erg_common/codeobj.rs
@@ -126,9 +126,15 @@ impl HasType for CodeObj {
     fn ref_t(&self) -> &Type {
         &Type::Code
     }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        todo!()
+    }
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl fmt::Debug for CodeObj {
diff --git a/compiler/erg_common/error.rs b/compiler/erg_common/error.rs
index 31409fc0d..2c2299339 100644
--- a/compiler/erg_common/error.rs
+++ b/compiler/erg_common/error.rs
@@ -317,7 +317,7 @@ impl ErrorCore {
     }
 
     pub fn unreachable(fn_name: &str, line: u32) -> Self {
-        Self::bug(0, Location::Unknown, fn_name, line)
+        Self::bug(line as usize, Location::Unknown, fn_name, line)
     }
 
     pub fn bug(errno: usize, loc: Location, fn_name: &str, line: u32) -> Self {
diff --git a/compiler/erg_common/traits.rs b/compiler/erg_common/traits.rs
index e2dc40e29..07b01c806 100644
--- a/compiler/erg_common/traits.rs
+++ b/compiler/erg_common/traits.rs
@@ -299,11 +299,8 @@ pub trait ImmutableStream<T>: Sized {
 // for Runnable::run
 fn expect_block(src: &str) -> bool {
     src.ends_with(&['=', ':'])
-        || src.ends_with(":=")
         || src.ends_with("->")
         || src.ends_with("=>")
-        || src.ends_with("do")
-        || src.ends_with("do!")
 }
 
 /// this trait implements REPL (Read-Eval-Print-Loop) automatically
@@ -497,6 +494,9 @@ pub trait HasType {
     fn ref_t(&self) -> &Type;
     // 関数呼び出しの場合、.ref_t()は戻り値を返し、signature_t()は関数全体の型を返す
     fn signature_t(&self) -> Option<&Type>;
+    // 最後にHIR全体の型変数を消すために使う
+    fn ref_mut_t(&mut self) -> &mut Type;
+    fn signature_mut_t(&mut self) -> Option<&mut Type>;
     #[inline]
     fn t(&self) -> Type {
         self.ref_t().clone()
diff --git a/compiler/erg_common/tsort.rs b/compiler/erg_common/tsort.rs
index aa95036c3..e9bf9ef4f 100644
--- a/compiler/erg_common/tsort.rs
+++ b/compiler/erg_common/tsort.rs
@@ -42,30 +42,35 @@ fn reorder_by_key<T: Eq, U>(mut g: Graph<T, U>, idx: Vec<T>) -> Graph<T, U> {
     g
 }
 
-fn dfs<T: Eq + Hash + Clone, U>(g: &Graph<T, U>, v: T, used: &mut Set<T>, idx: &mut Vec<T>) {
+fn dfs<T: Eq + Hash + Clone, U>(g: &Graph<T, U>, v: T, used: &mut Set<T>, idx: &mut Vec<T>) -> Result<(), ()> {
     used.insert(v.clone());
     for node_id in g.iter().find(|n| &n.id == &v).unwrap().depends_on.iter() {
+        // detecting cycles
+        if used.contains(node_id) && !idx.contains(node_id) {
+            return Err(());
+        }
         if !used.contains(node_id) {
-            dfs(g, node_id.clone(), used, idx);
+            dfs(g, node_id.clone(), used, idx)?;
         }
     }
     idx.push(v);
+    Ok(())
 }
 
 /// perform topological sort on a graph
-pub fn tsort<T: Eq + Hash + Clone, U>(g: Graph<T, U>) -> Graph<T, U> {
+pub fn tsort<T: Eq + Hash + Clone, U>(g: Graph<T, U>) -> Result<Graph<T, U>, ()> {
     let n = g.len();
     let mut idx = Vec::with_capacity(n);
     let mut used = Set::new();
     for v in g.iter() {
         if !used.contains(&v.id) {
-            dfs(&g, v.id.clone(), &mut used, &mut idx);
+            dfs(&g, v.id.clone(), &mut used, &mut idx)?;
         }
     }
-    reorder_by_key(g, idx)
+    Ok(reorder_by_key(g, idx))
 }
 
-fn _test() {
+fn _test() -> Result<(), ()> {
     let v = vec!["e", "d", "b", "a", "c"];
     let idx = vec![3, 2, 4, 1, 0];
     assert_eq!(vec!["a", "b", "c", "d", "e"], _reorder_by_idx(v, idx));
@@ -83,5 +88,6 @@ fn _test() {
         on_2.clone(),
     ];
     let dag = vec![en_0, o0_1, on_2, e0_3, ond_4];
-    assert_eq!(sorted, tsort(dag));
+    assert_eq!(sorted, tsort(dag)?);
+    Ok(())
 }
diff --git a/compiler/erg_common/ty.rs b/compiler/erg_common/ty.rs
index 356678c50..6de25b127 100644
--- a/compiler/erg_common/ty.rs
+++ b/compiler/erg_common/ty.rs
@@ -89,10 +89,15 @@ pub trait HasLevel {
 // REVIEW: TyBoundと微妙に役割が被っている
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Constraint {
+    /// :> T
     SupertypeOf(Type),
+    /// <: T
     SubtypeOf(Type),
+    /// :> Sub, <: Sup
     Sandwiched { sub: Type, sup: Type },
+    /// : T
     TypeOf(Type),
+    Uninited,
 }
 
 impl fmt::Display for Constraint {
@@ -102,11 +107,20 @@ impl fmt::Display for Constraint {
             Self::SubtypeOf(sup) => write!(f, "<: {sup}"),
             Self::Sandwiched { sub, sup } => write!(f, ":> {sub}, <: {sup}"),
             Self::TypeOf(ty) => write!(f, ": {}", ty),
+            Self::Uninited => write!(f, "<uninited>"),
         }
     }
 }
 
 impl Constraint {
+    pub const fn sandwiched(sub: Type, sup: Type) -> Self {
+        Self::Sandwiched { sub, sup }
+    }
+
+    pub const fn is_uninited(&self) -> bool {
+        matches!(self, Self::Uninited)
+    }
+
     pub fn typ(&self) -> Option<&Type> {
         match self {
             Self::TypeOf(ty) => Some(ty),
@@ -114,6 +128,13 @@ impl Constraint {
         }
     }
 
+    pub fn sub_type(&self) -> Option<&Type> {
+        match self {
+            Self::SupertypeOf(ty) => Some(ty),
+            _ => None,
+        }
+    }
+
     pub fn super_type(&self) -> Option<&Type> {
         match self {
             Self::SubtypeOf(ty) => Some(ty),
@@ -269,7 +290,23 @@ impl<T: Clone + HasLevel> Free<T> {
         }
     }
 
-    pub fn unwrap(self) -> T {
+    pub fn get_name(&self) -> Option<Str> {
+        match self.0.clone_inner() {
+            FreeKind::Linked(_) => panic!("the value is linked"),
+            FreeKind::Unbound { .. } => None,
+            FreeKind::NamedUnbound { name, .. } => Some(name),
+        }
+    }
+
+    pub fn unwrap_unbound(self) -> (Option<Str>, usize, Constraint) {
+        match self.0.clone_inner() {
+            FreeKind::Linked(_) => panic!("the value is linked"),
+            FreeKind::Unbound { constraint, lev, .. } => (None, lev, constraint),
+            | FreeKind::NamedUnbound { name, lev, constraint } => (Some(name), lev, constraint),
+        }
+    }
+
+    pub fn unwrap_linked(self) -> T {
         match self.0.clone_inner() {
             FreeKind::Linked(t) => t,
             FreeKind::Unbound { .. } | FreeKind::NamedUnbound { .. } => {
@@ -289,6 +326,14 @@ impl<T: Clone + HasLevel> Free<T> {
         })
     }
 
+    pub fn crack_constraint(&self) -> Ref<'_, Constraint> {
+        Ref::map(self.0.borrow(), |f| match f {
+            FreeKind::Linked(_) => panic!("the value is linked"),
+            FreeKind::Unbound { constraint, .. }
+            | FreeKind::NamedUnbound { constraint, .. } => constraint,
+        })
+    }
+
     pub fn type_of(&self) -> Option<Type> {
         self.0.borrow().constraint().and_then(|c| c.typ().cloned())
     }
@@ -307,6 +352,30 @@ impl<T: Clone + HasLevel> Free<T> {
         )
     }
 
+    pub fn constraint_is_typeof(&self) -> bool {
+        matches!(
+            &*self.0.borrow(),
+            FreeKind::Unbound { constraint, .. }
+            | FreeKind::NamedUnbound { constraint, .. } if constraint.typ().is_some()
+        )
+    }
+
+    pub fn constraint_is_supertypeof(&self) -> bool {
+        matches!(
+            &*self.0.borrow(),
+            FreeKind::Unbound { constraint, .. }
+            | FreeKind::NamedUnbound { constraint, .. } if constraint.sub_type().is_some()
+        )
+    }
+
+    pub fn constraint_is_subtypeof(&self) -> bool {
+        matches!(
+            &*self.0.borrow(),
+            FreeKind::Unbound { constraint, .. }
+            | FreeKind::NamedUnbound { constraint, .. } if constraint.super_type().is_some()
+        )
+    }
+
     pub fn is_linked(&self) -> bool {
         matches!(&*self.0.borrow(), FreeKind::Linked(_))
     }
@@ -812,6 +881,13 @@ impl TyParam {
             _ => true,
         }
     }
+
+    pub fn update_constraint(&self, new_constraint: Constraint) {
+        match self {
+            Self::Type(t) => { t.update_constraint(new_constraint) },
+            _ => {}
+        }
+    }
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -824,6 +900,7 @@ pub enum TyParamOrdering {
     NotEqual,     // Less or Greater
     GreaterEqual, // Greater or Equal
     Any,
+    NoRelation,
 }
 
 use TyParamOrdering::*;
@@ -877,7 +954,7 @@ impl TyParamOrdering {
             GreaterEqual => LessEqual,
             Equal => NotEqual,
             NotEqual => Equal,
-            Any => Any,
+            Any | NoRelation => Any,
         }
     }
 }
@@ -1692,6 +1769,8 @@ pub enum Type {
     }, // e.g. T.U
     ASTOmitted,         // call中のcalleeの型など、不要な部分に付ける
     Failure,            // when failed to infer
+    /// used to represent `TyParam` is not initialized (see `erg_compiler::context::instantiate_tp`)
+    Uninited,
 }
 
 impl fmt::Display for Type {
@@ -1802,6 +1881,10 @@ impl HasType for Type {
     fn ref_t(&self) -> &Type {
         self
     }
+    #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        self
+    }
     fn inner_ts(&self) -> Vec<Type> {
         match self {
             Self::Ref(t) | Self::RefMut(t) | Self::VarArgs(t) => {
@@ -1817,6 +1900,9 @@ impl HasType for Type {
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl HasLevel for Type {
@@ -2044,7 +2130,7 @@ impl Type {
         Self::poly("Iter", vec![TyParam::t(t)])
     }
 
-    pub fn refer(t: Type) -> Self {
+    pub fn ref_(t: Type) -> Self {
         Self::Ref(Box::new(t))
     }
 
@@ -2315,6 +2401,14 @@ impl Type {
         Self::Quantified(QuantifiedType::new(unbound_t, bounds))
     }
 
+    pub fn is_mono_q(&self) -> bool {
+        match self {
+            Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_mono_q(),
+            Self::MonoQVar(_) => true,
+            _ => false,
+        }
+    }
+
     pub fn mutate(self) -> Self {
         match self {
             Self::Int => Self::IntMut,
@@ -2403,10 +2497,14 @@ impl Type {
 
     pub fn rec_eq(&self, other: &Self) -> bool {
         match (self, other) {
-            (Self::FreeVar(v), other) | (other, Self::FreeVar(v)) => match &*v.borrow() {
+            (Self::FreeVar(v), other) => match &*v.borrow() {
                 FreeKind::Linked(t) => t.rec_eq(other),
                 _ => self == other,
             },
+            (self_, Self::FreeVar(v)) => match &*v.borrow() {
+                FreeKind::Linked(t) => t.rec_eq(self_),
+                _ => self_ == other,
+            },
             (Self::Ref(l), Self::Ref(r)) | (Self::RefMut(l), Self::RefMut(r)) => l.rec_eq(r),
             (Self::Subr(l), Self::Subr(r)) => {
                 match (&l.kind, &r.kind) {
@@ -2578,6 +2676,7 @@ impl Type {
             Self::MonoProj { .. } => "MonoProj",
             Self::ASTOmitted => "ASTOmitted",
             Self::Failure => "<Failure>",
+            Self::Uninited => "<Uninited>",
         }
     }
 
@@ -2662,7 +2761,7 @@ impl Type {
     pub fn typarams(&self) -> Vec<TyParam> {
         match self {
             Self::FreeVar(f) if f.is_linked() => f.crack().typarams(),
-            Self::FreeVar(_unbound) => todo!(),
+            Self::FreeVar(_unbound) => vec![],
             Self::Ref(t) | Self::RefMut(t) => vec![TyParam::t(*t.clone())],
             Self::And(param_ts) | Self::Or(param_ts) | Self::Not(param_ts) => {
                 param_ts.iter().map(|t| TyParam::t(t.clone())).collect()
@@ -2745,6 +2844,13 @@ impl Type {
             _ => None,
         }
     }
+
+    pub fn update_constraint(&self, new_constraint: Constraint) {
+        match self {
+            Self::FreeVar(fv) => { fv.update_constraint(new_constraint); },
+            _ => {},
+        }
+    }
 }
 
 pub mod type_constrs {
@@ -2770,6 +2876,11 @@ pub mod type_constrs {
         Type::mono_q(name)
     }
 
+    #[inline]
+    pub fn mono_proj<S: Into<Str>>(lhs: Type, rhs: S) -> Type {
+        Type::mono_proj(lhs, rhs)
+    }
+
     #[inline]
     pub fn poly<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Type {
         Type::poly(name, params)
@@ -2890,6 +3001,7 @@ impl From<&Type> for TypeCode {
                 "Proc" => Self::Proc,
                 _ => Self::Other,
             },
+            Type::Refinement(refine) => Self::from(&*refine.t),
             _ => Self::Other,
         }
     }
@@ -3148,6 +3260,8 @@ impl TypePair {
             {
                 Self::ProcProc
             }
+            (Type::Refinement(refine), r) => Self::new(&*refine.t, r),
+            (l, Type::Refinement(refine)) => Self::new(l, &*refine.t),
             (_, _) => Self::Others,
         }
     }
diff --git a/compiler/erg_common/value.rs b/compiler/erg_common/value.rs
index 43b1b248c..cd806f6cc 100644
--- a/compiler/erg_common/value.rs
+++ b/compiler/erg_common/value.rs
@@ -233,6 +233,9 @@ impl HasType for ValueObj {
     fn ref_t(&self) -> &Type {
         panic!("cannot get reference of the const")
     }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        panic!("cannot get mutable reference of the const")
+    }
     /// その要素だけの集合型を返す、クラスが欲しい場合は.classで
     #[inline]
     fn t(&self) -> Type {
@@ -246,6 +249,9 @@ impl HasType for ValueObj {
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl ValueObj {
diff --git a/compiler/erg_compiler/Cargo.toml b/compiler/erg_compiler/Cargo.toml
index b8e063c06..c6e3600e4 100644
--- a/compiler/erg_compiler/Cargo.toml
+++ b/compiler/erg_compiler/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_compiler"
-version = "0.2.2"
+version = "0.2.3"
 description = "Centimetre: the Erg compiler"
 authors = ["Shunsuke Shibayama <sbym1346@gmail.com>"]
 license = "MIT OR Apache-2.0"
@@ -15,8 +15,8 @@ debug = [ "erg_common/debug", "erg_parser/debug" ]
 japanese = [ "erg_common/japanese", "erg_parser/japanese" ]
 
 [dependencies]
-erg_common = { version = "0.2.2", path = "../erg_common" }
-erg_parser = { version = "0.2.2", path = "../erg_parser" }
+erg_common = { version = "0.2.3", path = "../erg_common" }
+erg_parser = { version = "0.2.3", path = "../erg_parser" }
 
 [lib]
 path = "lib.rs"
diff --git a/compiler/erg_compiler/context.rs b/compiler/erg_compiler/context.rs
index 697069f53..8e9414dbb 100644
--- a/compiler/erg_compiler/context.rs
+++ b/compiler/erg_compiler/context.rs
@@ -1,5 +1,6 @@
 //! Defines `Context`.
 //! `Context` is used for type inference and type checking.
+// use std::cmp::Ordering;
 use std::fmt;
 use std::mem;
 use std::option::Option; // conflicting to Type::Option
@@ -9,8 +10,6 @@ use erg_common::error::{ErrorCore, Location};
 use erg_common::levenshtein::levenshtein;
 use erg_common::set::Set;
 use erg_common::traits::{HasType, Locational, Stream};
-use erg_common::tsort::tsort;
-use erg_common::tsort::{Graph, Node};
 use erg_common::ty::fresh_varname;
 use erg_common::ty::{
     ConstObj, Constraint, FreeKind, HasLevel, IntervalOp, ParamTy, Predicate, RefinementType,
@@ -19,7 +18,7 @@ use erg_common::ty::{
 use erg_common::value::ValueObj;
 use erg_common::Str;
 use erg_common::{
-    assume_unreachable, enum_unwrap, fmt_slice, fmt_vec, fn_name, get_hash, log, set, try_map,
+    assume_unreachable, enum_unwrap, fmt_slice, fn_name, get_hash, log, set, try_map,
 };
 use Predicate as Pred;
 use TyParamOrdering::*;
@@ -33,6 +32,7 @@ use ast::{
 use erg_parser::ast;
 use erg_parser::token::{Token, TokenKind};
 
+use crate::error::readable_name;
 use crate::error::{binop_to_dname, unaryop_to_dname, TyCheckError, TyCheckErrors, TyCheckResult};
 use crate::eval::Evaluator;
 use crate::hir;
@@ -40,6 +40,53 @@ use crate::varinfo::{Mutability, ParamIdx, VarInfo, VarKind, Visibility};
 use Mutability::*;
 use Visibility::*;
 
+type Trait = Type;
+
+/// ```
+/// TyParamIdx::new(Add(R, O), O) => Nth(1)
+/// TyParamIdx::new(Add(R, F(O, I)), O) => Nested(Nth(1), 0)
+/// ```
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum TyParamIdx {
+    Nth(usize),
+    Nested(Box<TyParamIdx>, usize),
+}
+
+impl TyParamIdx {
+    pub fn search(search_from: &Type, target: &Type) -> Option<Self> {
+        match search_from {
+            Type::Poly{ params, .. } => {
+                for (i, tp) in params.iter().enumerate() {
+                    match tp {
+                        TyParam::Type(t) if t.rec_eq(target) => { return Some(Self::Nth(i)) },
+                        TyParam::Type(t) if t.is_monomorphic() => {},
+                        other => todo!("{other:?}"),
+                    }
+                }
+                None
+            },
+            _ => todo!(),
+        }
+    }
+
+    /// ```
+    /// Nested(Nth(1), 0).select(F(X, G(Y, Z))) == Y
+    /// ```
+    pub fn select(self, from: &Type) -> Type {
+        match self {
+            Self::Nth(n) => {
+                let tps = from.typarams();
+                let tp = tps.iter().nth(n).unwrap();
+                match tp {
+                    TyParam::Type(t) => *t.clone(),
+                    _ => todo!(),
+                }
+            },
+            Self::Nested(_, _) => todo!(),
+        }
+    }
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub enum DefaultInfo {
     NonDefault,
@@ -122,8 +169,6 @@ pub enum RegistrationMode {
 
 use RegistrationMode::*;
 
-type TyBoundGraph = Graph<Str, TyBound>;
-
 /// Context for instantiating a quantified type
 /// 量化型をインスタンス化するための文脈
 #[derive(Debug, Clone)]
@@ -134,158 +179,156 @@ pub struct TyVarContext {
 }
 
 impl TyVarContext {
-    pub fn new(level: usize, bounds: Set<TyBound>) -> Self {
+    pub fn new(level: usize, bounds: Set<TyBound>, ctx: &Context) -> Self {
         let mut self_ = Self {
             level,
             tyvar_instances: Dict::new(),
             typaram_instances: Dict::new(),
         };
-        for bound in Self::sort_bounds(bounds) {
-            self_.instantiate_bound(bound);
+        // TODO: this is valid but cause a crash: T <: Ord T
+        for bound in bounds.into_iter() {
+            self_.instantiate_bound(bound, ctx);
         }
         self_
     }
 
-    fn sort_bounds(_bounds: Set<TyBound>) -> impl Iterator<Item = TyBound> {
-        let mut graph = TyBoundGraph::new();
-        for bound in _bounds.into_iter() {
-            let depends_on = Self::bound_dependencies(&bound);
-            graph.push(Node::new(Str::rc(bound.lhs()), bound, depends_on));
-        }
-        let graph = tsort(graph);
-        graph.into_iter().map(|node| node.data)
-    }
-
-    fn bound_dependencies(_bound: &TyBound) -> Vec<Str> {
-        // TODO: Polymorphic lhs
-        match _bound {
-            TyBound::Subtype { sup, .. } => Self::rec_t_inner_qvars(sup, vec![]),
-            TyBound::Supertype { sub, .. } => Self::rec_t_inner_qvars(sub, vec![]),
-            TyBound::Sandwiched { mid, .. } => Self::rec_t_inner_qvars(mid, vec![]),
-            TyBound::Instance { t, .. } => Self::rec_t_inner_qvars(t, vec![]),
-        }
-    }
-
-    fn rec_t_inner_qvars(t: &Type, dep: Vec<Str>) -> Vec<Str> {
-        match t {
-            Type::MonoQVar(name) | Type::PolyQVar { name, .. } => {
-                [dep, vec![name.clone()]].concat()
-            }
-            Type::FreeVar(fv) if fv.is_linked() => Self::rec_t_inner_qvars(&fv.crack(), dep),
-            Type::Ref(t) | Type::RefMut(t) => Self::rec_t_inner_qvars(t, dep),
-            Type::Poly { params, .. } => params.iter().fold(dep, |acc, arg| {
-                [acc, Self::rec_tp_inner_qvars(arg, vec![])].concat()
-            }),
-            Type::VarArgs(t) => Self::rec_t_inner_qvars(&t, dep),
-            Type::Subr(_subr) => todo!(),
-            Type::Callable { param_ts: _, return_t: _ } => todo!(),
-            Type::And(_) | Type::Or(_) | Type::Not(_) => todo!(),
-            Type::Record(_) => todo!(),
-            Type::Quantified(_) => todo!(),
-            Type::Refinement(_) => todo!(),
-            _ => dep,
+    fn instantiate_const_template(&mut self, var_name: &str, _callee_name: &Str, ct: &ConstTemplate) -> TyParam {
+        match ct {
+            ConstTemplate::Obj(o) => {
+                match o {
+                    ConstObj::Type(t) if t.is_mono_q() => {
+                        if t.name() == "Self" {
+                            let constraint = Constraint::TypeOf(Type);
+                            let t = Type::named_free_var(Str::rc(var_name), self.level, constraint);
+                            TyParam::t(t)
+                        } else {
+                            todo!()
+                        }
+                    },
+                    ConstObj::Type(t) => TyParam::t(*t.clone()),
+                    v @ ConstObj::Value(_) => TyParam::ConstObj(v.clone()),
+                    other => todo!("{other}"),
+                }
+            },
+            ConstTemplate::App { .. } => {
+                todo!()
+            }
         }
     }
 
-    fn rec_tp_inner_qvars(tp: &TyParam, dep: Vec<Str>) -> Vec<Str> {
-        match tp {
-            TyParam::MonoQVar(name) | TyParam::PolyQVar { name, .. } => {
-                [dep, vec![name.clone()]].concat()
-            }
-            TyParam::FreeVar(fv) if fv.is_linked() => Self::rec_tp_inner_qvars(&fv.crack(), dep),
-            TyParam::Type(t) => Self::rec_t_inner_qvars(t, dep),
-            TyParam::App { args, .. } | TyParam::Array(args) | TyParam::Tuple(args) => {
-                args.iter().fold(dep, |acc, arg| {
-                    [acc, Self::rec_tp_inner_qvars(arg, vec![])].concat()
-                })
-            }
-            TyParam::UnaryOp { .. } => todo!(),
-            TyParam::BinOp { .. } => todo!(),
-            _ => dep,
+    fn instantiate_poly(&mut self, tvar_name: &str, name: &Str, params: Vec<TyParam>, ctx: &Context) -> Type {
+        if let Some(temp_defaults) = ctx.rec_get_const_param_defaults(&name) {
+            let c = ctx.rec_type_ctx_by_name(name).unwrap_or_else(|| panic!("{} not found", name));
+            let defined_params_len = c.params.len();
+            let given_params_len = params.len();
+            if defined_params_len < given_params_len { panic!() }
+            let inst_non_defaults = params.into_iter().map(|p| self.instantiate_tp(p)).collect();
+            let mut inst_defaults = vec![];
+            for c in temp_defaults.into_iter().take(defined_params_len - given_params_len) {
+                let c = self.instantiate_const_template(tvar_name, name, c);
+                inst_defaults.push(c);
+            }
+            Type::poly(
+                name,
+                [inst_non_defaults, inst_defaults].concat(),
+            )
+        } else {
+            Type::poly(
+                name,
+                params.into_iter().map(|p| self.instantiate_tp(p)).collect(),
+            )
         }
     }
 
-    fn instantiate_bound(&mut self, bound: TyBound) {
+    fn instantiate_bound(&mut self, bound: TyBound, ctx: &Context) {
         match bound {
             TyBound::Subtype { sub, sup } => {
                 let sup = match sup {
                     Type::Poly { name, params } => {
-                        let sup = Type::poly(
-                            name,
-                            params.into_iter().map(|p| self.instantiate_tp(p)).collect(),
-                        );
-                        sup
+                        self.instantiate_poly(sub.name(), &name, params, ctx)
                     }
                     Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
                     sup => sup,
                 };
                 let constraint = Constraint::SubtypeOf(sup);
-                let name = Str::rc(sub.name());
-                self.push_tyvar(name.clone(), Type::named_free_var(name, self.level, constraint));
+                if let Some(tv) = self.tyvar_instances.get(sub.name()) {
+                    tv.update_constraint(constraint);
+                } else if let Some(tp) = self.typaram_instances.get(sub.name()) {
+                    tp.update_constraint(constraint);
+                } else {
+                    let name = Str::rc(sub.name());
+                    self.push_tyvar(name.clone(), Type::named_free_var(name, self.level, constraint));
+                }
             }
             TyBound::Supertype { sup, sub } => {
                 let sub = match sub {
                     Type::Poly { name, params } => {
-                        let sub = Type::poly(
-                            name,
-                            params.into_iter().map(|p| self.instantiate_tp(p)).collect(),
-                        );
-                        sub
+                        self.instantiate_poly(sup.name(), &name, params, ctx)
                     }
                     Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
                     sub => sub,
                 };
                 let constraint = Constraint::SupertypeOf(sub);
-                let name = Str::rc(sup.name());
-                self.push_tyvar(name.clone(), Type::named_free_var(name, self.level, constraint));
+                if let Some(tv) = self.tyvar_instances.get(sup.name()) {
+                    tv.update_constraint(constraint);
+                } else if let Some(tp) = self.typaram_instances.get(sup.name()) {
+                    tp.update_constraint(constraint);
+                } else {
+                    let name = Str::rc(sup.name());
+                    self.push_tyvar(name.clone(), Type::named_free_var(name, self.level, constraint));
+                }
             }
             TyBound::Sandwiched { sub, mid, sup } => {
                 let sub = match sub {
                     Type::Poly { name, params } => {
-                        let sub = Type::poly(
-                            name,
-                            params.into_iter().map(|p| self.instantiate_tp(p)).collect(),
-                        );
-                        sub
+                        self.instantiate_poly(mid.name(), &name, params, ctx)
                     }
                     Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
                     sub => sub,
                 };
                 let sup = match sup {
                     Type::Poly { name, params } => {
-                        let sup = Type::poly(
-                            name,
-                            params.into_iter().map(|p| self.instantiate_tp(p)).collect(),
-                        );
-                        sup
+                        self.instantiate_poly(mid.name(), &name, params, ctx)
                     }
                     Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
                     sup => sup,
                 };
                 let constraint = Constraint::Sandwiched { sub, sup };
-                let name = Str::rc(mid.name());
-                self.push_tyvar(name.clone(), Type::named_free_var(name, self.level, constraint));
+                if let Some(tv) = self.tyvar_instances.get(mid.name()) {
+                    tv.update_constraint(constraint);
+                } else if let Some(tp) = self.typaram_instances.get(mid.name()) {
+                    tp.update_constraint(constraint);
+                } else {
+                    let name = Str::rc(mid.name());
+                    self.push_tyvar(name.clone(), Type::named_free_var(name, self.level, constraint));
+                }
             }
             TyBound::Instance { name, t } => {
                 let t = match t {
                     Type::Poly { name, params } => {
-                        let t = Type::poly(
-                            name,
-                            params.into_iter().map(|p| self.instantiate_tp(p)).collect(),
-                        );
-                        t
+                        self.instantiate_poly(&name[..], &name, params, ctx)
                     }
                     t => t,
                 };
+                let constraint = Constraint::TypeOf(t.clone());
                 // TODO: type-like types
                 if &t == &Type {
-                    let constraint = Constraint::TypeOf(t);
-                    self.push_tyvar(
-                        name.clone(),
-                        Type::named_free_var(name, self.level, constraint),
-                    );
+                    if let Some(tv) = self.tyvar_instances.get(&name) {
+                        tv.update_constraint(constraint);
+                    } else if let Some(tp) = self.typaram_instances.get(&name) {
+                        tp.update_constraint(constraint);
+                    } else {
+                        self.push_tyvar(
+                            name.clone(),
+                            Type::named_free_var(name, self.level, constraint),
+                        );
+                    }
                 } else {
-                    self.push_typaram(name.clone(), TyParam::named_free_var(name, self.level, t));
+                    if let Some(tp) = self.typaram_instances.get(&name) {
+                        tp.update_constraint(constraint);
+                    } else {
+                        self.push_typaram(name.clone(), TyParam::named_free_var(name, self.level, t));
+                    }
                 }
             }
         }
@@ -295,7 +338,7 @@ impl TyVarContext {
         todo!()
     }
 
-    pub(crate) fn instantiate_t(&self, quantified: Type) -> Type {
+    pub(crate) fn instantiate_t(&mut self, quantified: Type) -> Type {
         match quantified {
             Type::MonoQVar(n) => {
                 if let Some(t) = self.get_tyvar(&n) {
@@ -307,32 +350,38 @@ impl TyVarContext {
                         todo!()
                     }
                 } else {
-                    todo!()
+                    let tv = Type::named_free_var(n.clone(), self.level, Constraint::Uninited);
+                    self.push_tyvar(n, tv.clone());
+                    tv
                 }
             }
             other => todo!("{other}"),
         }
     }
 
-    fn instantiate_tp(&self, quantified: TyParam) -> TyParam {
+    fn instantiate_tp(&mut self, quantified: TyParam) -> TyParam {
         match quantified {
             TyParam::MonoQVar(n) => {
                 if let Some(t) = self.get_typaram(&n) {
-                    return t.clone();
+                    t.clone()
                 } else if let Some(t) = self.get_tyvar(&n) {
-                    return TyParam::t(t.clone());
+                    TyParam::t(t.clone())
                 } else {
-                    panic!("Type parameter {n} is not found. This is a bug.")
+                    let tp = TyParam::named_free_var(n.clone(), self.level, Type::Uninited);
+                    self.push_typaram(n, tp.clone());
+                    tp
                 }
             }
             TyParam::Type(t) => {
                 if let Type::MonoQVar(n) = *t {
                     if let Some(t) = self.get_typaram(&n) {
-                        return t.clone();
+                        t.clone()
                     } else if let Some(t) = self.get_tyvar(&n) {
-                        return TyParam::t(t.clone());
+                        TyParam::t(t.clone())
                     } else {
-                        panic!("Type variable {n} is not found. This is a bug.")
+                        let tv = Type::named_free_var(n.clone(), self.level, Constraint::Uninited);
+                        self.push_tyvar(n, tv.clone());
+                        TyParam::t(tv)
                     }
                 } else {
                     todo!("{t}")
@@ -369,6 +418,22 @@ impl TyVarContext {
     }
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum ConstTemplate {
+    Obj(ConstObj),
+    App{ name: Str, non_default_args: Vec<Type>, default_args: Vec<ConstTemplate> },
+}
+
+impl ConstTemplate {
+    pub const fn app(name: &'static str, non_default_args: Vec<Type>, default_args: Vec<ConstTemplate>) -> Self {
+        ConstTemplate::App {
+            name: Str::ever(name),
+            non_default_args,
+            default_args,
+        }
+    }
+}
+
 /// Represents the context of the current scope
 #[derive(Debug)]
 pub struct Context {
@@ -378,21 +443,28 @@ pub struct Context {
     // ユーザー定義APIでのみ使う
     pub(crate) bounds: Vec<TyBound>,
     pub(crate) preds: Vec<Predicate>,
-    // for looking up the parent scope
+    /// for looking up the parent scope
     pub(crate) outer: Option<Box<Context>>,
+    // e.g. { "Add": [ConstObjTemplate::App("Self", vec![])])
+    pub(crate) const_param_defaults: Dict<Str, Vec<ConstTemplate>>,
+    // Superclasses/supertraits by a patch are not included here
     // patchによってsuper class/traitになったものはここに含まれない
     pub(crate) super_classes: Vec<Type>, // if self is a patch, means patch classes
     pub(crate) super_traits: Vec<Type>,  // if self is not a trait, means implemented traits
-    // K: メソッド名, V: それを実装するパッチたち
-    // 提供メソッドはスコープごとに実装を切り替えることができる
-    pub(crate) _method_impl_patches: Dict<VarName, Vec<VarName>>,
-    // K: 多相トレイトの名前, V: 実装(小さい順)
-    // e.g. { "Add": [Add(Nat, Nat), Add(Int, Int), ...], ... }
-    pub(crate) poly_trait_impls: Dict<Str, Vec<Type>>,
-    // .0: 関係付けるパッチ(glue patch), .1: サブタイプになる型, .2: スーパータイプになるトレイト
-    // 一つの型ペアを接着パッチは同時に一つまでしか存在しないが、付け替えは可能
-    pub(crate) glue_patch_and_types: Vec<(VarName, Type, Type)>,
-    // stores declared names (not initialized)
+    /// K: method name, V: impl patch
+    /// Provided methods can switch implementations on a scope-by-scope basis
+    /// K: メソッド名, V: それを実装するパッチたち
+    /// 提供メソッドはスコープごとに実装を切り替えることができる
+    pub(crate) method_impl_patches: Dict<VarName, Vec<VarName>>,
+    /// K: name of the polymorphic trait, V: (type, monomorphised trait that the type implements)
+    /// K: 多相トレイトの名前, V: (型, その型が実装する単相化トレイト)
+    /// e.g. { "Add": [(Nat, Add(Nat)), (Int, Add(Int)), ...], ... }
+    pub(crate) poly_trait_impls: Dict<Str, Vec<(Type, Trait)>>,
+    /// .0: glue patch, .1: type as subtype, .2: trait as supertype
+    /// .0: 関係付けるパッチ(glue patch), .1: サブタイプになる型, .2: スーパータイプになるトレイト
+    /// 一つの型ペアを接着パッチは同時に一つまでしか存在しないが、付け替えは可能
+    pub(crate) glue_patch_and_types: Vec<(VarName, Type, Trait)>,
+    /// stores declared names (not initialized)
     pub(crate) decls: Dict<VarName, VarInfo>,
     // stores defined names
     // 型の一致はHashMapでは判定できないため、keyはVarNameとして1つずつ見ていく
@@ -404,7 +476,6 @@ pub struct Context {
     pub(crate) params: Vec<(Option<VarName>, VarInfo)>,
     pub(crate) locals: Dict<VarName, VarInfo>,
     pub(crate) consts: Dict<Str, ConstObj>,
-    // FIXME: Compilerが持つ
     pub(crate) eval: Evaluator,
     // stores user-defined type context
     pub(crate) types: Dict<Type, Context>,
@@ -504,7 +575,8 @@ impl Context {
             outer: outer.map(Box::new),
             super_classes,
             super_traits,
-            _method_impl_patches: Dict::default(),
+            const_param_defaults: Dict::default(),
+            method_impl_patches: Dict::default(),
             poly_trait_impls: Dict::default(),
             glue_patch_and_types: Vec::default(),
             params: params_,
@@ -968,7 +1040,7 @@ impl Context {
                     TyCheckError::return_type_error(
                         e.core.loc,
                         e.caused_by,
-                        name.inspect(),
+                        readable_name(name.inspect()),
                         spec_ret_t,
                         body_t,
                     )
@@ -1128,6 +1200,7 @@ impl Context {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
                         Constraint::TypeOf(t) => TyBound::instance(Str::rc(&name[..]), t.clone()),
+                        Constraint::Uninited => unreachable!(),
                     };
                     (TyParam::mono_q(&name), set! {bound})
                 }
@@ -1145,6 +1218,7 @@ impl Context {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
                         Constraint::TypeOf(t) => TyBound::instance(Str::rc(&name[..]), t.clone()),
+                        Constraint::Uninited => unreachable!(),
                     };
                     (TyParam::mono_q(name), set! {bound})
                 }
@@ -1187,6 +1261,7 @@ impl Context {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
                         Constraint::TypeOf(t) => TyBound::instance(Str::rc(&name[..]), t.clone()),
+                        Constraint::Uninited => unreachable!(),
                     };
                     (Type::mono(&name), set! {bound})
                 }
@@ -1204,6 +1279,7 @@ impl Context {
                             TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
                         }
                         Constraint::TypeOf(t) => TyBound::instance(Str::rc(&name[..]), t.clone()),
+                        Constraint::Uninited => unreachable!(),
                     };
                     (Type::mono(name), set! {bound})
                 }
@@ -1297,10 +1373,10 @@ impl Context {
     fn instantiate_tp(quantified: TyParam, tv_ctx: TyVarContext) -> (TyParam, TyVarContext) {
         match quantified {
             TyParam::MonoQVar(n) => {
-                if let Some(t) = tv_ctx.get_typaram(&n) {
-                    (t.clone(), tv_ctx)
-                } else if let Some(_t) = tv_ctx.get_tyvar(&n) {
-                    todo!()
+                if let Some(tp) = tv_ctx.get_typaram(&n) {
+                    (tp.clone(), tv_ctx)
+                } else if let Some(t) = tv_ctx.get_tyvar(&n) {
+                    (TyParam::t(t.clone()), tv_ctx)
                 } else {
                     panic!("type parameter {n} is not defined")
                 }
@@ -1332,8 +1408,16 @@ impl Context {
             MonoQVar(n) => {
                 if let Some(t) = tv_ctx.get_tyvar(&n) {
                     (t.clone(), tv_ctx)
-                } else if let Some(_t) = tv_ctx.get_typaram(&n) {
-                    todo!()
+                } else if let Some(tp) = tv_ctx.get_typaram(&n) {
+                    if let TyParam::Type(t) = tp {
+                        (*t.clone(), tv_ctx)
+                    } else {
+                        todo!(
+                            "typaram_insts: {}\ntyvar_insts:{}\n{tp}",
+                            tv_ctx.typaram_instances,
+                            tv_ctx.tyvar_instances,
+                        )
+                    }
                 } else {
                     panic!("the type variable {n} is not defined")
                 }
@@ -1397,7 +1481,7 @@ impl Context {
             }
             Ref(t) => {
                 let (t, tv_ctx) = Self::instantiate_t(*t, tv_ctx);
-                (Type::refer(t), tv_ctx)
+                (Type::ref_(t), tv_ctx)
             }
             RefMut(t) => {
                 let (t, tv_ctx) = Self::instantiate_t(*t, tv_ctx);
@@ -1425,7 +1509,7 @@ impl Context {
     fn instantiate(&self, quantified: Type, callee: &hir::Expr) -> TyCheckResult<Type> {
         match quantified {
             Quantified(quant) => {
-                let tv_ctx = TyVarContext::new(self.level, quant.bounds);
+                let tv_ctx = TyVarContext::new(self.level, quant.bounds, &self);
                 let (t, _) = Self::instantiate_t(*quant.unbound_callable, tv_ctx);
                 match &t {
                     Type::Subr(subr) => {
@@ -1482,9 +1566,11 @@ impl Context {
                     .iter()
                     .chain(subr.default_params.iter());
                 for (param_ty, pos_arg) in params.clone().zip(pos_args) {
+                    let arg_t = pos_arg.expr.ref_t();
+                    let param_t = &param_ty.ty;
                     self.sub_unify(
-                        pos_arg.expr.ref_t(),
-                        &param_ty.ty,
+                        arg_t,
+                        param_t,
                         None,
                         Some(pos_arg.loc()),
                     )
@@ -1492,13 +1578,13 @@ impl Context {
                         // REVIEW:
                         let name = callee.var_full_name().unwrap_or("".to_string());
                         let name =
-                            name + "::" + param_ty.name.as_ref().map(|s| &s[..]).unwrap_or("");
+                            name + "::" + param_ty.name.as_ref().map(|s| readable_name(&s[..])).unwrap_or("");
                         TyCheckError::type_mismatch_error(
                             e.core.loc,
                             e.caused_by,
                             &name[..],
-                            &param_ty.ty,
-                            pos_arg.expr.ref_t(),
+                            param_t,
+                            arg_t,
                         )
                     })?;
                     if let Some(name) = &param_ty.name {
@@ -1544,7 +1630,7 @@ impl Context {
     // FIXME:
     fn deref_tp(&self, tp: TyParam) -> TyCheckResult<TyParam> {
         match tp {
-            TyParam::FreeVar(fv) if fv.is_linked() => Ok(fv.unwrap()),
+            TyParam::FreeVar(fv) if fv.is_linked() => Ok(fv.unwrap_linked()),
             TyParam::Type(t) => Ok(TyParam::t(self.deref_tyvar(*t)?)),
             TyParam::App { name, mut args } => {
                 for param in args.iter_mut() {
@@ -1552,36 +1638,78 @@ impl Context {
                 }
                 Ok(TyParam::App { name, args })
             }
+            TyParam::BinOp { .. } => todo!(),
+            TyParam::UnaryOp { .. } => todo!(),
+            TyParam::Array(_) | TyParam::Tuple(_) => todo!(),
             t => Ok(t),
         }
     }
 
+    fn deref_constraint(&self, constraint: Constraint) -> TyCheckResult<Constraint> {
+        match constraint {
+            Constraint::SubtypeOf(sup) => {
+                Ok(Constraint::SubtypeOf(self.deref_tyvar(sup)?))
+            },
+            Constraint::Sandwiched { sub, sup } => {
+                Ok(Constraint::sandwiched(self.deref_tyvar(sub)?, self.deref_tyvar(sup)?))
+            },
+            Constraint::SupertypeOf(sub) => {
+                Ok(Constraint::SupertypeOf(self.deref_tyvar(sub)?))
+            },
+            Constraint::TypeOf(t) => {
+                Ok(Constraint::TypeOf(self.deref_tyvar(t)?))
+            },
+            _ => unreachable!(),
+        }
+    }
+
+    /// e.g.
+    /// ```
+    /// deref_tyvar(?T(<: Int)[n]): ?T => Int (if self.level <= n)
+    /// deref_tyvar((Int)): (Int) => Int
+    /// ```
     fn deref_tyvar(&self, t: Type) -> TyCheckResult<Type> {
         match t {
-            // in toplevel: ?T(<: Int)[n] should replaced to Int (if n > 0)
+            Type::FreeVar(fv) if fv.constraint_is_typeof() => Ok(Type::FreeVar(fv)),
+            // ?T(<: Int)[n] => Int
+            Type::FreeVar(fv) if fv.constraint_is_subtypeof() => {
+                if self.level <= fv.level().unwrap() {
+                    Ok(fv.crack_constraint().super_type().unwrap().clone())
+                } else {
+                    Ok(Type::FreeVar(fv))
+                }
+            },
+            // ?T(<: Add(?R(<: T), ?O(<: U)) => ?T(<: Add(T, U))
             Type::FreeVar(fv) if fv.is_unbound() => {
-                match fv.borrow().constraint().unwrap() {
-                    Constraint::SubtypeOf(sup)
-                    | Constraint::Sandwiched { sup, .. } if self.level <= fv.level().unwrap() => {
-                        return Ok(sup.clone());
-                    },
-                    // REVIEW: really?
-                    Constraint::SupertypeOf(sub) if self.level <= fv.level().unwrap() => {
-                        return Ok(sub.clone());
-                    },
-                    _ => {},
+                if self.level == 0 {
+                    match &*fv.crack_constraint() {
+                        Constraint::SupertypeOf(t)
+                        | Constraint::SubtypeOf(t) => Ok(t.clone()),
+                        Constraint::Sandwiched { sub, .. } => Ok(sub.clone()),
+                        Constraint::TypeOf(_) => {
+                            Err(TyCheckError::unreachable(fn_name!(), line!()))
+                        },
+                        _ => unreachable!(),
+                    }
+                } else {
+                    let new_constraint = fv.crack_constraint().clone();
+                    let new_constraint = self.deref_constraint(new_constraint)?;
+                    fv.update_constraint(new_constraint);
+                    Ok(Type::FreeVar(fv))
                 }
-                Ok(Type::FreeVar(fv))
             },
-            Type::FreeVar(fv) if fv.is_linked() => Ok(fv.unwrap()),
-            // 未連携型変数のチェックはモジュール全体の型検査が終わった後にやる
+            Type::FreeVar(fv) if fv.is_linked() => {
+                let t = fv.unwrap_linked();
+                self.deref_tyvar(t)
+            },
+            // 未連携型変数が残っているかのチェックはモジュール全体の型検査が終わった後にやる
             // Type::FreeVar(_) =>
             //    Err(TyCheckError::checker_bug(0, Location::Unknown, fn_name!(), line!())),
             Type::Poly { name, mut params } => {
                 for param in params.iter_mut() {
                     *param = self.deref_tp(mem::take(param))?;
                 }
-                Ok(Type::poly(name, params))
+                Ok(Type::Poly { name, params })
             }
             Type::Subr(mut subr) => {
                 match &mut subr.kind {
@@ -1610,40 +1738,81 @@ impl Context {
         }
     }
 
-    /// e.g.
-    /// monomorphise_t(Add(Nat, Nat)): (Add(Nat, Nat) => Nat)
-    /// monomorphise_t(Add(Nat, ?O)): (?O => Nat, Add(Nat, Nat) => Nat)
-    pub(crate) fn monomorphise(&self, maybe_poly: Type) -> TyCheckResult<Type> {
-        match maybe_poly {
-            Type::Subr(mut subr) => {
-                if let Some(self_t) = subr.kind.self_t_mut() {
-                    *self_t = self.monomorphise(mem::take(self_t))?;
-                }
-                for param_t in subr.non_default_params.iter_mut() {
-                    param_t.ty = self.monomorphise(mem::take(&mut param_t.ty))?;
+    pub(crate) fn deref_toplevel(&mut self, mut hir: hir::HIR) -> TyCheckResult<hir::HIR> {
+        self.level = 0;
+        for chunk in hir.module.iter_mut() {
+            self.deref_expr_t(chunk).map_err(|e| e)?;
+        }
+        Ok(hir)
+    }
+
+    fn deref_expr_t(&self, expr: &mut hir::Expr) -> TyCheckResult<()> {
+        match expr {
+            hir::Expr::Lit(_) => Ok(()),
+            hir::Expr::Accessor(acc) => {
+                let t = acc.ref_mut_t();
+                *t = self.deref_tyvar(mem::take(t))?;
+                match acc {
+                    hir::Accessor::Attr(attr) => {
+                        self.deref_expr_t(&mut attr.obj)?;
+                    }
+                    hir::Accessor::Local(_) => {}
+                    _ => todo!(),
                 }
-                for param_t in subr.default_params.iter_mut() {
-                    param_t.ty = self.monomorphise(mem::take(&mut param_t.ty))?;
+                Ok(())
+            },
+            hir::Expr::Array(_array) => {
+                todo!()
+            },
+            hir::Expr::Dict(_dict) => {
+                todo!()
+            }
+            hir::Expr::BinOp(binop) => {
+                let t = binop.signature_mut_t().unwrap();
+                *t = self.deref_tyvar(mem::take(t))?;
+                self.deref_expr_t(&mut binop.lhs)?;
+                self.deref_expr_t(&mut binop.rhs)?;
+                Ok(())
+            },
+            hir::Expr::UnaryOp(unaryop) => {
+                let t = unaryop.signature_mut_t().unwrap();
+                *t = self.deref_tyvar(mem::take(t))?;
+                self.deref_expr_t(&mut unaryop.expr)?;
+                Ok(())
+            },
+            hir::Expr::Call(call) => {
+                let t = call.signature_mut_t().unwrap();
+                *t = self.deref_tyvar(mem::take(t))?;
+                for arg in call.args.pos_args.iter_mut() {
+                    self.deref_expr_t(&mut arg.expr)?;
                 }
-                subr.return_t = Box::new(self.monomorphise(mem::take(&mut subr.return_t))?);
-                Ok(Type::Subr(subr))
+                Ok(())
             }
-            Type::Poly{ name, params } => {
-                let impls = self.rec_get_trait_impls(&name);
-                if impls.is_empty() {
-                    panic!("{} is not implemented", name);
+            hir::Expr::Decl(decl) => {
+                decl.t = self.deref_tyvar(mem::take(&mut decl.t))?;
+                Ok(())
+            },
+            hir::Expr::Def(def) => {
+                match &mut def.sig {
+                    hir::Signature::Var(var) => {
+                        var.t = self.deref_tyvar(mem::take(&mut var.t))?;
+                    },
+                    hir::Signature::Subr(subr) => {
+                        subr.t = self.deref_tyvar(mem::take(&mut subr.t))?;
+                    },
                 }
-                let min = self.smallest_t(impls.clone().into_iter()).unwrap_or_else(move || {
-                    panic!("cannot determine the smallest type: {}", fmt_vec(&impls))
-                });
-                dbg!(&min);
-                for (param, min_param) in params.iter().zip(min.typarams()) {
-                    self.unify_tp(param, &min_param, None, None, false)?;
+                for chunk in def.body.block.iter_mut() {
+                    self.deref_expr_t(chunk)?;
                 }
-                dbg!(&params);
-                Ok(min)
-            },
-            _ => Ok(maybe_poly),
+                Ok(())
+            }
+            hir::Expr::Lambda(lambda) => {
+                lambda.t = self.deref_tyvar(mem::take(&mut lambda.t))?;
+                for chunk in lambda.body.iter_mut() {
+                    self.deref_expr_t(chunk)?;
+                }
+                Ok(())
+            }
         }
     }
 
@@ -1887,6 +2056,11 @@ impl Context {
             (lt @ Type::FreeVar(lfv), rt @ Type::FreeVar(rfv))
                 if lfv.is_unbound() && rfv.is_unbound() =>
             {
+                if lfv.constraint_is_typeof() && !rfv.constraint_is_typeof() {
+                    lfv.update_constraint(rfv.crack_constraint().clone());
+                } else if rfv.constraint_is_typeof() && !lfv.constraint_is_typeof() {
+                    rfv.update_constraint(lfv.crack_constraint().clone());
+                }
                 if lfv.level().unwrap() > rfv.level().unwrap() {
                     lfv.link(rt);
                 } else {
@@ -2064,7 +2238,7 @@ impl Context {
                 }
                 Ok(())
             }
-            (l, r) if self.same_type_of(l, r, None, None) => Ok(()),
+            (l, r) if self.formal_same_type_of(l, r, None, None) => Ok(()),
             (l, r) => Err(TyCheckError::re_unification_error(
                 l,
                 r,
@@ -2076,6 +2250,10 @@ impl Context {
     }
 
     /// Assuming that `sub` is a subtype of `sup`, fill in the type variable to satisfy the assumption
+    ///
+    /// When comparing arguments and parameter, the left side is the argument (found) and the right side is the parameter (expected)
+    ///
+    /// The parameter type must be a supertype of the argument type
     /// ```
     /// sub_unify({I: Int | I == 0}, ?T(<: Ord)): (/* OK */)
     /// sub_unify(Int, ?T(:> Nat)): (?T :> Int)
@@ -2111,40 +2289,113 @@ impl Context {
                     | FreeKind::Unbound { constraint, .. } => match constraint {
                         // sub_unify(Nat, ?T(:> Int)): (/* OK */)
                         // sub_unify(Int, ?T(:> Nat)): (?T :> Int)
-                        Constraint::SupertypeOf(sub) if self.rec_full_supertype_of(l, sub) => {
+                        // sub_unify(Str, ?T(:> Int)): (/* ?T = Str or Int */) // TODO:
+                        Constraint::SupertypeOf(sub) => {
+                            if self.rec_full_supertype_of(l, sub) {
+                                *constraint = Constraint::SupertypeOf(l.clone());
+                            } else if self.rec_full_subtype_of(l, sub) {
+                                /* OK */
+                            } else {
+                                todo!()
+                            }
+                        }
+                        // sub_unify(Nat, ?T(<: Int)): (Nat <: ?T <: Int)
+                        // sub_unify(Nat, ?T(<: Add(?R, ?O))): (Nat <: ?T <: Add(?R, ?O))
+                        // sub_unify(Int, ?T(<: Nat)): (/* Error */)
+                        // sub_unify(Str, ?T(<: Int)): (/* Error */)
+                        Constraint::SubtypeOf(sup) => {
+                            if !self.rec_full_subtype_of(l, sup) {
+                                return Err(TyCheckError::subtyping_error(
+                                    l,
+                                    sup,
+                                    sub_loc,
+                                    sup_loc,
+                                    self.caused_by(),
+                                ))
+                            } else {
+                                *constraint = Constraint::sandwiched(l.clone(), mem::take(sup));
+                            }
+                        }
+                        // sub_unify(Nat, (Int <: ?T <: Ratio)): (/* OK */)
+                        // sub_unify(Int, (Nat <: ?T <: Ratio)): (Int <: ?T <: Ratio)
+                        // sub_unify(Str, (Nat <: ?T <: Ratio)): (/* Error */)
+                        // sub_unify({0}, ({1} <: ?T <: Nat)): ({0, 1} <: ?T <: Nat))
+                        Constraint::Sandwiched { sub, sup } => {
+                            if self.rec_full_no_relation_of(l, sup) {
+                                return Err(TyCheckError::subtyping_error(
+                                    l,
+                                    sup, // TODO:
+                                    sub_loc,
+                                    sup_loc,
+                                    self.caused_by(),
+                                ))
+                            } else {
+                                let union = self.union(l, sub);
+                                *constraint = Constraint::sandwiched(union, mem::take(sub));
+                            }
+                        }
+                        Constraint::TypeOf(_t) => {
                             *constraint = Constraint::SupertypeOf(l.clone());
+                        },
+                        _ => {}
+                    },
+                    _ => {}
+                }
+                return Ok(());
+            }
+            (Type::FreeVar(fv), r) if fv.is_unbound() => {
+                match &mut *fv.borrow_mut() {
+                    FreeKind::NamedUnbound { constraint, .. }
+                    | FreeKind::Unbound { constraint, .. } => match constraint {
+                        // sub_unify(?T(:> Int), Nat): (/* Error */)
+                        // sub_unify(?T(:> Nat), Int): (Nat <: ?T <: Int)
+                        // sub_unify(?T(:> Nat), Str): (/* Error */)
+                        Constraint::SupertypeOf(sub) => {
+                            if !self.rec_full_subtype_of(sub, r) {
+                                return Err(TyCheckError::subtyping_error(
+                                    sub,
+                                    r,
+                                    sub_loc,
+                                    sup_loc,
+                                    self.caused_by(),
+                                ))
+                            } else {
+                                *constraint = Constraint::sandwiched(sub.clone(), r.clone());
+                            }
                         }
-                        // sub_unify(Nat, ?T(<: Int)): (/* OK */)
-                        // sub_unify(Int, ?T(<: Nat)): Error!
-                        Constraint::SubtypeOf(sup) if self.rec_full_supertype_of(l, sup) => {
+                        // sub_unify(?T(<: Int), Nat): (?T(<: Nat))
+                        // sub_unify(?T(<: Nat), Int): (/* OK */)
+                        // sub_unify(?T(<: Str), Int): (/* Error */) // TODO:
+                        Constraint::SubtypeOf(sup)
+                            if self.rec_full_supertype_of(sup, r) =>
+                        {
+                            *constraint = Constraint::SubtypeOf(r.clone());
+                        }
+                        // sub_unify((Int <: ?T <: Ratio), Nat): (/* Error */)
+                        // sub_unify((Nat <: ?T <: Ratio), Int): (/* OK */)
+                        // sub_unify((Nat <: ?T <: Int), Str): (/* Error */)
+                        Constraint::Sandwiched { sub, sup: _ }
+                            if !self.rec_full_subtype_of(sub, r) =>
+                        {
                             return Err(TyCheckError::subtyping_error(
-                                l,
-                                sup,
+                                sub,
+                                r,
                                 sub_loc,
                                 sup_loc,
                                 self.caused_by(),
                             ))
                         }
-                        // sub_unify(Nat, (Ratio :> ?T :> Int)): (/* OK */)
-                        // sub_unify(Int, (Ratio :> ?T :> Nat)): (Ratio :> ?T :> Int)
-                        Constraint::Sandwiched { sub, sup }
-                            if self.rec_full_supertype_of(l, sub) =>
-                        {
-                            *constraint = Constraint::Sandwiched {
-                                sub: l.clone(),
-                                sup: mem::take(sup),
-                            };
-                        }
+                        // sub_unify(?T(: Type), Int): (?T(<: Int))
                         Constraint::TypeOf(_t) => {
-                            *constraint = Constraint::SupertypeOf(l.clone());
+                            *constraint = Constraint::SubtypeOf(r.clone());
                         },
                         _ => {}
                     },
                     _ => {}
                 }
                 return Ok(());
-            }
-            (Type::FreeVar(fv), _r) if fv.is_linked() => todo!(),
+            },
+            (Type::FreeVar(_fv), _r) => todo!(),
             (l @ Refinement(_), r @ Refinement(_)) => return self.unify(l, r, sub_loc, sup_loc),
             _ => {}
         }
@@ -2177,7 +2428,7 @@ impl Context {
                 if self.formal_supertype_of(l, maybe_sub, Some(&bounds), Some(&variance))
                     && self.formal_supertype_of(r, maybe_sup, Some(&bounds), Some(&variance))
                 {
-                    let tv_ctx = TyVarContext::new(self.level, bounds);
+                    let tv_ctx = TyVarContext::new(self.level, bounds, &self);
                     let (l, _) = Self::instantiate_t(l.clone(), tv_ctx.clone());
                     let (r, _) = Self::instantiate_t(r.clone(), tv_ctx);
                     Some((l, r))
@@ -2808,13 +3059,11 @@ impl Context {
         self.substitute_call(callee, &instance, pos_args, kw_args)?;
         log!("Substituted:\ninstance: {instance}");
         let res = self.deref_tyvar(instance)?;
-        log!("Eliminated:\nres: {res}\n");
+        log!("Derefed:\nres: {res}\n");
         let res = self.eval.eval_t_params(res, &self, self.level)?;
         log!("Params Evaluated:\nres: {res}\n");
         let res = self.deref_tyvar(res)?;
-        log!("Eliminated (2):\nres: {res}\n");
-        let res = self.monomorphise(res)?;
-        log!("Monomorphised:\nres: {res}\n");
+        log!("Derefed (2):\nres: {res}\n");
         self.propagate(&res, callee)?;
         log!("Propagated:\nres: {res}\n");
         Ok(res)
@@ -2829,7 +3078,7 @@ impl Context {
     ) -> bool {
         match (lhs, rhs) {
             (TyParam::Type(lhs), TyParam::Type(rhs)) => {
-                return self.same_type_of(lhs, rhs, bounds, lhs_variance)
+                return self.formal_same_type_of(lhs, rhs, bounds, lhs_variance)
             }
             (TyParam::Mono(l), TyParam::Mono(r)) => {
                 if let (Some((l, _)), Some((r, _))) = (
@@ -2837,7 +3086,7 @@ impl Context {
                     self.types.iter().find(|(t, _)| t.name() == &r[..]),
                 ) {
                     return self.formal_supertype_of(l, r, bounds, None)
-                        || self.subtype_of(l, r, bounds, lhs_variance);
+                        || self.formal_subtype_of(l, r, bounds, lhs_variance);
                 }
             }
             (TyParam::MonoQVar(name), other) | (other, TyParam::MonoQVar(name)) => {
@@ -2903,6 +3152,11 @@ impl Context {
         self.rec_full_supertype_of(rhs, lhs)
     }
 
+    /// !(L :> R || L <: R)
+    pub(crate) fn rec_full_no_relation_of(&self, lhs: &Type, rhs: &Type) -> bool {
+        !self.rec_full_supertype_of(lhs, rhs) && !self.rec_full_subtype_of(lhs, rhs)
+    }
+
     pub(crate) fn _rec_full_same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
         self.rec_full_supertype_of(lhs, rhs) && self.rec_full_subtype_of(lhs, rhs)
     }
@@ -3024,10 +3278,10 @@ impl Context {
                 && self.formal_supertype_of(&ls.return_t, &rs.return_t, bounds, lhs_variance) // covariant
                 && ls.non_default_params.iter()
                     .zip(rs.non_default_params.iter())
-                    .all(|(l, r)| self.subtype_of(&l.ty, &r.ty, bounds, lhs_variance))
+                    .all(|(l, r)| self.formal_subtype_of(&l.ty, &r.ty, bounds, lhs_variance))
                 && ls.default_params.iter()
                     .zip(rs.default_params.iter())
-                    .all(|(l, r)| self.subtype_of(&l.ty, &r.ty, bounds, lhs_variance))
+                    .all(|(l, r)| self.formal_subtype_of(&l.ty, &r.ty, bounds, lhs_variance))
                 // contravariant
             }
             // RefMut, OptionMut are invariant
@@ -3045,8 +3299,11 @@ impl Context {
                         Constraint::SubtypeOf(sup) => {
                             self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
                         }
-                        // `(?T :> X) :> Y` is true,
-                        Constraint::SupertypeOf(_) => true,
+                        // `(?T :> X) :> Y` is true
+                        // `(?T :> Str) :> Int` is true (?T :> Str or Int)
+                        Constraint::SupertypeOf(_sub) => {
+                            true
+                        },
                         // `(Nat <: ?T <: Ratio) :> Nat` can be true
                         Constraint::Sandwiched { sup, .. } => {
                             self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
@@ -3061,22 +3318,29 @@ impl Context {
                                 panic!()
                             }
                         }
+                        Constraint::Uninited => unreachable!(),
                     },
                 }
             }
-            (lhs, FreeVar(v)) => {
-                match &*v.borrow() {
+            (lhs, FreeVar(fv)) => {
+                match &*fv.borrow() {
                     FreeKind::Linked(t) => self.formal_supertype_of(lhs, t, bounds, lhs_variance),
                     FreeKind::Unbound { constraint, .. }
                     | FreeKind::NamedUnbound { constraint, .. } => match constraint {
-                        // `Nat :> (?T <: Int)` can be true => `X :> (?T <: Y)` can be true
-                        Constraint::SubtypeOf(_sup) => true,
+                        // ?T cannot be `Never`
+                        // `Nat :> (?T <: Int)` can be true
+                        // `Int :> (?T <: Nat)` can be true
+                        // `Str :> (?T <: Int)` is false
+                        Constraint::SubtypeOf(sup) => {
+                            self.formal_supertype_of(lhs, sup, bounds, lhs_variance)
+                            || self.formal_subtype_of(lhs, sup, bounds, lhs_variance)
+                        },
                         // `Int :> (?T :> Nat)` can be true, `Nat :> (?T :> Int)` is false
                         Constraint::SupertypeOf(sub) => {
                             self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
                         }
                         // `Int :> (Nat <: ?T <: Ratio)` can be true, `Nat :> (Int <: ?T <: Ratio)` is false
-                        Constraint::Sandwiched { sub, .. } => {
+                        Constraint::Sandwiched { sub, sup: _ } => {
                             self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
                         }
                         Constraint::TypeOf(t) => {
@@ -3086,6 +3350,7 @@ impl Context {
                                 panic!()
                             }
                         }
+                        Constraint::Uninited => unreachable!(),
                     },
                 }
             }
@@ -3120,8 +3385,12 @@ impl Context {
                 let nat = Type::Refinement(self.into_refinement(Nat));
                 self.formal_supertype_of(re, &nat, bounds, lhs_variance)
             }
-            // Int :> {I: Int | ...} == true, Real :> {I: Int | ...} == false, Int :> {I: Str| ...} == false
-            (l, Refinement(r)) => self.formal_supertype_of(l, &r.t, bounds, lhs_variance),
+            // Int :> {I: Int | ...} == true
+            // Real :> {I: Int | ...} == false
+            // Int :> {I: Str| ...} == false
+            (l, Refinement(r)) => {
+                self.formal_supertype_of(l, &r.t, bounds, lhs_variance)
+            },
             // ({I: Int | True} :> Int) == true, ({N: Nat | ...} :> Int) == false, ({I: Int | I >= 0} :> Int) == false
             (Refinement(l), r) => {
                 if l.preds
@@ -3186,7 +3455,7 @@ impl Context {
                         && lp.iter().zip(rp.iter()).zip(lhs_variance.iter()).all(
                             |((l, r), variance)| match (l, r, variance) {
                                 (TyParam::Type(l), TyParam::Type(r), Variance::Contravariant) => {
-                                    self.subtype_of(l, r, bounds, Some(lhs_variance))
+                                    self.formal_subtype_of(l, r, bounds, Some(lhs_variance))
                                 }
                                 (TyParam::Type(l), TyParam::Type(r), Variance::Covariant) => {
                                     self.formal_supertype_of(l, r, bounds, Some(lhs_variance))
@@ -3208,7 +3477,7 @@ impl Context {
                     if let Some(bound) = bs.iter().find(|b| b.mentions_as_subtype(name)) {
                         self.formal_supertype_of(bound.t(), r, bounds, lhs_variance)
                     } else if let Some(bound) = bs.iter().find(|b| b.mentions_as_instance(name)) {
-                        if self.same_type_of(bound.t(), &Type::Type, bounds, lhs_variance) {
+                        if self.formal_same_type_of(bound.t(), &Type::Type, bounds, lhs_variance) {
                             true
                         } else {
                             todo!()
@@ -3234,7 +3503,7 @@ impl Context {
     }
 
     /// lhs <: rhs?
-    pub(crate) fn subtype_of(
+    pub(crate) fn formal_subtype_of(
         &self,
         lhs: &Type,
         rhs: &Type,
@@ -3244,7 +3513,7 @@ impl Context {
         self.formal_supertype_of(rhs, lhs, bounds, lhs_variance)
     }
 
-    pub(crate) fn same_type_of(
+    pub(crate) fn formal_same_type_of(
         &self,
         lhs: &Type,
         rhs: &Type,
@@ -3252,7 +3521,7 @@ impl Context {
         lhs_variance: Option<&Vec<Variance>>,
     ) -> bool {
         self.formal_supertype_of(lhs, rhs, bounds, lhs_variance)
-            && self.subtype_of(lhs, rhs, bounds, lhs_variance)
+            && self.formal_subtype_of(lhs, rhs, bounds, lhs_variance)
     }
 
     fn try_cmp(
@@ -3330,6 +3599,8 @@ impl Context {
                         (Any, Less) => Some(Less),
                         (Any, Equal | LessEqual) => Some(LessEqual),
                         (Any, Greater | NotEqual | GreaterEqual | Any) => Some(Any),
+                        (l, r) =>
+                            todo!("cmp({inf}, {sup}) = {l:?}, cmp({inf}, {sup}) = {r:?}"),
                     }
                 } else { None }
             }
@@ -3385,7 +3656,7 @@ impl Context {
 
     fn union_refinement(&self, lhs: &RefinementType, rhs: &RefinementType) -> RefinementType {
         if !self.formal_supertype_of(&lhs.t, &rhs.t, None, None)
-            && !self.subtype_of(&lhs.t, &rhs.t, None, None)
+            && !self.formal_subtype_of(&lhs.t, &rhs.t, None, None)
         {
             log!("{lhs}\n{rhs}");
             todo!()
@@ -3563,24 +3834,25 @@ impl Context {
         match self.min(lhs, rhs) {
             Some(l) if l == lhs => TyParamOrdering::Less,
             Some(_) => TyParamOrdering::Greater,
-            None => todo!("{lhs}, {rhs}"),
+            None => TyParamOrdering::NoRelation,
         }
     }
 
     // TODO:
     fn smallest_pair<I: Iterator<Item = (Type, Type)>>(&self, ts: I) -> Option<(Type, Type)> {
-        ts.min_by(|(_, lhs), (_, rhs)| self.cmp_t(lhs, rhs).try_into().unwrap())
-    }
-
-    fn smallest_t<I: Iterator<Item = Type>>(&self, ts: I) -> Option<Type> {
-        ts.min_by(|lhs, rhs| {
-            let cmp = self.cmp_t(lhs, rhs);
-            cmp.try_into().unwrap_or_else(|_| panic!("{cmp:?}"))
+        ts.min_by(|(_, lhs), (_, rhs)| {
+            // HACK: Equal for unrelated types
+            // This doesn't work with [Nat, Str, Int] for example
+            self.cmp_t(lhs, rhs).try_into().unwrap() // _or(Ordering::Equal)
         })
     }
 
     fn smallest_ref_t<'t, I: Iterator<Item = &'t Type>>(&self, ts: I) -> Option<&'t Type> {
-        ts.min_by(|lhs, rhs| self.cmp_t(lhs, rhs).try_into().unwrap())
+        ts.min_by(|lhs, rhs| {
+            // HACK: Equal for unrelated types
+            // This doesn't work with [Int, Str, Nat] for example
+            self.cmp_t(lhs, rhs).try_into().unwrap() //_or(Ordering::Equal)
+        })
     }
 
     pub(crate) fn get_local(&self, name: &Token, namespace: &Str) -> TyCheckResult<ConstObj> {
@@ -3718,7 +3990,11 @@ impl Context {
     /// tと一致ないしそれよりも大きい型のContextを返す
     fn sorted_type_ctxs<'a>(&'a self, t: &'a Type) -> impl Iterator<Item = &'a Context> {
         let mut ctxs = self._type_ctxs(t).collect::<Vec<_>>();
-        ctxs.sort_by(|(lhs, _), (rhs, _)| self.cmp_t(lhs, rhs).try_into().unwrap());
+        ctxs.sort_by(|(lhs, _), (rhs, _)| {
+            // HACK: Equal for unrelated types
+            // This doesn't work with [Int, Str, Nat] for example
+            self.cmp_t(lhs, rhs).try_into().unwrap_or_else(|_| panic!("{lhs}, {rhs}")) // _or(Ordering::Equal)
+        });
         ctxs.into_iter().map(|(_, ctx)| ctx)
     }
 
@@ -3727,10 +4003,6 @@ impl Context {
         self.types.iter().filter_map(move |(maybe_sup, ctx)| {
             let bounds = ctx.type_params_bounds();
             let variance = ctx.type_params_variance();
-            if t.name().contains("Range") && maybe_sup.name().contains("Range") {
-                dbg!(&bounds, &variance);
-                dbg!(maybe_sup, t);
-            }
             if self.formal_supertype_of(maybe_sup, t, Some(&bounds), Some(&variance)) {
                 Some((maybe_sup, ctx))
             } else {
@@ -3773,17 +4045,32 @@ impl Context {
         None
     }
 
-    fn rec_get_trait_impls(&self, name: &Str) -> Vec<Type> {
-        let impls = if let Some(impls) = self.poly_trait_impls.get(name) {
-            impls.clone()
-        } else { vec![] };
+    pub(crate) fn rec_type_ctx_by_name<'a>(
+        &'a self,
+        t_name: &'a str,
+    ) -> Option<&'a Context> {
+        if let Some((_, ctx)) = self.types
+            .iter()
+            .find(|(t, _ctx)| t.name() == t_name)
+        {
+            return Some(ctx);
+        }
         if let Some(outer) = &self.outer {
-            [impls, outer.rec_get_trait_impls(name)].concat()
+            outer.rec_type_ctx_by_name(t_name)
         } else {
-            impls
+            None
         }
     }
 
+    fn rec_get_const_param_defaults(&self, name: &str) -> Option<&Vec<ConstTemplate>> {
+        if let Some(impls) = self.const_param_defaults.get(name) {
+            return Some(impls)
+        }
+        if let Some(outer) = &self.outer {
+            outer.rec_get_const_param_defaults(name)
+        } else { None }
+    }
+
     // 再帰サブルーチン/型の推論を可能にするため、予め登録しておく
     pub(crate) fn preregister(&mut self, block: &Vec<ast::Expr>) -> TyCheckResult<()> {
         for expr in block.iter() {
diff --git a/compiler/erg_compiler/effectcheck.rs b/compiler/erg_compiler/effectcheck.rs
index a5f1ec86c..a6761aaeb 100644
--- a/compiler/erg_compiler/effectcheck.rs
+++ b/compiler/erg_compiler/effectcheck.rs
@@ -48,10 +48,10 @@ impl SideEffectChecker {
                     self.check_def(def, true);
                 }
                 Expr::Call(call) => {
-                    for parg in call.args.pos_args().iter() {
+                    for parg in call.args.pos_args.iter() {
                         self.check_expr(&parg.expr, true);
                     }
-                    for kwarg in call.args.kw_args().iter() {
+                    for kwarg in call.args.kw_args.iter() {
                         self.check_expr(&kwarg.expr, true);
                     }
                 }
@@ -169,11 +169,11 @@ impl SideEffectChecker {
                         .push(EffectError::has_effect(expr, self.full_path()));
                 }
                 call.args
-                    .pos_args()
+                    .pos_args
                     .iter()
                     .for_each(|parg| self.check_expr(&parg.expr, allow_self_effect));
                 call.args
-                    .kw_args()
+                    .kw_args
                     .iter()
                     .for_each(|kwarg| self.check_expr(&kwarg.expr, allow_self_effect));
             }
diff --git a/compiler/erg_compiler/error.rs b/compiler/erg_compiler/error.rs
index 581cd53ac..2a62f2fe5 100644
--- a/compiler/erg_compiler/error.rs
+++ b/compiler/erg_compiler/error.rs
@@ -64,9 +64,9 @@ pub fn readable_name(name: &str) -> &str {
         "__pow__" => "`**`",
         "__mod__" => "`%`",
         "__rng__" => "`..`",
-        "__lrng__" => "`<..`",
-        "__rrng__" => "`..<`",
-        "__lrrng__" => "`<..<`",
+        "__lorng__" => "`<..`",
+        "__rorng__" => "`..<`",
+        "__orng__" => "`<..<`",
         "__and__" => "`and`",
         "__or__" => "`or`",
         "__in__" => "`in`",
@@ -373,7 +373,6 @@ impl TyCheckError {
         expect: &Type,
         found: &Type,
     ) -> Self {
-        let name = readable_name(name);
         Self::new(ErrorCore::new(0, TypeError, loc, switch_lang!(
             format!("the type of {name} is mismatched:\nexpected:  {GREEN}{expect}{RESET}\nbut found: {RED}{found}{RESET}"),
             format!("{name}の型が違います。\n予期した型: {GREEN}{expect}{RESET}\n与えられた型: {RED}{found}{RESET}")
@@ -387,7 +386,6 @@ impl TyCheckError {
         expect: &Type,
         found: &Type,
     ) -> Self {
-        let name = readable_name(name);
         Self::new(ErrorCore::new(0, TypeError, loc, switch_lang!(
             format!("the return type of {name} is mismatched:\nexpected:  {GREEN}{expect}{RESET}\nbut found: {RED}{found}{RESET}"),
             format!("{name}の戻り値の型が違います。\n予期した型: {GREEN}{expect}{RESET}\n与えられた型: {RED}{found}{RESET}")
@@ -395,7 +393,6 @@ impl TyCheckError {
     }
 
     pub fn uninitialized_error(loc: Location, caused_by: Str, name: &str, t: &Type) -> Self {
-        let name = readable_name(name);
         Self::new(
             ErrorCore::new(
                 0,
@@ -450,6 +447,15 @@ impl TyCheckError {
         )
     }
 
+    pub fn dummy_infer_error(fn_name: &str, line: u32) -> Self {
+        Self::new(ErrorCore::unreachable(fn_name, line), "".into())
+    }
+
+    pub fn not_relation(fn_name: &str, line: u32) -> Self {
+        Self::new(ErrorCore::unreachable(fn_name, line), "".into())
+    }
+
+
     pub fn reassign_error(loc: Location, caused_by: Str, name: &str) -> Self {
         let name = readable_name(name);
         Self::new(
diff --git a/compiler/erg_compiler/eval.rs b/compiler/erg_compiler/eval.rs
index b54ab5e38..2d13fe3ef 100644
--- a/compiler/erg_compiler/eval.rs
+++ b/compiler/erg_compiler/eval.rs
@@ -41,9 +41,9 @@ impl SubstContext {
         self_
     }
 
-    fn substitute(&self, quant_t: Type, ty_ctx: &Context, level: usize) -> TyCheckResult<Type> {
+    fn substitute(&self, quant_t: Type, ty_ctx: &Context, level: usize, ctx: &Context) -> TyCheckResult<Type> {
         let bounds = ty_ctx.type_params_bounds();
-        let tv_ctx = TyVarContext::new(level, bounds);
+        let tv_ctx = TyVarContext::new(level, bounds, ctx);
         let (inst, _) = Context::instantiate_t(quant_t, tv_ctx);
         for param in inst.typarams() {
             self.substitute_tp(&param, ty_ctx)?;
@@ -358,7 +358,7 @@ impl Evaluator {
                     if let Ok(obj) = ty_ctx.get_local(&Token::symbol(&rhs), &ctx.name) {
                         if let ConstObj::Type(quant_t) = obj {
                             let subst_ctx = SubstContext::new(&lhs, ty_ctx);
-                            let t = subst_ctx.substitute(*quant_t, ty_ctx, level)?;
+                            let t = subst_ctx.substitute(*quant_t, ty_ctx, level, ctx)?;
                             let t = self.eval_t_params(t, ctx, level)?;
                             return Ok(t);
                         } else {
@@ -366,9 +366,13 @@ impl Evaluator {
                         }
                     }
                 }
-                todo!()
+                if let Some(outer) = &ctx.outer {
+                    self.eval_t_params(Type::MonoProj { lhs, rhs }, outer, level)
+                } else {
+                    todo!("{lhs}.{rhs} not found in {}", erg_common::fmt_iter(ctx.rec_sorted_type_ctxs(&lhs)))
+                }
             }
-            Type::Ref(l) => Ok(Type::refer(self.eval_t_params(*l, ctx, level)?)),
+            Type::Ref(l) => Ok(Type::ref_(self.eval_t_params(*l, ctx, level)?)),
             Type::RefMut(l) => Ok(Type::ref_mut(self.eval_t_params(*l, ctx, level)?)),
             Type::VarArgs(l) => Ok(Type::var_args(self.eval_t_params(*l, ctx, level)?)),
             Type::Poly { name, mut params } => {
diff --git a/compiler/erg_compiler/hir.rs b/compiler/erg_compiler/hir.rs
index b2affa606..8f91b26aa 100644
--- a/compiler/erg_compiler/hir.rs
+++ b/compiler/erg_compiler/hir.rs
@@ -14,6 +14,8 @@ use erg_common::{
 use erg_parser::ast::{fmt_lines, DefId, Params, VarName, VarPattern};
 use erg_parser::token::{Token, TokenKind};
 
+use crate::error::readable_name;
+
 #[derive(Debug, Clone)]
 pub struct Literal {
     pub data: ValueObj, // for constant folding
@@ -26,10 +28,17 @@ impl HasType for Literal {
     fn ref_t(&self) -> &Type {
         &self.t
     }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
     #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl NestedDisplay for Literal {
@@ -129,8 +138,8 @@ impl KwArg {
 
 #[derive(Debug, Clone)]
 pub struct Args {
-    pos_args: Vec<PosArg>,
-    kw_args: Vec<KwArg>,
+    pub pos_args: Vec<PosArg>,
+    pub kw_args: Vec<KwArg>,
     paren: Option<(Token, Token)>,
 }
 
@@ -194,14 +203,6 @@ impl Args {
         self.kw_args.len()
     }
 
-    pub fn pos_args(&self) -> &[PosArg] {
-        &self.pos_args[..]
-    }
-
-    pub fn kw_args(&self) -> &[KwArg] {
-        &self.kw_args[..]
-    }
-
     pub fn push_pos(&mut self, pos: PosArg) {
         self.pos_args.push(pos);
     }
@@ -279,9 +280,17 @@ impl HasType for Local {
         &self.t
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl Locational for Local {
@@ -328,9 +337,17 @@ impl HasType for Attribute {
         &self.t
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl Attribute {
@@ -364,9 +381,17 @@ impl HasType for Subscript {
         &self.t
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl Subscript {
@@ -411,9 +436,21 @@ impl HasType for Accessor {
         }
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        match self {
+            Self::Local(n) | Self::SelfDot(n) => n.ref_mut_t(),
+            Self::Attr(a) => a.ref_mut_t(),
+            Self::Subscr(s) => s.ref_mut_t(),
+        }
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl Accessor {
@@ -435,11 +472,11 @@ impl Accessor {
 
     pub fn var_full_name(&self) -> Option<String> {
         match self {
-            Self::Local(local) => Some(local.inspect().to_string()),
+            Self::Local(local) => Some(readable_name(local.inspect()).to_string()),
             Self::Attr(attr) => attr
                 .obj
                 .var_full_name()
-                .map(|n| n + "." + attr.name.inspect()),
+                .map(|n| n + "." + readable_name(attr.name.inspect())),
             Self::Subscr(_) | Self::SelfDot(_) => todo!(),
         }
     }
@@ -468,9 +505,17 @@ impl HasType for Array {
         &self.t
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl NestedDisplay for Array {
@@ -495,7 +540,7 @@ impl Array {
         guard: Option<Expr>,
     ) -> Self {
         let elem_t = elems
-            .pos_args()
+            .pos_args
             .first()
             .map(|a| a.expr.t())
             .unwrap_or_else(|| Type::free_var(level, Constraint::TypeOf(Type::Type)));
@@ -525,6 +570,9 @@ impl HasType for Dict {
     fn ref_t(&self) -> &Type {
         todo!()
     }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        todo!()
+    }
     fn t(&self) -> Type {
         todo!()
     }
@@ -532,6 +580,10 @@ impl HasType for Dict {
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl NestedDisplay for Dict {
@@ -563,7 +615,7 @@ pub struct BinOp {
 
 impl NestedDisplay for BinOp {
     fn fmt_nest(&self, f: &mut fmt::Formatter<'_>, level: usize) -> fmt::Result {
-        write!(f, "`{}`:\n", self.op.content)?;
+        write!(f, "`{}`: {}:\n", self.op.content, self.sig_t)?;
         self.lhs.fmt_nest(f, level + 1)?;
         write!(f, "\n")?;
         self.rhs.fmt_nest(f, level + 1)
@@ -573,20 +625,27 @@ impl NestedDisplay for BinOp {
 impl HasType for BinOp {
     #[inline]
     fn ref_t(&self) -> &Type {
-        &self.sig_t.return_t().unwrap()
+        self.sig_t.return_t().unwrap()
+    }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        self.sig_t.mut_return_t().unwrap()
     }
     #[inline]
     fn lhs_t(&self) -> &Type {
-        &self.sig_t.lhs_t()
+        self.sig_t.lhs_t()
     }
     #[inline]
     fn rhs_t(&self) -> &Type {
-        &self.sig_t.rhs_t()
+        self.sig_t.rhs_t()
     }
     #[inline]
     fn signature_t(&self) -> Option<&Type> {
         Some(&self.sig_t)
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        Some(&mut self.sig_t)
+    }
 }
 
 impl_display_from_nested!(BinOp);
@@ -613,7 +672,10 @@ pub struct UnaryOp {
 impl HasType for UnaryOp {
     #[inline]
     fn ref_t(&self) -> &Type {
-        &self.sig_t.return_t().unwrap()
+        self.sig_t.return_t().unwrap()
+    }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        self.sig_t.mut_return_t().unwrap()
     }
     #[inline]
     fn lhs_t(&self) -> &Type {
@@ -627,6 +689,10 @@ impl HasType for UnaryOp {
     fn signature_t(&self) -> Option<&Type> {
         Some(&self.sig_t)
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        Some(&mut self.sig_t)
+    }
 }
 
 impl NestedDisplay for UnaryOp {
@@ -670,7 +736,11 @@ impl_display_from_nested!(Call);
 impl HasType for Call {
     #[inline]
     fn ref_t(&self) -> &Type {
-        &self.sig_t.return_t().unwrap()
+        self.sig_t.return_t().unwrap()
+    }
+    #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        self.sig_t.mut_return_t().unwrap()
     }
     #[inline]
     fn lhs_t(&self) -> &Type {
@@ -684,6 +754,10 @@ impl HasType for Call {
     fn signature_t(&self) -> Option<&Type> {
         Some(&self.sig_t)
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        Some(&mut self.sig_t)
+    }
 }
 
 impl Locational for Call {
@@ -718,6 +792,10 @@ impl HasType for Block {
         self.last().unwrap().ref_t()
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        self.last_mut().unwrap().ref_mut_t()
+    }
+    #[inline]
     fn t(&self) -> Type {
         self.last().unwrap().t()
     }
@@ -725,6 +803,10 @@ impl HasType for Block {
     fn signature_t(&self) -> Option<&Type> {
         self.last().unwrap().signature_t()
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        self.last_mut().unwrap().signature_mut_t()
+    }
 }
 
 impl NestedDisplay for Block {
@@ -805,7 +887,7 @@ pub struct Lambda {
     op: Token,
     pub body: Block,
     pub id: usize,
-    t: Type,
+    pub t: Type,
 }
 
 impl HasType for Lambda {
@@ -814,9 +896,17 @@ impl HasType for Lambda {
         &self.t
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl NestedDisplay for Lambda {
@@ -879,7 +969,7 @@ impl Signature {
 #[derive(Debug, Clone)]
 pub struct Decl {
     pub sig: Signature,
-    t: Type,
+    pub t: Type,
 }
 
 impl NestedDisplay for Decl {
@@ -991,6 +1081,19 @@ impl HasType for Expr {
             _ => &Type::NoneType,
         }
     }
+    fn ref_mut_t(&mut self) -> &mut Type {
+        match self {
+            Expr::Lit(lit) => lit.ref_mut_t(),
+            Expr::Accessor(accessor) => accessor.ref_mut_t(),
+            Expr::Array(array) => array.ref_mut_t(),
+            Expr::Dict(dict) => dict.ref_mut_t(),
+            Expr::BinOp(bin) => bin.ref_mut_t(),
+            Expr::UnaryOp(unary) => unary.ref_mut_t(),
+            Expr::Call(call) => call.ref_mut_t(),
+            Expr::Lambda(lambda) => lambda.ref_mut_t(),
+            _ => todo!(),
+        }
+    }
     fn signature_t(&self) -> Option<&Type> {
         match self {
             Expr::BinOp(bin) => bin.signature_t(),
@@ -999,6 +1102,14 @@ impl HasType for Expr {
             _ => None,
         }
     }
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        match self {
+            Expr::BinOp(bin) => bin.signature_mut_t(),
+            Expr::UnaryOp(unary) => unary.signature_mut_t(),
+            Expr::Call(call) => call.signature_mut_t(),
+            _ => None,
+        }
+    }
 }
 
 impl Expr {
diff --git a/compiler/erg_compiler/initialize.rs b/compiler/erg_compiler/initialize.rs
index b5452db42..ecd557378 100644
--- a/compiler/erg_compiler/initialize.rs
+++ b/compiler/erg_compiler/initialize.rs
@@ -10,14 +10,13 @@ use Type::*;
 
 use erg_parser::ast::VarName;
 
-use crate::context::{Context, DefaultInfo, ParamSpec};
+use crate::context::{Context, DefaultInfo, ParamSpec, ConstTemplate};
 use crate::varinfo::{Mutability, VarInfo, VarKind, Visibility};
 use DefaultInfo::*;
 use Mutability::*;
 use VarKind::*;
 use Visibility::*;
 
-// NOTE: TyParam::MonoQuantVarは生成時に型を指定する必要があるが、逆にそちらがあれば型境界を指定しなくてもよい
 impl Context {
     fn register_decl(&mut self, name: &'static str, t: Type, vis: Visibility) {
         let name = VarName::from_static(name);
@@ -47,6 +46,14 @@ impl Context {
         }
     }
 
+    fn register_const_param_defaults(&mut self, name: &'static str, params: Vec<ConstTemplate>) {
+        if self.const_param_defaults.get(name).is_some() {
+            panic!("already registered: {name}");
+        } else {
+            self.const_param_defaults.insert(Str::ever(name), params);
+        }
+    }
+
     fn register_type(&mut self, t: Type, ctx: Self, muty: Mutability) {
         if self.types.contains_key(&t) {
             panic!("{} has already been registered", t.name());
@@ -57,11 +64,11 @@ impl Context {
             for impl_trait in ctx.super_traits.iter() {
                 if !impl_trait.is_monomorphic() {
                     if let Some(impls) = self.poly_trait_impls.get_mut(impl_trait.name()) {
-                        impls.push(impl_trait.clone());
+                        impls.push((t.clone(), impl_trait.clone()));
                     } else {
                         self.poly_trait_impls.insert(
                             Str::rc(impl_trait.name()),
-                            vec![impl_trait.clone()],
+                            vec![(t.clone(), impl_trait.clone())],
                         );
                     }
                 }
@@ -78,10 +85,10 @@ impl Context {
             self.locals
                 .insert(name.clone(), VarInfo::new(Type, muty, Private, Builtin));
             for method_name in ctx.locals.keys() {
-                if let Some(patches) = self._method_impl_patches.get_mut(method_name) {
+                if let Some(patches) = self.method_impl_patches.get_mut(method_name) {
                     patches.push(name.clone());
                 } else {
-                    self._method_impl_patches
+                    self.method_impl_patches
                         .insert(method_name.clone(), vec![name.clone()]);
                 }
             }
@@ -100,127 +107,108 @@ impl Context {
     }
 
     /// see std/prelude.er
+    /// All type boundaries are defined in each subroutine
+    /// `push_subtype_bound`, etc. are used for type boundary determination in user-defined APIs
     // 型境界はすべて各サブルーチンで定義する
     // push_subtype_boundなどはユーザー定義APIの型境界決定のために使用する
     fn init_builtin_traits(&mut self) {
         let named = Self::mono_trait("Named", vec![], Self::TOP_LEVEL);
+        // Erg does not have a trait equivalent to `PartialEq` in Rust
+        // This means, Erg's `Float` cannot be compared with other `Float`
+        // use `l - r < EPSILON` to check if two floats are almost equal
         let mut eq = Self::poly_trait("Eq", vec![PS::t("R", WithDefault)], vec![], Self::TOP_LEVEL);
-        // __eq__: |Self <: Eq; R <: Eq()| Self(R).(R) -> Bool
-        let op_t = fn1_met(poly("Self", vec![ty_tp(mono_q("R"))]), mono_q("R"), Bool);
+        // __eq__: |Self <: Eq()| Self.(Self) -> Bool
+        let op_t = fn1_met(mono_q("Self"), mono_q("R"), Bool);
         let op_t = quant(
             op_t,
-            set! {subtype(mono_q("Self"), mono("Eq")), subtype(mono_q("R"), poly("Eq", vec![]))},
+            set! {
+                subtype(mono_q("Self"), poly("Eq", vec![ty_tp(mono_q("R"))])),
+                static_instance("R", Type)
+            },
         );
         eq.register_decl("__eq__", op_t.clone(), Public);
-        let mut ord = Self::poly_trait(
-            "Ord",
+        let mut partial_ord = Self::poly_trait(
+            "PartialOrd",
             vec![PS::t("R", WithDefault)],
-            vec![mono("Eq")],
+            vec![poly("PartialEq", vec![ty_tp(mono_q("R"))])],
             Self::TOP_LEVEL,
         );
         let op_t = fn1_met(poly("Self", vec![ty_tp(mono_q("R"))]), mono_q("R"), Bool);
         let op_t = quant(
             op_t,
-            set! {subtype(mono_q("Self"), mono("Ord")), subtype(mono_q("R"), poly("Ord", vec![]))},
+            set! {
+                subtype(mono_q("Self"), poly("PartialOrd", vec![ty_tp(mono_q("R"))])),
+                static_instance("R", Type)
+            },
+        );
+        partial_ord.register_decl("__lt__", op_t.clone(), Public);
+        let ord = Self::mono_trait(
+            "Ord",
+            vec![poly("Eq", vec![]), poly("PartialOrd", vec![])],
+            Self::TOP_LEVEL,
         );
-        ord.register_decl("__lt__", op_t.clone(), Public);
         let mut seq = Self::poly_trait(
             "Seq",
             vec![PS::t("T", NonDefault)],
             vec![poly("Output", vec![ty_tp(mono_q("T"))])],
             Self::TOP_LEVEL,
         );
-        let self_t = poly_q("Self", vec![TyParam::t(mono_q("T"))]);
+        let self_t = mono_q("Self");
         let t = fn0_met(self_t.clone(), Nat);
-        let t = quant(t, set! {subtype(self_t.clone(), mono("Seq"))});
+        let t = quant(t, set! {subtype(self_t.clone(), poly("Seq", vec![TyParam::erased(Type)]))});
         seq.register_decl("__len__", t, Public);
         let t = Type::fn1_met(self_t.clone(), Nat, mono_q("T"));
         let t = quant(
             t,
-            set! {subtype(self_t, mono("Seq")), static_instance("T", Type)},
+            set! {subtype(self_t, poly("Seq", vec![ty_tp(mono_q("T"))])), static_instance("T", Type)},
         );
+        // Seq.get: |Self <: Seq(T)| Self.(Nat) -> T
         seq.register_decl("get", t, Public);
         let params = vec![PS::t("T", NonDefault)];
         let input = Self::poly_trait("Input", params.clone(), vec![], Self::TOP_LEVEL);
         let output = Self::poly_trait("Output", params.clone(), vec![], Self::TOP_LEVEL);
-        let (r, o) = (mono_q("R"), mono_q("O"));
-        let (r_bound, o_bound) = (static_instance("R", Type), static_instance("O", Type));
-        let params = vec![PS::t("R", WithDefault), PS::t("O", WithDefault)];
-        let ty_params = vec![mono_q_tp("R"), mono_q_tp("O")];
+        let r = mono_q("R");
+        let r_bound = static_instance("R", Type);
+        let params = vec![PS::t("R", WithDefault)];
+        let ty_params = vec![ty_tp(mono_q("R"))];
         let mut add = Self::poly_trait("Add", params.clone(), vec![
             poly("Output", vec![ty_tp(mono_q("R"))]),
-            poly("Output", vec![ty_tp(mono_q("O"))]),
         ], Self::TOP_LEVEL);
         let self_bound = subtype(
-            poly_q("Self", ty_params.clone()),
+            mono_q("Self"),
             poly("Add", ty_params.clone()),
         );
-        let op_t = fn1_met(poly_q("Self", ty_params.clone()), r.clone(), o.clone());
-        let op_t = quant(op_t, set! {r_bound.clone(), o_bound.clone(), self_bound});
+        let op_t = fn1_met(poly_q("Self", ty_params.clone()), r.clone(), mono_proj(mono_q("Self"), "AddO"));
+        let op_t = quant(op_t, set! {r_bound.clone(), self_bound});
         add.register_decl("__add__", op_t, Public);
+        add.register_decl("AddO", Type, Public);
         let mut sub = Self::poly_trait("Sub", params.clone(), vec![
             poly("Output", vec![ty_tp(mono_q("R"))]),
-            poly("Output", vec![ty_tp(mono_q("O"))]),
         ], Self::TOP_LEVEL);
         let self_bound = subtype(
-            poly_q("Self", ty_params.clone()),
+            mono_q("Self"),
             poly("Sub", ty_params.clone()),
         );
-        let op_t = fn1_met(poly_q("Self", ty_params.clone()), r.clone(), o.clone());
-        let op_t = quant(op_t, set! {r_bound.clone(), o_bound.clone(), self_bound});
+        let op_t = fn1_met(poly_q("Self", ty_params.clone()), r.clone(), mono_proj(mono_q("Self"), "SubO"));
+        let op_t = quant(op_t, set! {r_bound.clone(), self_bound});
         sub.register_decl("__sub__", op_t, Public);
+        sub.register_decl("SubO", Type, Public);
         let mut mul = Self::poly_trait("Mul", params.clone(), vec![
             poly("Output", vec![ty_tp(mono_q("R"))]),
-            poly("Output", vec![ty_tp(mono_q("O"))]),
         ], Self::TOP_LEVEL);
-        let op_t = fn1_met(poly("Mul", ty_params.clone()), r.clone(), o.clone());
+        let op_t = fn1_met(poly("Mul", ty_params.clone()), r.clone(), mono_proj(mono_q("Self"), "MulO"));
         mul.register_decl("__mul__", op_t, Public);
+        mul.register_decl("MulO", Type, Public);
         let mut div = Self::poly_trait("Div", params.clone(), vec![
             poly("Output", vec![ty_tp(mono_q("R"))]),
-            poly("Output", vec![ty_tp(mono_q("O"))]),
         ], Self::TOP_LEVEL);
-        let op_t = fn1_met(poly("Div", ty_params.clone()), r, o);
+        let op_t = fn1_met(poly("Div", ty_params.clone()), r, mono_proj(mono_q("Self"), "DivO"));
         div.register_decl("__div__", op_t, Public);
-        /*let sup = poly(
-            "Add",
-            vec![
-                mono_q_tp("Self"),
-                TyParam::mono_proj(mono_q_tp("Self"), "AddO"),
-            ],
-        );
-        let mut closed_add = Self::mono_trait("SelfAdd", vec![sup], Self::TOP_LEVEL);
-        closed_add.register_decl("AddO", Type, Public);
-        let sup = poly(
-            "Sub",
-            vec![
-                mono_q_tp("Self"),
-                TyParam::mono_proj(mono_q_tp("Self"), "SubO"),
-            ],
-        );
-        let mut closed_sub = Self::mono_trait("SelfSub", vec![sup], Self::TOP_LEVEL);
-        closed_sub.register_decl("SubO", Type, Public);
-        let sup = poly(
-            "Mul",
-            vec![
-                mono_q_tp("Self"),
-                TyParam::mono_proj(mono_q_tp("Self"), "MulO"),
-            ],
-        );
-        let mut closed_mul = Self::mono_trait("SelfMul", vec![sup], Self::TOP_LEVEL);
-        closed_mul.register_decl("MulO", Type, Public);
-        let sup = Type::poly(
-            "Div",
-            vec![
-                mono_q_tp("Self"),
-                TyParam::mono_proj(mono_q_tp("Self"), "DivO"),
-            ],
-        );
-        let mut closed_div = Self::mono_trait("SelfDiv", vec![sup], Self::TOP_LEVEL);
-        closed_div.register_decl("DivO", Type, Public);
-        */
+        div.register_decl("DivO", Type, Public);
         self.register_type(mono("Named"), named, Const);
         self.register_type(poly("Eq", vec![ty_tp(mono_q("R"))]), eq, Const);
-        self.register_type(poly("Ord", vec![ty_tp(mono_q("R"))]), ord, Const);
+        self.register_type(poly("PartialOrd", vec![ty_tp(mono_q("R"))]), partial_ord, Const);
+        self.register_type(mono("Ord"), ord, Const);
         self.register_type(poly("Seq", vec![ty_tp(mono_q("T"))]), seq, Const);
         self.register_type(poly("Input", vec![ty_tp(mono_q("T"))]), input, Const);
         self.register_type(poly("Output", vec![ty_tp(mono_q("T"))]), output, Const);
@@ -229,6 +217,12 @@ impl Context {
         self.register_type(poly("Mul", ty_params.clone()), mul, Const);
         self.register_type(poly("Div", ty_params), div, Const);
         // self.register_type(mono("Num"), num, Const);
+        self.register_const_param_defaults("Eq", vec![ConstTemplate::Obj(ConstObj::t(mono_q("Self")))]);
+        self.register_const_param_defaults("PartialOrd", vec![ConstTemplate::app("Self", vec![], vec![])]);
+        self.register_const_param_defaults("Add", vec![ConstTemplate::Obj(ConstObj::t(mono_q("Self")))]);
+        self.register_const_param_defaults("Sub", vec![ConstTemplate::Obj(ConstObj::t(mono_q("Self")))]);
+        self.register_const_param_defaults("Mul", vec![ConstTemplate::Obj(ConstObj::t(mono_q("Self")))]);
+        self.register_const_param_defaults("Div", vec![ConstTemplate::Obj(ConstObj::t(mono_q("Self")))]);
     }
 
     fn init_builtin_classes(&mut self) {
@@ -259,12 +253,12 @@ impl Context {
             vec![Obj],
             vec![
                 mono("Num"),
+                // mono("Eq"), // Float doesn't have an Eq implementation
                 mono("Ord"),
-                mono("Eq"),
-                mono("Add"),
-                mono("Sub"),
-                mono("Mul"),
-                mono("Div"),
+                poly("Add", vec![ty_tp(Float)]),
+                poly("Sub", vec![ty_tp(Float)]),
+                poly("Mul", vec![ty_tp(Float)]),
+                poly("Div", vec![ty_tp(Float)]),
                 mono("Mutate"),
             ],
             Self::TOP_LEVEL,
@@ -274,6 +268,10 @@ impl Context {
         float.register_impl("__sub__", op_t.clone(), Const, Public);
         float.register_impl("__mul__", op_t.clone(), Const, Public);
         float.register_impl("__div__", op_t, Const, Public);
+        float.register_const("AddO", ConstObj::t(Float));
+        float.register_const("SubO", ConstObj::t(Float));
+        float.register_const("MulO", ConstObj::t(Float));
+        float.register_const("DivO", ConstObj::t(Float));
         float.register_impl("Real", Float, Const, Public);
         float.register_impl("Imag", Float, Const, Public);
         let mut ratio = Self::mono_class(
@@ -281,12 +279,12 @@ impl Context {
             vec![Obj],
             vec![
                 mono("Num"),
+                poly("Eq", vec![ty_tp(Ratio)]),
                 mono("Ord"),
-                mono("Eq"),
-                mono("Add"),
-                mono("Sub"),
-                mono("Mul"),
-                mono("Div"),
+                poly("Add", vec![ty_tp(Ratio)]),
+                poly("Sub", vec![ty_tp(Ratio)]),
+                poly("Mul", vec![ty_tp(Ratio)]),
+                poly("Div", vec![ty_tp(Ratio)]),
                 mono("Mutate"),
             ],
             Self::TOP_LEVEL,
@@ -296,21 +294,25 @@ impl Context {
         ratio.register_impl("__sub__", op_t.clone(), Const, Public);
         ratio.register_impl("__mul__", op_t.clone(), Const, Public);
         ratio.register_impl("__div__", op_t, Const, Public);
+        ratio.register_const("AddO", ConstObj::t(Ratio));
+        ratio.register_const("SubO", ConstObj::t(Ratio));
+        ratio.register_const("MulO", ConstObj::t(Ratio));
+        ratio.register_const("DivO", ConstObj::t(Ratio));
         ratio.register_impl("Real", Ratio, Const, Public);
         ratio.register_impl("Imag", Ratio, Const, Public);
         let mut int = Self::mono_class(
             "Int",
             vec![Obj],
             vec![
-                poly("Add", vec![ty_tp(Int), ty_tp(Int)]),
-                poly("Sub", vec![ty_tp(Int), ty_tp(Int)]),
-                poly("Mul", vec![ty_tp(Int), ty_tp(Int)]),
-                poly("Div", vec![ty_tp(Int), ty_tp(Ratio)]),
+                mono("Ord"),
+                poly("Eq", vec![ty_tp(Int)]),
+                poly("Add", vec![ty_tp(Int)]),
+                poly("Sub", vec![ty_tp(Int)]),
+                poly("Mul", vec![ty_tp(Int)]),
+                poly("Div", vec![ty_tp(Int)]),
                 mono("Num"),
                 mono("Rational"),
                 mono("Integral"),
-                // mono("SelfOrd"),
-                // mono("SelfEq"),
                 mono("Mutate"),
             ],
             Self::TOP_LEVEL,
@@ -321,21 +323,25 @@ impl Context {
         int.register_impl("__add__", op_t.clone(), Const, Public);
         int.register_impl("__sub__", op_t.clone(), Const, Public);
         int.register_impl("__mul__", op_t, Const, Public);
+        int.register_const("AddO", ConstObj::t(Int));
+        int.register_const("SubO", ConstObj::t(Int));
+        int.register_const("MulO", ConstObj::t(Int));
+        int.register_const("DivO", ConstObj::t(Ratio));
         int.register_impl("Real", Int, Const, Public);
         int.register_impl("Imag", Int, Const, Public);
         let mut nat = Self::mono_class(
             "Nat",
             vec![Int, Obj],
             vec![
-                poly("Add", vec![ty_tp(Nat), ty_tp(Nat)]),
-                poly("Sub", vec![ty_tp(Nat), ty_tp(Int)]),
-                poly("Mul", vec![ty_tp(Nat), ty_tp(Nat)]),
-                poly("Div", vec![ty_tp(Nat), ty_tp(Ratio)]),
+                mono("Ord"),
+                poly("Eq", vec![ty_tp(Nat)]),
+                poly("Add", vec![ty_tp(Nat)]),
+                poly("Sub", vec![ty_tp(Nat)]),
+                poly("Mul", vec![ty_tp(Nat)]),
+                poly("Div", vec![ty_tp(Nat)]),
                 mono("Num"),
                 mono("Rational"),
                 mono("Integral"),
-                // mono("SelfOrd"),
-                // mono("SelfEq"),
                 mono("Mutate"),
             ],
             Self::TOP_LEVEL,
@@ -356,6 +362,10 @@ impl Context {
             Immutable,
             Public,
         );
+        nat.register_const("AddO", ConstObj::t(Nat));
+        nat.register_const("SubO", ConstObj::t(Int));
+        nat.register_const("MulO", ConstObj::t(Nat));
+        nat.register_const("DivO", ConstObj::t(Ratio));
         nat.register_impl("Real", Nat, Const, Public);
         nat.register_impl("Imag", Nat, Const, Public);
         let mut bool_ = Self::mono_class(
@@ -365,8 +375,8 @@ impl Context {
                 mono("Num"),
                 mono("Rational"),
                 mono("Integral"),
-                // mono("SelfOrd"),
-                // mono("SelfEq"),
+                poly("Eq", vec![ty_tp(Bool)]),
+                mono("Ord"),
                 // mono("SelfAdd"),
                 // mono("SelfSub"),
                 // mono("SelfMul"),
@@ -380,7 +390,14 @@ impl Context {
         let mut str_ = Self::mono_class(
             "Str",
             vec![Obj],
-            vec![mono("Eq"), mono("Mutate"), poly("Seq", vec![ty_tp(Str)]), poly("Add", vec![ty_tp(Str), ty_tp(Str)])],
+            vec![
+                poly("Eq", vec![ty_tp(Str)]),
+                mono("Ord"),
+                mono("Mutate"),
+                poly("Seq", vec![ty_tp(Str)]),
+                poly("Add", vec![ty_tp(Str)]),
+                poly("Mul", vec![ty_tp(Nat)])
+            ],
             Self::TOP_LEVEL,
         );
         str_.register_impl("__add__", fn1_met(Str, Str, Str), Const, Public);
@@ -395,12 +412,14 @@ impl Context {
             Immutable,
             Public,
         );
+        str_.register_const("AddO", ConstObj::t(Str));
+        str_.register_const("MulO", ConstObj::t(Str));
         let mut array = Self::poly_class(
             "Array",
             vec![PS::t_nd("T"), PS::named_nd("N", Nat)],
             vec![Obj],
             vec![
-                mono("Eq"),
+                poly("Eq", vec![ty_tp(Type::poly("Array", vec![ty_tp(mono_q("T")), mono_q_tp("N")]))]),
                 mono("Mutate"),
                 poly("Seq", vec![ty_tp(mono_q("T"))]),
                 poly("Output", vec![ty_tp(mono_q("T"))]),
@@ -430,7 +449,10 @@ impl Context {
         let mut type_ = Self::mono_class(
             "Type",
             vec![Obj],
-            vec![mono("Eq"), mono("Named")],
+            vec![
+                poly("Eq", vec![ty_tp(Type)]),
+                mono("Named")
+            ],
             Self::TOP_LEVEL,
         );
         type_.register_impl(
@@ -442,16 +464,18 @@ impl Context {
         let module = Self::mono_class(
             "Module",
             vec![Obj],
-            vec![mono("Eq"), mono("Named")],
+            vec![
+                poly("Eq", vec![ty_tp(Module)]),
+                mono("Named")
+            ],
             Self::TOP_LEVEL,
         );
-        let array_mut_t = Type::poly("Array!", vec![TyParam::t(mono_q("T")), mono_q_tp("N")]);
+        let array_mut_t = Type::poly("Array!", vec![ty_tp(mono_q("T")), mono_q_tp("N")]);
         let mut array_mut = Self::poly_class(
             "Array!",
             vec![PS::t_nd("T"), PS::named_nd("N", NatMut)],
-            vec![Obj],
+            vec![poly("Range", vec![ty_tp(mono_q("T")), mono_q_tp("N")]), Obj],
             vec![
-                mono("Eq"),
                 mono("Mutate"),
                 poly("Seq", vec![ty_tp(mono_q("T"))]),
             ],
@@ -461,7 +485,7 @@ impl Context {
             Type::ref_mut(array_mut_t.clone()),
             Some(Type::ref_mut(poly(
                 "Array!",
-                vec![TyParam::t(mono_q("T")), mono_q_tp("N") + value(1)],
+                vec![ty_tp(mono_q("T")), mono_q_tp("N") + value(1)],
             ))),
             vec![param_t("elem", mono_q("T"))],
             vec![],
@@ -478,7 +502,7 @@ impl Context {
             vec![PS::t_nd("T")],
             vec![Obj],
             vec![
-                mono("Eq"),
+                poly("Eq", vec![ty_tp(Type::poly("Range", vec![ty_tp(mono_q("T"))]))]),
                 mono("Mutate"),
                 poly("Seq", vec![ty_tp(mono_q("T"))]),
                 poly("Output", vec![ty_tp(mono_q("T"))]),
@@ -554,7 +578,7 @@ impl Context {
 
     fn init_builtin_procs(&mut self) {
         let t_print = nd_proc(
-            vec![param_t("objs", Type::var_args(Type::refer(Obj)))],
+            vec![param_t("objs", Type::var_args(Type::ref_(Obj)))],
             NoneType,
         );
         let t_input = nd_proc(vec![param_t("msg", Str)], Str);
@@ -593,37 +617,41 @@ impl Context {
         /* binary */
         let l = mono_q("L");
         let r = mono_q("R");
-        let o = mono_q("O");
-        let params = vec![mono_q_tp("R"), mono_q_tp("O")];
-        let op_t = Type::func2(l.clone(), r.clone(), o.clone());
+        let params = vec![ty_tp(mono_q("R"))];
+        let op_t = Type::func2(l.clone(), r.clone(), mono_proj(mono_q("L"), "AddO"));
         let op_t = quant(
             op_t,
             set! {
                 static_instance("R", Type),
-                static_instance("O", Type),
                 subtype(l.clone(), poly("Add", params.clone()))
             },
         );
         self.register_impl("__add__", op_t, Const, Private);
-        let op_t = Type::func2(l.clone(), r.clone(), o.clone());
+        let op_t = Type::func2(l.clone(), r.clone(), mono_proj(mono_q("L"), "SubO"));
         let op_t = quant(
             op_t,
             set! {
                 static_instance("R", Type),
-                static_instance("O", Type),
                 subtype(l.clone(), poly("Sub", params.clone()))
             },
         );
         self.register_impl("__sub__", op_t, Const, Private);
-        let op_t = Type::func2(l.clone(), r.clone(), o.clone());
-        let op_t = quant(op_t, set! {subtype(l.clone(), poly("Mul", params.clone()))});
+        let op_t = Type::func2(l.clone(), r.clone(), mono_proj(mono_q("L"), "MulO"));
+        let op_t = quant(op_t, set! {
+            static_instance("R", Type),
+            subtype(l.clone(), poly("Mul", params.clone()))
+        });
         self.register_impl("__mul__", op_t, Const, Private);
-        let op_t = Type::func2(l.clone(), r.clone(), o.clone());
-        let op_t = quant(op_t, set! {subtype(l, poly("Mul", params.clone()))});
+        let op_t = Type::func2(l.clone(), r.clone(), mono_proj(mono_q("L"), "DivO"));
+        let op_t = quant(op_t, set! {
+            static_instance("R", Type),
+            subtype(l, poly("Mul", params.clone()))
+        });
         self.register_impl("__div__", op_t, Const, Private);
         let m = mono_q("M");
         let op_t = Type::func2(m.clone(), m.clone(), m.clone());
         let op_t = quant(op_t, set! {subtype(m, poly("Mul", vec![]))});
+        // TODO: add bound: M == MulO
         self.register_impl("__pow__", op_t, Const, Private);
         let d = mono_q("D");
         let op_t = Type::func2(d.clone(), d.clone(), d.clone());
@@ -636,7 +664,7 @@ impl Context {
         self.register_impl("__ne__", op_t, Const, Private);
         let o = mono_q("O");
         let op_t = Type::func2(o.clone(), o.clone(), Bool);
-        let op_t = quant(op_t, set! {subtype(o, poly("Ord", vec![]))});
+        let op_t = quant(op_t, set! {subtype(o, mono("Ord"))});
         self.register_impl("__lt__", op_t.clone(), Const, Private);
         self.register_impl("__le__", op_t.clone(), Const, Private);
         self.register_impl("__gt__", op_t.clone(), Const, Private);
@@ -652,7 +680,7 @@ impl Context {
         self.register_decl("__neg__", op_t, Private);
         let t = mono_q("T");
         let op_t = Type::func2(t.clone(), t.clone(), Type::range(t.clone()));
-        let op_t = quant(op_t, set! {subtype(t, mono("Ord"))});
+        let op_t = quant(op_t, set! {subtype(t.clone(), mono("Ord"))});
         self.register_decl("__rng__", op_t.clone(), Private);
         self.register_decl("__lorng__", op_t.clone(), Private);
         self.register_decl("__rorng__", op_t.clone(), Private);
@@ -681,17 +709,11 @@ impl Context {
             vec![
                 poly(
                     "Add",
-                    vec![
-                        TyParam::from(&o..=&p),
-                        TyParam::from(m.clone() + o.clone()..=n.clone() + p.clone()),
-                    ],
+                    vec![TyParam::from(&o..=&p)],
                 ),
                 poly(
                     "Sub",
-                    vec![
-                        TyParam::from(&o..=&p),
-                        TyParam::from(m.clone() - p.clone()..=n.clone() - o.clone()),
-                    ],
+                    vec![TyParam::from(&o..=&p)],
                 ),
             ],
             Self::TOP_LEVEL,
@@ -705,9 +727,11 @@ impl Context {
         let op_t = fn1_met(
             Type::from(&m..=&n),
             Type::from(&o..=&p),
-            Type::from(m - p..=n - o),
+            Type::from(m.clone() - p.clone()..=n.clone() - o.clone()),
         );
         interval.register_impl("__sub__", op_t, Const, Public);
+        interval.register_const("AddO", ConstObj::t(Type::from(m.clone() + o.clone()..=n.clone() + p.clone())));
+        interval.register_const("SubO", ConstObj::t(Type::from(m - p..=n - o)));
         self.register_patch("Interval", interval, Const);
         // eq.register_impl("__ne__", op_t,         Const, Public);
         // ord.register_impl("__le__", op_t.clone(), Const, Public);
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index d7fb8a4d8..75798fa31 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -12,7 +12,7 @@ use erg_parser::ast;
 use erg_parser::ast::AST;
 
 use crate::context::{Context, ContextKind, RegistrationMode};
-use crate::error::{LowerError, LowerErrors, LowerResult, LowerWarnings};
+use crate::error::{LowerError, LowerErrors, LowerResult, LowerWarnings, readable_name};
 use crate::hir;
 use crate::hir::HIR;
 use crate::varinfo::Visibility;
@@ -36,7 +36,7 @@ impl ASTLowerer {
                 Some(Context::init_builtins()),
                 vec![],
                 vec![],
-                0,
+                Context::TOP_LEVEL,
             ),
             errs: LowerErrors::empty(),
             warns: LowerWarnings::empty(),
@@ -54,7 +54,7 @@ impl ASTLowerer {
             Err(LowerError::type_mismatch_error(
                 loc,
                 self.ctx.caused_by(),
-                name,
+                readable_name(name),
                 expect,
                 found,
             ))
@@ -179,8 +179,8 @@ impl ASTLowerer {
         let mut obj = self.lower_expr(*call.obj, false)?;
         let t = self.ctx.get_call_t(
             &mut obj,
-            hir_args.pos_args(),
-            hir_args.kw_args(),
+            &hir_args.pos_args,
+            &hir_args.kw_args,
             &self.ctx.name,
         )?;
         Ok(hir::Call::new(obj, hir_args, t))
@@ -302,7 +302,7 @@ impl ASTLowerer {
                             .outer
                             .as_mut()
                             .unwrap()
-                            .import_mod(name, &call.args.pos_args().first().unwrap().expr)?;
+                            .import_mod(name, &call.args.pos_args.first().unwrap().expr)?;
                     }
                 } else {
                     todo!()
@@ -401,6 +401,7 @@ impl ASTLowerer {
             }
         }
         let hir = HIR::new(ast.name, module);
+        let hir = self.ctx.deref_toplevel(hir)?;
         log!(
             "[DEBUG] {}() has completed, found errors: {}",
             fn_name!(),
diff --git a/compiler/erg_compiler/ownercheck.rs b/compiler/erg_compiler/ownercheck.rs
index 2d6a2a43a..c04e9a52f 100644
--- a/compiler/erg_compiler/ownercheck.rs
+++ b/compiler/erg_compiler/ownercheck.rs
@@ -143,15 +143,15 @@ impl OwnershipChecker {
                         let (nd_ownerships, d_ownerships): (Vec<_>, Vec<_>) = non_defaults
                             .iter()
                             .enumerate()
-                            .partition(|(i, _)| *i == call.args.pos_args().len());
+                            .partition(|(i, _)| *i == call.args.pos_args.len());
                         for (parg, (_, ownership)) in
-                            call.args.pos_args().iter().zip(nd_ownerships.into_iter())
+                            call.args.pos_args.iter().zip(nd_ownerships.into_iter())
                         {
                             self.check_expr(&parg.expr, *ownership);
                         }
                         for (kwarg, (_, ownership)) in call
                             .args
-                            .kw_args()
+                            .kw_args
                             .iter()
                             .zip(d_ownerships.into_iter().chain(defaults.iter().enumerate()))
                         {
@@ -159,10 +159,10 @@ impl OwnershipChecker {
                         }
                     }
                     ArgsOwnership::VarArgs(ownership) => {
-                        for parg in call.args.pos_args().iter() {
+                        for parg in call.args.pos_args.iter() {
                             self.check_expr(&parg.expr, ownership);
                         }
-                        for kwarg in call.args.kw_args().iter() {
+                        for kwarg in call.args.kw_args.iter() {
                             self.check_expr(&kwarg.expr, ownership);
                         }
                     }
@@ -178,12 +178,12 @@ impl OwnershipChecker {
                 self.check_expr(&unary.expr, ownership);
             }
             Expr::Array(arr) => {
-                for a in arr.elems.pos_args().iter() {
+                for a in arr.elems.pos_args.iter() {
                     self.check_expr(&a.expr, ownership);
                 }
             }
             Expr::Dict(dict) => {
-                for a in dict.attrs.kw_args().iter() {
+                for a in dict.attrs.kw_args.iter() {
                     // self.check_expr(&a.key);
                     self.check_expr(&a.expr, ownership);
                 }
diff --git a/compiler/erg_compiler/varinfo.rs b/compiler/erg_compiler/varinfo.rs
index 7db05a178..a55105b45 100644
--- a/compiler/erg_compiler/varinfo.rs
+++ b/compiler/erg_compiler/varinfo.rs
@@ -142,9 +142,17 @@ impl HasType for VarInfo {
         &self.t
     }
     #[inline]
+    fn ref_mut_t(&mut self) -> &mut Type {
+        &mut self.t
+    }
+    #[inline]
     fn signature_t(&self) -> Option<&Type> {
         None
     }
+    #[inline]
+    fn signature_mut_t(&mut self) -> Option<&mut Type> {
+        None
+    }
 }
 
 impl VarInfo {
diff --git a/compiler/erg_parser/Cargo.toml b/compiler/erg_parser/Cargo.toml
index 7c4ae7820..d73f33624 100644
--- a/compiler/erg_parser/Cargo.toml
+++ b/compiler/erg_parser/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "erg_parser"
-version = "0.2.2"
+version = "0.2.3"
 description = "The Erg parser"
 authors = ["mtshiba <sbym1346@gmail.com>"]
 license = "MIT OR Apache-2.0"
@@ -14,7 +14,7 @@ debug = [ "erg_common/debug" ]
 japanese = [ "erg_common/japanese" ]
 
 [dependencies]
-erg_common = { version = "0.2.2", path = "../erg_common" }
+erg_common = { version = "0.2.3", path = "../erg_common" }
 
 [lib]
 path = "lib.rs"