Issue with bounded recursive match types

[SimonGuilloud]

Compiler version

3.3.1

Minimized example

trait A[N]

type B[N] <: A[N] = N match {
  case 0 => A[0]
  case _ => A[N]
}

Output

Found:    A[(0 : Int)]
Required: A[N]

Expectation

It seems like this should compile. I'm not sure if this is a bug or intended behaviour, but I found no reference to this situation. A real life scenario would have for example a trait A0 extending A[0].

[sjrd]

There is no GADT reasoning inside match types. So no, this does not compile.

[SimonGuilloud]

OK! But what is the GADT (or even ADT) in this example? It rather seems to me the issue is that there is no reasoning about the value of N in individual branch.
Is there a way to force this to compile, (something like asInstanceOf for types)?

[dwijnand]

GADT reasoning is the name for any subtyping constraints that are learnt from a match case (more rarely also referred to as "subtype reconstruction"). Here, it's recording that N <: 0, which we don't do at the moment. Doing so is an enhancement/request.

You can force this to compile by intersecting the type you wanted to return with the bound you have. So, in the minimisation, A[0] & A[N].

[SimonGuilloud]

GADT reasoning is the name for any subtyping constraints that are learnt from a match case (more rarely also referred to as "subtype reconstruction"). Here, it's recording that N <: 0, which we don't do at the moment. Doing so is an enhancement/request.

You can force this to compile by intersecting the type you wanted to return with the bound you have. So, in the minimisation, A[0] & A[N].

Great, thanks for the explanation!

[Linyxus]

I guess we could close this as not planned?

[smarter]

There is no GADT reasoning inside match types.

There is some common logic since #14563 which recently lead to #20032

[Linyxus]

It seems that this minimisation should not compile. In the match case the constraint we get is N <: 0 but to type check the body the required constraint is 0 <: N, which we cannot prove anyway.

WDYT? @dwijnand

[dwijnand]

Hmm, perhaps. On the other hand 0 is a singleton (as well as Int being final), which I mention because those are criteria in refinementIsInvariant. But ultimately I think you're right, if we call B[0 & Other] it's just a bounds violation to return A[0].