Match type fails to reduce when it doesn't look like it needs to reduce

[s5bug]

Compiler version

3.3.3
3.4.2
3.5.0-RC7

Minimized code

enum Typ {
  case Fun[L <: Typ, R <: Typ](l: L, r: R)
}

enum Expr[T <: Typ] {
  case Fun[L <: Typ, R <: Typ](body: Expr[R]) extends Expr[Typ.Fun[L, R]]
}

type Interpreted[T <: Typ] = T match {
  case Typ.Fun[l, r] => Function1[Interpreted[l], Interpreted[r]]
}

def interpret[T <: Typ](e: Expr[T]): Interpreted[T] = e match {
  case f: Expr.Fun[l, r] =>
    (i: Interpreted[l]) => interpret(f.body)
}

Output

-- [E007] Type Mismatch Error: -------------------------------------------------
3 |    (i: Interpreted[l]) => interpret(f.body)
  |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |Found:    Interpreted[l] => Interpreted[r]
  |Required: Interpreted[T]
  |
  |where:    T is a type in method interpret which is an alias of Typ.Fun[l, r]
  |          l is a type in method interpret with bounds <: Typ
  |          r is a type in method interpret with bounds <: Typ
  |
  |
  |Note: a match type could not be fully reduced:
  |
  |  trying to reduce  Interpreted[l]
  |  failed since selector l
  |  does not match  case Typ.Fun[l, r] => Interpreted[l] => Interpreted[r]
  |  and cannot be shown to be disjoint from it either.
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: {
  |   def $anonfun(i: Interpreted[l]): Interpreted[r] =
  |     {
  |       interpret[r](f.body)
  |     }
  |   closure($anonfun)
  | }
  | I tried to show that
  |   Interpreted[l] => Interpreted[r]
  | conforms to
  |   Interpreted[T]
  | but none of the attempts shown below succeeded:
  |
  |   ==> Interpreted[l] => Interpreted[r]  <:  Interpreted[T]
  |     ==> Interpreted[l] => Interpreted[r]  <:  T match {
  |    case Typ.Fun[l, r] => Interpreted[l] => Interpreted[r]
  |  }  = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------
1 error found

Expectation

I would want to believe that the knowledge of T is a type in method interpret which is an alias of Typ.Fun[l, r] would cause the trace to be the following:

 ==> Interpreted[l] => Interpreted[r]  <:  Interpreted[T]
   ==> Interpreted[l] => Interpreted[r]  <:  T match {
  case Typ.Fun[l, r] => Interpreted[l] => Interpreted[r]
}
     ==> Interpreted[l] => Interpreted[r] <: Interpreted[l] => Interpreted[r]

Otherwise I don't see how it's possible to create a lambda for Interpreted[l] => Interpreted[r]/how to use Interpreted[l] as a parameter type.

[nrinaudo]

I'd really like to get some confirmation that this is indeed a bug, if possible. A fix would be lovely, of course, but that's a lot more work and uncertainty.

But knowing whether it's a bug allows me to move forward:

• if it is, I can work around it with a well placed asInstanceOf and a comment to revisit with later versions of the compiler that might fix it.
• if it's not, I need to find a different encoding.

For example, something that I've confirmed to work even if heavier and more cumbersome would be to use a GADT to allow the compiler to get its types right:

enum TypeRepr[A <: Typ]:
  case Fun[L <: Typ, R <: Typ](l: TypeRepr[L], r: TypeRepr[R]) extends TypeRepr[Typ.Fun[L, R]]

case class Result[A <: Typ](value: Interpreted[A], repr: TypeRepr[A])

[sjrd]

This looks more related to GADT handling than to match types per se. Unless it's some unfortunate interaction between match types and GADT handling.

I'm not familiar enough with what GADT support is supposed to handle. Perhaps @dwijnand can chime in?

[nrinaudo]

I don't think it is - the issue really is match types failing to, well, match - but I also don't have your expertise on the compiler, so my intuition might be very wrong.

But what I'm really asking is: should the compiler be able to work the match type out, or am I placing unreasonable expectations on it? I'm perfectly ok with working around a current limitation of the compiler, or to find a different encoding, I just would like to know which one I must do :)

[sjrd]

It's related to GADTs because T is declared as basically unconstrained. So clearly, Interpreted[T] cannot reduce as such. T only becomes "better" thanks to GADT reasoning, because we happened to match on a thing of type Expr[T] and therefore learned something more about T that we don't know just by looking at its declaration.

[dwijnand]

Perhaps @dwijnand can chime in?

Tried to look fast, but I need to look slower - I'll try to get to this this week.

[nrinaudo]

Oh - would there be a way to constrain it (more than "must be a subtype of Typ", which is already there) that would make this work?

[dwijnand]

We track the gadt info in the reductionContext (via contextInfo), but then we don't use it for the scrutinee. Something like

-                cmp.matchCases(scrutinee.normalized, cases.map(MatchTypeCaseSpec.analyze))
+                val scrut =
+                  scrutinee.tryNormalize.orElse:
+                    scrutinee match
+                      case tp: TypeRef =>
+                        ctx.gadt.bounds(tp.symbol) match
+                          case TypeAlias(alias) => alias
+                          case _ => tp
+                      case tp => tp
+                cmp.matchCases(scrut, cases.map(MatchTypeCaseSpec.analyze))

seems to fix the test case, but I haven't taken it further than that.

[nrinaudo]

Oh. Regardless of when this happens, can I understand this to mean that this is indeed a bug, my design is sound and the compiler will eventually handle it as it should?

If so that is great news, thanks for taking the time to review!