A match type cannot be used as the result type of a pattern match involving extractor patterns

[johnynek]

using scala 3.0.0

the following code compiles:

package example    
    
sealed trait Nat     
case object Zero extends Nat    
case class Succ[N <: Nat](n: N) extends Nat       
                
type Inc[N <: Nat] <: Nat =                
  N match {     
    case Zero.type => Succ[Zero.type]    
    case Succ[n] => Succ[Inc[n]]    
  }             
                
object Nat {    
  def inc[N <: Nat](n: N): Inc[N] =
    n match {    
      case _: Zero.type => Succ(Zero)                                      
      case s: Succ[a] => Succ(inc(s.n))                     
    }                                 
}   

but if I change def inc to:

object Nat {    
  def inc[N <: Nat](n: N): Inc[N] =           
    n match {    
      case Zero => Succ(Zero)                                              
      case s @ Succ(_) => Succ(inc(s.n))                    
    }                                 
}     

I get:

[error] -- [E007] Type Mismatch Error: /Users/oboykin/oss_code/scala3_examples/src/main/scala/Nat.scala:16:23 
[error] 16 |      case Zero => Succ(Zero)
[error]    |                   ^^^^^^^^^^
[error]    |Found:    example.Succ[example.Zero.type]
[error]    |Required: example.Inc[N]
[error]    |
[error]    |where:    N is a type in method inc with bounds >: (?1 : example.Zero.type) and <: example.Nat
[error] -- [E007] Type Mismatch Error: /Users/oboykin/oss_code/scala3_examples/src/main/scala/Nat.scala:17:30 
[error] 17 |      case s @ Succ(_) => Succ(inc(s.n))
[error]    |                          ^^^^^^^^^^^^^^
[error]    |Found:    example.Succ[example.Inc[N$1]]
[error]    |Required: example.Inc[N]
[error]    |
[error]    |where:    N   is a type in method inc with bounds >: (?2 : example.Succ[N$1]) and <: example.Nat
[error]    |          N$1 is a type in method inc with bounds <: example.Nat
[error] two errors found

I don't see how, for a sealed trait there is any difference in these matches. And since they should match the exact same values, why can't the compiler typecheck the second version, which is more natural.

This is very related to a previous bug report: #6709

[johnynek]

put another way case Zero matching should imply that N =:= Zero.type but it seems the type checker does not know that. I have to explicitly match on type to prove that. For a sealed trait, it seems like it should know that. Similarly, it should know that if Succ(_) matches n: N then N =:= Succ[N1] for some N1 <: Nat.

[smarter]

This is a missing feature, not a bug, the rules under which a pattern match can be typed with a match type are detailed in http://dotty.epfl.ch/docs/reference/new-types/match-types.html#dependent-typing which says in particular:

The match expression patterns are all Typed Patterns

So extractor patterns are not supported.

[johnynek]

@smarter can't complete adt matches like this be rewritten as a typed-pattern by the compiler? Is there some subtlety I'm missing, or is it just something that hasn't been implemented yet?

[smarter]

A lot of things can be implemented given enough time and energy, but I'll let @OlivierBlanvillain comment on the specifics :). I'll note that we only rewrite extractor patterns into type tests in the PatternMatcher phase which happens after typechecking. And the code that is of interest here is https://github.com/lampepfl/dotty/blob/a059dbc4c8185fecd003857e9d88c3ff43306322/compiler/src/dotty/tools/dotc/typer/Typer.scala#L1486-L1509 which does mention that this could be extended, so patches welcome I guess!

[OlivierBlanvillain]

This is something that's on the roadmap (but lower priority than bug fixing). Your use case should be straightforward to support because Succ's unapply method already contains enough information to conclude that case Succ(_) translate to a type test pattern:

// parts of what comes out of `case class Succ[N <: Nat](n: N) extends Nat`
object Succ {
  def unapply(x$1: Succ): Succ = x$1
}