Match Types arguments with bounds (yet another)

[zraffer]

Compiler version

3.0.0-M3

Minimized code

object TMP:
  final class Tu1[Ar1]
  type Pr11[T <: Tu1[_]] =
    T match {case Tu1[ar1] => ar1}

  final class Tu2[Ar1 <: Tu1[_], Ar2 <: Pr11[Ar1]]
  type Pr21[T <: Tu2[_,_]] <: Tu1[_] =
    T match {case Tu2[ar1, ar2] => ar1}
  type Pr22[T <: Tu2[_,_]] <: Pr11[Pr21[T]] =
    T match {case Tu2[ar1, ar2] => ar2} // error here!

  type Copy[T <: Tu2[_,_]] = Tu2[Pr21[T], Pr22[T]]

emits error about ar2 bound

Expectation

The code should be typechecked well.

Note: it is modified version of #6697 The topic of these exercises are obvious typelevel copying of typelevel tuples via typelevel projections. Now with bound of an argument being itself a projection.

[OlivierBlanvillain]

Have you tried giving Pr21[T] a name? I'm not sure the compiler know how to unify wildcards that way...

[zraffer]

Oh, I see. We can wrap the definition of argument bound Ar2 <: Pr11[Ar1] into Ar2 <: Tu1[Pr11[Ar1]] and it starts to typecheck well. However it seems to be an ugly workaround since we have to carry Tu1[_] wrapper (or something like that) all over code along with projections to extract an actual argument from the wrapper. Did I miss something?

On Thu, 28 Jan 2021 at 11:58, Olivier Blanvillain notifications@github.com wrote:

Have you tried giving Pr21[T] a name? I'm not sure the compiler know how to unify wildcards that way...

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[dwijnand]

Have you tried giving Pr21[T] a name? I'm not sure the compiler know how to unify wildcards that way...

I'm not 100% sure if "unify wildcards" and "capture conversion" are 1:1, but at least here I think I debugged that it fails because capture conversion fails, and that's because T (which is the "leftRoot") isn't stable. And a short attempt at overriding that still failed (but I forgot why now).

@OlivierBlanvillain do you think we should close this as "won't fix", or do you think it's something that should be made to work?

[dwijnand]

Looked at this last week (with @Decel) and I recorded that I think this needs some "subtype reconstruction" (aka "GADT reasoning"), so that we record that in T match {case Tu2[ar1, ar2] => RHS1 ...} that T <: Tu2[ar1, ar2] while typing RHS1.

[dwijnand]

I mention that because I discovered that to fix https://github.com/lampepfl/dotty/issues/13741 I also need that inference.