diff --git a/src/erg_compiler/codegen.rs b/src/erg_compiler/codegen.rs
index 45710a64..d26c33fc 100644
--- a/src/erg_compiler/codegen.rs
+++ b/src/erg_compiler/codegen.rs
@@ -317,6 +317,7 @@ impl CodeGenerator {
         let name = escape_name(name);
         match self.rec_search(&name) {
             Some(st @ (StoreLoadKind::Local | StoreLoadKind::Global)) => {
+                let st = if current_is_toplevel { StoreLoadKind::Local } else { st };
                 self.mut_cur_block_codeobj().names.push(name);
                 Name::new(st, self.cur_block_codeobj().names.len() - 1)
             }
@@ -932,6 +933,13 @@ impl CodeGenerator {
             }
             Expr::BinOp(bin) => {
                 // TODO: and/orのプリミティブ命令の実装
+                // Range operators are not operators in Python
+                match &bin.op.kind {
+                    // l..<r == range(l, r)
+                    TokenKind::RightOpen => { self.emit_load_name_instr(Str::ever("range")).unwrap(); },
+                    TokenKind::LeftOpen | TokenKind::Closed | TokenKind::Open => todo!(),
+                    _ => {}
+                }
                 let type_pair = TypePair::new(bin.lhs_t(), bin.rhs_t());
                 self.codegen_expr(*bin.lhs);
                 self.codegen_expr(*bin.rhs);
@@ -950,7 +958,8 @@ impl CodeGenerator {
                     | TokenKind::NotEq
                     | TokenKind::Gre
                     | TokenKind::GreEq => COMPARE_OP,
-                    TokenKind::Closed => ERG_BINARY_RANGE,
+                    TokenKind::LeftOpen | TokenKind::RightOpen
+                    | TokenKind::Closed | TokenKind::Open => CALL_FUNCTION, // ERG_BINARY_RANGE,
                     _ => {
                         self.errs.push(CompileError::feature_error(
                             self.cfg.input.clone(),
@@ -968,11 +977,18 @@ impl CodeGenerator {
                     TokenKind::NotEq => 3,
                     TokenKind::Gre => 4,
                     TokenKind::GreEq => 5,
+                    TokenKind::LeftOpen | TokenKind::RightOpen
+                    | TokenKind::Closed | TokenKind::Open => 2,
                     _ => type_pair as u8,
                 };
                 self.write_instr(instr);
                 self.write_arg(arg);
                 self.stack_dec();
+                match &bin.op.kind {
+                    TokenKind::LeftOpen | TokenKind::RightOpen
+                    | TokenKind::Open | TokenKind::Closed => { self.stack_dec(); },
+                    _ => {}
+                }
             }
             Expr::Call(call) => {
                 // TODO: unwrap
diff --git a/src/erg_compiler/context.rs b/src/erg_compiler/context.rs
index 69987886..ebae59a0 100644
--- a/src/erg_compiler/context.rs
+++ b/src/erg_compiler/context.rs
@@ -1495,7 +1495,9 @@ impl Context {
 
     /// Assuming that `sub` is a subtype of `sup`, fill in the type variable to satisfy the assumption
     /// ```
-    /// sub_unify({I: Int | I == 0}, ?T(<: Ord)): (Ord :> ?T :> {I: Int | I == 0})
+    /// sub_unify({I: Int | I == 0}, ?T(<: Ord)): (/* OK */)
+    /// sub_unify(Int, ?T(:> Nat)): (?T :> Int)
+    /// sub_unify(Nat, ?T(:> Int)): (/* OK */)
     /// sub_unify(Nat, Add(?R, ?O)): (?R => Nat, ?O => Nat)
     /// sub_unify([?T; 0], Mutate): (/* OK */)
     /// ```
@@ -1516,9 +1518,32 @@ impl Context {
             ))
         }
         match (maybe_sub, maybe_sup) {
-            (_l, Type::FreeVar(fv)) if fv.is_unbound() => {
-                todo!()
+            (l, Type::FreeVar(fv)) if fv.is_unbound() => {
+                match &mut *fv.borrow_mut() {
+                    FreeKind::NamedUnbound{ constraint, .. }
+                    | FreeKind::Unbound{ constraint, .. } => match constraint {
+                        // sub_unify(Nat, ?T(:> Int)): (/* OK */)
+                        // sub_unify(Int, ?T(:> Nat)): (?T :> Int)
+                        Constraint::SupertypeOf(sub) if self.rec_supertype_of(l, sub) => {
+                            *constraint = Constraint::SupertypeOf(l.clone());
+                        },
+                        // sub_unify(Nat, ?T(<: Int)): (/* OK */)
+                        // sub_unify(Int, ?T(<: Nat)): Error!
+                        Constraint::SubtypeOf(sup) if self.rec_supertype_of(l, sup) => {
+                            return Err(TyCheckError::subtyping_error(l, sup, sub_loc, sup_loc, self.caused_by()))
+                        },
+                        // sub_unify(Nat, (Ratio :> ?T :> Int)): (/* OK */)
+                        // sub_unify(Int, (Ratio :> ?T :> Nat)): (Ratio :> ?T :> Int)
+                        Constraint::Sandwiched{ sub, sup } if self.rec_supertype_of(l, sub) => {
+                            *constraint = Constraint::Sandwiched{ sub: l.clone(), sup: mem::take(sup) };
+                        },
+                        _ => {}
+                    },
+                    _ => {},
+                }
+                return Ok(())
             },
+            (Type::FreeVar(fv), _r) if fv.is_linked() => todo!(),
             (l @ Refinement(_), r @ Refinement(_)) => {
                 return self.unify(l ,r, sub_loc, sup_loc)
             },
@@ -2434,13 +2459,19 @@ impl Context {
     fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
         match (l, r) {
             // |T <: Nat| <: |T <: Int|
-            // |T :> Nat| <: |T :> Int|
             // |I: Nat| <: |I: Int|
             (Constraint::SubtypeOf(lhs), Constraint::SubtypeOf(rhs))
-            | (Constraint::SupertypeOf(lhs), Constraint::SupertypeOf(rhs))
             | (Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) =>
                 self.rec_subtype_of(lhs, rhs),
+            // |Int <: T| <: |Nat <: T|
+            (Constraint::SupertypeOf(lhs), Constraint::SupertypeOf(rhs)) =>
+                self.rec_supertype_of(lhs, rhs),
             (Constraint::SubtypeOf(_), Constraint::TypeOf(Type)) => true,
+            // |Int <: T <: Ratio| <: |Nat <: T <: Complex|
+            (
+                Constraint::Sandwiched{ sub: lsub, sup: lsup },
+                Constraint::Sandwiched{ sub: rsub, sup: rsup },
+            ) => self.rec_supertype_of(lsub, rsub) && self.rec_subtype_of(lsup, rsup),
             _ => false,
         }
     }
diff --git a/src/erg_compiler/error.rs b/src/erg_compiler/error.rs
index 82c76f87..a99b80d3 100644
--- a/src/erg_compiler/error.rs
+++ b/src/erg_compiler/error.rs
@@ -392,6 +392,19 @@ passed keyword args:    {RED}{kw_args_len}{RESET}"),
         ), None), caused_by)
     }
 
+    pub fn subtyping_error(sub_t: &Type, sup_t: &Type, sub_loc: Option<Location>, sup_loc: Option<Location>, caused_by: Str) -> Self {
+        let loc = match (sub_loc, sup_loc) {
+            (Some(l), Some(r)) => Location::pair(l, r),
+            (Some(l), None) => l,
+            (None, Some(r)) => r,
+            (None, None) => Location::Unknown,
+        };
+        Self::new(ErrorCore::new(0, TypeError, loc, switch_lang!(
+            format!("subtype constraints cannot be satisfied:\nsubtype: {YELLOW}{sub_t}{RESET}\nsupertype: {YELLOW}{sup_t}{RESET}"),
+            format!("部分型制約を満たせません:\nサブタイプ: {YELLOW}{sub_t}{RESET}\nスーパータイプ: {YELLOW}{sup_t}{RESET}")
+        ), None), caused_by)
+    }
+
     pub fn pred_unification_error(lhs: &Predicate, rhs: &Predicate, caused_by: Str) -> Self {
         Self::new(ErrorCore::new(0, TypeError, Location::Unknown, switch_lang!(
             format!("predicate unification failed:\nlhs: {YELLOW}{lhs}{RESET}\nrhs: {YELLOW}{rhs}{RESET}"),