diff --git a/src/ast/descriptor.rs b/src/ast/descriptor.rs
index 509f370..082f3dc 100644
--- a/src/ast/descriptor.rs
+++ b/src/ast/descriptor.rs
@@ -228,6 +228,7 @@ impl PropertyType {
     /// Open types allow extra keys; closed types must match exactly.
     pub fn is_subtype(t1: &PropertyType, t2: &PropertyType) -> bool {
         match (t1, t2) {
+            (PropertyType::Zero, _) => true,
             (PropertyType::Open(_), PropertyType::Open(_)) => {
                 // Check common keys
                 t1.keys()
diff --git a/src/ast/label.rs b/src/ast/label.rs
index a319d55..06aa185 100644
--- a/src/ast/label.rs
+++ b/src/ast/label.rs
@@ -50,10 +50,12 @@ impl LabelType {
             (LabelType::And(left, right), _) => {
                 LabelType::is_subtype(left, l2) || LabelType::is_subtype(right, l2)
             }
+            (LabelType::Or(left, right), _) => {
+                LabelType::is_subtype(left, l2) && LabelType::is_subtype(right, l2)
+            }
             (_, LabelType::Or(left, right)) => {
                 LabelType::is_subtype(l1, left) || LabelType::is_subtype(l1, right)
             }
-            _ => false,
         }
     }
 }
diff --git a/src/ast/types.rs b/src/ast/types.rs
index 2147cc8..b8e7b26 100644
--- a/src/ast/types.rs
+++ b/src/ast/types.rs
@@ -36,34 +36,19 @@ impl SimpleType {
                 let meet2 = SimpleType::meet(a, t2);
                 SimpleType::union(&meet1, &meet2)
             }
-            _ if SimpleType::gradual_eq(a, b) => a.clone(),
+            _ if a == b => a.clone(),
             _ => SimpleType::Zero, // Incompatible types
         }
     }
 
-    /// Returns true if t1 and t2 are considered equal under the gradual type system.
-    /// StarType is treated as equal to anything.
-    pub fn gradual_eq(t1: &SimpleType, t2: &SimpleType) -> bool {
-        match (t1, t2) {
-            (SimpleType::Star, _) | (_, SimpleType::Star) => true,
-            (SimpleType::Union(t1a, t1b), _) => {
-                SimpleType::gradual_eq(t1a, t2) || SimpleType::gradual_eq(t1b, t2)
-            }
-            (_, SimpleType::Union(t2a, t2b)) => {
-                SimpleType::gradual_eq(t1, t2a) || SimpleType::gradual_eq(t1, t2b)
-            }
-            _ => t1 == t2,
-        }
-    }
-
     /// Returns true if t1 is a (gradual) subtype of t2.
     /// Used in type tests and type refinements.
     pub fn is_subtype(t1: &SimpleType, t2: &SimpleType) -> bool {
         match (t1, t2) {
             (SimpleType::Star, _) | (_, SimpleType::Star) => true,
-            (_, SimpleType::Zero) => true,
+            (SimpleType::Zero, _) => true,
             (SimpleType::Union(t1a, t1b), _) => {
-                SimpleType::is_subtype(t1a, t2) && SimpleType::is_subtype(t1b, t2)
+                SimpleType::is_subtype(t1a, t2) || SimpleType::is_subtype(t1b, t2)
             }
             (_, SimpleType::Union(t2a, t2b)) => {
                 SimpleType::is_subtype(t1, t2a) || SimpleType::is_subtype(t1, t2b)
diff --git a/src/typechecker/checker.rs b/src/typechecker/checker.rs
index 2902027..da0cffa 100644
--- a/src/typechecker/checker.rs
+++ b/src/typechecker/checker.rs
@@ -243,8 +243,8 @@ impl Typechecker {
 
                 match Self::binop_delta(op) {
                     Some((expected_t1, expected_t2, result_t)) => {
-                        if SimpleType::gradual_eq(&t1, &expected_t1)
-                            && SimpleType::gradual_eq(&t2, &expected_t2)
+                        if SimpleType::meet(&t1, &expected_t1) != SimpleType::Zero
+                            && SimpleType::meet(&t2, &expected_t2) != SimpleType::Zero
                         {
                             result_t
                         } else {
@@ -270,7 +270,7 @@ impl Typechecker {
 
                 match Self::unop_delta(op) {
                     Some((expected_t, result_t)) => {
-                        if SimpleType::gradual_eq(&t, &expected_t) {
+                        if SimpleType::meet(&t, &expected_t) != SimpleType::Zero {
                             result_t
                         } else {
                             self.warnings
diff --git a/src/typechecker/variable_type.rs b/src/typechecker/variable_type.rs
index 9bab96c..80b8033 100644
--- a/src/typechecker/variable_type.rs
+++ b/src/typechecker/variable_type.rs
@@ -216,6 +216,7 @@ impl VariableType {
     /// General meet operator (greatest lower bound).
     pub fn meet(a: &VariableType, b: &VariableType) -> Result<VariableType, String> {
         match (a, b) {
+            (VariableType::Zero, _) | (_, VariableType::Zero) => Ok(VariableType::Zero),
             (VariableType::List(inner_a), VariableType::List(inner_b)) => Ok(VariableType::List(
                 Box::new(VariableType::meet(inner_a, inner_b)?),
             )),
@@ -227,14 +228,13 @@ impl VariableType {
                 let r1 = VariableType::meet(t1, b);
                 let r2 = VariableType::meet(t2, b);
                 match (r1, r2) {
-                    (Ok(v1), Ok(v2)) => Ok(VariableType::Union(Box::new(v1), Box::new(v2))),
+                    (Ok(v1), Ok(v2)) => Ok(VariableType::join(v1, v2)),
                     (Ok(v1), Err(_)) => Ok(v1),
                     (Err(_), Ok(v2)) => Ok(v2),
                     (Err(e1), Err(_)) => Err(e1),
                 }
             }
             (_, VariableType::Union(_, _)) => VariableType::meet(b, a),
-            (VariableType::Zero, _) | (_, VariableType::Zero) => Ok(VariableType::Zero),
             _ => Err(format!(
                 "Meet undefined between variable types {:?} and {:?}",
                 a, b
@@ -263,6 +263,7 @@ impl VariableType {
     /// Checks if t1 is a subtype of t2.
     pub fn is_subtype(t1: &VariableType, t2: &VariableType) -> bool {
         match (t1, t2) {
+            (VariableType::Zero, _) => true,
             (VariableType::Node(n1), VariableType::Node(n2)) => {
                 DescriptorType::is_subtype(&n1.0, &n2.0)
             }