Spurious level errors for `Contains`

[Linyxus]

Compiler version

main

Minimized code

import language.experimental.captureChecking
import caps.*
def test1() =
  val z: Any^ = ???
  def onlyWithZ[C^](using c: Contains[C, z.type]) = ???
  onlyWithZ[{z}]     // error, but should be ok
def test2(z: Any^) =
  def onlyWithZ[C^](using c: Contains[C, z.type]) = ???
  onlyWithZ[{z}]     // ok

Output

[info] running (fork) dotty.tools.dotc.Main -d /Users/linyxus/Workspace/dotty/compiler/../out/default-last-scalac-out.jar -classpath /Users/linyxus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.16/scala-library-2.13.16.jar:/Users/linyxus/Workspace/dotty/library/../out/bootstrap/scala3-library-bootstrapped/scala-3.8.0-RC1-bin-SNAPSHOT-nonbootstrapped/scala3-library_3-3.8.0-RC1-bin-SNAPSHOT.jar -color:never issues/cclevel-contains.scala
-- [E007] Type Mismatch Error: issues/cclevel-contains.scala:6:16 ----------------------------------------------------------------------------------------------------------------------
6 |  onlyWithZ[{z}]     // error, but should be ok
  |                ^
  |                Found:    scala.caps.Contains.containsImpl[scala.caps.CapSet^, (z : Any^)^{z}]
  |                Required: scala.caps.Contains[scala.caps.CapSet^{z}, (z : Any^)^{z}]
  |
  |                Note that capability cap is not included in capture set {z}.
  |
  |                where:    ^   refers to a fresh root capability in the type of value z
  |                          cap is a fresh root capability in the type of value z
  |
  | longer explanation available when compiling with `-explain`
1 error found
[error] nonzero exit code returned from runner: 1
[error] (scala3-compiler / Compile / runMain) nonzero exit code returned from runner: 1
[error] Total time: 2 s, completed 23 Sept 2025, 13:31:39

Expectation

There should be no error. A leftover issue from PR #23934.

[bracevac]

IMO, the real question is whether we have legit uses of Contains that warrant having it
and pouring resources into fixing it.

The test case that is broken was made by yours truly to explore the limits of capture polymorphism and Contains.

We didn't need it in the stdlib, but is there maybe a use in Gears? Maybe @natsukagami and @odersky can chime in?

I find Contains problematic in the sense that misleads (and eventually disappoints) a user into thinking that we can have general givens involving capture sets. But what we can do is fairly narrow.

[natsukagami]

I don't think Gears no longer needs it

[Linyxus]

I don't see why the "legit uses" of Contains matter that much. Avoid "pouring resources into fixing it" is just hiding away from the problem. This issue may be a facade of more general problems of the level checking scheme.