Unreducible app of HK type when nesting dependent func + match types

[alcestes]

Minimized code

case class More(); case class Stop();

sealed abstract class DSL
case class Fun[F <: More|Stop => DSL](cont: F) extends DSL
case class Nop() extends DSL

type Match2[X <: More|Stop] <: DSL = X match {
  case More => Fun[(y: More|Stop) => Match1[y.type]]
  case Stop => Nop
}
type Match1[X] <: DSL = X match {
  case More => Nop
  case Stop => Nop
}

def fun2(x: More|Stop): Match2[x.type] = x match {
  case _: More => Fun(fun1)
  case _: Stop => Nop()
}

def fun1(y: More|Stop): Match1[y.type] = y match {
  case _: More => Nop()
  case _: Stop => Nop()
}

Output

[error] -- [E043] Type Error: MatchTypes.scala:19:1 
[error] 19 |}
[error]    | ^
[error]    |unreducible application of higher-kinded type Match1 to wildcard arguments in subpart Match1[? <: More | Stop] of inferred type 
[error]    |  (x : More | Stop) match {
[error]    |    case More => Fun[(y: More | Stop) => Match1[y.type]]
[error]    |    case Stop => Nop
[error]    |  } <: DSL
[error]    |
[error] one error found

Expectation

Type-checking should succeed.

Notes

• The error arises whenever I try to nest 2+ levels of dependent function types + match types

• Indeed, if fun2() is commented out, then the type-checking of fun1() succeeds

• The whole code above appears to type-check correctly when using VS Code with the Dotty extension:

  • the types reported by the IDE appear correct
  • if one tries to replace Fun(fun1) with Nop() in fun2(), the resulting error message correctly reports the expected type
  • if the body of fun1() is inlined in fun2(), its type is correctly inferred and type-checking succeeds

• The error is reported by the PostTyper compiler phase, which is not executed by the Dotty extension for VS Code

[odersky]

This would need more info to determine whether it's really a bug or whether the reported error is a true one.

[alcestes]

I'll be happy to provide more info --- just let me know what I can do :-)

I am very keen on understanding whether this issue is a real bug, and whether it can be fixed --- because were it solved, it would be possible to represent a form of session types in Dotty.

[alcestes]

@odersky here is another (simpler) example that highlights the issue.

case class A();
case class B();

type M2[X <: A|B] = X match {
  case A => A
  case B => B
}

def f2(x: A|B): M2[x.type] = x match {
  case _: A => A()
  case _: B => B()
}

// This definition of type M1 works: function f1() below compiles
/*
type M1[X <: A|B] = X match {
  case A => A
  case B => (x: A|B) => x.type match { // Should be equivalent to M2[x.type]
    case A => A
    case B => B
  }
}
*/

// This definition of type M1 causes an error when f1() below is compiled:
// "unreducible application of higher-kinded type M2"
type M1[X <: A|B] = X match {
  case A => A
  case B => (x: A|B) => M2[x.type]
}

def f1(x: A|B): M1[x.type] = x match {
  case _: A => A()
  case _: B => (x: A|B) => f2(x)
}

The code above does not compile:

[E043] Type Error: MatchBug2.scala:35:1 
[error] 35 |}
[error]    | ^
[error]    |unreducible application of higher-kinded type M2 to wildcard arguments in subpart M2[? <: A | B] of inferred type 
[error]    |  (x : A | B) match {
[error]    |    case A => A
[error]    |    case B => (x: A | B) => M2[x.type]
[error]    |  }

However, if M2[x.type] is manually expanded and inlined in M1 (as in the commented-out version of M1 above), then no errors are reported.

[ScalaZio]

Although I have been following this bug for 6 months now, I deeply regret I didn't post earlier.
This bug breaks

1. the compositionality of Match types (ie you can not compose one Match type with a nested one)
2. the compositionality of Match types with Dependent types. (ie you can not compose Match types with Dependent types)
3. it breaks the type alias - (that is the assertion that a type alias can be replaced with its definition).

Any one of these are sufficiently serious bugs, that I had expected that it would be dealt with in a week or two as a high priority bug. Six months later, without any obvious progress, I am becoming concerned this this bug has not received the attention it deserves.

A) Can the bug status tag be restored.
B) Can high priority tag be added

C) What further information (if any) is required?
The problem seems clear to me. However,
Martin Odersky writes:
This would need more info to determine whether it's really a bug or whether the reported error is a true one.
to which
Alceste Scalas replies:
I'll be happy to provide more info --- just let me know what I can do :-)
Martin Odersky didn't reply to this, to say what information he would like.

Firstly this is a definitely a bug.
I have stated above three breaks from the expected behavior of Scala 3, each of which are serious bugs.
I have explored with Scalas a number of nuances, when Match types can be nested, and when bug 9999 prevents them from being nested, when type alias work with match types and when not.
There is also the issue of Match types not providing case specific type restriction. However this is a question of deductive power, not correctness, while the three bugs above break correctness.
And these basic breaks are clear from the examples above.
I, Alceste and the others with this problem can provide you further examples. However, Alceste has provided clearest, most minimal examples I can think of. I trust they make the problem as clear to you as they do to me.

Thanks
Peter

[ScalaZio]

I thought I would make one further comment regarding priority.
I aware of several projects with people in at least 8 countries (Australia, Denmark, UK, Jordan, India, US, Sweden, Turkey) who are concerned about this bug, or have projects that are blocked by this bug.
However this most important to me is the work that Alceste has pioneered bring behavior types (like session types) to Scala 3 and ZIO. This requires multiple nested Match types.

This is the type of bug that passes unit testing of atomic features, but is exposed when those features are composed into a larger application. As soon as more people develop larger applications with Scala3, I expect there will be far more complaints about this bug.

[smarter]

Six months later, without any obvious progress, I am becoming concerned this this bug has not received the attention it deserves.

Attention is a finite resource: over the last month alone, about 150 new issues were created and the same number of issues (both old and new) were closed, so it's inevitable that things slip through, especially if they're not straight-forward. So yes, if you think an issue is important it's not a bad idea to leave a comment explaining why to raise awareness about it.

[odersky]

Thanks for the detailed reports. I believe I was able to fix this.