diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index c1c346ed..2e79e7b4 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -257,10 +257,6 @@ impl Context {
             self.register_cache(lhs, rhs, judge);
             return judge;
         }
-        /*if self._find_compatible_patch(lhs, rhs).is_some() {
-            self.register_cache(lhs, rhs, true);
-            return true;
-        }*/
         self.register_cache(lhs, rhs, false);
         false
     }
@@ -269,14 +265,13 @@ impl Context {
         self.nominal_supertype_of(rhs, lhs)
     }
 
-    fn _find_compatible_patch(&self, sup: &Type, sub: &Type) -> Option<Str> {
-        // let subst_ctx = SubstContext::try_new(sub, self, Location::Unknown)?;
+    fn _find_compatible_patch(&self, sup: &Type, sub: &Type) -> Option<&Context> {
         for patch in self._all_patches().into_iter() {
             if let ContextKind::GluePatch(tr_inst) = &patch.kind {
                 if self.subtype_of(sub, &tr_inst.sub_type)
                     && self.subtype_of(&tr_inst.sup_trait, sup)
                 {
-                    return Some(patch.name.clone());
+                    return Some(patch);
                 }
             }
         }
@@ -436,11 +431,14 @@ impl Context {
                 }
                 FreeKind::Unbound { constraint: _, .. }
                 | FreeKind::NamedUnbound { constraint: _, .. } => {
-                    let (sub, _sup) = rfv.get_subsup().unwrap();
-                    rfv.forced_undoable_link(lhs);
-                    let res = self.supertype_of(lhs, &sub);
-                    rfv.undo();
-                    res
+                    if let Some((sub, _sup)) = rfv.get_subsup() {
+                        rfv.forced_undoable_link(lhs);
+                        let res = self.supertype_of(lhs, &sub);
+                        rfv.undo();
+                        res
+                    } else {
+                        todo!("{lhs} / {rhs}");
+                    }
                 }
             },
             (Type::Record(lhs), Type::Record(rhs)) => {
@@ -660,53 +658,6 @@ impl Context {
         }
     }
 
-    /*fn is_super_constr(&self, constr: &Constraint, rhs: &Type) -> bool {
-        match constr {
-            // `(?T <: Int) :> Nat` can be true, `(?T <: Nat) :> Int` is false
-            // `(?T <: Eq(?T)) :> Nat` can be true, but this requires special judgment
-            // `(?T :> X) :> Y` is true
-            // `(?T :> Str) :> Int` is true (?T :> Str or Int)
-            // `(Nat <: ?T <: Ratio) :> Nat` can be true
-            Constraint::Sandwiched { sup, .. } => self.supertype_of(sup, rhs),
-            // (?v: Type, rhs): OK
-            // (?v: Nat, rhs): Something wrong
-            // Class <: Type, but Nat <!: Type (Nat: Type)
-            Constraint::TypeOf(t) => {
-                if self.supertype_of(&Type, t) {
-                    true
-                } else {
-                    panic!()
-                }
-            }
-            Constraint::Uninited => unreachable!(),
-        }
-    }
-
-    fn is_sub_constr(&self, lhs: &Type, constr: &Constraint) -> bool {
-        match constr {
-            // ?T cannot be `Never`
-            // `Nat :> (?T <: Int)` can be true
-            // `Int :> (?T <: Nat)` can be true
-            // * so sup is unrelated
-            // `Str :> (?T <: Int)` is false
-            // `Int :> (?T :> Nat)` can be true, `Nat :> (?T :> Int)` is false
-            // `Int :> (Nat <: ?T <: Ratio)` can be true, `Nat :> (Int <: ?T <: Ratio)` is false
-            //  Eq(Int) :> ?M(:> Int, <: Mul(?M) and Add(?M))
-            Constraint::Sandwiched {
-                sub,
-                sup: _,
-            } => self.supertype_of(lhs, sub),
-            Constraint::TypeOf(t) => {
-                if self.supertype_of(&Type, t) {
-                    true
-                } else {
-                    panic!()
-                }
-            }
-            Constraint::Uninited => unreachable!(),
-        }
-    }*/
-
     pub(crate) fn poly_supertype_of(
         &self,
         typ: &Type,
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index 483b6a1e..36b427ea 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -1412,8 +1412,11 @@ impl Context {
         match t {
             Type::FreeVar(fv) if fv.is_linked() => self.get_nominal_super_type_ctxs(&fv.crack()),
             Type::FreeVar(fv) => {
-                let sup = fv.get_sup().unwrap();
-                self.get_nominal_super_type_ctxs(&sup)
+                if let Some(sup) = fv.get_sup() {
+                    self.get_nominal_super_type_ctxs(&sup)
+                } else {
+                    self.get_nominal_super_type_ctxs(&Type)
+                }
             }
             Type::And(l, r) => {
                 match (
@@ -2087,6 +2090,7 @@ impl Context {
         }
     }
 
+    // TODO:
     /// Int.meta_type() == ClassType (<: Type)
     /// Show.meta_type() == TraitType (<: Type)
     /// [Int; 3].meta_type() == [ClassType; 3] (<: Type)
diff --git a/compiler/erg_compiler/context/instantiate.rs b/compiler/erg_compiler/context/instantiate.rs
index 0b30076f..2cf42ca3 100644
--- a/compiler/erg_compiler/context/instantiate.rs
+++ b/compiler/erg_compiler/context/instantiate.rs
@@ -20,6 +20,7 @@ use erg_parser::token::TokenKind;
 use erg_parser::Parser;
 
 use crate::ty::constructors::*;
+use crate::ty::free::CanbeFree;
 use crate::ty::free::{Constraint, HasLevel};
 use crate::ty::typaram::{IntervalOp, TyParam, TyParamOrdering};
 use crate::ty::value::ValueObj;
@@ -835,6 +836,30 @@ impl Context {
         for bound in bounds.iter() {
             self.instantiate_ty_bound(bound, &mut tv_cache, mode)?;
         }
+        for tv in tv_cache.tyvar_instances.values() {
+            if tv.constraint().unwrap().is_uninited() {
+                return Err(TyCheckErrors::from(TyCheckError::no_var_error(
+                    self.cfg.input.clone(),
+                    line!() as usize,
+                    bounds.loc(),
+                    self.caused_by(),
+                    &tv.local_name(),
+                    self.get_similar_name(&tv.local_name()),
+                )));
+            }
+        }
+        for tp in tv_cache.typaram_instances.values() {
+            if tp.constraint().unwrap().is_uninited() {
+                return Err(TyCheckErrors::from(TyCheckError::no_var_error(
+                    self.cfg.input.clone(),
+                    line!() as usize,
+                    bounds.loc(),
+                    self.caused_by(),
+                    &tp.to_string(),
+                    self.get_similar_name(&tp.to_string()),
+                )));
+            }
+        }
         Ok(tv_cache)
     }
 
diff --git a/compiler/erg_compiler/lib/std/semver.er b/compiler/erg_compiler/lib/std/semver.er
index efd9915c..700da5bf 100644
--- a/compiler/erg_compiler/lib/std/semver.er
+++ b/compiler/erg_compiler/lib/std/semver.er
@@ -22,4 +22,6 @@
 
 if! __name__ == "__main__", do!:
     v = .Version.new(0, 0, 1)
+    assert v.minor == 0
+    assert v.pre == None
     assert v != .Version.new(0, 0, 2)