diff --git a/compiler/erg_compiler/context/initialize/mod.rs b/compiler/erg_compiler/context/initialize/mod.rs
index a4bf9734..d0bcfb45 100644
--- a/compiler/erg_compiler/context/initialize/mod.rs
+++ b/compiler/erg_compiler/context/initialize/mod.rs
@@ -269,7 +269,7 @@ impl Context {
         let op_t = fn1_met(
             mono_q("Self"),
             mono_q("R"),
-            option(builtin_mono("Ordering")),
+            or(builtin_mono("Ordering"), NoneType),
         );
         let op_t = quant(
             op_t,
@@ -534,7 +534,7 @@ impl Context {
         let mut int_partial_ord = Self::builtin_methods("PartialOrd", 2);
         int_partial_ord.register_builtin_impl(
             "__partial_cmp__",
-            fn1_met(Int, Int, option(builtin_mono("Ordering"))),
+            fn1_met(Int, Int, or(builtin_mono("Ordering"), NoneType)),
             Const,
             Public,
         );
@@ -1575,7 +1575,7 @@ impl Context {
             vec![param_t("err_message", Str)],
             NoneType,
         );
-        let t_classof = nd_func(vec![param_t("old", Obj)], None, option(Class));
+        let t_classof = nd_func(vec![param_t("old", Obj)], None, Class);
         let t_compile = nd_func(vec![param_t("src", Str)], None, Code);
         let t_cond = nd_func(
             vec![
@@ -1596,7 +1596,7 @@ impl Context {
             ],
             None,
             vec![param_t("else", nd_func(vec![], None, mono_q("T")))],
-            option(mono_q("T")),
+            or(mono_q("T"), NoneType),
         );
         let t_if = quant(t_if, set! {static_instance("T", Type)});
         let t_import = nd_func(
@@ -1724,7 +1724,7 @@ impl Context {
             ],
             None,
             vec![param_t("else", nd_proc(vec![], None, mono_q("T")))],
-            option(mono_q("T")),
+            or(mono_q("T"), NoneType),
         );
         let t_if = quant(t_if, set! {static_instance("T", Type)});
         let t_for = nd_proc(
diff --git a/compiler/erg_compiler/context/initialize/py_mods/socket.rs b/compiler/erg_compiler/context/initialize/py_mods/socket.rs
index 175cf165..9839f70e 100644
--- a/compiler/erg_compiler/context/initialize/py_mods/socket.rs
+++ b/compiler/erg_compiler/context/initialize/py_mods/socket.rs
@@ -1,6 +1,6 @@
 use erg_common::vis::Visibility;
 
-use erg_type::constructors::{builtin_mono, func, option, param_t};
+use erg_type::constructors::{builtin_mono, func, or, param_t};
 use erg_type::Type;
 use Type::*;
 
@@ -24,7 +24,7 @@ impl Context {
                     param_t("family", Int),
                     param_t("type", Int),
                     param_t("proto", Int),
-                    param_t("fileno", option(Int)),
+                    param_t("fileno", or(Int, NoneType)),
                 ],
                 builtin_mono("Socket!"),
             ),
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index 86fe41f5..dea6e54a 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -454,6 +454,22 @@ impl Context {
                 // TODO: deref_predicate
                 Ok(refinement(refine.var, t, refine.preds))
             }
+            Type::And(l, r) => {
+                let l = self.deref_tyvar(*l, variance, loc)?;
+                let r = self.deref_tyvar(*r, variance, loc)?;
+                Ok(self.intersection(&l, &r))
+            }
+            Type::Or(l, r) => {
+                let l = self.deref_tyvar(*l, variance, loc)?;
+                let r = self.deref_tyvar(*r, variance, loc)?;
+                Ok(self.union(&l, &r))
+            }
+            Type::Not(l, r) => {
+                let l = self.deref_tyvar(*l, variance, loc)?;
+                let r = self.deref_tyvar(*r, variance, loc)?;
+                // TODO: complement
+                Ok(not(l, r))
+            }
             t => Ok(t),
         }
     }
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index eac7cd6e..f5cfff10 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -1301,7 +1301,10 @@ impl ASTLowerer {
         let hir = HIR::new(ast.name, module);
         log!(info "HIR (not resolved, current errs: {}):\n{hir}", self.errs.len());
         let hir = match self.ctx.resolve(hir) {
-            Ok(hir) => hir,
+            Ok(hir) => {
+                log!(info "HIR (resolved):\n{hir}");
+                hir
+            }
             Err((hir, errs)) => {
                 self.errs.extend(errs.into_iter());
                 log!(err "the resolving process has failed. errs:  {}", self.errs.len());
@@ -1315,7 +1318,6 @@ impl ASTLowerer {
             }
         }
         if self.errs.is_empty() {
-            log!(info "HIR:\n{hir}");
             log!(info "the AST lowering process has completed.");
             Ok((hir, LowerWarnings::from(self.warns.take_all())))
         } else {
diff --git a/compiler/erg_type/constructors.rs b/compiler/erg_type/constructors.rs
index 8a7edd93..8dcbee02 100644
--- a/compiler/erg_type/constructors.rs
+++ b/compiler/erg_type/constructors.rs
@@ -127,13 +127,13 @@ pub fn ref_mut(before: Type, after: Option<Type>) -> Type {
     }
 }
 
-pub fn option(t: Type) -> Type {
+/*pub fn option(t: Type) -> Type {
     builtin_poly("Option", vec![TyParam::t(t)])
 }
 
 pub fn option_mut(t: Type) -> Type {
     builtin_poly("Option!", vec![TyParam::t(t)])
-}
+}*/
 
 pub fn subr_t(
     kind: SubrKind,