Type parameters inferred as Any on GADT

[mpilquist]

Compiler version

3.1.1

Minimized code

//> using scala "3.1.1"
trait Monad[F[_]]:
  def pure[A](a: A): F[A]
  extension [A](fa: F[A])
    def flatMap[B](f: A => F[B]): F[B]
    def map[B](f: A => B): F[B]

enum Pull[+F[_], +O, +R]:
  case Uncons(value: Pull[F, O, R]) extends Pull[F, Nothing, Either[R, (O, Pull[F, O, R])]]

  def step[F2[x] >: F[x], O2 >: O, R2 >: R](using F: Monad[F2]): F2[Either[R2, (O2, Pull[F2, O2, R2])]] =
    this match
      case Uncons(v) => v.step(using F).map(e => Left(e))

object Pull:
  extension [F[_], O, R](self: Pull[F, O, R])
    def stepViaExtension(using F: Monad[F]): F[Either[R, (O, Pull[F, O, R])]] =
      self match
        case Uncons(v) => v.stepViaExtension.map(Left(_))

Output

step fails to compile with this error:

[error] ./foo.scala:13:55: Found:    (e : Either[Any, (Any, Pull[F2, Any, Any])])
[error] Required: R2
[error]
[error] where:    F2 is a type in method step with bounds >: [x] =>> F[x] and <: [x] =>> Any
[error]           R2 is a type in method step with bounds >: R
[error]       case Uncons(v) => v.step(using F).map(e => Left(e))
[error]                                                       ^

Expectation

Any is inferred for each of the type params of v. The equivalent match written as an extension method without bounded super types infers correctly.

[smarter]

There's a lot going on in this code snippet, could you simplify it to a truly minimal example?

[mpilquist]

This may be a minimization:

//> using scala "3.1.1"
enum Pull[+F[_], +R]:
  case Uncons(value: Pull[F, R]) extends Pull[F, Pull[F, R]]

def step[F[_], R](p: Pull[F, R]): F[Pull[F, R]] =
  p match
    case Pull.Uncons(v) => step(v)

[error] ./foo.scala:7:33: Found:    (v : Pull[F, Any])
[error] Required: Pull[F, R]
[error]
[error] where:    F is a type in method step with bounds <: [_] =>> Any
[error]           R is a type in method step with bounds >: Pull[F, Any]
[error]     case Pull.Uncons(v) => step(v)
[error]

[smarter]

./foo.scala:7:33: Found: (v : Pull[F, Any])

What would you expect to see instead of Any here? It doesn't seem like R would fit, since if v has type Pull[F, R] that would imply that p has type Pull[F, Pull[F, R]] whereas it has type Pull[F, R].

[mpilquist]

Hm, Pull[F, R] along with R =:= Pull[F, R]? Is that nonsensical?

I realized the original version infers v: Pull[F, Any, Any] in both the method and the extension method examples. The extension method version types v.stepViaExtension.map(Left(_)) as F[Left[Either[Any, (Any, Pull[F, Any, Any])], Nothing]] and it accepts that as a subtype of F[Either[R, (O, Pull[F, O, R])]].

[smarter]

R =:= Pull[F, R]

This would be a weird recursive type definition which I'm fairly sure we can't support (the best we can do is f-bounded types where a type appears in its own upper-bound, but not in its own lower-bound). I also don't think that would be sound but it's hard to say as-is since there's no way to create a value of type Pull.

[smarter]

Closing since there doesn't seem to be an agreed-upon bug here, but feel free to reopen with a different example or more precise description of what should happen.