diff --git a/compiler/erg_compiler/context/compare.rs b/compiler/erg_compiler/context/compare.rs
index af5707e1..3f56e264 100644
--- a/compiler/erg_compiler/context/compare.rs
+++ b/compiler/erg_compiler/context/compare.rs
@@ -20,7 +20,7 @@ use Type::*;
 
 use crate::context::cache::{SubtypePair, GLOBAL_TYPE_CACHE};
 use crate::context::eval::SubstContext;
-use crate::context::instantiate::TyVarContext;
+use crate::context::instantiate::TyVarInstContext;
 use crate::context::{Context, TraitInstance, Variance};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -619,8 +619,8 @@ impl Context {
             }
             (Quantified(l), Quantified(r)) => {
                 // REVIEW: maybe this should be `unreachable`
-                let l_tv_ctx = TyVarContext::new(self.level, l.bounds.clone(), self);
-                let r_tv_ctx = TyVarContext::new(self.level, r.bounds.clone(), self);
+                let l_tv_ctx = TyVarInstContext::new(self.level, l.bounds.clone(), self);
+                let r_tv_ctx = TyVarInstContext::new(self.level, r.bounds.clone(), self);
                 let l_callable = self
                     .instantiate_t(
                         l.unbound_callable.as_ref().clone(),
@@ -639,7 +639,7 @@ impl Context {
             }
             (Quantified(q), r) => {
                 // REVIEW: maybe this should be `unreachable`
-                let tmp_tv_ctx = TyVarContext::new(self.level, q.bounds.clone(), self);
+                let tmp_tv_ctx = TyVarInstContext::new(self.level, q.bounds.clone(), self);
                 let q_callable = self
                     .instantiate_t(
                         q.unbound_callable.as_ref().clone(),
diff --git a/compiler/erg_compiler/context/eval.rs b/compiler/erg_compiler/context/eval.rs
index 349bab76..7fff63a7 100644
--- a/compiler/erg_compiler/context/eval.rs
+++ b/compiler/erg_compiler/context/eval.rs
@@ -24,7 +24,7 @@ use crate::ty::typaram::{OpKind, TyParam};
 use crate::ty::value::ValueObj;
 use crate::ty::{ConstSubr, HasType, Predicate, SubrKind, TyBound, Type, UserConstSubr, ValueArgs};
 
-use crate::context::instantiate::TyVarContext;
+use crate::context::instantiate::TyVarInstContext;
 use crate::context::{ClassDefType, Context, ContextKind, RegistrationMode};
 use crate::error::{EvalError, EvalErrors, EvalResult, SingleEvalResult, TyCheckResult};
 
@@ -172,7 +172,7 @@ impl<'c> SubstContext<'c> {
     }
 
     pub fn substitute(&self, quant_t: Type) -> TyCheckResult<Type> {
-        let tv_ctx = TyVarContext::new(self.ctx.level, self.bounds.clone(), self.ctx);
+        let tv_ctx = TyVarInstContext::new(self.ctx.level, self.bounds.clone(), self.ctx);
         let inst = self.ctx.instantiate_t(quant_t, &tv_ctx, self.loc)?;
         for param in inst.typarams() {
             self.substitute_tp(&param)?;
@@ -425,7 +425,7 @@ impl Context {
                 Signature::Subr(subr) => {
                     let bounds =
                         self.instantiate_ty_bounds(&subr.bounds, RegistrationMode::Normal)?;
-                    Some(TyVarContext::new(self.level, bounds, self))
+                    Some(TyVarInstContext::new(self.level, bounds, self))
                 }
                 Signature::Var(_) => None,
             };
@@ -507,7 +507,7 @@ impl Context {
     /// FIXME: grow
     fn eval_const_lambda(&self, lambda: &Lambda) -> EvalResult<ValueObj> {
         let bounds = self.instantiate_ty_bounds(&lambda.sig.bounds, RegistrationMode::Normal)?;
-        let tv_ctx = TyVarContext::new(self.level, bounds, self);
+        let tv_ctx = TyVarInstContext::new(self.level, bounds, self);
         let mut non_default_params = Vec::with_capacity(lambda.sig.params.non_defaults.len());
         for sig in lambda.sig.params.non_defaults.iter() {
             let pt =
diff --git a/compiler/erg_compiler/context/inquire.rs b/compiler/erg_compiler/context/inquire.rs
index 48a5f785..380e5195 100644
--- a/compiler/erg_compiler/context/inquire.rs
+++ b/compiler/erg_compiler/context/inquire.rs
@@ -1397,6 +1397,11 @@ impl Context {
         Some(vec![ctx].into_iter().chain(sups))
     }
 
+    pub(crate) fn _get_super_traits(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
+        self.get_nominal_type_ctx(typ)
+            .map(|ctx| ctx.super_traits.clone().into_iter())
+    }
+
     /// if `typ` is a refinement type, include the base type (refine.t)
     pub(crate) fn get_super_classes(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
         self.get_nominal_type_ctx(typ).map(|ctx| {
diff --git a/compiler/erg_compiler/context/instantiate.rs b/compiler/erg_compiler/context/instantiate.rs
index ff395c20..e1229522 100644
--- a/compiler/erg_compiler/context/instantiate.rs
+++ b/compiler/erg_compiler/context/instantiate.rs
@@ -33,23 +33,23 @@ use RegistrationMode::*;
 /// Context for instantiating a quantified type
 /// 量化型をインスタンス化するための文脈
 #[derive(Debug, Clone)]
-pub struct TyVarContext {
+pub struct TyVarInstContext {
     level: usize,
     pub(crate) tyvar_instances: Dict<Str, Type>,
     pub(crate) typaram_instances: Dict<Str, TyParam>,
 }
 
-impl fmt::Display for TyVarContext {
+impl fmt::Display for TyVarInstContext {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         write!(
             f,
-            "TyVarContext {{ tyvar_instances: {}, typaram_instances: {} }}",
+            "TyVarInstContext {{ tyvar_instances: {}, typaram_instances: {} }}",
             self.tyvar_instances, self.typaram_instances,
         )
     }
 }
 
-impl TyVarContext {
+impl TyVarInstContext {
     pub fn new(level: usize, bounds: Set<TyBound>, ctx: &Context) -> Self {
         let mut self_ = Self {
             level,
@@ -509,7 +509,7 @@ impl Context {
             .ok()
             .map(|t| enum_unwrap!(t, Type::Subr));
         let bounds = self.instantiate_ty_bounds(&sig.bounds, PreRegister)?;
-        let tv_ctx = TyVarContext::new(self.level, bounds, self);
+        let tv_ctx = TyVarInstContext::new(self.level, bounds, self);
         let mut non_defaults = vec![];
         for (n, p) in sig.params.non_defaults.iter().enumerate() {
             let opt_decl_t = opt_decl_sig_t
@@ -558,7 +558,7 @@ impl Context {
         &self,
         sig: &ParamSignature,
         opt_decl_t: Option<&ParamTy>,
-        tmp_tv_ctx: Option<&TyVarContext>,
+        tmp_tv_ctx: Option<&TyVarInstContext>,
         mode: RegistrationMode,
     ) -> TyCheckResult<Type> {
         let spec_t = if let Some(spec_with_op) = &sig.t_spec {
@@ -595,7 +595,7 @@ impl Context {
         &self,
         sig: &ParamSignature,
         opt_decl_t: Option<&ParamTy>,
-        tmp_tv_ctx: Option<&TyVarContext>,
+        tmp_tv_ctx: Option<&TyVarInstContext>,
         mode: RegistrationMode,
     ) -> TyCheckResult<ParamTy> {
         let t = self.instantiate_param_sig_t(sig, opt_decl_t, tmp_tv_ctx, mode)?;
@@ -618,7 +618,7 @@ impl Context {
         &self,
         predecl: &PreDeclTypeSpec,
         opt_decl_t: Option<&ParamTy>,
-        tmp_tv_ctx: Option<&TyVarContext>,
+        tmp_tv_ctx: Option<&TyVarInstContext>,
     ) -> TyCheckResult<Type> {
         match predecl {
             ast::PreDeclTypeSpec::Simple(simple) => {
@@ -632,7 +632,7 @@ impl Context {
         &self,
         simple: &SimpleTypeSpec,
         opt_decl_t: Option<&ParamTy>,
-        tmp_tv_ctx: Option<&TyVarContext>,
+        tmp_tv_ctx: Option<&TyVarInstContext>,
     ) -> TyCheckResult<Type> {
         match &simple.name.inspect()[..] {
             "_" | "Obj" => Ok(Type::Obj),
@@ -740,7 +740,7 @@ impl Context {
         &self,
         p: &ParamTySpec,
         opt_decl_t: Option<&ParamTy>,
-        tmp_tv_ctx: Option<&TyVarContext>,
+        tmp_tv_ctx: Option<&TyVarInstContext>,
         mode: RegistrationMode,
     ) -> TyCheckResult<ParamTy> {
         let t = self.instantiate_typespec(&p.ty, opt_decl_t, tmp_tv_ctx, mode)?;
@@ -754,7 +754,7 @@ impl Context {
         &self,
         spec: &TypeSpec,
         opt_decl_t: Option<&ParamTy>,
-        tmp_tv_ctx: Option<&TyVarContext>,
+        tmp_tv_ctx: Option<&TyVarInstContext>,
         mode: RegistrationMode,
     ) -> TyCheckResult<Type> {
         match spec {
@@ -897,7 +897,7 @@ impl Context {
     fn instantiate_tp(
         &self,
         quantified: TyParam,
-        tmp_tv_ctx: &TyVarContext,
+        tmp_tv_ctx: &TyVarInstContext,
         loc: Location,
     ) -> TyCheckResult<TyParam> {
         match quantified {
@@ -950,7 +950,7 @@ impl Context {
                 // K('U) -> K(?U)
                 else {
                     let ctx = self.get_nominal_type_ctx(&t).unwrap();
-                    let tv_ctx = TyVarContext::new(self.level, ctx.bounds(), self);
+                    let tv_ctx = TyVarInstContext::new(self.level, ctx.bounds(), self);
                     let t = self.instantiate_t(*t, &tv_ctx, loc)?;
                     Ok(TyParam::t(t))
                 }
@@ -970,7 +970,7 @@ impl Context {
     pub(crate) fn instantiate_t(
         &self,
         unbound: Type,
-        tmp_tv_ctx: &TyVarContext,
+        tmp_tv_ctx: &TyVarInstContext,
         loc: Location,
     ) -> TyCheckResult<Type> {
         match unbound {
@@ -1121,7 +1121,7 @@ impl Context {
     pub(crate) fn instantiate(&self, quantified: Type, callee: &hir::Expr) -> TyCheckResult<Type> {
         match quantified {
             Quantified(quant) => {
-                let tmp_tv_ctx = TyVarContext::new(self.level, quant.bounds, self);
+                let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self);
                 let t = self.instantiate_t(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?;
                 match &t {
                     Type::Subr(subr) => {
@@ -1141,7 +1141,7 @@ impl Context {
             // HACK: {op: |T|(T -> T) | op == F} => ?T -> ?T
             Refinement(refine) if refine.t.is_quantified() => {
                 let quant = enum_unwrap!(*refine.t, Type::Quantified);
-                let tmp_tv_ctx = TyVarContext::new(self.level, quant.bounds, self);
+                let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self);
                 let t = self.instantiate_t(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?;
                 match &t {
                     Type::Subr(subr) => {
diff --git a/compiler/erg_compiler/context/mod.rs b/compiler/erg_compiler/context/mod.rs
index b275a0d1..15c8d2e3 100644
--- a/compiler/erg_compiler/context/mod.rs
+++ b/compiler/erg_compiler/context/mod.rs
@@ -39,7 +39,7 @@ use ast::{DefId, VarName};
 use erg_parser::ast;
 use erg_parser::token::Token;
 
-use crate::context::instantiate::{ConstTemplate, TyVarContext};
+use crate::context::instantiate::{ConstTemplate, TyVarInstContext};
 use crate::error::{SingleTyCheckResult, TyCheckError, TyCheckErrors, TyCheckResult};
 use crate::mod_cache::SharedModuleCache;
 use crate::varinfo::{Mutability, ParamIdx, VarInfo, VarKind};
@@ -380,7 +380,7 @@ pub struct Context {
     pub(crate) patches: Dict<VarName, Context>,
     pub(crate) mod_cache: Option<SharedModuleCache>,
     pub(crate) py_mod_cache: Option<SharedModuleCache>,
-    pub(crate) tv_ctx: Option<TyVarContext>,
+    pub(crate) tv_ctx: Option<TyVarInstContext>,
     pub(crate) level: usize,
 }
 
@@ -840,7 +840,7 @@ impl Context {
         name: &str,
         kind: ContextKind,
         vis: Visibility,
-        tv_ctx: Option<TyVarContext>,
+        tv_ctx: Option<TyVarInstContext>,
     ) -> TyCheckResult<()> {
         let name = if vis.is_public() {
             format!("{parent}.{name}", parent = self.name)
diff --git a/compiler/erg_compiler/context/register.rs b/compiler/erg_compiler/context/register.rs
index e5b310f6..70a1648c 100644
--- a/compiler/erg_compiler/context/register.rs
+++ b/compiler/erg_compiler/context/register.rs
@@ -34,7 +34,7 @@ use Mutability::*;
 use RegistrationMode::*;
 use Visibility::*;
 
-use super::instantiate::TyVarContext;
+use super::instantiate::TyVarInstContext;
 use super::OperationKind;
 
 impl Context {
@@ -517,7 +517,7 @@ impl Context {
             ast::Signature::Subr(sig) => {
                 if sig.is_const() {
                     let bounds = self.instantiate_ty_bounds(&sig.bounds, PreRegister)?;
-                    let tv_ctx = TyVarContext::new(self.level, bounds, self);
+                    let tv_ctx = TyVarInstContext::new(self.level, bounds, self);
                     let vis = def.sig.vis();
                     self.grow(__name__, ContextKind::Proc, vis, Some(tv_ctx))?;
                     let (obj, const_t) = match self.eval_const_block(&def.body.block) {
diff --git a/compiler/erg_compiler/context/test.rs b/compiler/erg_compiler/context/test.rs
index c17ab9a0..282e2002 100644
--- a/compiler/erg_compiler/context/test.rs
+++ b/compiler/erg_compiler/context/test.rs
@@ -9,7 +9,7 @@ use crate::ty::typaram::TyParam;
 use crate::ty::{Predicate, TyBound, Type};
 use Type::*;
 
-use crate::context::instantiate::TyVarContext;
+use crate::context::instantiate::TyVarInstContext;
 use crate::context::Context;
 
 impl Context {
@@ -54,7 +54,7 @@ impl Context {
         let unbound_t = func1(t.clone(), t);
         let quantified = quant(unbound_t.clone(), bounds.clone());
         println!("quantified      : {quantified}");
-        let tv_ctx = TyVarContext::new(self.level + 1, bounds, self);
+        let tv_ctx = TyVarInstContext::new(self.level + 1, bounds, self);
         println!("tv_ctx: {tv_ctx}");
         let inst = self
             .instantiate_t(unbound_t, &tv_ctx, Location::Unknown)
diff --git a/compiler/erg_compiler/context/tyvar.rs b/compiler/erg_compiler/context/tyvar.rs
index dada9394..7b454431 100644
--- a/compiler/erg_compiler/context/tyvar.rs
+++ b/compiler/erg_compiler/context/tyvar.rs
@@ -15,8 +15,7 @@ use crate::ty::value::ValueObj;
 use crate::ty::{HasType, Predicate, TyBound, Type};
 
 use crate::context::eval::SubstContext;
-use crate::context::{Context, TyVarContext, Variance};
-// use crate::context::instantiate::TyVarContext;
+use crate::context::{Context, TyVarInstContext, Variance};
 use crate::error::{SingleTyCheckResult, TyCheckError, TyCheckErrors, TyCheckResult};
 use crate::hir;
 
@@ -81,7 +80,7 @@ impl Context {
             // NOTE: `?T(<: TraitX) -> Int` should be `TraitX -> Int`
             // However, the current Erg cannot handle existential types, so it quantifies anyway
             /*if !maybe_unbound_t.return_t().unwrap().has_qvar() {
-                let mut tv_ctx = TyVarContext::new(self.level, bounds.clone(), self);
+                let mut tv_ctx = TyVarInstContext::new(self.level, bounds.clone(), self);
                 let inst = Self::instantiate_t(
                     maybe_unbound_t,
                     &mut tv_ctx,
@@ -532,7 +531,7 @@ impl Context {
         for inst in self.get_trait_impls(trait_).into_iter() {
             let sub_type = if inst.sub_type.has_qvar() {
                 let sub_ctx = self.get_nominal_type_ctx(&inst.sub_type).unwrap();
-                let tv_ctx = TyVarContext::new(self.level, sub_ctx.bounds(), self);
+                let tv_ctx = TyVarInstContext::new(self.level, sub_ctx.bounds(), self);
                 self.instantiate_t(inst.sub_type, &tv_ctx, Location::Unknown)
                     .unwrap()
             } else {
@@ -540,7 +539,7 @@ impl Context {
             };
             let sup_trait = if inst.sup_trait.has_qvar() {
                 let sup_ctx = self.get_nominal_type_ctx(&inst.sup_trait).unwrap();
-                let tv_ctx = TyVarContext::new(self.level, sup_ctx.bounds(), self);
+                let tv_ctx = TyVarInstContext::new(self.level, sup_ctx.bounds(), self);
                 self.instantiate_t(inst.sup_trait, &tv_ctx, Location::Unknown)
                     .unwrap()
             } else {
@@ -1470,7 +1469,24 @@ impl Context {
                     params: rps,
                 },
             ) => {
+                // e.g. Set(?T) <: Eq(Set(?T))
                 if ln != rn {
+                    if let Some(sub_ctx) = self.get_nominal_type_ctx(maybe_sub) {
+                        let subst_ctx = SubstContext::new(maybe_sub, self, loc);
+                        for sup_trait in sub_ctx.super_traits.iter() {
+                            let sup_trait = if sup_trait.has_qvar() {
+                                subst_ctx.substitute(sup_trait.clone())?
+                            } else {
+                                sup_trait.clone()
+                            };
+                            if self.supertype_of(maybe_sup, &sup_trait) {
+                                for (l_maybe_sub, r_maybe_sup) in sup_trait.typarams().iter().zip(rps.iter()) {
+                                    self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
+                                }
+                                return Ok(());
+                            }
+                        }
+                    }
                     return Err(TyCheckErrors::from(TyCheckError::unification_error(
                         self.cfg.input.clone(),
                         line!() as usize,
diff --git a/compiler/erg_compiler/lower.rs b/compiler/erg_compiler/lower.rs
index 673cf9f2..a216d8e9 100644
--- a/compiler/erg_compiler/lower.rs
+++ b/compiler/erg_compiler/lower.rs
@@ -26,7 +26,7 @@ use crate::ty::typaram::TyParam;
 use crate::ty::value::{GenTypeObj, TypeKind, TypeObj, ValueObj};
 use crate::ty::{HasType, ParamTy, Type};
 
-use crate::context::instantiate::TyVarContext;
+use crate::context::instantiate::TyVarInstContext;
 use crate::context::{
     ClassDefType, Context, ContextKind, OperationKind, RegistrationMode, TraitInstance,
 };
@@ -785,7 +785,7 @@ impl ASTLowerer {
         let bounds = self
             .ctx
             .instantiate_ty_bounds(&lambda.sig.bounds, RegistrationMode::Normal)?;
-        let tv_ctx = TyVarContext::new(self.ctx.level, bounds, &self.ctx);
+        let tv_ctx = TyVarInstContext::new(self.ctx.level, bounds, &self.ctx);
         self.ctx.grow(&name, kind, Private, Some(tv_ctx))?;
         if let Err(errs) = self.ctx.assign_params(&lambda.sig.params, None) {
             self.errs.extend(errs.into_iter());
@@ -869,7 +869,7 @@ impl ASTLowerer {
                 let bounds = self
                     .ctx
                     .instantiate_ty_bounds(&sig.bounds, RegistrationMode::Normal)?;
-                let tv_ctx = TyVarContext::new(self.ctx.level, bounds, &self.ctx);
+                let tv_ctx = TyVarInstContext::new(self.ctx.level, bounds, &self.ctx);
                 self.ctx.grow(&name, kind, vis, Some(tv_ctx))?;
                 self.lower_subr_def(sig, def.body)
             }