Rechecking inferred type arguments fails.

[sstucki]

Minimized code

type Foo[+X >: Nothing <: Nothing] = Nothing
type Bar[+X >: Any     <: Any]     = Nothing

sealed trait Comp[-A, -B, -F[+X >: A <: B], +C, +D, +G[+Y >: C <: D]]
case class Refl[A, B, F[+X >: A <: B]]() extends Comp[A, B, F, A, B, F]

// OK (but fails with -Ycheck:typer).
val foobar: Comp[Nothing, Nothing, Foo, Any, Any, Bar] = Refl()

// Fails: a version of `foobar` with explicit type arguments.
// (The type arguments were extracted using -Xprint:typer).
val foobar2: Comp[Nothing, Nothing, Foo, Any, Any, Bar] =
  Refl[Any, Any, [X >: Any] =>> Nothing]()

Output

-- [E007] Type Mismatch Error: CompFail.scala:13:40 --------------------------
13 |  Refl[Any, Any, [X >: Any] =>> Nothing]()
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |  Found:    Refl[Any, Any, [X >: Any] =>> Nothing]
   |  Required: Comp[Nothing, Nothing, Foo, Any, Any, Bar]
1 error found

Expectation

This probably shouldn't type check, but I'm really not sure. In any case, the versions with and without explicit type arguments should behave the same way.

The correct behavior here probably depends on how bounds of (abstract) type operators should be handled in subtype checking, which is presumably related to issues #6499/#6320.

Mentioning @Blaisorblade and @smarter since this resulted from a discussion we had.