From 8e0fe62352d3f7fc4595d49299cbc1d0d0b8b578 Mon Sep 17 00:00:00 2001
From: Jack Huey <jack.huey@umassmed.edu>
Date: Fri, 27 Nov 2020 17:34:44 -0500
Subject: [PATCH] When unifying, if we find two subtype goals that are inverse
 of each other, relate with invariance instead

---
 chalk-integration/src/interner.rs | 15 ++++++++++++++-
 chalk-ir/src/debug.rs             | 10 ++++++++--
 chalk-solve/src/infer/unify.rs    | 20 +++++++++++++++++---
 tests/test/misc.rs                | 19 +++++++++++++++++++
 4 files changed, 58 insertions(+), 6 deletions(-)

diff --git a/chalk-integration/src/interner.rs b/chalk-integration/src/interner.rs
index 3e20018b5c0..2f461201895 100644
--- a/chalk-integration/src/interner.rs
+++ b/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)]
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 6998b3050cc..4a13346d203 100644
--- a/chalk-ir/src/debug.rs
+++ b/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
         )
     }
 }
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
index 886fb15dfef..b57d8b1c99a 100644
--- a/chalk-solve/src/infer/unify.rs
+++ b/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));
+        }
     }
 }
 
diff --git a/tests/test/misc.rs b/tests/test/misc.rs
index 52d3f455a9d..83913cf3bea 100644
--- a/tests/test/misc.rs
+++ b/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"
+        }
+    }
+}