Always relate with Invariant to non-General inference vars

chalk-engine/src/simplify.rs

@@ -79,11 +79,6 @@ impl<I: Interner> Forest<I> {
                     Err(_) => return FallibleOrFloundered::NoSolution,
                 },
                 GoalData::SubtypeGoal(goal) => {
-                    if goal.a.inference_var(context.program().interner()).is_some()
-                        && goal.b.inference_var(context.program().interner()).is_some()
-                    {
-                        return FallibleOrFloundered::Floundered;
-                    }
                     match infer.relate_tys_into_ex_clause(
                         context.program().interner(),
                         context.unification_database(),
@@ -93,8 +88,13 @@ impl<I: Interner> Forest<I> {
                         &goal.b,
                         &mut ex_clause,
                     ) {
-                        Ok(()) => {}
-                        Err(_) => return FallibleOrFloundered::NoSolution,
+                        FallibleOrFloundered::Ok(_) => {}
+                        FallibleOrFloundered::Floundered => {
+                            return FallibleOrFloundered::Floundered
+                        }
+                        FallibleOrFloundered::NoSolution => {
+                            return FallibleOrFloundered::NoSolution
+                        }
                     }
                 }
                 GoalData::DomainGoal(domain_goal) => {

chalk-engine/src/slg.rs

@@ -213,7 +213,7 @@ pub trait UnificationOps<I: Interner> {
         a: &Ty<I>,
         b: &Ty<I>,
         ex_clause: &mut ExClause<I>,
-    ) -> Fallible<()>;
+    ) -> FallibleOrFloundered<()>;
 }
 
 #[derive(Clone)]
@@ -349,11 +349,27 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
         a: &Ty<I>,
         b: &Ty<I>,
         ex_clause: &mut ExClause<I>,
-    ) -> Fallible<()> {
-        let result = self
-            .infer
-            .relate(interner, db, environment, variance, a, b)?;
-        Ok(into_ex_clause(interner, result, ex_clause))
+    ) -> FallibleOrFloundered<()> {
+        let a_norm = self.infer.normalize_ty_shallow(interner, a);
+        let a = a_norm.as_ref().unwrap_or(a);
+        let b_norm = self.infer.normalize_ty_shallow(interner, b);
+        let b = b_norm.as_ref().unwrap_or(b);
+
+        if matches!(
+            a.kind(interner),
+            TyKind::InferenceVar(_, TyVariableKind::General)
+        ) && matches!(
+            b.kind(interner),
+            TyKind::InferenceVar(_, TyVariableKind::General)
+        ) {
+            return FallibleOrFloundered::Floundered;
+        }
+        let result = match self.infer.relate(interner, db, environment, variance, a, b) {
+            Ok(r) => r,
+            Err(_) => return FallibleOrFloundered::Floundered,
+        };
+        into_ex_clause(interner, result, ex_clause);
+        FallibleOrFloundered::Ok(())
     }
 }
 

chalk-integration/src/interner.rs

@@ -28,12 +28,25 @@ impl Debug for RawId {
     }
 }
 
-#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Copy, Clone, PartialEq, Eq, Hash)]
 pub enum ChalkFnAbi {
     Rust,
     C,
 }
 
+impl Debug for ChalkFnAbi {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            fmt,
+            "{}",
+            match self {
+                ChalkFnAbi::Rust => "\"rust\"",
+                ChalkFnAbi::C => "\"c\"",
+            },
+        )
+    }
+}
+
 /// The default "interner" and the only interner used by chalk
 /// itself. In this interner, no interning actually occurs.
 #[derive(Debug, Copy, Clone, Hash, PartialOrd, Ord, PartialEq, Eq)]

chalk-ir/src/debug.rs

@@ -273,8 +273,14 @@ impl<I: Interner> Debug for FnPointer<I> {
         } = self;
         write!(
             fmt,
-            "for<{}> {:?} {:?} {:?}",
-            num_binders, sig.safety, sig.abi, substitution
+            "{}{:?} for<{}> {:?}",
+            match sig.safety {
+                Safety::Unsafe => "unsafe ",
+                Safety::Safe => "",
+            },
+            sig.abi,
+            num_binders,
+            substitution
         )
     }
 }

chalk-recursive/src/fulfill.rs

@@ -8,8 +8,8 @@ use chalk_ir::zip::Zip;
 use chalk_ir::{
     Binders, Canonical, ConstrainedSubst, Constraint, Constraints, DomainGoal, Environment, EqGoal,
     Fallible, GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClauseImplication,
-    QuantifierKind, Substitution, SubtypeGoal, UCanonical, UnificationDatabase, UniverseMap,
-    Variance,
+    QuantifierKind, Substitution, SubtypeGoal, Ty, TyKind, TyVariableKind, UCanonical,
+    UnificationDatabase, UniverseMap, Variance,
 };
 use chalk_solve::debug_span;
 use rustc_hash::FxHashSet;
@@ -119,6 +119,8 @@ pub(super) trait RecursiveInferenceTable<I: Interner> {
         T: Fold<I, Result = T> + HasInterner<Interner = I>;
 
     fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool;
+
+    fn normalize_ty_shallow(&mut self, interner: &I, leaf: &Ty<I>) -> Option<Ty<I>>;
 }
 
 /// A `Fulfill` is where we actually break down complex goals, instantiate
@@ -298,7 +300,7 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
         environment: &Environment<I>,
         goal: Goal<I>,
     ) -> Fallible<()> {
-        let interner = self.interner();
+        let interner = self.solver.interner();
         match goal.data(interner) {
             GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
                 let subgoal = self
@@ -334,9 +336,18 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
                 self.unify(&environment, Variance::Invariant, &a, &b)?;
             }
             GoalData::SubtypeGoal(SubtypeGoal { a, b }) => {
-                if a.inference_var(self.interner()).is_some()
-                    && b.inference_var(self.interner()).is_some()
-                {
+                let a_norm = self.infer.normalize_ty_shallow(interner, a);
+                let a = a_norm.as_ref().unwrap_or(a);
+                let b_norm = self.infer.normalize_ty_shallow(interner, b);
+                let b = b_norm.as_ref().unwrap_or(b);
+
+                if matches!(
+                    a.kind(interner),
+                    TyKind::InferenceVar(_, TyVariableKind::General)
+                ) && matches!(
+                    b.kind(interner),
+                    TyKind::InferenceVar(_, TyVariableKind::General)
+                ) {
                     self.cannot_prove = true;
                 } else {
                     self.unify(&environment, Variance::Covariant, &a, &b)?;

chalk-recursive/src/solve.rs

@@ -8,7 +8,8 @@ use chalk_ir::zip::Zip;
 use chalk_ir::{
     Binders, Canonical, ClausePriority, DomainGoal, Environment, Fallible, Floundered, GenericArg,
     Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData,
-    ProgramClauseImplication, Substitution, UCanonical, UnificationDatabase, UniverseMap, Variance,
+    ProgramClauseImplication, Substitution, Ty, UCanonical, UnificationDatabase, UniverseMap,
+    Variance,
 };
 use chalk_solve::clauses::program_clauses_for_goal;
 use chalk_solve::debug_span;
@@ -317,4 +318,8 @@ impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I>
     fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool {
         truncate::needs_truncation(interner, &mut self.infer, max_size, value)
     }
+
+    fn normalize_ty_shallow(&mut self, interner: &I, leaf: &Ty<I>) -> Option<Ty<I>> {
+        self.infer.normalize_ty_shallow(interner, leaf)
+    }
 }

chalk-solve/src/infer/unify.rs

@@ -96,33 +96,43 @@ impl<'t, I: Interner> Unifier<'t, I> {
 
         match (a.kind(interner), b.kind(interner)) {
             // Relating two inference variables:
+            // First, if either variable is a float or int kind, then we always
+            // unify if they match. This is because float and ints don't have
+            // subtype relationships.
+            // If both kinds are general then:
             // If `Invariant`, unify them in the underlying ena table.
             // If `Covariant` or `Contravariant`, push `SubtypeGoal`
             (&TyKind::InferenceVar(var1, kind1), &TyKind::InferenceVar(var2, kind2)) => {
-                match variance {
-                    Variance::Invariant => {
-                        if kind1 == kind2 {
-                            self.unify_var_var(var1, var2)
-                        } else if kind1 == TyVariableKind::General {
-                            self.unify_general_var_specific_ty(var1, b.clone())
-                        } else if kind2 == TyVariableKind::General {
-                            self.unify_general_var_specific_ty(var2, a.clone())
-                        } else {
-                            debug!(
-                                "Tried to unify mis-matching inference variables: {:?} and {:?}",
-                                kind1, kind2
-                            );
-                            Err(NoSolution)
+                if matches!(kind1, TyVariableKind::General)
+                    && matches!(kind2, TyVariableKind::General)
+                {
+                    // Both variable kinds are general; so unify if invariant, otherwise push subtype goal
+                    match variance {
+                        Variance::Invariant => self.unify_var_var(var1, var2),
+                        Variance::Covariant => {
+                            self.push_subtype_goal(a.clone(), b.clone());
+                            Ok(())
+                        }
+                        Variance::Contravariant => {
+                            self.push_subtype_goal(b.clone(), a.clone());
+                            Ok(())
                         }
                     }
-                    Variance::Covariant => {
-                        self.push_subtype_goal(a.clone(), b.clone());
-                        Ok(())
-                    }
-                    Variance::Contravariant => {
-                        self.push_subtype_goal(b.clone(), a.clone());
-                        Ok(())
-                    }
+                } else if kind1 == kind2 {
+                    // At least one kind is not general, but they match, so unify
+                    self.unify_var_var(var1, var2)
+                } else if kind1 == TyVariableKind::General {
+                    // First kind is general, second isn't, unify
+                    self.unify_general_var_specific_ty(var1, b.clone())
+                } else if kind2 == TyVariableKind::General {
+                    // Second kind is general, first isn't, unify
+                    self.unify_general_var_specific_ty(var2, a.clone())
+                } else {
+                    debug!(
+                        "Tried to unify mis-matching inference variables: {:?} and {:?}",
+                        kind1, kind2
+                    );
+                    Err(NoSolution)
                 }
             }
 

tests/test/misc.rs

@@ -759,3 +759,26 @@ fn empty_definite_guidance() {
         }
     }
 }
+
+#[test]
+fn ambiguous_unification_in_fn() {
+    test! {
+        program {
+            trait FnOnce<Args> {
+                type Output;
+            }
+
+            struct MyClosure<T> {}
+            impl<T> FnOnce<(T,)> for MyClosure<fn(T) -> ()> {
+                type Output = ();
+            }
+        }
+        goal {
+            exists<int T, U> {
+                MyClosure<fn(&'static U) -> ()>: FnOnce<(&'static T,)>
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}