Deduplicate constraints based on superclasses

Author: purefunctor

compiler-core/checking/src/algorithm.rs

@@ -122,7 +122,7 @@ fn check_type_items<Q: ExternalQueries>(
                 type_item::check_type_item(state, context, *item)?;
 
                 build_data_constructor_types(state, context, slice::from_ref(item))?;
-                state.commit_binding_group(context);
+                state.commit_binding_group(context)?;
             }
             Scc::Mutual(items) => {
                 let with_signature = items
@@ -142,14 +142,14 @@ fn check_type_items<Q: ExternalQueries>(
                 }
 
                 build_data_constructor_types(state, context, &without_signature)?;
-                state.commit_binding_group(context);
+                state.commit_binding_group(context)?;
 
                 for item in &with_signature {
                     type_item::check_type_item(state, context, *item)?;
                 }
 
                 build_data_constructor_types(state, context, &with_signature)?;
-                state.commit_binding_group(context);
+                state.commit_binding_group(context)?;
             }
         }
     }
@@ -304,7 +304,7 @@ fn check_value_groups<Q: ExternalQueries>(
                     state.term_binding_group(context, [*item]);
                 }
                 term_item::check_value_group(state, context, *item)?;
-                state.commit_binding_group(context);
+                state.commit_binding_group(context)?;
             }
             Scc::Mutual(items) => {
                 let with_signature = items
@@ -325,12 +325,12 @@ fn check_value_groups<Q: ExternalQueries>(
                 for item in &without_signature {
                     term_item::check_value_group(state, context, *item)?;
                 }
-                state.commit_binding_group(context);
+                state.commit_binding_group(context)?;
 
                 for item in &with_signature {
                     term_item::check_value_group(state, context, *item)?;
                 }
-                state.commit_binding_group(context);
+                state.commit_binding_group(context)?;
             }
             _ => {}
         }

compiler-core/checking/src/algorithm/constraint.rs

@@ -114,13 +114,17 @@ where
     Ok(residual)
 }
 
-struct ConstraintApplication {
-    file_id: FileId,
-    item_id: TypeItemId,
-    arguments: Vec<TypeId>,
+#[derive(Clone, PartialEq, Eq, Hash)]
+pub(crate) struct ConstraintApplication {
+    pub(crate) file_id: FileId,
+    pub(crate) item_id: TypeItemId,
+    pub(crate) arguments: Vec<TypeId>,
 }
 
-fn constraint_application(state: &mut CheckState, id: TypeId) -> Option<ConstraintApplication> {
+pub(crate) fn constraint_application(
+    state: &mut CheckState,
+    id: TypeId,
+) -> Option<ConstraintApplication> {
     let mut arguments = vec![];
     let mut current_id = id;
     loop {
@@ -164,7 +168,7 @@ where
 }
 
 /// Discovers superclass constraints for a given constraint.
-fn elaborate_superclasses<Q>(
+pub(crate) fn elaborate_superclasses<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
     constraint: TypeId,
@@ -206,7 +210,7 @@ where
             bindings.insert(level, argument);
         }
 
-        for &(superclass, _kind) in &class_info.superclasses {
+        for &(superclass, _) in &class_info.superclasses {
             let localized = transfer::localize(state, context, superclass);
             let substituted = ApplyBindings::on(state, &bindings, localized);
             constraints.push(substituted);
@@ -260,7 +264,7 @@ where
     Ok(result)
 }
 
-fn get_class_info<Q>(
+pub(crate) fn get_class_info<Q>(
     state: &CheckState,
     context: &CheckContext<Q>,
     file_id: FileId,

compiler-core/checking/src/algorithm/quantify.rs

@@ -1,15 +1,20 @@
 use std::fmt::Write;
 use std::sync::Arc;
 
+use building_types::QueryResult;
 use indexmap::IndexSet;
 use itertools::Itertools;
 use petgraph::prelude::DiGraphMap;
 use petgraph::visit::{DfsPostOrder, Reversed};
 use rustc_hash::FxHashSet;
 use smol_str::SmolStrBuilder;
 
+use crate::ExternalQueries;
+use crate::algorithm::constraint::{
+    ConstraintApplication, constraint_application, elaborate_superclasses,
+};
 use crate::algorithm::fold::Zonk;
-use crate::algorithm::state::CheckState;
+use crate::algorithm::state::{CheckContext, CheckState};
 use crate::algorithm::substitute::{ShiftLevels, SubstituteUnification, UniToLevel};
 use crate::core::{ForallBinder, RowType, Type, TypeId, debruijn};
 
@@ -52,8 +57,8 @@ pub fn quantify(state: &mut CheckState, id: TypeId) -> Option<(TypeId, debruijn:
     Some((quantified, size))
 }
 
-/// Output of constraint quantification.
-pub struct QuantifyConstraints {
+/// The result of generalisation including constraints.
+pub struct QuantifiedWithConstraints {
     /// The quantified type with generalisable constraints.
     pub quantified: TypeId,
     /// The number of quantified type variables.
@@ -73,19 +78,24 @@ pub struct QuantifyConstraints {
 ///
 /// Generalisable constraints are added to the signature before generalisation.
 /// Ambiguous and unsatisfied constraints are returned for error reporting.
-pub fn quantify_with_constraints(
+pub fn quantify_with_constraints<Q>(
     state: &mut CheckState,
+    context: &CheckContext<Q>,
     type_id: TypeId,
     constraints: Vec<TypeId>,
-) -> Option<QuantifyConstraints> {
+) -> QueryResult<Option<QuantifiedWithConstraints>>
+where
+    Q: ExternalQueries,
+{
     if constraints.is_empty() {
-        let (quantified, size) = quantify(state, type_id)?;
-        return Some(QuantifyConstraints {
-            quantified,
-            size,
-            ambiguous: vec![],
-            unsatisfied: vec![],
-        });
+        let Some((quantified, size)) = quantify(state, type_id) else {
+            return Ok(None);
+        };
+
+        let quantified_with_constraints =
+            QuantifiedWithConstraints { quantified, size, ambiguous: vec![], unsatisfied: vec![] };
+
+        return Ok(Some(quantified_with_constraints));
     }
 
     let unsolved_graph = collect_unification(state, type_id);
@@ -108,14 +118,74 @@ pub fn quantify_with_constraints(
     }
 
     // Subtle: stable ordering for consistent output
-    let valid = valid.into_iter().sorted();
+    let valid = valid.into_iter().sorted().collect_vec();
+    let minimized = minimize_by_superclasses(state, context, valid)?;
 
-    let constrained_type = valid.rfold(type_id, |constrained, constraint| {
+    let constrained_type = minimized.into_iter().rfold(type_id, |constrained, constraint| {
         state.storage.intern(Type::Constrained(constraint, constrained))
     });
 
-    let (quantified, size) = quantify(state, constrained_type)?;
-    Some(QuantifyConstraints { quantified, size, ambiguous, unsatisfied })
+    let Some((quantified, size)) = quantify(state, constrained_type) else {
+        return Ok(None);
+    };
+
+    let quantified_with_constraints =
+        QuantifiedWithConstraints { quantified, size, ambiguous, unsatisfied };
+
+    Ok(Some(quantified_with_constraints))
+}
+
+/// Removes constraints that are implied by other constraints via superclass relationships.
+///
+/// For example, given constraints `[Apply f, Applicative f, Functor f]`, this function
+/// returns only `[Applicative f]` because `Applicative` implies both `Apply` and `Functor`.
+///
+/// Uses GHC's algorithm (mkMinimalBySCs): O(n × superclass_depth)
+/// 1. Build the union of all superclass constraints
+/// 2. Filter out constraints that appear in the union
+fn minimize_by_superclasses<Q>(
+    state: &mut CheckState,
+    context: &CheckContext<Q>,
+    constraints: Vec<TypeId>,
+) -> QueryResult<Vec<TypeId>>
+where
+    Q: ExternalQueries,
+{
+    if constraints.len() <= 1 {
+        return Ok(constraints);
+    }
+
+    // Collect the set of all superclasses, including transitive ones.
+    let mut superclasses = FxHashSet::default();
+    for &constraint in &constraints {
+        for application in superclass_applications(state, context, constraint)? {
+            superclasses.insert(application);
+        }
+    }
+
+    // Remove constraints found in the superclasses, keeping the most specific.
+    let minimized = constraints.into_iter().filter(|&constraint| {
+        constraint_application(state, constraint)
+            .map_or(true, |constraint| !superclasses.contains(&constraint))
+    });
+
+    Ok(minimized.collect_vec())
+}
+
+fn superclass_applications<Q>(
+    state: &mut CheckState,
+    context: &CheckContext<Q>,
+    constraint: TypeId,
+) -> QueryResult<Vec<ConstraintApplication>>
+where
+    Q: ExternalQueries,
+{
+    let mut superclasses = vec![];
+    elaborate_superclasses(state, context, constraint, &mut superclasses)?;
+    Ok(superclasses
+        .into_iter()
+        .filter_map(|constraint| constraint_application(state, constraint))
+        .collect())
 }
 
 fn generate_type_name(id: u32) -> smol_str::SmolStr {

compiler-core/checking/src/algorithm/state.rs

@@ -596,14 +596,16 @@ impl CheckState {
         constraint::solve_constraints(self, context, wanted, given)
     }
 
-    pub fn commit_binding_group<Q>(&mut self, context: &CheckContext<Q>)
+    pub fn commit_binding_group<Q>(&mut self, context: &CheckContext<Q>) -> QueryResult<()>
     where
         Q: ExternalQueries,
     {
         let mut residuals = mem::take(&mut self.binding_group.residual);
         for (item_id, type_id) in mem::take(&mut self.binding_group.terms) {
             let constraints = residuals.remove(&item_id).unwrap_or_default();
-            if let Some(result) = quantify::quantify_with_constraints(self, type_id, constraints) {
+            if let Some(result) =
+                quantify::quantify_with_constraints(self, context, type_id, constraints)?
+            {
                 self.with_error_step(ErrorStep::TermDeclaration(item_id), |this| {
                     for constraint in result.ambiguous {
                         let constraint = transfer::globalize(this, context, constraint);
@@ -636,6 +638,8 @@ impl CheckState {
                 self.checked.synonyms.insert(item_id, synonym);
             }
         }
+
+        Ok(())
     }
 
     /// Executes an action with an [`ErrorStep`] in scope.

tests-integration/fixtures/checking/117_do_ado_constrained/Main.snap

@@ -10,13 +10,11 @@ pure :: forall (f :: Type -> Type) (a :: Type). Applicative f => a -> f a
 discard :: forall (m :: Type -> Type) (a :: Type) (b :: Type). Discard m => m a -> (a -> m b) -> m b
 bind :: forall (m :: Type -> Type) (a :: Type) (b :: Type). Bind m => m a -> (a -> m b) -> m b
 testDo :: forall (m :: Type -> Type). Monad m => m (Tuple Int String)
-testDo' :: forall (t63 :: Type -> Type). Bind t63 => Applicative t63 => t63 (Tuple Int String)
+testDo' :: forall (t63 :: Type -> Type). Bind t63 => t63 (Tuple Int String)
 testAdo :: forall (f :: Type -> Type). Applicative f => f (Tuple Int String)
-testAdo' ::
-  forall (t93 :: Type -> Type).
-    Apply t93 => Applicative t93 => Functor t93 => t93 (Tuple Int String)
+testAdo' :: forall (t93 :: Type -> Type). Applicative t93 => t93 (Tuple Int String)
 testDoDiscard :: forall (m :: Type -> Type). Monad m => m Int
-testDoDiscard' :: forall (t109 :: Type -> Type). Discard t109 => Applicative t109 => t109 Int
+testDoDiscard' :: forall (t109 :: Type -> Type). Discard t109 => t109 Int
 
 Types
 Tuple :: Type -> Type -> Type