diff --git a/compiler/erg_common/traits.rs b/compiler/erg_common/traits.rs
index 5eca8507..1356f7f1 100644
--- a/compiler/erg_common/traits.rs
+++ b/compiler/erg_common/traits.rs
@@ -466,6 +466,13 @@ macro_rules! impl_locational {
             }
         }
     };
+    ($T: ty, $inner: ident) => {
+        impl Locational for $T {
+            fn loc(&self) -> Location {
+                self.$inner.loc()
+            }
+        }
+    };
 }
 
 pub trait NestedDisplay {
diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index fcf16fd0..765647bb 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -2,6 +2,7 @@
 use std::cmp::Ordering;
 use std::option::Option; // conflicting to Type::Option
 
+use erg_type::constructors::or;
 use erg_type::free::fresh_varname;
 use erg_type::free::{Constraint, FreeKind, FreeTyVar};
 use erg_type::typaram::{TyParam, TyParamOrdering};
@@ -675,7 +676,7 @@ impl Context {
                 let t = self.into_refinement(t.clone());
                 Type::Refinement(self.union_refinement(&t, r))
             }
-            (l, r) => Type::or(l.clone(), r.clone()),
+            (l, r) => or(l.clone(), r.clone()),
         }
     }
 
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index 59f46652..7e0bc46e 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -17,6 +17,9 @@ use ast::VarName;
 use erg_parser::ast;
 use erg_parser::token::Token;
 
+use erg_type::constructors::{
+    func, mono, mono_proj, poly, ref_, ref_mut, refinement, subr_t, var_args,
+};
 use erg_type::free::Constraint;
 use erg_type::typaram::TyParam;
 use erg_type::value::ValueObj;
@@ -142,7 +145,7 @@ impl Context {
                     pos_arg.loc(),
                     self.caused_by(),
                     "match",
-                    &Type::mono("LambdaFunc"),
+                    &mono("LambdaFunc"),
                     t,
                 ));
             }
@@ -192,7 +195,7 @@ impl Context {
         }
         let param_ty = ParamTy::anonymous(match_target_expr_t.clone());
         let param_ts = [vec![param_ty], branch_ts.to_vec()].concat();
-        let t = Type::func(param_ts, vec![], return_t);
+        let t = func(param_ts, vec![], return_t);
         Ok(t)
     }
 
@@ -440,7 +443,7 @@ impl Context {
                             }
                         }
                     }
-                    Ok(Type::poly(t_name, new_params))
+                    Ok(poly(t_name, new_params))
                 } else {
                     Ok(min)
                 }
@@ -457,7 +460,7 @@ impl Context {
                     new_default_params.push(ParamTy::new(param.name, t));
                 }
                 let new_return_t = self.resolve_trait(*subr.return_t)?;
-                let t = Type::subr(
+                let t = subr_t(
                     subr.kind, // TODO: resolve self
                     new_non_default_params,
                     new_default_params,
@@ -467,23 +470,23 @@ impl Context {
             }
             Type::MonoProj { lhs, rhs } => {
                 let new_lhs = self.resolve_trait(*lhs)?;
-                Ok(Type::mono_proj(new_lhs, rhs))
+                Ok(mono_proj(new_lhs, rhs))
             }
             Type::Refinement(refine) => {
                 let new_t = self.resolve_trait(*refine.t)?;
-                Ok(Type::refinement(refine.var, new_t, refine.preds))
+                Ok(refinement(refine.var, new_t, refine.preds))
             }
             Type::Ref(t) => {
                 let new_t = self.resolve_trait(*t)?;
-                Ok(Type::ref_(new_t))
+                Ok(ref_(new_t))
             }
             Type::RefMut(t) => {
                 let new_t = self.resolve_trait(*t)?;
-                Ok(Type::ref_mut(new_t))
+                Ok(ref_mut(new_t))
             }
             Type::VarArgs(t) => {
                 let new_t = self.resolve_trait(*t)?;
-                Ok(Type::var_args(new_t))
+                Ok(var_args(new_t))
             }
             Type::Callable { .. } => todo!(),
             Type::And(_, _) | Type::Or(_, _) | Type::Not(_, _) => todo!(),
diff --git a/compiler/erg_compiler/context/instantiate.rs b/compiler/erg_compiler/context/instantiate.rs
index 5d912963..ebbebf6a 100644
--- a/compiler/erg_compiler/context/instantiate.rs
+++ b/compiler/erg_compiler/context/instantiate.rs
@@ -18,6 +18,7 @@ use ast::{
 use erg_parser::ast;
 use erg_parser::token::TokenKind;
 
+use erg_type::constructors::*;
 use erg_type::typaram::{IntervalOp, TyParam, TyParamOrdering};
 use erg_type::value::ValueObj;
 use erg_type::{ParamTy, Predicate, SubrKind, TyBound, Type};
@@ -80,7 +81,7 @@ impl TyVarContext {
                 ValueObj::Type(t) if t.is_mono_q() => {
                     if &t.name()[..] == "Self" {
                         let constraint = Constraint::type_of(Type);
-                        let t = Type::named_free_var(Str::rc(var_name), self.level, constraint);
+                        let t = named_free_var(Str::rc(var_name), self.level, constraint);
                         TyParam::t(t)
                     } else {
                         todo!()
@@ -129,9 +130,9 @@ impl TyVarContext {
                 self.push_or_init_typaram(&c.tvar_name().unwrap(), &c);
                 inst_defaults.push(c);
             }
-            Type::poly(name, [inst_non_defaults, inst_defaults].concat())
+            poly(name, [inst_non_defaults, inst_defaults].concat())
         } else {
-            Type::poly(
+            poly(
                 name,
                 params
                     .into_iter()
@@ -156,25 +157,21 @@ impl TyVarContext {
                     Type::Poly { name, params } => {
                         self.instantiate_poly(mid.name(), &name, params, ctx)
                     }
-                    Type::MonoProj { lhs, rhs } => {
-                        Type::mono_proj(self.instantiate_qvar(*lhs), rhs)
-                    }
+                    Type::MonoProj { lhs, rhs } => mono_proj(self.instantiate_qvar(*lhs), rhs),
                     sub => sub,
                 };
                 let sup_instance = match sup {
                     Type::Poly { name, params } => {
                         self.instantiate_poly(mid.name(), &name, params, ctx)
                     }
-                    Type::MonoProj { lhs, rhs } => {
-                        Type::mono_proj(self.instantiate_qvar(*lhs), rhs)
-                    }
+                    Type::MonoProj { lhs, rhs } => mono_proj(self.instantiate_qvar(*lhs), rhs),
                     sup => sup,
                 };
                 let name = mid.name();
                 let constraint = Constraint::sandwiched(sub_instance, sup_instance);
                 self.push_or_init_tyvar(
                     &name,
-                    &Type::named_free_var(name.clone(), self.level, constraint),
+                    &named_free_var(name.clone(), self.level, constraint),
                 );
             }
             TyBound::Instance { name, t } => {
@@ -194,7 +191,7 @@ impl TyVarContext {
                     } else {
                         self.push_or_init_tyvar(
                             &name,
-                            &Type::named_free_var(name.clone(), self.level, constraint),
+                            &named_free_var(name.clone(), self.level, constraint),
                         );
                     }
                 } else {
@@ -227,7 +224,7 @@ impl TyVarContext {
                         todo!()
                     }
                 } else {
-                    let tv = Type::named_free_var(n.clone(), self.level, Constraint::Uninited);
+                    let tv = named_free_var(n.clone(), self.level, Constraint::Uninited);
                     self.push_or_init_tyvar(&n, &tv);
                     tv
                 }
@@ -256,7 +253,7 @@ impl TyVarContext {
                     } else if let Some(t) = self.get_tyvar(&n) {
                         TyParam::t(t.clone())
                     } else {
-                        let tv = Type::named_free_var(n.clone(), self.level, Constraint::Uninited);
+                        let tv = named_free_var(n.clone(), self.level, Constraint::Uninited);
                         self.push_or_init_tyvar(&n, &tv);
                         TyParam::t(tv)
                     }
@@ -363,7 +360,7 @@ impl Context {
         let spec_t = if let Some(s) = sig.t_spec.as_ref() {
             self.instantiate_typespec(s, mode)?
         } else {
-            Type::free_var(self.level, Constraint::type_of(Type))
+            free_var(self.level, Constraint::type_of(Type))
         };
         if let Some(eval_t) = opt_eval_t {
             self.sub_unify(&eval_t, &spec_t, None, sig.t_spec.as_ref().map(|s| s.loc()))?;
@@ -408,7 +405,7 @@ impl Context {
             } else {
                 self.level + 1
             };
-            Type::free_var(level, Constraint::type_of(Type))
+            free_var(level, Constraint::type_of(Type))
         };
         if let Some(eval_ret_t) = eval_ret_t {
             self.sub_unify(
@@ -419,9 +416,9 @@ impl Context {
             )?;
         }
         Ok(if sig.ident.is_procedural() {
-            Type::proc(non_defaults, defaults, spec_return_t)
+            proc(non_defaults, defaults, spec_return_t)
         } else {
-            Type::func(non_defaults, defaults, spec_return_t)
+            func(non_defaults, defaults, spec_return_t)
         })
     }
 
@@ -436,7 +433,7 @@ impl Context {
             self.instantiate_typespec(spec, mode)?
         } else {
             match &sig.pat {
-                ast::ParamPattern::Lit(lit) => Type::enum_t(set![eval_lit(lit)]),
+                ast::ParamPattern::Lit(lit) => enum_t(set![eval_lit(lit)]),
                 // TODO: Array<Lit>
                 _ => {
                     let level = if mode == PreRegister {
@@ -444,7 +441,7 @@ impl Context {
                     } else {
                         self.level + 1
                     };
-                    Type::free_var(level, Constraint::type_of(Type))
+                    free_var(level, Constraint::type_of(Type))
                 }
             }
         };
@@ -486,12 +483,12 @@ impl Context {
                     let t = self.instantiate_const_expr_as_type(&first.expr)?;
                     let len = args.next().unwrap();
                     let len = self.instantiate_const_expr(&len.expr);
-                    Ok(Type::array(t, len))
+                    Ok(array(t, len))
                 } else {
-                    Ok(Type::mono("GenericArray"))
+                    Ok(mono("GenericArray"))
                 }
             }
-            other if simple.args.is_empty() => Ok(Type::mono(Str::rc(other))),
+            other if simple.args.is_empty() => Ok(mono(Str::rc(other))),
             other => {
                 // FIXME: kw args
                 let params = simple.args.pos_args().map(|arg| match &arg.expr {
@@ -500,7 +497,7 @@ impl Context {
                         todo!()
                     }
                 });
-                Ok(Type::poly(Str::rc(other), params.collect()))
+                Ok(poly(Str::rc(other), params.collect()))
             }
         }
     }
@@ -520,9 +517,7 @@ impl Context {
         expr: &ast::ConstExpr,
     ) -> TyCheckResult<Type> {
         match expr {
-            ast::ConstExpr::Accessor(ast::ConstAccessor::Local(name)) => {
-                Ok(Type::mono(name.inspect()))
-            }
+            ast::ConstExpr::Accessor(ast::ConstAccessor::Local(name)) => Ok(mono(name.inspect())),
             _ => todo!(),
         }
     }
@@ -547,27 +542,27 @@ impl Context {
         match spec {
             TypeSpec::PreDeclTy(predecl) => self.instantiate_predecl_t(predecl),
             // TODO: Flatten
-            TypeSpec::And(lhs, rhs) => Ok(Type::and(
+            TypeSpec::And(lhs, rhs) => Ok(and(
                 self.instantiate_typespec(lhs, mode)?,
                 self.instantiate_typespec(rhs, mode)?,
             )),
-            TypeSpec::Not(lhs, rhs) => Ok(Type::not(
+            TypeSpec::Not(lhs, rhs) => Ok(not(
                 self.instantiate_typespec(lhs, mode)?,
                 self.instantiate_typespec(rhs, mode)?,
             )),
-            TypeSpec::Or(lhs, rhs) => Ok(Type::or(
+            TypeSpec::Or(lhs, rhs) => Ok(or(
                 self.instantiate_typespec(lhs, mode)?,
                 self.instantiate_typespec(rhs, mode)?,
             )),
             TypeSpec::Array { .. } => todo!(),
             // FIXME: unwrap
-            TypeSpec::Tuple(tys) => Ok(Type::tuple(
+            TypeSpec::Tuple(tys) => Ok(tuple(
                 tys.iter()
                     .map(|spec| self.instantiate_typespec(spec, mode).unwrap())
                     .collect(),
             )),
             // TODO: エラー処理(リテラルでない、ダブりがある)はパーサーにやらせる
-            TypeSpec::Enum(set) => Ok(Type::enum_t(
+            TypeSpec::Enum(set) => Ok(enum_t(
                 set.pos_args()
                     .map(|arg| {
                         if let ast::ConstExpr::Lit(lit) = &arg.expr {
@@ -593,7 +588,7 @@ impl Context {
                 if let Some(Greater) = self.rec_try_cmp(&l, &r) {
                     panic!("{l}..{r} is not a valid interval type (should be lhs <= rhs)")
                 }
-                Ok(Type::int_interval(op, l, r))
+                Ok(int_interval(op, l, r))
             }
             TypeSpec::Subr(subr) => {
                 let non_defaults = try_map(subr.non_defaults.iter(), |p| {
@@ -603,7 +598,7 @@ impl Context {
                     self.instantiate_func_param_spec(p, mode)
                 })?;
                 let return_t = self.instantiate_typespec(&subr.return_t, mode)?;
-                Ok(Type::subr(
+                Ok(subr_t(
                     self.instantiate_subr_kind(&subr.kind)?,
                     non_defaults,
                     defaults,
@@ -639,7 +634,7 @@ impl Context {
         // TODO: 高階型変数
         match bound {
             TypeBoundSpec::Subtype { sub, sup } => Ok(TyBound::subtype_of(
-                Type::mono_q(sub.inspect().clone()),
+                mono_q(sub.inspect().clone()),
                 self.instantiate_typespec(sup, mode)?,
             )),
             TypeBoundSpec::Instance { name, ty } => Ok(TyBound::instance(
@@ -714,7 +709,7 @@ impl Context {
                 for param in params.iter_mut() {
                     *param = Self::instantiate_tp(mem::take(param), tv_ctx);
                 }
-                Type::poly_q(name, params)
+                poly_q(name, params)
             }
             Refinement(mut refine) => {
                 refine.preds = refine
@@ -754,7 +749,7 @@ impl Context {
                     p.ty = Self::instantiate_t(mem::take(&mut p.ty), tv_ctx);
                 }
                 let return_t = Self::instantiate_t(*subr.return_t, tv_ctx);
-                Type::subr(kind, subr.non_default_params, subr.default_params, return_t)
+                subr_t(kind, subr.non_default_params, subr.default_params, return_t)
             }
             Record(mut dict) => {
                 for v in dict.values_mut() {
@@ -764,25 +759,25 @@ impl Context {
             }
             Ref(t) => {
                 let t = Self::instantiate_t(*t, tv_ctx);
-                Type::ref_(t)
+                ref_(t)
             }
             RefMut(t) => {
                 let t = Self::instantiate_t(*t, tv_ctx);
-                Type::ref_mut(t)
+                ref_mut(t)
             }
             VarArgs(t) => {
                 let t = Self::instantiate_t(*t, tv_ctx);
-                Type::var_args(t)
+                var_args(t)
             }
             MonoProj { lhs, rhs } => {
                 let lhs = Self::instantiate_t(*lhs, tv_ctx);
-                Type::mono_proj(lhs, rhs)
+                mono_proj(lhs, rhs)
             }
             Poly { name, mut params } => {
                 for param in params.iter_mut() {
                     *param = Self::instantiate_tp(mem::take(param), tv_ctx);
                 }
-                Type::poly(name, params)
+                poly(name, params)
             }
             Quantified(_) => {
                 panic!("a quantified type should not be instantiated, instantiate the inner type")
@@ -804,7 +799,7 @@ impl Context {
                                 self.unify(l, r, None, Some(callee.loc()))?;
                             }
                             // if callee is a Module object or some named one
-                            (None, Some(r)) if self.rec_subtype_of(r, &Type::mono("Named")) => {}
+                            (None, Some(r)) if self.rec_subtype_of(r, &mono("Named")) => {}
                             (None, None) => {}
                             (l, r) => todo!("{l:?}, {r:?}"),
                         }
diff --git a/compiler/erg_compiler/context/register.rs b/compiler/erg_compiler/context/register.rs
index f31eda46..43338bc9 100644
--- a/compiler/erg_compiler/context/register.rs
+++ b/compiler/erg_compiler/context/register.rs
@@ -9,6 +9,7 @@ use erg_type::free::HasLevel;
 use ast::{DefId, VarName};
 use erg_parser::ast;
 
+use erg_type::constructors::{enum_t, func, proc};
 use erg_type::value::ValueObj;
 use erg_type::{HasType, ParamTy, SubrType, TyBound, Type};
 use Type::*;
@@ -344,13 +345,13 @@ impl Context {
             ))
         } else {
             let sub_t = if sig.ident.is_procedural() {
-                Type::proc(
+                proc(
                     non_default_params.clone(),
                     default_params.clone(),
                     body_t.clone(),
                 )
             } else {
-                Type::func(
+                func(
                     non_default_params.clone(),
                     default_params.clone(),
                     body_t.clone(),
@@ -393,7 +394,7 @@ impl Context {
                 let eval_body_t = || {
                     self.eval
                         .eval_const_block(&def.body.block, self)
-                        .map(|c| Type::enum_t(set![c]))
+                        .map(|c| enum_t(set![c]))
                 };
                 match &def.sig {
                     ast::Signature::Subr(sig) => {
diff --git a/compiler/erg_compiler/context/test.rs b/compiler/erg_compiler/context/test.rs
index a93ec0a1..430cfb7d 100644
--- a/compiler/erg_compiler/context/test.rs
+++ b/compiler/erg_compiler/context/test.rs
@@ -1,6 +1,8 @@
 //! test module for `Context`
 use erg_common::Str;
 use erg_common::{enum_unwrap, set};
+
+use erg_type::constructors::{func1, mono_q, poly, quant, refinement};
 use erg_type::typaram::TyParam;
 use erg_type::{Predicate, TyBound, Type};
 use Type::*;
@@ -13,7 +15,7 @@ impl Context {
         // Nat :> {I: Int | I >= 1} ?
         let lhs = Nat;
         let var = Str::ever("I");
-        let rhs = Type::refinement(
+        let rhs = refinement(
             var.clone(),
             Type::Int,
             set! { Predicate::eq(var, TyParam::value(1)) },
@@ -26,7 +28,7 @@ impl Context {
     }
 
     pub fn test_resolve_trait(&self) -> Result<(), ()> {
-        let t = Type::poly("Add", vec![TyParam::t(Nat)]);
+        let t = poly("Add", vec![TyParam::t(Nat)]);
         match self.resolve_trait(t) {
             Ok(Nat) => Ok(()),
             Ok(other) => {
@@ -44,7 +46,7 @@ impl Context {
     pub fn test_resolve_trait_inner1(&self) -> Result<(), ()> {
         let name = Str::ever("Add");
         let params = vec![TyParam::t(Nat)];
-        let maybe_trait = Type::poly(name.clone(), params);
+        let maybe_trait = poly(name.clone(), params);
         let mut min = Type::Obj;
         for pair in self.rec_get_trait_impls(&name) {
             if self.rec_supertype_of(&pair.sup_trait, &maybe_trait) {
@@ -59,12 +61,12 @@ impl Context {
     }
 
     pub fn test_instantiation_and_generalization(&self) -> Result<(), ()> {
-        let t = Type::mono_q("T");
-        let eq = Type::poly("Eq", vec![TyParam::t(t.clone())]);
+        let t = mono_q("T");
+        let eq = poly("Eq", vec![TyParam::t(t.clone())]);
         let bound = TyBound::subtype_of(t.clone(), eq.clone());
         let bounds = set! {bound};
-        let unbound_t = Type::func1(t.clone(), t.clone());
-        let quantified = Type::quantified(unbound_t.clone(), bounds.clone());
+        let unbound_t = func1(t.clone(), t.clone());
+        let quantified = quant(unbound_t.clone(), bounds.clone());
         println!("quantified      : {quantified}");
         let mut tv_ctx = TyVarContext::new(self.level + 1, bounds, self);
         println!("tv_ctx: {tv_ctx}");
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index 4e528e22..1209c776 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -7,6 +7,8 @@ use erg_common::set::Set;
 use erg_common::traits::Stream;
 use erg_common::Str;
 use erg_common::{assume_unreachable, fn_name, log, set};
+
+use erg_type::constructors::*;
 use erg_type::free::{Constraint, FreeKind, HasLevel};
 use erg_type::typaram::TyParam;
 use erg_type::value::ValueObj;
@@ -75,7 +77,7 @@ impl Context {
         if bounds.is_empty() {
             maybe_unbound_t
         } else {
-            Type::quantified(maybe_unbound_t, bounds)
+            quant(maybe_unbound_t, bounds)
         }
     }
 
@@ -106,13 +108,13 @@ impl Context {
                 FreeKind::Unbound { id, constraint, .. } => {
                     let name = id.to_string();
                     self.generalize_constraint(&name, constraint, bounds, lazy_inits);
-                    Type::mono_q(name)
+                    mono_q(name)
                 }
                 FreeKind::NamedUnbound {
                     name, constraint, ..
                 } => {
                     self.generalize_constraint(name, constraint, bounds, lazy_inits);
-                    Type::mono_q(name)
+                    mono_q(name)
                 }
                 _ => assume_unreachable!(),
             },
@@ -140,18 +142,18 @@ impl Context {
                     p.ty = self.generalize_t_inner(mem::take(&mut p.ty), bounds, lazy_inits);
                 });
                 let return_t = self.generalize_t_inner(*subr.return_t, bounds, lazy_inits);
-                Type::subr(kind, subr.non_default_params, subr.default_params, return_t)
+                subr_t(kind, subr.non_default_params, subr.default_params, return_t)
             }
             Callable { .. } => todo!(),
-            Ref(t) => Type::ref_(self.generalize_t_inner(*t, bounds, lazy_inits)),
-            RefMut(t) => Type::ref_mut(self.generalize_t_inner(*t, bounds, lazy_inits)),
-            VarArgs(t) => Type::var_args(self.generalize_t_inner(*t, bounds, lazy_inits)),
+            Ref(t) => ref_(self.generalize_t_inner(*t, bounds, lazy_inits)),
+            RefMut(t) => ref_mut(self.generalize_t_inner(*t, bounds, lazy_inits)),
+            VarArgs(t) => var_args(self.generalize_t_inner(*t, bounds, lazy_inits)),
             Poly { name, mut params } => {
                 let params = params
                     .iter_mut()
                     .map(|p| self.generalize_tp(mem::take(p), bounds, lazy_inits))
                     .collect::<Vec<_>>();
-                Type::poly(name, params)
+                poly(name, params)
             }
             // REVIEW: その他何でもそのまま通していいのか?
             other => other,
@@ -175,7 +177,7 @@ impl Context {
                     let sub = self.generalize_t_inner(sub.clone(), bounds, lazy_inits);
                     let sup = self.generalize_t_inner(sup.clone(), bounds, lazy_inits);
                     // let bs = sub_bs.concat(sup_bs);
-                    bounds.insert(TyBound::sandwiched(sub, Type::mono_q(name.clone()), sup));
+                    bounds.insert(TyBound::sandwiched(sub, mono_q(name.clone()), sup));
                 }
                 Constraint::TypeOf(t) => {
                     let t = self.generalize_t_inner(t.clone(), bounds, lazy_inits);
@@ -315,15 +317,15 @@ impl Context {
             }
             Type::Ref(t) => {
                 let t = self.deref_tyvar(*t)?;
-                Ok(Type::ref_(t))
+                Ok(ref_(t))
             }
             Type::RefMut(t) => {
                 let t = self.deref_tyvar(*t)?;
-                Ok(Type::ref_mut(t))
+                Ok(ref_mut(t))
             }
             Type::VarArgs(t) => {
                 let t = self.deref_tyvar(*t)?;
-                Ok(Type::var_args(t))
+                Ok(var_args(t))
             }
             Type::Callable { .. } => todo!(),
             Type::Record(mut rec) => {
@@ -335,7 +337,7 @@ impl Context {
             Type::Refinement(refine) => {
                 let t = self.deref_tyvar(*refine.t)?;
                 // TODO: deref_predicate
-                Ok(Type::refinement(refine.var, t, refine.preds))
+                Ok(refinement(refine.var, t, refine.preds))
             }
             t => Ok(t),
         }
@@ -505,7 +507,7 @@ impl Context {
                 } else if allow_divergence
                     && (self.eq_tp(tp, &TyParam::value(Inf))
                         || self.eq_tp(tp, &TyParam::value(NegInf)))
-                    && self.rec_subtype_of(&fv_t, &Type::mono("Num"))
+                    && self.rec_subtype_of(&fv_t, &mono("Num"))
                 {
                     fv.link(tp);
                     Ok(())
@@ -836,7 +838,7 @@ impl Context {
                 },
             ) => {
                 if ln != rn {
-                    let before_t = Type::poly(ln.clone(), lps.clone());
+                    let before_t = poly(ln.clone(), lps.clone());
                     return Err(TyCheckError::re_unification_error(
                         line!() as usize,
                         &before_t,
diff --git a/compiler/erg_compiler/eval.rs b/compiler/erg_compiler/eval.rs
index 344dcf11..4199e71b 100644
--- a/compiler/erg_compiler/eval.rs
+++ b/compiler/erg_compiler/eval.rs
@@ -12,6 +12,9 @@ use OpKind::*;
 use erg_parser::ast::*;
 use erg_parser::token::{Token, TokenKind};
 
+use erg_type::constructors::{
+    enum_t, mono_proj, poly, ref_, ref_mut, refinement, subr_t, var_args,
+};
 use erg_type::typaram::{OpKind, TyParam};
 use erg_type::value::ValueObj;
 use erg_type::{Predicate, SubrKind, TyBound, Type};
@@ -445,7 +448,7 @@ impl Evaluator {
                     p.ty = self.eval_t_params(mem::take(&mut p.ty), ctx, level)?;
                 }
                 let return_t = self.eval_t_params(*subr.return_t, ctx, level)?;
-                Ok(Type::subr(
+                Ok(subr_t(
                     kind,
                     subr.non_default_params,
                     subr.default_params,
@@ -457,7 +460,7 @@ impl Evaluator {
                 for pred in refine.preds.into_iter() {
                     preds.insert(self.eval_pred(pred, ctx)?);
                 }
-                Ok(Type::refinement(refine.var, *refine.t, preds))
+                Ok(refinement(refine.var, *refine.t, preds))
             }
             // [?T; 0].MutType! == [?T; !0]
             Type::MonoProj { lhs, rhs } => {
@@ -474,7 +477,7 @@ impl Evaluator {
                     }
                 }
                 if let Some(outer) = &ctx.outer {
-                    self.eval_t_params(Type::mono_proj(*lhs, rhs), outer, level)
+                    self.eval_t_params(mono_proj(*lhs, rhs), outer, level)
                 } else {
                     todo!(
                         "{lhs}.{rhs} not found in [{}]",
@@ -484,14 +487,14 @@ impl Evaluator {
                     )
                 }
             }
-            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::Ref(l) => Ok(ref_(self.eval_t_params(*l, ctx, level)?)),
+            Type::RefMut(l) => Ok(ref_mut(self.eval_t_params(*l, ctx, level)?)),
+            Type::VarArgs(l) => Ok(var_args(self.eval_t_params(*l, ctx, level)?)),
             Type::Poly { name, mut params } => {
                 for p in params.iter_mut() {
                     *p = self.eval_tp(&mem::take(p), ctx)?;
                 }
-                Ok(Type::poly(name, params))
+                Ok(poly(name, params))
             }
             other if other.is_monomorphic() => Ok(other),
             other => todo!("{other}"),
@@ -545,7 +548,7 @@ impl Evaluator {
         let p = self.eval_tp(p, ctx)?;
         match p {
             TyParam::Value(ValueObj::Mut(v)) => Ok(v.borrow().class().mutate()),
-            TyParam::Value(v) => Ok(Type::enum_t(set![v])),
+            TyParam::Value(v) => Ok(enum_t(set![v])),
             TyParam::Erased(t) => Ok((*t).clone()),
             TyParam::FreeVar(fv) => {
                 if let Some(t) = fv.type_of() {
@@ -558,7 +561,7 @@ impl Evaluator {
             TyParam::Mono(name) => ctx
                 .consts
                 .get(&name)
-                .map(|v| Type::enum_t(set![v.clone()]))
+                .map(|v| enum_t(set![v.clone()]))
                 .ok_or_else(|| EvalError::unreachable(fn_name!(), line!())),
             TyParam::MonoQVar(name) => {
                 panic!("Not instantiated type variable: {name}")
diff --git a/compiler/erg_compiler/hir.rs b/compiler/erg_compiler/hir.rs
index 25704b71..6c2c6841 100644
--- a/compiler/erg_compiler/hir.rs
+++ b/compiler/erg_compiler/hir.rs
@@ -10,13 +10,15 @@ use erg_common::{
     impl_locational_for_enum, impl_nested_display_for_chunk_enum, impl_nested_display_for_enum,
     impl_stream_for_wrapper,
 };
-use erg_type::typaram::TyParam;
-use erg_type::value::ValueObj;
-use erg_type::{impl_t, impl_t_for_enum, HasType, Type};
 
 use erg_parser::ast::{fmt_lines, DefId, Identifier, Params, VarPattern};
 use erg_parser::token::{Token, TokenKind};
 
+use erg_type::constructors::array;
+use erg_type::typaram::TyParam;
+use erg_type::value::ValueObj;
+use erg_type::{impl_t, impl_t_for_enum, HasType, Type};
+
 use crate::error::readable_name;
 use crate::eval::type_from_token_kind;
 
@@ -517,7 +519,7 @@ impl_t!(NormalArray);
 
 impl NormalArray {
     pub fn new(l_sqbr: Token, r_sqbr: Token, elem_t: Type, elems: Args) -> Self {
-        let t = Type::array(elem_t, TyParam::value(elems.len()));
+        let t = array(elem_t, TyParam::value(elems.len()));
         Self {
             l_sqbr,
             r_sqbr,
diff --git a/compiler/erg_compiler/initialize.rs b/compiler/erg_compiler/initialize.rs
index 7ac85ad8..3e2fbde1 100644
--- a/compiler/erg_compiler/initialize.rs
+++ b/compiler/erg_compiler/initialize.rs
@@ -4,6 +4,7 @@
 use erg_common::vis::Visibility;
 use erg_common::Str;
 use erg_common::{debug_power_assert, set};
+
 use erg_type::constructors::*;
 use erg_type::typaram::TyParam;
 use erg_type::value::ValueObj;
@@ -119,8 +120,8 @@ impl Context {
         let named = Self::mono_trait("Named", vec![], Self::TOP_LEVEL);
         let mut mutable = Self::mono_trait("Mutable", vec![], Self::TOP_LEVEL);
         let proj = mono_proj(mono_q("Self"), "ImmutType");
-        let f_t = Type::func(vec![param_t("old", proj.clone())], vec![], proj);
-        let t = Type::pr1_met(mono_q("Self"), None, f_t, NoneType);
+        let f_t = func(vec![param_t("old", proj.clone())], vec![], proj);
+        let t = pr1_met(mono_q("Self"), None, f_t, NoneType);
         let t = quant(t, set! { subtypeof(mono_q("Self"), mono("Immutizable")) });
         mutable.register_decl("update!", t, Public);
         let mut immutizable =
@@ -129,7 +130,7 @@ impl Context {
         let mut mutizable = Self::mono_trait("Mutizable", vec![], Self::TOP_LEVEL);
         mutizable.register_decl("MutType!", Type, Public);
         let mut in_ = Self::poly_trait("In", vec![PS::t("T", NonDefault)], vec![], Self::TOP_LEVEL);
-        let op_t = Type::fn1_met(poly("In", vec![ty_tp(mono_q("T"))]), mono_q("T"), Bool);
+        let op_t = fn1_met(poly("In", vec![ty_tp(mono_q("T"))]), mono_q("T"), Bool);
         let op_t = quant(op_t, set! { static_instance("T", Type) });
         in_.register_decl("__in__", op_t, Public);
         // Erg does not have a trait equivalent to `PartialEq` in Rust
@@ -184,7 +185,7 @@ impl Context {
             set! {subtypeof(self_t.clone(), poly("Seq", vec![TyParam::erased(Type)]))},
         );
         seq.register_decl("__len__", t, Public);
-        let t = Type::fn1_met(self_t.clone(), Nat, mono_q("T"));
+        let t = fn1_met(self_t.clone(), Nat, mono_q("T"));
         let t = quant(
             t,
             set! {subtypeof(self_t, poly("Seq", vec![ty_tp(mono_q("T"))])), static_instance("T", Type)},
@@ -309,18 +310,8 @@ impl Context {
         obj.register_impl("__sizeof__", fn0_met(Obj, Nat), Const, Public);
         obj.register_impl("__repr__", fn0_met(Obj, Str), Immutable, Public);
         obj.register_impl("__str__", fn0_met(Obj, Str), Immutable, Public);
-        obj.register_impl(
-            "__dict__",
-            fn0_met(Obj, Type::dict(Str, Obj)),
-            Immutable,
-            Public,
-        );
-        obj.register_impl(
-            "__bytes__",
-            fn0_met(Obj, Type::mono("Bytes")),
-            Immutable,
-            Public,
-        );
+        obj.register_impl("__dict__", fn0_met(Obj, dict(Str, Obj)), Immutable, Public);
+        obj.register_impl("__bytes__", fn0_met(Obj, mono("Bytes")), Immutable, Public);
         obj.register_const("MutType!", ValueObj::t(mono("Obj!")));
         // let mut record = Self::mono_trait("Record", vec![Obj], Self::TOP_LEVEL);
         // let mut class = Self::mono_class("Class", vec![Type, Obj], Self::TOP_LEVEL);
@@ -377,7 +368,7 @@ impl Context {
         nat.register_impl("__mul__", op_t, Const, Public);
         nat.register_impl(
             "times!",
-            Type::pr_met(
+            pr_met(
                 Nat,
                 None,
                 vec![param_t("p", nd_proc(vec![], NoneType))],
@@ -484,7 +475,7 @@ impl Context {
         str_.register_impl("__add__", fn1_met(Str, Str, Str), Const, Public);
         str_.register_impl(
             "replace",
-            Type::fn_met(
+            fn_met(
                 Str,
                 vec![param_t("pat", Str), param_t("into", Str)],
                 vec![],
@@ -506,26 +497,21 @@ impl Context {
             ],
             Self::TOP_LEVEL,
         );
-        type_.register_impl(
-            "mro",
-            Type::array(Type, TyParam::erased(Nat)),
-            Immutable,
-            Public,
-        );
+        type_.register_impl("mro", array(Type, TyParam::erased(Nat)), Immutable, Public);
         let module = Self::mono_class(
             "Module",
             vec![Obj],
             vec![poly("Eq", vec![ty_tp(Module)]), mono("Named")],
             Self::TOP_LEVEL,
         );
-        let mut array = Self::poly_class(
+        let mut array_ = Self::poly_class(
             "Array",
             vec![PS::t_nd("T"), PS::named_nd("N", Nat)],
             vec![Obj],
             vec![
                 poly(
                     "Eq",
-                    vec![ty_tp(Type::poly(
+                    vec![ty_tp(poly(
                         "Array",
                         vec![ty_tp(mono_q("T")), mono_q_tp("N")],
                     ))],
@@ -538,42 +524,39 @@ impl Context {
         );
         let n = mono_q_tp("N");
         let m = mono_q_tp("M");
-        let array_t = Type::array(mono_q("T"), n.clone());
-        let t = Type::fn_met(
+        let array_t = array(mono_q("T"), n.clone());
+        let t = fn_met(
             array_t.clone(),
-            vec![param_t("rhs", Type::array(mono_q("T"), m.clone()))],
+            vec![param_t("rhs", array(mono_q("T"), m.clone()))],
             vec![],
-            Type::array(mono_q("T"), n + m),
+            array(mono_q("T"), n + m),
         );
         let t = quant(
             t,
             set! {static_instance("N", Nat), static_instance("M", Nat)},
         );
-        array.register_impl("concat", t, Immutable, Public);
+        array_.register_impl("concat", t, Immutable, Public);
         let n = mono_q_tp("N");
         let array_inner = mono_q("T");
-        let array_t = Type::array(array_inner.clone(), n.clone());
+        let array_t = array(array_inner.clone(), n.clone());
         let proj_t = mono_proj(array_inner.clone(), "ImmutType");
-        let t = Type::fn_met(
+        let t = fn_met(
             array_t.clone(),
-            vec![param_t(
-                "f",
-                Type::nd_func(vec![anon(proj_t.clone())], proj_t),
-            )],
+            vec![param_t("f", nd_func(vec![anon(proj_t.clone())], proj_t))],
             vec![],
-            Type::NoneType,
+            NoneType,
         );
         let t = quant(
             t,
-            set! {static_instance("N", Nat), static_instance("T", Type::mono("Mutable"))},
+            set! {static_instance("N", Nat), static_instance("T", mono("Mutable"))},
         );
-        array.register_impl("map!", t, Immutable, Public);
-        let mut_type = ValueObj::t(Type::poly(
+        array_.register_impl("map!", t, Immutable, Public);
+        let mut_type = ValueObj::t(poly(
             "Array!",
             vec![TyParam::t(mono_q("T")), TyParam::mono_q("N").mutate()],
         ));
         // [T; N].MutType! = [T; !N] (neither [T!; N] nor [T; N]!)
-        array.register_const("MutType!", mut_type);
+        array_.register_const("MutType!", mut_type);
         let mut int_mut = Self::mono_class(
             "Int!",
             vec![Int, Obj],
@@ -583,9 +566,9 @@ impl Context {
         int_mut.register_const("ImmutType", ValueObj::t(Int));
         let f_t = param_t(
             "f",
-            Type::func(vec![param_t("old", mono("Int"))], vec![], mono("Int")),
+            func(vec![param_t("old", mono("Int"))], vec![], mono("Int")),
         );
-        let t = Type::pr_met(mono("Int!"), None, vec![f_t], vec![], mono("Int!"));
+        let t = pr_met(mono("Int!"), None, vec![f_t], vec![], mono("Int!"));
         int_mut.register_impl("update!", t, Immutable, Public);
         let mut nat_mut = Self::mono_class(
             "Int!",
@@ -596,9 +579,9 @@ impl Context {
         nat_mut.register_const("ImmutType", ValueObj::t(Nat));
         let f_t = param_t(
             "f",
-            Type::func(vec![param_t("old", mono("Nat"))], vec![], mono("Nat")),
+            func(vec![param_t("old", mono("Nat"))], vec![], mono("Nat")),
         );
-        let t = Type::pr_met(mono("Nat!"), None, vec![f_t], vec![], mono("Nat!"));
+        let t = pr_met(mono("Nat!"), None, vec![f_t], vec![], mono("Nat!"));
         nat_mut.register_impl("update!", t, Immutable, Public);
         let mut float_mut = Self::mono_class(
             "Float!",
@@ -609,9 +592,9 @@ impl Context {
         float_mut.register_const("ImmutType", ValueObj::t(Float));
         let f_t = param_t(
             "f",
-            Type::func(vec![param_t("old", mono("Float"))], vec![], mono("Float")),
+            func(vec![param_t("old", mono("Float"))], vec![], mono("Float")),
         );
-        let t = Type::pr_met(mono("Float!"), None, vec![f_t], vec![], mono("Float!"));
+        let t = pr_met(mono("Float!"), None, vec![f_t], vec![], mono("Float!"));
         float_mut.register_impl("update!", t, Immutable, Public);
         let mut ratio_mut = Self::mono_class(
             "Ratio!",
@@ -622,9 +605,9 @@ impl Context {
         ratio_mut.register_const("ImmutType", ValueObj::t(Ratio));
         let f_t = param_t(
             "f",
-            Type::func(vec![param_t("old", mono("Ratio"))], vec![], mono("Ratio")),
+            func(vec![param_t("old", mono("Ratio"))], vec![], mono("Ratio")),
         );
-        let t = Type::pr_met(mono("Ratio!"), None, vec![f_t], vec![], mono("Ratio!"));
+        let t = pr_met(mono("Ratio!"), None, vec![f_t], vec![], mono("Ratio!"));
         ratio_mut.register_impl("update!", t, Immutable, Public);
         let mut bool_mut = Self::mono_class(
             "Bool!",
@@ -635,9 +618,9 @@ impl Context {
         bool_mut.register_const("ImmutType", ValueObj::t(Bool));
         let f_t = param_t(
             "f",
-            Type::func(vec![param_t("old", mono("Bool"))], vec![], mono("Bool")),
+            func(vec![param_t("old", mono("Bool"))], vec![], mono("Bool")),
         );
-        let t = Type::pr_met(mono("Bool!"), None, vec![f_t], vec![], mono("Bool!"));
+        let t = pr_met(mono("Bool!"), None, vec![f_t], vec![], mono("Bool!"));
         bool_mut.register_impl("update!", t, Immutable, Public);
         let mut str_mut = Self::mono_class(
             "Str!",
@@ -648,11 +631,11 @@ impl Context {
         str_mut.register_const("ImmutType", ValueObj::t(Str));
         let f_t = param_t(
             "f",
-            Type::func(vec![param_t("old", mono("Str"))], vec![], mono("Str")),
+            func(vec![param_t("old", mono("Str"))], vec![], mono("Str")),
         );
-        let t = Type::pr_met(mono("Str!"), None, vec![f_t], vec![], mono("Str!"));
+        let t = pr_met(mono("Str!"), None, vec![f_t], vec![], mono("Str!"));
         str_mut.register_impl("update!", t, Immutable, Public);
-        let array_mut_t = Type::poly("Array!", vec![ty_tp(mono_q("T")), mono_q_tp("N")]);
+        let array_mut_t = 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", mono("Nat!"))],
@@ -660,15 +643,15 @@ impl Context {
             vec![mono("Mutate"), poly("Seq", vec![ty_tp(mono_q("T"))])],
             Self::TOP_LEVEL,
         );
-        let t = Type::pr_met(
-            Type::ref_mut(array_mut_t.clone()),
-            Some(Type::ref_mut(poly(
+        let t = pr_met(
+            ref_mut(array_mut_t.clone()),
+            Some(ref_mut(poly(
                 "Array!",
                 vec![ty_tp(mono_q("T")), mono_q_tp("N") + value(1)],
             ))),
             vec![param_t("elem", mono_q("T"))],
             vec![],
-            Type::NoneType,
+            NoneType,
         );
         let t = quant(
             t,
@@ -677,13 +660,13 @@ impl Context {
         array_mut.register_impl("push!", t, Immutable, Public);
         let f_t = param_t(
             "f",
-            Type::func(
+            func(
                 vec![param_t("old", array_t.clone())],
                 vec![],
                 array_t.clone(),
             ),
         );
-        let t = Type::pr_met(
+        let t = pr_met(
             array_mut_t.clone(),
             None,
             vec![f_t],
@@ -691,16 +674,13 @@ impl Context {
             array_mut_t.clone(),
         );
         array_mut.register_impl("update!", t, Immutable, Public);
-        let range_t = Type::poly("Range", vec![TyParam::t(mono_q("T"))]);
+        let range_t = poly("Range", vec![TyParam::t(mono_q("T"))]);
         let range = Self::poly_class(
             "Range",
             vec![PS::t_nd("T")],
             vec![Obj],
             vec![
-                poly(
-                    "Eq",
-                    vec![ty_tp(Type::poly("Range", vec![ty_tp(mono_q("T"))]))],
-                ),
+                poly("Eq", vec![ty_tp(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"))]),
@@ -708,8 +688,8 @@ impl Context {
             Self::TOP_LEVEL,
         );
         self.register_type(Obj, obj, Const);
-        // self.register_type(Type::mono("Record"), vec![], record, Const);
-        // self.register_type(Type::mono("Class"), vec![], class, Const);
+        // self.register_type(mono("Record"), vec![], record, Const);
+        // self.register_type(mono("Class"), vec![], class, Const);
         self.register_type(Int, int, Const);
         self.register_type(Nat, nat, Const);
         self.register_type(Float, float, Const);
@@ -718,7 +698,7 @@ impl Context {
         self.register_type(Str, str_, Const);
         self.register_type(Type, type_, Const);
         self.register_type(Module, module, Const);
-        self.register_type(array_t, array, Const);
+        self.register_type(array_t, array_, Const);
         self.register_type(mono("Int!"), int_mut, Const);
         self.register_type(mono("Nat!"), nat_mut, Const);
         self.register_type(mono("Float!"), float_mut, Const);
@@ -736,7 +716,7 @@ impl Context {
             vec![param_t("err_message", Str)],
             NoneType,
         );
-        let t_classof = nd_func(vec![param_t("old", Obj)], Type::option(Class));
+        let t_classof = nd_func(vec![param_t("old", Obj)], option(Class));
         let t_compile = nd_func(vec![param_t("src", Str)], Code);
         let t_cond = nd_func(
             vec![
@@ -756,11 +736,11 @@ impl Context {
                 param_t("then", nd_func(vec![], mono_q("T"))),
             ],
             vec![param_t("else", nd_func(vec![], mono_q("T")))],
-            Type::option(mono_q("T")),
+            option(mono_q("T")),
         );
         let t_if = quant(t_if, set! {static_instance("T", Type)});
         let t_import = nd_func(vec![param_t("path", Str)], Module);
-        let t_log = nd_func(vec![param_t("objs", Type::var_args(Obj))], NoneType);
+        let t_log = nd_func(vec![param_t("objs", var_args(Obj))], NoneType);
         let t_pyimport = nd_func(vec![param_t("path", Str)], Module);
         let t_quit = func(vec![], vec![param_t("code", Int)], NoneType);
         self.register_impl("abs", t_abs, Const, Private);
@@ -782,7 +762,7 @@ impl Context {
 
     fn init_builtin_procs(&mut self) {
         let t_print = proc(
-            vec![param_t("objects", Type::var_args(Type::ref_(Obj)))],
+            vec![param_t("objects", var_args(ref_(Obj)))],
             vec![
                 param_t("sep", Str),
                 param_t("end", Str),
@@ -798,12 +778,12 @@ impl Context {
                 param_t("then", nd_proc(vec![], mono_q("T"))),
             ],
             vec![param_t("else", nd_proc(vec![], mono_q("T")))],
-            Type::option(mono_q("T")),
+            option(mono_q("T")),
         );
         let t_if = quant(t_if, set! {static_instance("T", Type)});
         let t_for = nd_proc(
             vec![
-                param_t("iter", Type::iter(mono_q("T"))),
+                param_t("iter", iter(mono_q("T"))),
                 param_t("p", nd_proc(vec![anon(mono_q("T"))], NoneType)),
             ],
             NoneType,
@@ -840,7 +820,7 @@ impl Context {
             },
         );
         self.register_impl("__add__", op_t, Const, Private);
-        let op_t = Type::bin_op(l.clone(), r.clone(), mono_proj(mono_q("L"), "SubO"));
+        let op_t = bin_op(l.clone(), r.clone(), mono_proj(mono_q("L"), "SubO"));
         let op_t = quant(
             op_t,
             set! {
@@ -849,7 +829,7 @@ impl Context {
             },
         );
         self.register_impl("__sub__", op_t, Const, Private);
-        let op_t = Type::bin_op(l.clone(), r.clone(), mono_proj(mono_q("L"), "MulO"));
+        let op_t = bin_op(l.clone(), r.clone(), mono_proj(mono_q("L"), "MulO"));
         let op_t = quant(
             op_t,
             set! {
@@ -858,7 +838,7 @@ impl Context {
             },
         );
         self.register_impl("__mul__", op_t, Const, Private);
-        let op_t = Type::bin_op(l.clone(), r.clone(), mono_proj(mono_q("L"), "DivO"));
+        let op_t = bin_op(l.clone(), r.clone(), mono_proj(mono_q("L"), "DivO"));
         let op_t = quant(
             op_t,
             set! {
@@ -868,45 +848,45 @@ impl Context {
         );
         self.register_impl("__div__", op_t, Const, Private);
         let m = mono_q("M");
-        let op_t = Type::bin_op(m.clone(), m.clone(), m.clone());
+        let op_t = bin_op(m.clone(), m.clone(), m.clone());
         let op_t = quant(op_t, set! {subtypeof(m, poly("Mul", vec![]))});
         // TODO: add bound: M == MulO
         self.register_impl("__pow__", op_t, Const, Private);
         let d = mono_q("D");
-        let op_t = Type::bin_op(d.clone(), d.clone(), d.clone());
+        let op_t = bin_op(d.clone(), d.clone(), d.clone());
         let op_t = quant(op_t, set! {subtypeof(d, poly("Div", vec![]))});
         self.register_impl("__mod__", op_t, Const, Private);
         let e = mono_q("E");
-        let op_t = Type::bin_op(e.clone(), e.clone(), Bool);
+        let op_t = bin_op(e.clone(), e.clone(), Bool);
         let op_t = quant(op_t, set! {subtypeof(e, poly("Eq", vec![]))});
         self.register_impl("__eq__", op_t.clone(), Const, Private);
         self.register_impl("__ne__", op_t, Const, Private);
         let o = mono_q("O");
-        let op_t = Type::bin_op(o.clone(), o.clone(), Bool);
+        let op_t = bin_op(o.clone(), o.clone(), Bool);
         let op_t = quant(op_t, set! {subtypeof(o, mono("Ord"))});
         self.register_impl("__lt__", op_t.clone(), Const, Private);
         self.register_impl("__le__", op_t.clone(), Const, Private);
         self.register_impl("__gt__", op_t.clone(), Const, Private);
         self.register_impl("__ge__", op_t, Const, Private);
-        self.register_impl("__and__", Type::bin_op(Bool, Bool, Bool), Const, Private);
-        self.register_impl("__or__", Type::bin_op(Bool, Bool, Bool), Const, Private);
+        self.register_impl("__and__", bin_op(Bool, Bool, Bool), Const, Private);
+        self.register_impl("__or__", bin_op(Bool, Bool, Bool), Const, Private);
         let t = mono_q("T");
-        let op_t = Type::bin_op(t.clone(), t.clone(), Type::range(t.clone()));
+        let op_t = bin_op(t.clone(), t.clone(), range(t.clone()));
         let op_t = quant(op_t, set! {subtypeof(t.clone(), mono("Ord"))});
         self.register_decl("__rng__", op_t.clone(), Private);
         self.register_decl("__lorng__", op_t.clone(), Private);
         self.register_decl("__rorng__", op_t.clone(), Private);
         self.register_decl("__orng__", op_t, Private);
-        let op_t = Type::bin_op(mono_q("T"), poly("In", vec![ty_tp(mono_q("T"))]), Bool);
+        let op_t = bin_op(mono_q("T"), poly("In", vec![ty_tp(mono_q("T"))]), Bool);
         let op_t = quant(op_t, set! { static_instance("T", Type) });
         self.register_impl("__in__", op_t, Const, Private);
         /* unary */
         // TODO: Boolの+/-は警告を出したい
-        let op_t = Type::func1(mono_q("T"), Type::mono_proj(mono_q("T"), "MutType!"));
+        let op_t = func1(mono_q("T"), mono_proj(mono_q("T"), "MutType!"));
         let op_t = quant(op_t, set! {subtypeof(mono_q("T"), mono("Mutate"))});
         self.register_impl("__mutate__", op_t, Const, Private);
         let n = mono_q("N");
-        let op_t = Type::func1(n.clone(), n.clone());
+        let op_t = func1(n.clone(), n.clone());
         let op_t = quant(op_t, set! {subtypeof(n, mono("Num"))});
         self.register_decl("__pos__", op_t.clone(), Private);
         self.register_decl("__neg__", op_t, Private);
@@ -960,12 +940,12 @@ impl Context {
 
     pub(crate) fn init_py_math_mod() -> Self {
         let mut math = Context::module("math".into(), 10);
-        math.register_impl("pi", Type::Float, Immutable, Public);
-        math.register_impl("tau", Type::Float, Immutable, Public);
-        math.register_impl("e", Type::Float, Immutable, Public);
-        math.register_impl("sin", Type::func1(Float, Float), Immutable, Public);
-        math.register_impl("cos", Type::func1(Float, Float), Immutable, Public);
-        math.register_impl("tan", Type::func1(Float, Float), Immutable, Public);
+        math.register_impl("pi", Float, Immutable, Public);
+        math.register_impl("tau", Float, Immutable, Public);
+        math.register_impl("e", Float, Immutable, Public);
+        math.register_impl("sin", func1(Float, Float), Immutable, Public);
+        math.register_impl("cos", func1(Float, Float), Immutable, Public);
+        math.register_impl("tan", func1(Float, Float), Immutable, Public);
         math
     }
 
@@ -973,11 +953,11 @@ impl Context {
         let mut random = Context::module("random".into(), 10);
         random.register_impl(
             "seed!",
-            Type::proc(
+            proc(
                 vec![],
                 vec![
-                    param_t("a", Type::mono("Num")), // TODO: NoneType, int, float, str, bytes, bytearray
-                    param_t("version", Type::Int),
+                    param_t("a", mono("Num")), // TODO: NoneType, int, float, str, bytes, bytearray
+                    param_t("version", Int),
                 ],
                 NoneType,
             ),
@@ -991,7 +971,7 @@ impl Context {
             Public,
         );
         let t = nd_proc(
-            vec![param_t("seq", Type::poly("Seq", vec![ty_tp(mono_q("T"))]))],
+            vec![param_t("seq", poly("Seq", vec![ty_tp(mono_q("T"))]))],
             mono_q("T"),
         );
         let t = quant(t, set! {static_instance("T", Type)});
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index 952f2fbe..878753a0 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -11,6 +11,7 @@ use erg_common::{fn_name, log, switch_lang};
 use erg_parser::ast;
 use erg_parser::ast::AST;
 
+use erg_type::constructors::{array, array_mut, func, mono, poly, proc, quant};
 use erg_type::typaram::TyParam;
 use erg_type::value::ValueObj;
 use erg_type::{HasType, ParamTy, Type};
@@ -160,34 +161,34 @@ impl ASTLowerer {
         match maybe_len {
             Some(v @ ValueObj::Nat(_)) => {
                 if elem.ref_t().is_mut() {
-                    Type::poly(
+                    poly(
                         "ArrayWithMutType!",
                         vec![TyParam::t(elem.t()), TyParam::Value(v)],
                     )
                 } else {
-                    Type::array(elem.t(), TyParam::Value(v))
+                    array(elem.t(), TyParam::Value(v))
                 }
             }
-            Some(v @ ValueObj::Mut(_)) if v.class() == Type::mono("Nat!") => {
+            Some(v @ ValueObj::Mut(_)) if v.class() == mono("Nat!") => {
                 if elem.ref_t().is_mut() {
-                    Type::poly(
+                    poly(
                         "ArrayWithMutTypeAndLength!",
                         vec![TyParam::t(elem.t()), TyParam::Value(v)],
                     )
                 } else {
-                    Type::array_mut(elem.t(), TyParam::Value(v))
+                    array_mut(elem.t(), TyParam::Value(v))
                 }
             }
             Some(other) => todo!("{other} is not a Nat object"),
             // TODO: [T; !_]
             None => {
                 if elem.ref_t().is_mut() {
-                    Type::poly(
+                    poly(
                         "ArrayWithMutType!",
                         vec![TyParam::t(elem.t()), TyParam::erased(Type::Nat)],
                     )
                 } else {
-                    Type::array(elem.t(), TyParam::erased(Type::Nat))
+                    array(elem.t(), TyParam::erased(Type::Nat))
                 }
             }
         }
@@ -346,14 +347,14 @@ impl ASTLowerer {
             })?;
         self.pop_append_errs();
         let t = if is_procedural {
-            Type::proc(non_default_params, default_params, body.t())
+            proc(non_default_params, default_params, body.t())
         } else {
-            Type::func(non_default_params, default_params, body.t())
+            func(non_default_params, default_params, body.t())
         };
         let t = if bounds.is_empty() {
             t
         } else {
-            Type::quantified(t, bounds)
+            quant(t, bounds)
         };
         Ok(hir::Lambda::new(id, lambda.sig.params, lambda.op, body, t))
     }
diff --git a/compiler/erg_parser/ast.rs b/compiler/erg_parser/ast.rs
index db4c27e6..b1453b41 100644
--- a/compiler/erg_parser/ast.rs
+++ b/compiler/erg_parser/ast.rs
@@ -47,13 +47,7 @@ impl NestedDisplay for Literal {
 }
 
 impl_display_from_nested!(Literal);
-
-impl Locational for Literal {
-    #[inline]
-    fn loc(&self) -> Location {
-        self.token.loc()
-    }
-}
+impl_locational!(Literal, token);
 
 impl From<Token> for Literal {
     #[inline]
@@ -81,12 +75,7 @@ impl NestedDisplay for PosArg {
 }
 
 impl_display_from_nested!(PosArg);
-
-impl Locational for PosArg {
-    fn loc(&self) -> Location {
-        self.expr.loc()
-    }
-}
+impl_locational!(PosArg, expr);
 
 impl PosArg {
     pub const fn new(expr: Expr) -> Self {
@@ -108,12 +97,7 @@ impl NestedDisplay for KwArg {
 }
 
 impl_display_from_nested!(KwArg);
-
-impl Locational for KwArg {
-    fn loc(&self) -> Location {
-        Location::concat(&self.keyword, &self.expr)
-    }
-}
+impl_locational!(KwArg, keyword, expr);
 
 impl KwArg {
     pub const fn new(keyword: Token, expr: Expr) -> Self {
@@ -226,7 +210,7 @@ impl NestedDisplay for Local {
 }
 
 impl_display_from_nested!(Local);
-impl_locational!(Local, symbol, symbol);
+impl_locational!(Local, symbol);
 
 impl Local {
     pub const fn new(symbol: Token) -> Self {
@@ -804,13 +788,7 @@ impl NestedDisplay for ConstLocal {
 }
 
 impl_display_from_nested!(ConstLocal);
-
-impl Locational for ConstLocal {
-    #[inline]
-    fn loc(&self) -> Location {
-        self.symbol.loc()
-    }
-}
+impl_locational!(ConstLocal, symbol);
 
 impl ConstLocal {
     pub const fn new(symbol: Token) -> Self {
@@ -1078,11 +1056,7 @@ impl NestedDisplay for ConstPosArg {
     }
 }
 
-impl Locational for ConstPosArg {
-    fn loc(&self) -> Location {
-        self.expr.loc()
-    }
-}
+impl_locational!(ConstPosArg, expr);
 
 impl ConstPosArg {
     pub const fn new(expr: ConstExpr) -> Self {
@@ -1102,11 +1076,7 @@ impl NestedDisplay for ConstKwArg {
     }
 }
 
-impl Locational for ConstKwArg {
-    fn loc(&self) -> Location {
-        Location::concat(&self.keyword, &self.expr)
-    }
-}
+impl_locational!(ConstKwArg, keyword, expr);
 
 impl ConstKwArg {
     pub const fn new(keyword: Token, expr: ConstExpr) -> Self {
diff --git a/compiler/erg_type/constructors.rs b/compiler/erg_type/constructors.rs
index e91de40b..3c653e22 100644
--- a/compiler/erg_type/constructors.rs
+++ b/compiler/erg_type/constructors.rs
@@ -10,64 +10,391 @@ pub const fn anon(ty: Type) -> ParamTy {
     ParamTy::anonymous(ty)
 }
 
-#[inline]
-pub fn mono<S: Into<Str>>(name: S) -> Type {
-    Type::mono(name)
+/// Top := {=}
+#[allow(non_snake_case)]
+pub const fn Top() -> Type {
+    Type::Mono(Str::ever("Top"))
+}
+/// Bottom := {}
+#[allow(non_snake_case)]
+pub const fn Bottom() -> Type {
+    Type::Mono(Str::ever("Bottom"))
 }
 
 #[inline]
-pub fn mono_q<S: Into<Str>>(name: S) -> Type {
-    Type::mono_q(name)
+pub fn free_var(level: usize, constraint: Constraint) -> Type {
+    Type::FreeVar(Free::new_unbound(level, constraint))
 }
 
 #[inline]
-pub fn mono_proj<S: Into<Str>>(lhs: Type, rhs: S) -> Type {
-    Type::mono_proj(lhs, rhs)
+pub fn named_free_var(name: Str, level: usize, constraint: Constraint) -> Type {
+    Type::FreeVar(Free::new_named_unbound(name, level, constraint))
+}
+
+pub fn array(elem_t: Type, len: TyParam) -> Type {
+    poly("Array", vec![TyParam::t(elem_t), len])
+}
+
+pub fn array_mut(elem_t: Type, len: TyParam) -> Type {
+    poly("Array!", vec![TyParam::t(elem_t), len])
+}
+
+pub fn dict(k_t: Type, v_t: Type) -> Type {
+    poly("Dict", vec![TyParam::t(k_t), TyParam::t(v_t)])
+}
+
+pub fn tuple(args: Vec<Type>) -> Type {
+    poly("Tuple", args.into_iter().map(TyParam::t).collect())
 }
 
 #[inline]
-pub fn poly<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Type {
-    Type::poly(name, params)
+pub fn var_args(elem_t: Type) -> Type {
+    Type::VarArgs(Box::new(elem_t))
 }
 
 #[inline]
-pub fn poly_q<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Type {
-    Type::poly_q(name, params)
+pub fn range(t: Type) -> Type {
+    poly("Range", vec![TyParam::t(t)])
+}
+
+pub fn enum_t(s: Set<ValueObj>) -> Type {
+    assert!(is_homogeneous(&s));
+    let name = Str::from(fresh_varname());
+    let preds = s
+        .iter()
+        .map(|o| Predicate::eq(name.clone(), TyParam::value(o.clone())))
+        .collect();
+    let refine = RefinementType::new(name, inner_class(&s), preds);
+    Type::Refinement(refine)
 }
 
 #[inline]
-pub fn func(non_default_params: Vec<ParamTy>, default_params: Vec<ParamTy>, ret: Type) -> Type {
-    Type::func(non_default_params, default_params, ret)
+pub fn int_interval<P: Into<TyParam>, Q: Into<TyParam>>(op: IntervalOp, l: P, r: Q) -> Type {
+    let l = l.into();
+    let r = r.into();
+    let l = l.try_into().unwrap_or_else(|l| todo!("{l}"));
+    let r = r.try_into().unwrap_or_else(|r| todo!("{r}"));
+    let name = Str::from(fresh_varname());
+    let pred = match op {
+        IntervalOp::LeftOpen if l == TyParam::value(NegInf) => Predicate::le(name.clone(), r),
+        // l<..r => {I: classof(l) | I >= l+ε and I <= r}
+        IntervalOp::LeftOpen => Predicate::and(
+            Predicate::ge(name.clone(), TyParam::succ(l)),
+            Predicate::le(name.clone(), r),
+        ),
+        IntervalOp::RightOpen if r == TyParam::value(Inf) => Predicate::ge(name.clone(), l),
+        // l..<r => {I: classof(l) | I >= l and I <= r-ε}
+        IntervalOp::RightOpen => Predicate::and(
+            Predicate::ge(name.clone(), l),
+            Predicate::le(name.clone(), TyParam::pred(r)),
+        ),
+        // l..r => {I: classof(l) | I >= l and I <= r}
+        IntervalOp::Closed => Predicate::and(
+            Predicate::ge(name.clone(), l),
+            Predicate::le(name.clone(), r),
+        ),
+        IntervalOp::Open if l == TyParam::value(NegInf) && r == TyParam::value(Inf) => {
+            return refinement(name, Type::Int, set! {})
+        }
+        // l<..<r => {I: classof(l) | I >= l+ε and I <= r-ε}
+        IntervalOp::Open => Predicate::and(
+            Predicate::ge(name.clone(), TyParam::succ(l)),
+            Predicate::le(name.clone(), TyParam::pred(r)),
+        ),
+    };
+    refinement(name, Type::Int, set! {pred})
 }
 
-#[inline]
-pub fn proc(non_default_params: Vec<ParamTy>, default_params: Vec<ParamTy>, ret: Type) -> Type {
-    Type::proc(non_default_params, default_params, ret)
+pub fn iter(t: Type) -> Type {
+    poly("Iter", vec![TyParam::t(t)])
 }
 
+pub fn ref_(t: Type) -> Type {
+    Type::Ref(Box::new(t))
+}
+
+pub fn ref_mut(t: Type) -> Type {
+    Type::RefMut(Box::new(t))
+}
+
+pub fn option(t: Type) -> Type {
+    poly("Option", vec![TyParam::t(t)])
+}
+
+pub fn option_mut(t: Type) -> Type {
+    poly("Option!", vec![TyParam::t(t)])
+}
+
+pub fn subr_t(
+    kind: SubrKind,
+    non_default_params: Vec<ParamTy>,
+    default_params: Vec<ParamTy>,
+    return_t: Type,
+) -> Type {
+    Type::Subr(SubrType::new(
+        kind,
+        non_default_params,
+        default_params,
+        return_t,
+    ))
+}
+
+pub fn func(
+    non_default_params: Vec<ParamTy>,
+    default_params: Vec<ParamTy>,
+    return_t: Type,
+) -> Type {
+    Type::Subr(SubrType::new(
+        SubrKind::Func,
+        non_default_params,
+        default_params,
+        return_t,
+    ))
+}
+
+pub fn func1(param_t: Type, return_t: Type) -> Type {
+    func(vec![ParamTy::anonymous(param_t)], vec![], return_t)
+}
+
+pub fn kind1(param: Type) -> Type {
+    func1(param, Type::Type)
+}
+
+pub fn func2(l: Type, r: Type, return_t: Type) -> Type {
+    func(
+        vec![ParamTy::anonymous(l), ParamTy::anonymous(r)],
+        vec![],
+        return_t,
+    )
+}
+
+pub fn bin_op(l: Type, r: Type, return_t: Type) -> Type {
+    nd_func(
+        vec![
+            ParamTy::named(Str::ever("lhs"), l.clone()),
+            ParamTy::named(Str::ever("rhs"), r.clone()),
+        ],
+        return_t,
+    )
+}
+
+pub fn anon_param_func(
+    non_default_params: Vec<Type>,
+    default_params: Vec<Type>,
+    return_t: Type,
+) -> Type {
+    let non_default_params = non_default_params
+        .into_iter()
+        .map(ParamTy::anonymous)
+        .collect();
+    let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
+    func(non_default_params, default_params, return_t)
+}
+
+pub fn proc(
+    non_default_params: Vec<ParamTy>,
+    default_params: Vec<ParamTy>,
+    return_t: Type,
+) -> Type {
+    Type::Subr(SubrType::new(
+        SubrKind::Proc,
+        non_default_params,
+        default_params,
+        return_t,
+    ))
+}
+
+pub fn proc1(param_t: Type, return_t: Type) -> Type {
+    proc(vec![ParamTy::anonymous(param_t)], vec![], return_t)
+}
+
+pub fn proc2(l: Type, r: Type, return_t: Type) -> Type {
+    proc(
+        vec![ParamTy::anonymous(l), ParamTy::anonymous(r)],
+        vec![],
+        return_t,
+    )
+}
+
+pub fn anon_param_proc(
+    non_default_params: Vec<Type>,
+    default_params: Vec<Type>,
+    return_t: Type,
+) -> Type {
+    let non_default_params = non_default_params
+        .into_iter()
+        .map(ParamTy::anonymous)
+        .collect();
+    let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
+    proc(non_default_params, default_params, return_t)
+}
+
+pub fn fn_met(
+    self_t: Type,
+    non_default_params: Vec<ParamTy>,
+    default_params: Vec<ParamTy>,
+    return_t: Type,
+) -> Type {
+    Type::Subr(SubrType::new(
+        SubrKind::FuncMethod(Box::new(self_t)),
+        non_default_params,
+        default_params,
+        return_t,
+    ))
+}
+
+pub fn fn0_met(self_t: Type, return_t: Type) -> Type {
+    fn_met(self_t, vec![], vec![], return_t)
+}
+
+pub fn fn1_met(self_t: Type, input_t: Type, return_t: Type) -> Type {
+    fn_met(self_t, vec![ParamTy::anonymous(input_t)], vec![], return_t)
+}
+
+pub fn anon_param_fn_met(
+    self_t: Type,
+    non_default_params: Vec<Type>,
+    default_params: Vec<Type>,
+    return_t: Type,
+) -> Type {
+    let non_default_params = non_default_params
+        .into_iter()
+        .map(ParamTy::anonymous)
+        .collect();
+    let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
+    fn_met(self_t, non_default_params, default_params, return_t)
+}
+
+pub fn pr_met(
+    self_before: Type,
+    self_after: Option<Type>,
+    non_default_params: Vec<ParamTy>,
+    default_params: Vec<ParamTy>,
+    return_t: Type,
+) -> Type {
+    Type::Subr(SubrType::new(
+        SubrKind::pr_met(self_before, self_after),
+        non_default_params,
+        default_params,
+        return_t,
+    ))
+}
+
+pub fn pr0_met(self_before: Type, self_after: Option<Type>, return_t: Type) -> Type {
+    pr_met(self_before, self_after, vec![], vec![], return_t)
+}
+
+pub fn pr1_met(self_before: Type, self_after: Option<Type>, input_t: Type, return_t: Type) -> Type {
+    pr_met(
+        self_before,
+        self_after,
+        vec![ParamTy::anonymous(input_t)],
+        vec![],
+        return_t,
+    )
+}
+
+pub fn anon_param_pr_met(
+    self_before: Type,
+    self_after: Option<Type>,
+    non_default_params: Vec<Type>,
+    default_params: Vec<Type>,
+    return_t: Type,
+) -> Type {
+    let non_default_params = non_default_params
+        .into_iter()
+        .map(ParamTy::anonymous)
+        .collect();
+    let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
+    pr_met(
+        self_before,
+        self_after,
+        non_default_params,
+        default_params,
+        return_t,
+    )
+}
+
+/// function type with non-default parameters
 #[inline]
 pub fn nd_func(params: Vec<ParamTy>, ret: Type) -> Type {
-    Type::nd_func(params, ret)
+    func(params, vec![], ret)
 }
 
 #[inline]
 pub fn nd_proc(params: Vec<ParamTy>, ret: Type) -> Type {
-    Type::nd_proc(params, ret)
+    proc(params, vec![], ret)
+}
+
+pub fn callable(param_ts: Vec<Type>, return_t: Type) -> Type {
+    Type::Callable {
+        param_ts,
+        return_t: Box::new(return_t),
+    }
 }
 
 #[inline]
-pub fn fn0_met(self_t: Type, return_t: Type) -> Type {
-    Type::fn0_met(self_t, return_t)
+pub fn mono<S: Into<Str>>(name: S) -> Type {
+    Type::Mono(name.into())
 }
 
 #[inline]
-pub fn fn1_met(self_t: Type, input_t: Type, return_t: Type) -> Type {
-    Type::fn1_met(self_t, input_t, return_t)
+pub fn mono_q<S: Into<Str>>(name: S) -> Type {
+    Type::MonoQVar(name.into())
 }
 
 #[inline]
+pub fn poly<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Type {
+    Type::Poly {
+        name: name.into(),
+        params,
+    }
+}
+
+#[inline]
+pub fn poly_q<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Type {
+    Type::PolyQVar {
+        name: name.into(),
+        params,
+    }
+}
+
+#[inline]
+pub fn mono_proj<S: Into<Str>>(lhs: Type, rhs: S) -> Type {
+    Type::MonoProj {
+        lhs: Box::new(lhs),
+        rhs: rhs.into(),
+    }
+}
+
+/// ```rust
+/// {I: Int | I >= 0}
+/// => Refinement{
+///     layout: TyParam::MonoQ "I",
+///     bounds: [TyBound::Instance("I", "Int")],
+///     preds: [Predicate::GreaterEqual("I", 0)]
+/// }
+/// ```
+#[inline]
+pub fn refinement(var: Str, t: Type, preds: Set<Predicate>) -> Type {
+    Type::Refinement(RefinementType::new(var, t, preds))
+}
+
+/// quantified((T -> T), T: Type) => |T: Type| T -> T
 pub fn quant(unbound_t: Type, bounds: Set<TyBound>) -> Type {
-    Type::quantified(unbound_t, bounds)
+    Type::Quantified(QuantifiedType::new(unbound_t, bounds))
+}
+
+pub fn and(lhs: Type, rhs: Type) -> Type {
+    Type::And(Box::new(lhs), Box::new(rhs))
+}
+
+pub fn or(lhs: Type, rhs: Type) -> Type {
+    Type::Or(Box::new(lhs), Box::new(rhs))
+}
+
+pub fn not(lhs: Type, rhs: Type) -> Type {
+    Type::Not(Box::new(lhs), Box::new(rhs))
 }
 
 #[inline]
diff --git a/compiler/erg_type/deserialize.rs b/compiler/erg_type/deserialize.rs
index 915871aa..4c4b1eaf 100644
--- a/compiler/erg_type/deserialize.rs
+++ b/compiler/erg_type/deserialize.rs
@@ -10,6 +10,7 @@ use erg_common::{fn_name, switch_lang};
 use erg_common::{RcArray, Str};
 
 use crate::codeobj::CodeObj;
+use crate::constructors::array;
 use crate::typaram::TyParam;
 use crate::value::ValueObj;
 use crate::{HasType, Type};
@@ -295,7 +296,7 @@ impl Deserializer {
                 Ok(strs)
             }
             other => Err(DeserializeError::type_error(
-                &Type::array(Type::Str, TyParam::erased(Type::Nat)),
+                &array(Type::Str, TyParam::erased(Type::Nat)),
                 other.ref_t(),
             )),
         }
diff --git a/compiler/erg_type/lib.rs b/compiler/erg_type/lib.rs
index 73c96841..8e840dbb 100644
--- a/compiler/erg_type/lib.rs
+++ b/compiler/erg_type/lib.rs
@@ -18,6 +18,7 @@ use erg_common::vis::Field;
 use erg_common::{enum_unwrap, fmt_option, fmt_set_split_with, set, Str};
 
 use crate::codeobj::CodeObj;
+use crate::constructors::{and, int_interval, mono, Top};
 use crate::free::{fresh_varname, Constraint, Free, FreeKind, FreeTyVar, HasLevel, Level};
 use crate::typaram::{IntervalOp, TyParam};
 use crate::value::value_set::*;
@@ -255,7 +256,7 @@ impl TyBound {
 
     pub fn instance(name: Str, t: Type) -> Self {
         if t == Type::Type {
-            Self::sandwiched(Type::Never, Type::mono(name), Type::Obj)
+            Self::sandwiched(Type::Never, mono(name), Type::Obj)
         } else {
             Self::Instance { name, t }
         }
@@ -1217,27 +1218,27 @@ impl Default for Type {
 
 impl From<Range<TyParam>> for Type {
     fn from(r: Range<TyParam>) -> Self {
-        Type::int_interval(IntervalOp::RightOpen, r.start, r.end)
+        int_interval(IntervalOp::RightOpen, r.start, r.end)
     }
 }
 
 impl From<Range<&TyParam>> for Type {
     fn from(r: Range<&TyParam>) -> Self {
-        Type::int_interval(IntervalOp::RightOpen, r.start.clone(), r.end.clone())
+        int_interval(IntervalOp::RightOpen, r.start.clone(), r.end.clone())
     }
 }
 
 impl From<RangeInclusive<TyParam>> for Type {
     fn from(r: RangeInclusive<TyParam>) -> Self {
         let (start, end) = r.into_inner();
-        Type::int_interval(IntervalOp::Closed, start, end)
+        int_interval(IntervalOp::Closed, start, end)
     }
 }
 
 impl From<RangeInclusive<&TyParam>> for Type {
     fn from(r: RangeInclusive<&TyParam>) -> Self {
         let (start, end) = r.into_inner();
-        Type::int_interval(IntervalOp::Closed, start.clone(), end.clone())
+        int_interval(IntervalOp::Closed, start.clone(), end.clone())
     }
 }
 
@@ -1266,7 +1267,7 @@ impl From<&str> for Type {
             "Never" => Self::Never,
             "Inf" => Self::Inf,
             "NegInf" => Self::NegInf,
-            "_" => Self::Top(),
+            "_" => Top(),
             other => Self::Mono(Str::rc(other)),
         }
     }
@@ -1437,398 +1438,6 @@ impl Type {
     pub const NEVER: &'static Self = &Self::Never;
     pub const FAILURE: &'static Self = &Self::Failure;
 
-    /// Top := {=}
-    #[allow(non_snake_case)]
-    pub const fn Top() -> Self {
-        Self::Mono(Str::ever("Top"))
-    }
-    /// Bottom := {}
-    #[allow(non_snake_case)]
-    pub const fn Bottom() -> Self {
-        Self::Mono(Str::ever("Bottom"))
-    }
-
-    #[inline]
-    pub fn free_var(level: usize, constraint: Constraint) -> Self {
-        Self::FreeVar(Free::new_unbound(level, constraint))
-    }
-
-    #[inline]
-    pub fn named_free_var(name: Str, level: usize, constraint: Constraint) -> Self {
-        Self::FreeVar(Free::new_named_unbound(name, level, constraint))
-    }
-
-    pub fn array(elem_t: Type, len: TyParam) -> Self {
-        Self::poly("Array", vec![TyParam::t(elem_t), len])
-    }
-
-    pub fn array_mut(elem_t: Type, len: TyParam) -> Self {
-        Self::poly("Array!", vec![TyParam::t(elem_t), len])
-    }
-
-    pub fn dict(k_t: Type, v_t: Type) -> Self {
-        Self::poly("Dict", vec![TyParam::t(k_t), TyParam::t(v_t)])
-    }
-
-    pub fn tuple(args: Vec<Type>) -> Self {
-        Self::poly("Tuple", args.into_iter().map(TyParam::t).collect())
-    }
-
-    #[inline]
-    pub fn var_args(elem_t: Type) -> Self {
-        Self::VarArgs(Box::new(elem_t))
-    }
-
-    #[inline]
-    pub fn range(t: Type) -> Self {
-        Self::poly("Range", vec![TyParam::t(t)])
-    }
-
-    pub fn enum_t(s: Set<ValueObj>) -> Self {
-        assert!(is_homogeneous(&s));
-        let name = Str::from(fresh_varname());
-        let preds = s
-            .iter()
-            .map(|o| Predicate::eq(name.clone(), TyParam::value(o.clone())))
-            .collect();
-        let refine = RefinementType::new(name, inner_class(&s), preds);
-        Self::Refinement(refine)
-    }
-
-    #[inline]
-    pub fn int_interval<P: Into<TyParam>, Q: Into<TyParam>>(op: IntervalOp, l: P, r: Q) -> Self {
-        let l = l.into();
-        let r = r.into();
-        let l = l.try_into().unwrap_or_else(|l| todo!("{l}"));
-        let r = r.try_into().unwrap_or_else(|r| todo!("{r}"));
-        let name = Str::from(fresh_varname());
-        let pred = match op {
-            IntervalOp::LeftOpen if l == TyParam::value(NegInf) => Predicate::le(name.clone(), r),
-            // l<..r => {I: classof(l) | I >= l+ε and I <= r}
-            IntervalOp::LeftOpen => Predicate::and(
-                Predicate::ge(name.clone(), TyParam::succ(l)),
-                Predicate::le(name.clone(), r),
-            ),
-            IntervalOp::RightOpen if r == TyParam::value(Inf) => Predicate::ge(name.clone(), l),
-            // l..<r => {I: classof(l) | I >= l and I <= r-ε}
-            IntervalOp::RightOpen => Predicate::and(
-                Predicate::ge(name.clone(), l),
-                Predicate::le(name.clone(), TyParam::pred(r)),
-            ),
-            // l..r => {I: classof(l) | I >= l and I <= r}
-            IntervalOp::Closed => Predicate::and(
-                Predicate::ge(name.clone(), l),
-                Predicate::le(name.clone(), r),
-            ),
-            IntervalOp::Open if l == TyParam::value(NegInf) && r == TyParam::value(Inf) => {
-                return Type::refinement(name, Type::Int, set! {})
-            }
-            // l<..<r => {I: classof(l) | I >= l+ε and I <= r-ε}
-            IntervalOp::Open => Predicate::and(
-                Predicate::ge(name.clone(), TyParam::succ(l)),
-                Predicate::le(name.clone(), TyParam::pred(r)),
-            ),
-        };
-        Type::refinement(name, Type::Int, set! {pred})
-    }
-
-    pub fn iter(t: Type) -> Self {
-        Self::poly("Iter", vec![TyParam::t(t)])
-    }
-
-    pub fn ref_(t: Type) -> Self {
-        Self::Ref(Box::new(t))
-    }
-
-    pub fn ref_mut(t: Type) -> Self {
-        Self::RefMut(Box::new(t))
-    }
-
-    pub fn option(t: Type) -> Self {
-        Self::poly("Option", vec![TyParam::t(t)])
-    }
-
-    pub fn option_mut(t: Type) -> Self {
-        Self::poly("Option!", vec![TyParam::t(t)])
-    }
-
-    pub fn subr(
-        kind: SubrKind,
-        non_default_params: Vec<ParamTy>,
-        default_params: Vec<ParamTy>,
-        return_t: Type,
-    ) -> Self {
-        Self::Subr(SubrType::new(
-            kind,
-            non_default_params,
-            default_params,
-            return_t,
-        ))
-    }
-
-    pub fn func(
-        non_default_params: Vec<ParamTy>,
-        default_params: Vec<ParamTy>,
-        return_t: Type,
-    ) -> Self {
-        Self::Subr(SubrType::new(
-            SubrKind::Func,
-            non_default_params,
-            default_params,
-            return_t,
-        ))
-    }
-
-    pub fn func1(param_t: Type, return_t: Type) -> Self {
-        Self::func(vec![ParamTy::anonymous(param_t)], vec![], return_t)
-    }
-
-    pub fn kind1(param: Type) -> Self {
-        Self::func1(param, Type::Type)
-    }
-
-    pub fn func2(l: Type, r: Type, return_t: Type) -> Self {
-        Self::func(
-            vec![ParamTy::anonymous(l), ParamTy::anonymous(r)],
-            vec![],
-            return_t,
-        )
-    }
-
-    pub fn bin_op(l: Type, r: Type, return_t: Type) -> Self {
-        Self::nd_func(
-            vec![
-                ParamTy::named(Str::ever("lhs"), l.clone()),
-                ParamTy::named(Str::ever("rhs"), r.clone()),
-            ],
-            return_t,
-        )
-    }
-
-    pub fn anon_param_func(
-        non_default_params: Vec<Type>,
-        default_params: Vec<Type>,
-        return_t: Type,
-    ) -> Self {
-        let non_default_params = non_default_params
-            .into_iter()
-            .map(ParamTy::anonymous)
-            .collect();
-        let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
-        Self::func(non_default_params, default_params, return_t)
-    }
-
-    pub fn proc(
-        non_default_params: Vec<ParamTy>,
-        default_params: Vec<ParamTy>,
-        return_t: Type,
-    ) -> Self {
-        Self::Subr(SubrType::new(
-            SubrKind::Proc,
-            non_default_params,
-            default_params,
-            return_t,
-        ))
-    }
-
-    pub fn proc1(param_t: Type, return_t: Type) -> Self {
-        Self::proc(vec![ParamTy::anonymous(param_t)], vec![], return_t)
-    }
-
-    pub fn proc2(l: Type, r: Type, return_t: Type) -> Self {
-        Self::proc(
-            vec![ParamTy::anonymous(l), ParamTy::anonymous(r)],
-            vec![],
-            return_t,
-        )
-    }
-
-    pub fn anon_param_proc(
-        non_default_params: Vec<Type>,
-        default_params: Vec<Type>,
-        return_t: Type,
-    ) -> Self {
-        let non_default_params = non_default_params
-            .into_iter()
-            .map(ParamTy::anonymous)
-            .collect();
-        let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
-        Self::proc(non_default_params, default_params, return_t)
-    }
-
-    pub fn fn_met(
-        self_t: Type,
-        non_default_params: Vec<ParamTy>,
-        default_params: Vec<ParamTy>,
-        return_t: Type,
-    ) -> Self {
-        Self::Subr(SubrType::new(
-            SubrKind::FuncMethod(Box::new(self_t)),
-            non_default_params,
-            default_params,
-            return_t,
-        ))
-    }
-
-    pub fn fn0_met(self_t: Type, return_t: Type) -> Self {
-        Self::fn_met(self_t, vec![], vec![], return_t)
-    }
-
-    pub fn fn1_met(self_t: Type, input_t: Type, return_t: Type) -> Self {
-        Self::fn_met(self_t, vec![ParamTy::anonymous(input_t)], vec![], return_t)
-    }
-
-    pub fn anon_param_fn_met(
-        self_t: Type,
-        non_default_params: Vec<Type>,
-        default_params: Vec<Type>,
-        return_t: Type,
-    ) -> Self {
-        let non_default_params = non_default_params
-            .into_iter()
-            .map(ParamTy::anonymous)
-            .collect();
-        let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
-        Self::fn_met(self_t, non_default_params, default_params, return_t)
-    }
-
-    pub fn pr_met(
-        self_before: Type,
-        self_after: Option<Type>,
-        non_default_params: Vec<ParamTy>,
-        default_params: Vec<ParamTy>,
-        return_t: Type,
-    ) -> Self {
-        Self::Subr(SubrType::new(
-            SubrKind::pr_met(self_before, self_after),
-            non_default_params,
-            default_params,
-            return_t,
-        ))
-    }
-
-    pub fn pr0_met(self_before: Type, self_after: Option<Type>, return_t: Type) -> Self {
-        Self::pr_met(self_before, self_after, vec![], vec![], return_t)
-    }
-
-    pub fn pr1_met(
-        self_before: Type,
-        self_after: Option<Type>,
-        input_t: Type,
-        return_t: Type,
-    ) -> Self {
-        Self::pr_met(
-            self_before,
-            self_after,
-            vec![ParamTy::anonymous(input_t)],
-            vec![],
-            return_t,
-        )
-    }
-
-    pub fn anon_param_pr_met(
-        self_before: Type,
-        self_after: Option<Type>,
-        non_default_params: Vec<Type>,
-        default_params: Vec<Type>,
-        return_t: Type,
-    ) -> Self {
-        let non_default_params = non_default_params
-            .into_iter()
-            .map(ParamTy::anonymous)
-            .collect();
-        let default_params = default_params.into_iter().map(ParamTy::anonymous).collect();
-        Self::pr_met(
-            self_before,
-            self_after,
-            non_default_params,
-            default_params,
-            return_t,
-        )
-    }
-
-    /// function type with non-default parameters
-    #[inline]
-    pub fn nd_func(params: Vec<ParamTy>, ret: Type) -> Type {
-        Type::func(params, vec![], ret)
-    }
-
-    #[inline]
-    pub fn nd_proc(params: Vec<ParamTy>, ret: Type) -> Type {
-        Type::proc(params, vec![], ret)
-    }
-
-    pub fn callable(param_ts: Vec<Type>, return_t: Type) -> Self {
-        Self::Callable {
-            param_ts,
-            return_t: Box::new(return_t),
-        }
-    }
-
-    #[inline]
-    pub fn mono<S: Into<Str>>(name: S) -> Self {
-        Self::Mono(name.into())
-    }
-
-    #[inline]
-    pub fn mono_q<S: Into<Str>>(name: S) -> Self {
-        Self::MonoQVar(name.into())
-    }
-
-    #[inline]
-    pub fn poly<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Self {
-        Self::Poly {
-            name: name.into(),
-            params,
-        }
-    }
-
-    #[inline]
-    pub fn poly_q<S: Into<Str>>(name: S, params: Vec<TyParam>) -> Self {
-        Self::PolyQVar {
-            name: name.into(),
-            params,
-        }
-    }
-
-    #[inline]
-    pub fn mono_proj<S: Into<Str>>(lhs: Type, rhs: S) -> Self {
-        Self::MonoProj {
-            lhs: Box::new(lhs),
-            rhs: rhs.into(),
-        }
-    }
-
-    /// ```rust
-    /// {I: Int | I >= 0}
-    /// => Refinement{
-    ///     layout: TyParam::MonoQ "I",
-    ///     bounds: [TyBound::Instance("I", "Int")],
-    ///     preds: [Predicate::GreaterEqual("I", 0)]
-    /// }
-    /// ```
-    #[inline]
-    pub fn refinement(var: Str, t: Type, preds: Set<Predicate>) -> Self {
-        Self::Refinement(RefinementType::new(var, t, preds))
-    }
-
-    /// quantified((T -> T), T: Type) => |T: Type| T -> T
-    pub fn quantified(unbound_t: Type, bounds: Set<TyBound>) -> Self {
-        Self::Quantified(QuantifiedType::new(unbound_t, bounds))
-    }
-
-    pub fn and(lhs: Self, rhs: Self) -> Self {
-        Self::And(Box::new(lhs), Box::new(rhs))
-    }
-
-    pub fn or(lhs: Self, rhs: Self) -> Self {
-        Self::Or(Box::new(lhs), Box::new(rhs))
-    }
-
-    pub fn not(lhs: Self, rhs: Self) -> Self {
-        Self::Not(Box::new(lhs), Box::new(rhs))
-    }
-
     pub fn is_mono_q(&self) -> bool {
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_mono_q(),
@@ -1840,12 +1449,12 @@ impl Type {
     /// 本来は型環境が必要
     pub fn mutate(self) -> Self {
         match self {
-            Self::Int => Self::mono("Int!"),
-            Self::Nat => Self::mono("Nat!"),
-            Self::Ratio => Self::mono("Ratio!"),
-            Self::Float => Self::mono("Float!"),
-            Self::Bool => Self::mono("Bool!"),
-            Self::Str => Self::mono("Str!"),
+            Self::Int => mono("Int!"),
+            Self::Nat => mono("Nat!"),
+            Self::Ratio => mono("Ratio!"),
+            Self::Float => mono("Float!"),
+            Self::Bool => mono("Bool!"),
+            Self::Str => mono("Str!"),
             _ => todo!(),
         }
     }
@@ -1958,7 +1567,7 @@ impl Type {
             (Self::Record(l), Self::Record(r)) => Self::Record(l.clone().concat(r.clone())),
             (t, Self::Obj) | (Self::Obj, t) => t.clone(),
             (_, Self::Never) | (Self::Never, _) => Self::Never,
-            (l, r) => Self::and(l.clone(), r.clone()),
+            (l, r) => and(l.clone(), r.clone()),
         }
     }
 
diff --git a/compiler/erg_type/typaram.rs b/compiler/erg_type/typaram.rs
index e1c8bdc0..7d7d28f4 100644
--- a/compiler/erg_type/typaram.rs
+++ b/compiler/erg_type/typaram.rs
@@ -4,6 +4,7 @@ use std::ops::{Add, Div, Mul, Neg, Range, RangeInclusive, Sub};
 
 use erg_common::traits::LimitedDisplay;
 
+use crate::constructors::{int_interval, mono};
 use crate::free::{Constraint, FreeKind, FreeTyParam, HasLevel, Level};
 use crate::value::ValueObj;
 use crate::Str;
@@ -346,13 +347,13 @@ impl Neg for TyParam {
 
 impl From<Range<TyParam>> for TyParam {
     fn from(r: Range<TyParam>) -> Self {
-        Self::t(Type::int_interval(IntervalOp::RightOpen, r.start, r.end))
+        Self::t(int_interval(IntervalOp::RightOpen, r.start, r.end))
     }
 }
 
 impl From<Range<&TyParam>> for TyParam {
     fn from(r: Range<&TyParam>) -> Self {
-        Self::t(Type::int_interval(
+        Self::t(int_interval(
             IntervalOp::RightOpen,
             r.start.clone(),
             r.end.clone(),
@@ -363,18 +364,14 @@ impl From<Range<&TyParam>> for TyParam {
 impl From<RangeInclusive<TyParam>> for TyParam {
     fn from(r: RangeInclusive<TyParam>) -> Self {
         let (start, end) = r.into_inner();
-        Self::t(Type::int_interval(IntervalOp::Closed, start, end))
+        Self::t(int_interval(IntervalOp::Closed, start, end))
     }
 }
 
 impl From<RangeInclusive<&TyParam>> for TyParam {
     fn from(r: RangeInclusive<&TyParam>) -> Self {
         let (start, end) = r.into_inner();
-        Self::t(Type::int_interval(
-            IntervalOp::Closed,
-            start.clone(),
-            end.clone(),
-        ))
+        Self::t(int_interval(IntervalOp::Closed, start.clone(), end.clone()))
     }
 }
 
@@ -452,7 +449,7 @@ impl TyParam {
 
     // TODO: polymorphic type
     pub fn array_t(t: Str, len: TyParam) -> Self {
-        Self::Array(vec![TyParam::t(Type::mono(t)), len])
+        Self::Array(vec![TyParam::t(mono(t)), len])
     }
 
     pub fn free_var(level: usize, t: Type) -> Self {
diff --git a/compiler/erg_type/value.rs b/compiler/erg_type/value.rs
index 1a2bf918..77661993 100644
--- a/compiler/erg_type/value.rs
+++ b/compiler/erg_type/value.rs
@@ -17,6 +17,7 @@ use erg_common::{fmt_iter, impl_display_from_debug, switch_lang};
 use erg_common::{RcArray, Str};
 
 use crate::codeobj::CodeObj;
+use crate::constructors::{array, mono, poly, refinement};
 use crate::free::fresh_varname;
 use crate::typaram::TyParam;
 use crate::{ConstSubr, HasType, Predicate, Type};
@@ -247,7 +248,7 @@ impl HasType for ValueObj {
     fn t(&self) -> Type {
         let name = Str::from(fresh_varname());
         let pred = Predicate::eq(name.clone(), TyParam::Value(self.clone()));
-        Type::refinement(name, self.class(), set! {pred})
+        refinement(name, self.class(), set! {pred})
     }
     fn signature_t(&self) -> Option<&Type> {
         None
@@ -353,7 +354,7 @@ impl ValueObj {
             Self::Str(_) => Type::Str,
             Self::Bool(_) => Type::Bool,
             // TODO:
-            Self::Array(arr) => Type::array(
+            Self::Array(arr) => array(
                 arr.iter().next().unwrap().class(),
                 TyParam::value(arr.len()),
             ),
@@ -370,12 +371,12 @@ impl ValueObj {
             Self::Inf => Type::Inf,
             Self::NegInf => Type::NegInf,
             Self::Mut(m) => match &*m.borrow() {
-                Self::Int(_) => Type::mono("Int!"),
-                Self::Nat(_) => Type::mono("Nat!"),
-                Self::Float(_) => Type::mono("Float!"),
-                Self::Str(_) => Type::mono("Str!"),
-                Self::Bool(_) => Type::mono("Bool!"),
-                Self::Array(arr) => Type::poly(
+                Self::Int(_) => mono("Int!"),
+                Self::Nat(_) => mono("Nat!"),
+                Self::Float(_) => mono("Float!"),
+                Self::Str(_) => mono("Str!"),
+                Self::Bool(_) => mono("Bool!"),
+                Self::Array(arr) => poly(
                     "Array!",
                     vec![
                         TyParam::t(arr.iter().next().unwrap().class()),