From e2b8b36b7a06e6d6534719f10c98a9133c42446a Mon Sep 17 00:00:00 2001
From: Douglas Creager <dcreager@dcreager.net>
Date: Mon, 4 Aug 2025 17:22:09 -0400
Subject: [PATCH] constraints and sets and sets

---
 crates/ty_python_semantic/src/types.rs        | 16 ++++
 .../src/types/unification.rs                  | 80 +++++++++++++++++++
 2 files changed, 96 insertions(+)
 create mode 100644 crates/ty_python_semantic/src/types/unification.rs

diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index c171013e20..526b0c0990 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -90,6 +90,7 @@ mod string_annotation;
 mod subclass_of;
 mod tuple;
 mod type_ordering;
+mod unification;
 mod unpacker;
 mod visitor;
 
@@ -8670,6 +8671,21 @@ pub(super) fn walk_intersection_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>
 }
 
 impl<'db> IntersectionType<'db> {
+    /// Create an intersection from a list of elements
+    /// (which may be eagerly simplified into a different variant of [`Type`] altogether).
+    pub fn from_elements<I, T>(db: &'db dyn Db, elements: I) -> Type<'db>
+    where
+        I: IntoIterator<Item = T>,
+        T: Into<Type<'db>>,
+    {
+        elements
+            .into_iter()
+            .fold(IntersectionBuilder::new(db), |builder, element| {
+                builder.add_positive(element.into())
+            })
+            .build()
+    }
+
     /// Return a new `IntersectionType` instance with the positive and negative types sorted
     /// according to a canonical ordering, and other normalizations applied to each element as applicable.
     ///
diff --git a/crates/ty_python_semantic/src/types/unification.rs b/crates/ty_python_semantic/src/types/unification.rs
new file mode 100644
index 0000000000..7c566f500d
--- /dev/null
+++ b/crates/ty_python_semantic/src/types/unification.rs
@@ -0,0 +1,80 @@
+//! Implements the _tallying_ algorithm from [[POPL2015][]], which finds the unification of a
+//! set of subtyping constraints.
+//!
+//! [POPL2015]: https://doi.org/10.1145/2676726.2676991
+
+// XXX
+#![allow(dead_code)]
+
+use crate::Db;
+use crate::types::{IntersectionType, Type, TypeVarInstance, UnionType};
+
+/// A constraint that the type `s` must be a subtype of the type `t`. Tallying will find all
+/// substitutions of any type variables in `s` and `t` that ensure that this subtyping holds.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub(crate) struct Constraint<'db> {
+    pub(crate) lower: Type<'db>,
+    pub(crate) typevar: TypeVarInstance<'db>,
+    pub(crate) upper: Type<'db>,
+}
+
+impl<'db> Constraint<'db> {
+    /// Returns whether this constraint subsumes `other` — if it constrains the same typevar and
+    /// has tighter bounds.
+    fn subsumes(self, db: &'db dyn Db, other: Self) -> bool {
+        self.typevar == other.typevar
+            && other.lower.is_assignable_to(db, self.lower)
+            && self.upper.is_assignable_to(db, other.upper)
+    }
+
+    /// Merges another constraint into this one. Panics if the two constraints have different
+    /// typevars.
+    fn merge(&mut self, db: &'db dyn Db, other: Self) {
+        debug_assert!(self.typevar == other.typevar);
+        self.lower = UnionType::from_elements(db, [self.lower, other.lower]);
+        self.upper = IntersectionType::from_elements(db, [self.upper, other.upper]);
+    }
+}
+
+/// A set of merged constraints. We guarantee that no constraint in the set subsumes another, and
+/// that no two constraints in the set have the same typevar.
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub(crate) struct ConstraintSet<'db> {
+    constraints: Vec<Constraint<'db>>,
+}
+
+impl<'db> ConstraintSet<'db> {
+    /// Returns an empty constraint set
+    fn empty() -> Self {
+        Self {
+            constraints: vec![],
+        }
+    }
+
+    /// Adds a new constraint to this set, ensuring that no constraint in the set subsumes another,
+    /// and that no two constraints in the set have the same typevar.
+    fn add(&mut self, db: &'db dyn Db, constraint: Constraint<'db>) {
+        for existing in &mut self.constraints {
+            if constraint.typevar == existing.typevar {
+                existing.merge(db, constraint);
+                return;
+            }
+        }
+        self.constraints.push(constraint);
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub(crate) struct ConstraintSetSet<'db>(Vec<ConstraintSet<'db>>);
+
+impl<'db> ConstraintSetSet<'db> {
+    /// Returns the set of constraint sets that is unsolvable.
+    pub(crate) fn none() -> Self {
+        Self(vec![])
+    }
+
+    /// Returns the set of constraints set that is always satisfied.
+    pub(crate) fn always() -> Self {
+        Self(vec![ConstraintSet::empty()])
+    }
+}