diff --git a/crates/erg_compiler/context/compare.rs b/crates/erg_compiler/context/compare.rs
index 50670c7ee..e8428c4ce 100644
--- a/crates/erg_compiler/context/compare.rs
+++ b/crates/erg_compiler/context/compare.rs
@@ -605,12 +605,10 @@ impl Context {
             (Structural(_), Refinement(refine)) => self.supertype_of(lhs, &refine.t),
             // Int :> {I: Int | ...} == true
             // Int :> {I: Str| ...} == false
-            // Eq({1, 2}) :> {1, 2} (= {I: Int | I == 1 or I == 2})
-            // => Eq(Int) :> Eq({1, 2}) :> {1, 2}
-            // => true
             // Bool :> {1} == true
             // Bool :> {2} == false
             // [2, 3]: {A: Array(Nat) | A.prod() == 6}
+            // Array({1, 2}, _) :> {[3, 4]} == false
             (l, Refinement(r)) => {
                 // Type / {S: Set(Str) | S == {"a", "b"}}
                 if let Pred::Equal { rhs, .. } = r.pred.as_ref() {
@@ -623,9 +621,11 @@ impl Context {
                 } else if self.subtype_of(l, &r.t) {
                     return false;
                 }
-                let l = l.derefine();
-                if self.supertype_of(&l, &r.t) {
-                    return true;
+                if r.t.is_monomorphic() {
+                    let l = l.derefine();
+                    if self.supertype_of(&l, &r.t) {
+                        return true;
+                    }
                 }
                 let l = Type::Refinement(l.clone().into_refinement());
                 self.structural_supertype_of(&l, rhs)
@@ -1141,6 +1141,8 @@ impl Context {
     /// union(Nat, Int) == Int
     /// union(Int, Str) == Int or Str
     /// union(?T(<: Str), ?U(<: Int)) == ?T or ?U
+    /// union(Array(Int, 2), Array(Str, 2)) == Array(Int or Str, 2)
+    /// union(Array(Int, 2), Array(Str, 3)) == Array(Int, 2) or Array(Int, 3)
     /// ```
     pub(crate) fn union(&self, lhs: &Type, rhs: &Type) -> Type {
         if lhs == rhs {
@@ -1151,6 +1153,16 @@ impl Context {
                 self.union(&fv.crack(), other)
             }
             (Refinement(l), Refinement(r)) => Type::Refinement(self.union_refinement(l, r)),
+            (Refinement(refine), other) | (other, Refinement(refine))
+                if other.qual_name() == refine.t.qual_name() =>
+            {
+                let union = self.union(other, &refine.t);
+                if union.is_union_type() {
+                    self.simple_union(lhs, rhs)
+                } else {
+                    union
+                }
+            }
             (Structural(l), Structural(r)) => self.union(l, r).structuralize(),
             // Int..Obj or Nat..Obj ==> Int..Obj
             // Str..Obj or Int..Obj ==> Str..Obj or Int..Obj
@@ -1192,6 +1204,11 @@ impl Context {
         }
     }
 
+    /// ```erg
+    /// union_tp(1, 1) => Some(1)
+    /// union_tp(1, 2) => None
+    /// union_tp(?N, 2) => Some(2) # REVIEW:
+    /// ```
     pub(crate) fn union_tp(&self, lhs: &TyParam, rhs: &TyParam) -> Option<TyParam> {
         match (lhs, rhs) {
             (TyParam::Value(ValueObj::Type(l)), TyParam::Value(ValueObj::Type(r))) => {
@@ -1215,6 +1232,17 @@ impl Context {
                 }
                 Some(TyParam::Array(tps))
             }
+            (fv @ TyParam::FreeVar(f), other) | (other, fv @ TyParam::FreeVar(f))
+                if f.is_unbound() =>
+            {
+                let fv_t = self.get_tp_t(fv).ok()?.derefine();
+                let other_t = self.get_tp_t(other).ok()?.derefine();
+                if self.same_type_of(&fv_t, &other_t) {
+                    Some(other.clone())
+                } else {
+                    None
+                }
+            }
             (_, _) => {
                 if self.eq_tp(lhs, rhs) {
                     Some(lhs.clone())
diff --git a/crates/erg_compiler/context/eval.rs b/crates/erg_compiler/context/eval.rs
index d1ae5f7b1..8600bb339 100644
--- a/crates/erg_compiler/context/eval.rs
+++ b/crates/erg_compiler/context/eval.rs
@@ -95,8 +95,8 @@ fn op_to_name(op: OpKind) -> &'static str {
 
 #[derive(Debug, Default)]
 pub struct UndoableLinkedList {
-    tys: Shared<Set<Type>>,
-    tps: Shared<Set<TyParam>>,
+    tys: Shared<Vec<Type>>, // not Set
+    tps: Shared<Vec<TyParam>>,
 }
 
 impl Drop for UndoableLinkedList {
@@ -113,17 +113,17 @@ impl Drop for UndoableLinkedList {
 impl UndoableLinkedList {
     pub fn new() -> Self {
         Self {
-            tys: Shared::new(set! {}),
-            tps: Shared::new(set! {}),
+            tys: Shared::new(vec![]),
+            tps: Shared::new(vec![]),
         }
     }
 
     pub fn push_t(&self, t: &Type) {
-        self.tys.borrow_mut().insert(t.clone());
+        self.tys.borrow_mut().push(t.clone());
     }
 
     pub fn push_tp(&self, tp: &TyParam) {
-        self.tps.borrow_mut().insert(tp.clone());
+        self.tps.borrow_mut().push(tp.clone());
     }
 }
 
@@ -152,7 +152,6 @@ impl<'c> Substituter<'c> {
     /// qt: Iterable(T), st: Array(Int, 3)
     /// qt: Array(T, N), st: Array!(Int, 3) # TODO
     /// ```
-    /// use `undo_substitute_typarams` after executing this method
     pub(crate) fn substitute_typarams(
         ctx: &'c Context,
         qt: &Type,