diff --git a/cedar-policy-core/src/batched_evaluator.rs b/cedar-policy-core/src/batched_evaluator.rs
index 6c2c88927..9645d1e2b 100644
--- a/cedar-policy-core/src/batched_evaluator.rs
+++ b/cedar-policy-core/src/batched_evaluator.rs
@@ -96,6 +96,7 @@ pub fn is_authorized_batched(
     let initial_evaluator = Evaluator {
         request: &request,
         entities: &entities,
+        schema,
         extensions: Extensions::all_available(),
     };
     let mut residuals: Vec<ResidualPolicy> = policy_residual_map(&request, ps, schema)?
@@ -145,6 +146,7 @@ pub fn is_authorized_batched(
         let evaluator = Evaluator {
             request: &request,
             entities: &entities,
+            schema,
             extensions: Extensions::all_available(),
         };
 
diff --git a/cedar-policy-core/src/tpe.rs b/cedar-policy-core/src/tpe.rs
index 7b42fc969..12e671ff2 100644
--- a/cedar-policy-core/src/tpe.rs
+++ b/cedar-policy-core/src/tpe.rs
@@ -89,6 +89,7 @@ pub fn is_authorized<'a>(
     let evaluator = Evaluator {
         request,
         entities,
+        schema,
         extensions: Extensions::all_available(),
     };
     let residuals = policy_residual_map(request, ps, schema)?
diff --git a/cedar-policy-core/src/tpe/evaluator.rs b/cedar-policy-core/src/tpe/evaluator.rs
index 5fa627a8b..f55ab2989 100644
--- a/cedar-policy-core/src/tpe/evaluator.rs
+++ b/cedar-policy-core/src/tpe/evaluator.rs
@@ -24,6 +24,8 @@ use crate::{
     extensions::Extensions,
 };
 
+use crate::validator::types::Type;
+use crate::validator::ValidatorSchema;
 use crate::{
     tpe::entities::PartialEntities,
     tpe::request::PartialRequest,
@@ -35,6 +37,7 @@ use crate::{
 pub struct Evaluator<'e> {
     pub(crate) request: &'e PartialRequest,
     pub(crate) entities: &'e PartialEntities,
+    pub(crate) schema: &'e ValidatorSchema,
     pub(crate) extensions: &'e Extensions<'e>,
 }
 
@@ -209,19 +212,20 @@ impl Evaluator<'_> {
             }
             ResidualKind::Is { expr, entity_type } => {
                 let expr = self.interpret(expr);
+                if let Some(expr_ety) = expr
+                    .ty()
+                    .as_entity_lub()
+                    .and_then(|ety| ety.get_single_entity())
+                {
+                    if !expr.can_error_assuming_well_formed() {
+                        return mk_concrete((expr_ety == entity_type).into());
+                    }
+                }
                 match &expr {
                     Residual::Concrete { value, .. } => match value.get_as_entity() {
                         Ok(uid) => mk_concrete((uid.entity_type() == entity_type).into()),
                         Err(_) => mk_error(), // <error> is <entity_type> => <error>
                     },
-                    Residual::Partial {
-                        kind: ResidualKind::Var(Var::Principal),
-                        ..
-                    } => mk_concrete((entity_type == self.request.principal_type()).into()),
-                    Residual::Partial {
-                        kind: ResidualKind::Var(Var::Resource),
-                        ..
-                    } => mk_concrete((entity_type == self.request.resource_type()).into()),
                     Residual::Partial { .. } => mk_residual(ResidualKind::Is {
                         expr: Arc::new(expr),
                         entity_type: entity_type.clone(),
@@ -246,6 +250,26 @@ impl Evaluator<'_> {
             ResidualKind::BinaryApp { op, arg1, arg2 } => {
                 let arg1 = self.interpret(arg1);
                 let arg2 = self.interpret(arg2);
+                let must_be_false = match op {
+                    BinaryOp::HasTag => !Type::may_have_tags(self.schema, arg1.ty()),
+                    BinaryOp::Eq => Type::are_types_disjoint(arg1.ty(), arg2.ty()),
+                    BinaryOp::In => {
+                        match (arg1.ty().as_entity_lub(), arg2.ty().as_set_or_entity_lub()) {
+                            // `in` must be false if `arg1` cannot have an ancestor with type of `arg2`
+                            (Some(lhs_lub), Some(rhs_lub)) => {
+                                !self.schema.any_descendent_of(lhs_lub, rhs_lub)
+                            }
+                            _ => false,
+                        }
+                    }
+                    _ => false,
+                };
+                if must_be_false
+                    && !arg1.can_error_assuming_well_formed()
+                    && !arg2.can_error_assuming_well_formed()
+                {
+                    return mk_concrete(false.into());
+                }
                 let binapp_residual = |arg1, arg2| {
                     mk_residual(ResidualKind::BinaryApp {
                         op: *op,
@@ -391,6 +415,14 @@ impl Evaluator<'_> {
             }
             ResidualKind::HasAttr { expr, attr } => {
                 let expr = self.interpret(expr);
+                if !Type::may_have_attr(self.schema, expr.ty(), attr)
+                    && !expr.can_error_assuming_well_formed()
+                {
+                    // The residual can't error and cannot have `attr`, so `has` is alway `false`.
+                    // We can't have an analogous reduction to `true` because the concrete semantics
+                    // for `has` is `false` when the entity isn't present.
+                    return mk_concrete(false.into());
+                }
                 match &expr {
                     Residual::Concrete { value, .. } => {
                         if let Ok(r) = value.get_as_record() {
@@ -670,6 +702,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -713,6 +746,7 @@ mod tests {
             )
             .unwrap(),
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -736,6 +770,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -808,6 +843,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -880,6 +916,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -891,9 +928,13 @@ mod tests {
             interpret_typed_str_to_str("if false then resource else 2"),
             @"2"
         );
+        assert_snapshot!(
+            interpret_typed_str_to_str(r#"if (resource == Document::"C") then Document::"A" else Document::"B""#),
+            @r#"if (resource == Document::"C") then Document::"A" else Document::"B""#
+        );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"if (resource == User::"alice") then Document::"A" else Document::"B""#),
-            @r#"if (resource == User::"alice") then Document::"B" else Document::"B""#
+            @r#"Document::"B""#
         );
         assert_snapshot!(
             interpret_typed_str_to_str(&r#"if (9223372036854775807 * 2) == 0 then resource else Document::"A""#),
@@ -933,6 +974,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -961,6 +1003,14 @@ mod tests {
             interpret_typed_str_to_str("principal.baz is Document"),
             @"(principal.baz) is Document"
         );
+        assert_snapshot!(
+            interpret_typed_str_to_str(r#"(if principal == User::"alice" then User::"bob" else User::"jane") is Document"#),
+            @"false"
+        );
+        assert_snapshot!(
+            interpret_typed_str_to_str(r#"(if principal == User::"alice" then User::"bob" else User::"jane") is User"#),
+            @"true"
+        );
         assert_snapshot!(
             interpret_typed_str_to_str("User::\"alice\" is User"),
             @"true"
@@ -991,6 +1041,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1033,6 +1084,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1087,6 +1139,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1141,6 +1194,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1208,6 +1262,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1268,6 +1323,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1285,7 +1341,7 @@ mod tests {
         );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"principal has other"#),
-            @"principal has other"
+            @"false"
         );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"E::"f" has s"#),
@@ -1345,6 +1401,7 @@ mod tests {
             request: &req,
             entities: &entities,
             extensions: Extensions::all_available(),
+            schema: &schema,
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
         assert_snapshot!(
@@ -1378,11 +1435,58 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_schema_informed_has_reduction() {
+        let schema = parse_schema(
+            r#"
+            entity User;
+            entity Doc { b: Bool };
+            action get appliesTo { principal: User, resource: Doc, context: {} };
+            "#,
+        );
+        let req = PartialRequest::new(
+            parse_partial_euid("User"),
+            r#"Action::"get""#.parse().unwrap(),
+            parse_partial_euid(r#"Doc"#),
+            None,
+            &schema,
+        )
+        .unwrap();
+        let entities = PartialEntities::from_json_value(
+            serde_json::json!([ { "uid": { "type": "Doc", "id": "mine" } },]),
+            &schema,
+        )
+        .unwrap();
+        let eval = Evaluator {
+            request: &req,
+            entities: &entities,
+            schema: &schema,
+            extensions: Extensions::all_available(),
+        };
+        let interp = |e| interpret_typed_str_to_str(&eval, e, &schema);
+
+        assert_snapshot!(interp(r#"principal has a"#), @"false");
+        assert_snapshot!(interp(r#"principal has a && principal.a"#), @"false");
+        assert_snapshot!(interp(r#"context has a"#), @"false");
+        assert_snapshot!(interp(r#"{} has a"#), @"false");
+        assert_snapshot!(interp(r#"{a: principal} has b"#), @"false");
+        assert_snapshot!(interp(r#"(if principal == User::"alice" then {a: 1} else {a: 2}) has b"#), @"false");
+        assert_snapshot!(interp(r#"(if principal == User::"alice" then User::"bob" else User::"jane") has a"#), @"false");
+
+        // The schema guarantees that `resource` has the attribute, but the entity might not exist,
+        // so we can't reduce to true.
+        assert_snapshot!(interp(r#"resource has b"#), @"resource has b");
+        // Here the partial entities tell us that `Doc::"mine"` does exist, so
+        // we could reduce to `true` in a reasonable future extension.
+        assert_snapshot!(interp(r#"Doc::"mine" has b"#), @r#"Doc::"mine" has b"#);
+    }
+
     #[test]
     fn test_set() {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
 
@@ -1410,6 +1514,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -1466,6 +1571,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1571,6 +1677,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1608,6 +1715,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -1641,6 +1749,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1658,7 +1767,7 @@ mod tests {
         );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"principal == E::"""#),
-            @r#"principal == E::"""#
+            @"false"
         );
 
         assert_snapshot!(
@@ -1690,6 +1799,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1719,6 +1829,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &PartialEntities::new(),
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1768,6 +1879,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1847,6 +1959,44 @@ mod tests {
         );
     }
 
+    #[test]
+    fn test_binary_app_in_unrelated_types() {
+        let schema = parse_schema(
+            r#"
+            entity Org;
+            entity User in Org;
+            entity Unrelated;
+            action get appliesTo {
+                principal: User,
+                resource: Unrelated,
+            };"#,
+        );
+        let req = PartialRequest::new(
+            parse_partial_euid("User"),
+            r#"Action::"get""#.parse().unwrap(),
+            parse_partial_euid("Unrelated"),
+            None,
+            &schema,
+        )
+        .unwrap();
+        let eval = Evaluator {
+            request: &req,
+            entities: &PartialEntities::new(),
+            schema: &schema,
+            extensions: Extensions::all_available(),
+        };
+        let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
+
+        assert_snapshot!(
+            interpret_typed_str_to_str(r#"principal in resource"#),
+            @"false"
+        );
+        assert_snapshot!(
+            interpret_typed_str_to_str(r#"principal in [resource]"#),
+            @"false"
+        );
+    }
+
     #[test]
     fn test_binary_app_in_empty_set() {
         let schema = parse_schema(
@@ -1878,6 +2028,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1937,6 +2088,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1971,6 +2123,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -1999,23 +2152,23 @@ mod tests {
             @r#"(User::"undefined".hasTag("s")) && ((User::"undefined".getTag("s")) == "bar")"#
         );
 
-        // `E` entities can't have tags, but `hasTag` is still well-typed. These could all reduce to
-        // `false`, but only the explicit empty tag case does atm.
+        // `E` declares no tags in the schema, so `hasTag` on any `E` operand reduces to `false`
+        // regardless of whether concrete tag data is present.
         assert_snapshot!(
             interpret_typed_str_to_str(r#"E::"empty_tags".hasTag("s") && E::"empty_tags".getTag("s") == "bar" "#),
             @"false"
         );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"E::"none_tags".hasTag("s") && E::"none_tags".getTag("s") == "bar" "#),
-            @r#"E::"none_tags".hasTag("s")"#
+            @"false"
         );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"E::"undefined_tags".hasTag("s") && E::"undefined_tags".getTag("s") == "bar" "#),
-            @r#"E::"undefined_tags".hasTag("s")"#
+            @"false"
         );
         assert_snapshot!(
             interpret_typed_str_to_str(r#"E::"undefined".hasTag("s") && E::"undefined".getTag("s") == "bar" "#),
-            @r#"E::"undefined".hasTag("s")"#
+            @"false"
         );
 
         // Residual on the left prevents eliminating `error()` expression even through it's unreachable
@@ -2031,6 +2184,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -2080,6 +2234,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -2123,6 +2278,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema);
@@ -2151,6 +2307,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -2177,6 +2334,7 @@ mod tests {
         let eval = Evaluator {
             request: &concrete_user_req(),
             entities: &PartialEntities::new(),
+            schema: &schema(),
             extensions: Extensions::all_available(),
         };
         let interpret_typed_str_to_str = |e| interpret_typed_str_to_str(&eval, e, &schema());
@@ -2241,6 +2399,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
 
@@ -2284,6 +2443,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
 
@@ -2327,6 +2487,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
 
@@ -2372,6 +2533,7 @@ mod tests {
         let eval = Evaluator {
             request: &req,
             entities: &entities,
+            schema: &schema,
             extensions: Extensions::all_available(),
         };
 
diff --git a/cedar-policy-core/src/validator/schema.rs b/cedar-policy-core/src/validator/schema.rs
index f6ec3d076..62ff372bc 100644
--- a/cedar-policy-core/src/validator/schema.rs
+++ b/cedar-policy-core/src/validator/schema.rs
@@ -42,7 +42,10 @@ use crate::validator::{
     cedar_schema::SchemaWarning,
     json_schema,
     partition_nonempty::PartitionNonEmpty,
-    types::{Attributes, EntityKind, OpenTag, RequestEnv, Type, TypeIterator, UnlinkedRequestEnv},
+    types::{
+        Attributes, EntityKind, EntityLUB, OpenTag, RequestEnv, Type, TypeIterator,
+        UnlinkedRequestEnv,
+    },
     ValidationMode,
 };
 
@@ -1051,6 +1054,37 @@ impl ValidatorSchema {
         descendants
     }
 
+    /// Checks if an action of entity type `lhs_ety` may be a descendant of an
+    /// action of entity type `rhs_ety` in the action hierarchy.
+    /// Lean counterpart: <https://github.com/cedar-policy/cedar-spec/blob/7e231a68b0e0eb1b8ce1362e81de4568671a668a/cedar-lean/Cedar/Validation/Types.lean#L202>
+    fn maybe_action_descendent_of(&self, lhs_ety: &EntityType, rhs_ety: &EntityType) -> bool {
+        self.action_ids().any(|action| {
+            action.name().entity_type() == rhs_ety
+                && action
+                    .descendants()
+                    .any(|desc| desc.entity_type() == lhs_ety)
+        })
+    }
+
+    /// Checks if `lhs_ety` may be a descendant of `rhs_ety`, either in the
+    /// entity or action hierarchy. If this function returns `false`, then
+    /// `lhs in rhs` cannot possibly evaluate to `true` for entities of these
+    /// types.
+    /// Lean counterpart: <https://github.com/cedar-policy/cedar-spec/blob/7e231a68b0e0eb1b8ce1362e81de4568671a668a/cedar-lean/Cedar/Validation/Types.lean#L205>
+    fn descendent_of(&self, lhs_ety: &EntityType, rhs_ety: &EntityType) -> bool {
+        self.get_entity_types_in(rhs_ety).contains(&lhs_ety)
+            || self.maybe_action_descendent_of(lhs_ety, rhs_ety)
+    }
+
+    /// Check if some entity type in `lhs` may be a descendant of some entity
+    /// type in `rhs`, either in the entity or action hierarchy. If this
+    /// function returns `false`, then `lhs in rhs` cannot possibly evaluate to
+    /// `true`.
+    pub(crate) fn any_descendent_of(&self, lhs: &EntityLUB, rhs: &EntityLUB) -> bool {
+        lhs.iter()
+            .any(|lhs| rhs.iter().any(|rhs| self.descendent_of(lhs, rhs)))
+    }
+
     /// Get all action entities in the schema where `action in euids` evaluates
     /// to `true`. This includes all actions which are descendants of some
     /// element of `euids`, and all elements of `euids`.
diff --git a/cedar-policy-core/src/validator/typecheck.rs b/cedar-policy-core/src/validator/typecheck.rs
index f2c6f4c01..8c9e82060 100644
--- a/cedar-policy-core/src/validator/typecheck.rs
+++ b/cedar-policy-core/src/validator/typecheck.rs
@@ -29,7 +29,7 @@ use std::sync::Arc;
 use std::{borrow::Cow, collections::HashSet};
 
 use crate::ast::UnwrapInfallible;
-use crate::validator::types::{BoolType, EntityLUB};
+use crate::validator::types::BoolType;
 use crate::validator::{
     extension_schema::ExtensionFunctionType,
     extensions::ExtensionSchemas,
@@ -1740,32 +1740,6 @@ impl<'a> SingleEnvTypechecker<'a> {
         }
     }
 
-    /// Checks if `lhs_ety` may be a descendant of `rhs_ety` in the action hierarchy.
-    /// We assume that `lhs_ety` is an action entity type, but `rhs_ety` can be any entity type.
-    /// Lean counterpart: <https://github.com/cedar-policy/cedar-spec/blob/7e231a68b0e0eb1b8ce1362e81de4568671a668a/cedar-lean/Cedar/Validation/Types.lean#L202>
-    fn check_action_in_entity_type(&self, lhs_ety: &EntityType, rhs_ety: &EntityType) -> bool {
-        lhs_ety == rhs_ety
-            || self.schema.action_ids().any(|action| {
-                action.name().entity_type() == rhs_ety
-                    && action
-                        .descendants()
-                        .any(|desc| desc.entity_type() == lhs_ety)
-            })
-    }
-
-    /// Check if an entity type in `lhs` may be a descendant of some entity type
-    /// in rhs, either in the entity or action hierarchy. If this function
-    /// returns `false`, then `lhs in rhs` cannot possibly evaluate to `true`,
-    /// meaning that the expression can have type `False`.
-    fn any_entity_type_decedent_of(&self, lhs: &EntityLUB, rhs: &EntityLUB) -> bool {
-        lhs.iter().any(|lhs| {
-            rhs.iter().any(|rhs| {
-                self.schema.get_entity_types_in(rhs).contains(&lhs)
-                    || self.check_action_in_entity_type(lhs, rhs)
-            })
-        })
-    }
-
     /// Handles typechecking of `in` expressions. This is complicated because it
     /// requires searching the schema to determine if an `in` expression
     /// consisting of variables and literals can ever be true. When we find that
@@ -1833,23 +1807,14 @@ impl<'a> SingleEnvTypechecker<'a> {
                             rhs_expr,
                         ),
                     _ => {
-                        let lhs_etys = match lhs_expr.data() {
-                            Some(Type::Entity(EntityKind::Entity(lhs_etys))) => Some(lhs_etys),
-                            _ => None,
-                        };
-                        let rhs_etys = match rhs_expr.data() {
-                            Some(Type::Entity(EntityKind::Entity(rhs_etys))) => Some(rhs_etys),
-                            Some(Type::Set {
-                                element_type: Some(element_type),
-                            }) => match element_type.as_ref() {
-                                Type::Entity(EntityKind::Entity(rhs_etys)) => Some(rhs_etys),
-                                _ => None,
-                            },
-                            _ => None,
-                        };
+                        let lhs_etys = lhs_expr.data().as_ref().and_then(Type::as_entity_lub);
+                        let rhs_etys = rhs_expr
+                            .data()
+                            .as_ref()
+                            .and_then(Type::as_set_or_entity_lub);
                         match (lhs_etys, rhs_etys) {
                             (Some(lhs_etys), Some(rhs_etys))
-                                if !self.any_entity_type_decedent_of(lhs_etys, rhs_etys) =>
+                                if !self.schema.any_descendent_of(lhs_etys, rhs_etys) =>
                             {
                                 TypecheckAnswer::success(
                                     ExprBuilder::with_data(Some(Type::Bool(BoolType::False)))
diff --git a/cedar-policy-core/src/validator/types.rs b/cedar-policy-core/src/validator/types.rs
index 8732efced..a93f09809 100644
--- a/cedar-policy-core/src/validator/types.rs
+++ b/cedar-policy-core/src/validator/types.rs
@@ -372,7 +372,7 @@ impl Type {
                     // common, are disjoint types.
                     // Entity types least-upper-bounds that have entity types in
                     // common, are not disjoint types.
-                    lub1.is_disjoint(&lub2)
+                    lub1.is_disjoint(lub2)
                 } else {
                     false // conservatively false, not promising disjointness; see notes on this function
                 }
@@ -464,6 +464,49 @@ impl Type {
         }
     }
 
+    /// Get `self` as a specific entity type (or set of types in permissive
+    /// validation). Returns `None` for non-entity types and for `AnyEntity`.
+    pub(crate) fn as_entity_lub(&self) -> Option<&EntityLUB> {
+        match &self {
+            Type::Entity(entity_kind) => entity_kind.as_entity_lub(),
+            _ => None,
+        }
+    }
+
+    /// Get `self` as a specific entity type, or, if `self` is a set, then the
+    /// element type as an entity type.  Returns `None` if `self` is neither an
+    /// entity or set of entity, and for `AnyEntity`.
+    pub(crate) fn as_set_or_entity_lub(&self) -> Option<&EntityLUB> {
+        match self {
+            Type::Entity(_) => self.as_entity_lub(),
+            Type::Set {
+                element_type: Some(element_type),
+            } => element_type.as_entity_lub(),
+            _ => None,
+        }
+    }
+
+    /// Could a value of type `ty` have any tags, according to `schema`?
+    ///
+    /// Returns `false` only when `ty` is an entity type without tags declared
+    /// in the schema.
+    #[cfg(feature = "tpe")]
+    pub(crate) fn may_have_tags(schema: &ValidatorSchema, ty: &Type) -> bool {
+        match ty {
+            Type::Entity(EntityKind::Entity(entity_lub)) => {
+                entity_lub.lub_elements.iter().any(|entity| {
+                    schema
+                        .get_entity_type(entity)
+                        .is_some_and(|entity_type| entity_type.tag_type().is_some())
+                })
+            }
+            // Non-entity types cannot have tags, but `hasTag` is only
+            // well-typed on entities, so this case is not expected. The safe
+            // behavior is to assume they might have tags.
+            _ => true,
+        }
+    }
+
     /// Is this validator type "consistent with" the given Core `SchemaType`.
     /// Meaning, is there at least some value that could have this `SchemaType` and
     /// this validator type simultaneously.
@@ -1096,10 +1139,10 @@ pub enum EntityKind {
 }
 
 impl EntityKind {
-    pub(crate) fn as_entity_lub(&self) -> Option<EntityLUB> {
+    pub(crate) fn as_entity_lub(&self) -> Option<&EntityLUB> {
         match self {
             EntityKind::AnyEntity => None,
-            EntityKind::Entity(lub) => Some(lub.clone()),
+            EntityKind::Entity(lub) => Some(lub),
         }
     }
 
diff --git a/cedar-policy/CHANGELOG.md b/cedar-policy/CHANGELOG.md
index d7acdebb1..57db289ed 100644
--- a/cedar-policy/CHANGELOG.md
+++ b/cedar-policy/CHANGELOG.md
@@ -17,6 +17,10 @@ Cedar Language Version: TBD
 ### Fixed
 - In the experimental `protobufs` feature, the `Schema::decode` function now accepts schemas that reference `Action` entity types not defined in the schema. This was previously  rejected (#2491).
 
+### Added
+
+- For the experimental `tpe` feature, TPE now reduces `has`, `hasTag`, `in` and `==` applied to non-erroring but unknown expressions when the schema provides enough information to determine the concrete value of the operation.
+
 ## [4.12.0] - 2026-07-28
 
 Cedar Language Version: 4.5