When unifying, if we find two subtype goals that are inverse of each …

…other, relate with invariance instead

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-solve/src/infer/unify.rs

@@ -1071,9 +1071,23 @@ impl<'t, I: Interner> Unifier<'t, I> {
 
     /// Pushes a goal of `a` being a subtype of `b`.
     fn push_subtype_goal(&mut self, a: Ty<I>, b: Ty<I>) {
-        let subtype_goal = GoalData::SubtypeGoal(SubtypeGoal { a, b }).intern(self.interner());
-        self.goals
-            .push(InEnvironment::new(self.environment, subtype_goal));
+        let inverse = self.goals.iter().position(|g| {
+            if g.environment != *self.environment {
+                return false;
+            }
+            match g.goal.data(self.interner()) {
+                GoalData::SubtypeGoal(SubtypeGoal { a: a1, b: b1 }) => a == *b1 && b == *a1,
+                _ => false,
+            }
+        });
+        if let Some(inverse) = inverse {
+            self.goals.remove(inverse);
+            self.relate_ty_ty(Variance::Invariant, &a, &b).unwrap();
+        } else {
+            let subtype_goal = GoalData::SubtypeGoal(SubtypeGoal { a, b }).intern(self.interner());
+            self.goals
+                .push(InEnvironment::new(self.environment, subtype_goal));
+        }
     }
 }
 

tests/test/misc.rs

@@ -759,3 +759,22 @@ fn empty_definite_guidance() {
         }
     }
 }
+
+#[test]
+fn ambiguous_unification_in_fn() {
+    test! {
+        program {
+            trait FnOnce<Args> {}
+
+            struct MyClosure<T> {}
+            impl<T> FnOnce<T> for MyClosure<fn(T) -> ()> {}
+        }
+        goal {
+            exists<T, U> {
+                MyClosure<fn(U) -> ()>: FnOnce<T>
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}