refine propagation for idempotent maps

Linyxus · Linyxus · commit dd88672e1222 · 2022-11-10T23:11:49.000+01:00
For an idempotent map f and a set C, we do not need to propagate x ∈ f(C) back
to C when x comes from f(y) for some y ∈ C.
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
@@ -546,7 +546,7 @@ object CaptureSet:
           else CompareResult.fail(this)
         }
         .andAlso {
-          if (origin ne source) && mapIsIdempotent then
+          if (origin ne source) && (origin ne initial) && mapIsIdempotent then
             // `tm` is idempotent, propagate back elems from image set.
             // This is sound, since we know that for `r in newElems: tm(r) = r`, hence
             // `r` is _one_ possible solution in `source` that would make an `r` appear in this set.

Original file line number	Diff line number	Diff line change
`@@ -546,7 +546,7 @@ object CaptureSet:`
`546`	`546`	`else CompareResult.fail(this)`
`547`	`547`	`}`
`548`	`548`	`.andAlso {`
`549`		`- if (origin ne source) && mapIsIdempotent then`
	`549`	`+ if (origin ne source) && (origin ne initial) && mapIsIdempotent then`
`550`	`550`	// `tm` is idempotent, propagate back elems from image set.
`551`	`551`	// This is sound, since we know that for `r in newElems: tm(r) = r`, hence
`552`	`552`	// `r` is _one_ possible solution in `source` that would make an `r` appear in this set.