Canonicalize more

crates/hir-analysis/src/lib.rs

@@ -40,6 +40,7 @@ pub struct Jar(
     ty::trait_lower::collect_implementor_methods,
     // Method collection.
     ty::method_table::collect_methods,
+    ty::method_table::probe_method,
     // Item Definition analysis.
     ty::def_analysis::check_recursive_adt,
     ty::def_analysis::analyze_adt,

crates/hir-analysis/src/ty/constraint.rs

@@ -21,9 +21,10 @@ use crate::{
     ty::{
         adt_def::{lower_adt, AdtRefId},
         binder::Binder,
+        canonical::Canonical,
         func_def::HirFuncDefKind,
         trait_lower::{lower_impl_trait, lower_trait},
-        ty_def::{inference_keys, TyVarSort},
+        ty_def::TyVarSort,
         unify::InferenceKey,
     },
     HirAnalysisDb,
@@ -53,18 +54,7 @@ pub(crate) fn ty_constraints(db: &dyn HirAnalysisDb, ty: TyId) -> ConstraintList
         args.push(ty_var);
     }
 
-    let constraints = base_constraints.instantiate(db, &args);
-
-    // If the constraint type contains unbound type parameters, we just ignore it.
-    let mut new_constraints = BTreeSet::new();
-    for &pred in constraints.predicates(db) {
-        if inference_keys(db, pred.ty(db)).is_empty() {
-            new_constraints.insert(pred);
-        }
-    }
-
-    let ingot = constraints.ingot(db);
-    ConstraintListId::new(db, new_constraints, ingot)
+    base_constraints.instantiate(db, &args)
 }
 
 /// Collect super traits of the given trait.
@@ -210,15 +200,19 @@ pub(crate) fn collect_func_def_constraints_impl(
 /// Describes a predicate indicating `ty` implements `trait_`.
 #[salsa::interned]
 pub struct PredicateId {
-    pub(super) ty: TyId,
-    pub(super) trait_inst: TraitInstId,
+    pub(super) ty: Canonical<TyId>,
+    pub(super) trait_inst: Canonical<TraitInstId>,
 }
 
 impl PredicateId {
     pub fn pretty_print(self, db: &dyn HirAnalysisDb) -> String {
         let ty = self.ty(db);
         let trait_ = self.trait_inst(db);
-        format!("{}: {}", ty.pretty_print(db), trait_.pretty_print(db))
+        format!(
+            "{}: {}",
+            ty.value.pretty_print(db),
+            trait_.value.pretty_print(db)
+        )
     }
 }
 
@@ -386,7 +380,7 @@ impl<'db> ConstraintCollector<'db> {
     fn can_remove(&mut self, predicates: PredicateListId, goal: PredicateId) -> bool {
         let goal_ty = goal.ty(self.db);
 
-        if !goal_ty.has_param(self.db) {
+        if !goal_ty.value.has_param(self.db) {
             return true;
         }
 
@@ -397,7 +391,11 @@ impl<'db> ConstraintCollector<'db> {
     }
 
     fn push_predicate(&mut self, ty: TyId, trait_inst: TraitInstId) {
-        let pred = PredicateId::new(self.db, ty, trait_inst);
+        let pred = PredicateId::new(
+            self.db,
+            Canonical::canonicalize(self.db, ty),
+            Canonical::canonicalize(self.db, trait_inst),
+        );
         self.predicates.insert(pred);
     }
 

crates/hir-analysis/src/ty/constraint_solver.rs

@@ -6,6 +6,7 @@
 use rustc_hash::FxHashSet;
 
 use super::{
+    canonical::Canonical,
     constraint::{collect_trait_constraints, AssumptionListId, PredicateId},
     fold::TyFoldable,
     trait_def::{ingot_trait_env, TraitEnv, TraitInstId},
@@ -82,9 +83,6 @@ pub(crate) fn is_goal_satisfiable(
     goal: Goal,
     assumptions: AssumptionListId,
 ) -> GoalSatisfiability {
-    if goal.ty(db).has_invalid(db) {
-        return GoalSatisfiability::Satisfied;
-    }
     ConstraintSolver::new(db, goal, assumptions).solve()
 }
 
@@ -127,8 +125,9 @@ impl<'db> ConstraintSolver<'db> {
     /// The main entry point of the constraint solver, which performs actual
     /// solving.
     fn solve(self) -> GoalSatisfiability {
-        let goal_ty = self.goal.ty(self.db);
-        let goal_trait = self.goal.trait_inst(self.db);
+        let mut table = UnificationTable::new(self.db);
+        let goal_ty = self.goal.ty(self.db).decanonicalize(&mut table);
+        let goal_trait = self.goal.trait_inst(self.db).decanonicalize(&mut table);
 
         // If the goal type is already invalid, we don't need to do anything.
         if goal_ty.has_invalid(self.db) {
@@ -146,22 +145,29 @@ impl<'db> ConstraintSolver<'db> {
         // current goal.
         let Some(sub_goals) = self
             .env
-            .impls_of_trait(self.db, goal_trait)
+            .impls_of_trait(
+                self.db,
+                self.assumptions.ingot(self.db),
+                self.goal.trait_inst(self.db),
+            )
             .iter()
             .find_map(|impl_| {
-                let mut table = UnificationTable::new(self.db);
+                let snapshot = table.snapshot();
                 let gen_impl = table.instantiate_with_fresh_vars(*impl_);
 
                 // If the `impl` can matches the goal by unifying the goal type, then we can
                 // obtain a subgoals which is specified by the `impl`.
-                if table.unify(gen_impl.ty(self.db), goal_ty).is_ok()
+                let res = if table.unify(gen_impl.ty(self.db), goal_ty).is_ok()
                     && table.unify(gen_impl.trait_(self.db), goal_trait).is_ok()
                 {
                     let constraints = impl_.instantiate_identity().constraints(self.db);
                     Some(constraints.fold_with(&mut table))
                 } else {
                     None
-                }
+                };
+
+                table.rollback_to(snapshot);
+                res
             })
         else {
             return GoalSatisfiability::NotSatisfied(self.goal);
@@ -190,9 +196,10 @@ impl<'db> ConstraintSolver<'db> {
             let trait_ = pred.trait_inst(self.db);
             let ty = pred.ty(self.db);
 
-            for &super_trait in trait_.def(self.db).super_traits(self.db).iter() {
-                let super_trait = super_trait.instantiate(self.db, trait_.args(self.db));
-                let super_pred = PredicateId::new(self.db, ty, super_trait);
+            for &super_trait in trait_.value.def(self.db).super_traits(self.db).iter() {
+                let super_trait = super_trait.instantiate(self.db, trait_.value.args(self.db));
+                let super_pred =
+                    PredicateId::new(self.db, ty, Canonical::canonicalize(self.db, super_trait));
                 assumptions.insert(super_pred);
             }
         }

crates/hir-analysis/src/ty/def_analysis.rs

@@ -27,6 +27,7 @@ use super::{
     diagnostics::{ImplDiag, TraitConstraintDiag, TraitLowerDiag, TyDiagCollection, TyLowerDiag},
     func_def::FuncDef,
     method_cmp::compare_impl_method,
+    method_table::probe_method,
     trait_def::{ingot_trait_env, Implementor, TraitDef},
     trait_lower::{lower_trait, lower_trait_ref, TraitRefLowerError},
     ty_def::{InvalidCause, TyData, TyId},
@@ -44,7 +45,6 @@ use crate::{
             ImplTraitDefDiagAccumulator, TraitDefDiagAccumulator, TypeAliasDefDiagAccumulator,
         },
         func_def::lower_func,
-        method_table::collect_methods,
         trait_def::does_impl_trait_conflict,
         trait_lower::lower_impl_trait,
         ty_lower::{lower_hir_ty, lower_type_alias},
@@ -391,10 +391,9 @@ impl<'db> DefAnalyzer<'db> {
             return true;
         }
 
-        let method_table = collect_methods(self.db, func.ingot(self.db));
-
-        for cand in method_table.probe_eager(
+        for &cand in probe_method(
             self.db,
+            self.scope().ingot(self.db.as_hir_db()),
             Canonical::canonicalize(self.db, self_ty),
             func.name(self.db),
         ) {
@@ -1170,7 +1169,13 @@ fn analyze_impl_trait_specific_error(
     let target_ty_span: DynLazySpan = impl_trait.lazy_span().ty().into();
     for &super_trait in trait_def.super_traits(db) {
         let super_trait = super_trait.instantiate(db, trait_inst.args(db));
-        let goal = PredicateId::new(db, implementor.skip_binder().ty(db), super_trait);
+        let goal = PredicateId::new(
+            db,
+            Canonical {
+                value: implementor.skip_binder().ty(db),
+            },
+            Canonical { value: super_trait },
+        );
         is_satisfied(goal, target_ty_span.clone())
     }
 

crates/hir-analysis/src/ty/diagnostics.rs

@@ -1711,8 +1711,8 @@ impl TraitConstraintDiag {
         let goal = pred.trait_inst(db);
         let msg = format!(
             "`{}` doesn't implement `{}`",
-            ty.pretty_print(db),
-            goal.pretty_print(db)
+            ty.value.pretty_print(db),
+            goal.value.pretty_print(db)
         );
         Self::TraitBoundNotSat(span, msg)
     }
@@ -1726,8 +1726,8 @@ impl TraitConstraintDiag {
         let ty = pred.ty(db);
         let msg = format!(
             "infinite evaluation recursion occurs when checking `{}: {}` ",
-            ty.pretty_print(db),
-            goal.pretty_print(db)
+            ty.value.pretty_print(db),
+            goal.value.pretty_print(db)
         );
         Self::InfiniteBoundRecursion(span, msg)
     }

crates/hir-analysis/src/ty/fold.rs

@@ -1,10 +1,12 @@
 use std::collections::BTreeSet;
 
 use super::{
+    canonical::Canonical,
     constraint::{PredicateId, PredicateListId},
     trait_def::{Implementor, TraitInstId},
     ty_check::ExprProp,
     ty_def::{TyData, TyId},
+    unify::UnificationTable,
     visitor::TyVisitable,
 };
 use crate::{
@@ -150,9 +152,20 @@ impl<'db> TyFoldable<'db> for PredicateId {
     where
         F: TyFolder<'db>,
     {
-        let ty = self.ty(folder.db()).fold_with(folder);
-        let trait_inst = self.trait_inst(folder.db()).fold_with(folder);
-        Self::new(folder.db(), ty, trait_inst)
+        let mut table = UnificationTable::new(folder.db());
+        let ty = self
+            .ty(folder.db())
+            .decanonicalize(&mut table)
+            .fold_with(folder);
+        let trait_inst = self
+            .trait_inst(folder.db())
+            .decanonicalize(&mut table)
+            .fold_with(folder);
+        Self::new(
+            folder.db(),
+            Canonical::canonicalize(folder.db(), ty),
+            Canonical::canonicalize(folder.db(), trait_inst),
+        )
     }
 }
 

crates/hir-analysis/src/ty/method_cmp.rs

@@ -262,7 +262,7 @@ fn compare_constraints(
     if unsatisfied_goals.is_empty() {
         true
     } else {
-        unsatisfied_goals.sort_by_key(|goal| goal.ty(db).pretty_print(db));
+        unsatisfied_goals.sort_by_key(|goal| goal.ty(db).value.pretty_print(db));
         sink.push(
             ImplDiag::method_stricter_bound(db, impl_m.name_span(db), &unsatisfied_goals).into(),
         );