it sound

Author: lcnr

compiler/rustc_type_ir/src/search_graph/mod.rs

@@ -199,27 +199,27 @@ impl UsageKind {
 /// This is a necessary condition to rebase provisional cache
 /// entries.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub enum AllPathsToHeadCoinductive {
+pub enum AllPathsToHeadForcedAmbiguity {
     Yes,
     No,
 }
-impl From<PathKind> for AllPathsToHeadCoinductive {
-    fn from(path: PathKind) -> AllPathsToHeadCoinductive {
+impl From<PathKind> for AllPathsToHeadForcedAmbiguity {
+    fn from(path: PathKind) -> AllPathsToHeadForcedAmbiguity {
         match path {
-            PathKind::Coinductive => AllPathsToHeadCoinductive::Yes,
-            _ => AllPathsToHeadCoinductive::No,
+            PathKind::ForcedAmbiguity => AllPathsToHeadForcedAmbiguity::Yes,
+            _ => AllPathsToHeadForcedAmbiguity::No,
         }
     }
 }
-impl AllPathsToHeadCoinductive {
+impl AllPathsToHeadForcedAmbiguity {
     #[must_use]
     fn merge(self, other: impl Into<Self>) -> Self {
         match (self, other.into()) {
-            (AllPathsToHeadCoinductive::Yes, AllPathsToHeadCoinductive::Yes) => {
-                AllPathsToHeadCoinductive::Yes
+            (AllPathsToHeadForcedAmbiguity::Yes, AllPathsToHeadForcedAmbiguity::Yes) => {
+                AllPathsToHeadForcedAmbiguity::Yes
             }
-            (AllPathsToHeadCoinductive::No, _) | (_, AllPathsToHeadCoinductive::No) => {
-                AllPathsToHeadCoinductive::No
+            (AllPathsToHeadForcedAmbiguity::No, _) | (_, AllPathsToHeadForcedAmbiguity::No) => {
+                AllPathsToHeadForcedAmbiguity::No
             }
         }
     }
@@ -269,7 +269,7 @@ impl AvailableDepth {
 /// when rebasing provisional cache results.
 #[derive(Clone, Debug, PartialEq, Eq, Default)]
 struct CycleHeads {
-    heads: BTreeMap<StackDepth, AllPathsToHeadCoinductive>,
+    heads: BTreeMap<StackDepth, AllPathsToHeadForcedAmbiguity>,
 }
 
 impl CycleHeads {
@@ -297,19 +297,19 @@ impl CycleHeads {
     fn insert(
         &mut self,
         head: StackDepth,
-        path_from_entry: impl Into<AllPathsToHeadCoinductive> + Copy,
+        path_from_entry: impl Into<AllPathsToHeadForcedAmbiguity> + Copy,
     ) {
         self.heads.entry(head).or_insert(path_from_entry.into()).and_merge(path_from_entry);
     }
 
     fn merge(&mut self, heads: &CycleHeads) {
         for (&head, &path_from_entry) in heads.heads.iter() {
             self.insert(head, path_from_entry);
-            debug_assert!(matches!(self.heads[&head], AllPathsToHeadCoinductive::Yes));
+            debug_assert!(matches!(self.heads[&head], AllPathsToHeadForcedAmbiguity::Yes));
         }
     }
 
-    fn iter(&self) -> impl Iterator<Item = (StackDepth, AllPathsToHeadCoinductive)> + '_ {
+    fn iter(&self) -> impl Iterator<Item = (StackDepth, AllPathsToHeadForcedAmbiguity)> + '_ {
         self.heads.iter().map(|(k, v)| (*k, *v))
     }
 
@@ -325,9 +325,8 @@ impl CycleHeads {
             }
 
             let path_from_entry = match step_kind {
-                PathKind::Coinductive => AllPathsToHeadCoinductive::Yes,
-                // TODO
-                PathKind::Unknown | PathKind::Inductive | PathKind::ForcedAmbiguity => {
+                PathKind::ForcedAmbiguity => AllPathsToHeadForcedAmbiguity::Yes,
+                PathKind::Unknown | PathKind::Inductive | PathKind::Coinductive => {
                     path_from_entry
                 }
             };
@@ -873,12 +872,12 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
                 // to its heads are coinductive. In this case these cycle
                 // kinds won't change, no matter the goals between these
                 // heads and the provisional cache entry.
-                if heads.iter().any(|(_, p)| matches!(p, AllPathsToHeadCoinductive::No)) {
+                if heads.iter().any(|(_, p)| matches!(p, AllPathsToHeadForcedAmbiguity::No)) {
                     return false;
                 }
 
                 // The same for nested goals of the cycle head.
-                if stack_entry.heads.iter().any(|(_, p)| matches!(p, AllPathsToHeadCoinductive::No))
+                if stack_entry.heads.iter().any(|(_, p)| matches!(p, AllPathsToHeadForcedAmbiguity::No))
                 {
                     return false;
                 }