Correlating match types with pattern matching expressions

[johnynek]

I've been trying to use match types to implement a type-level binary nat type.

Here is the code I would ideally like to work:

object Main {

  enum BinNat {
    case Zero
    // 2n + 1
    case Odd[N <: BinNat](n: N)
    // 2(n + 1)
    case Even[N <: BinNat](n: N)
  }

  import BinNat._

  type Inc[N <: BinNat] <: BinNat =
    N match {
      case Zero.type => Odd[Zero.type]
      case Odd[n] => Even[n]
      case Even[n] => Odd[Inc[n]]
    }

  def inc(b: BinNat): Inc[b.type] =
    b match {
      case Zero => Odd(Zero)
      case Odd(n) => Even(n)
      case Even(n) =>
        // 2(n + 1) + 1 = 2(inc(n)) + 1
        Odd(inc(n))
    }
}

The error message I get is:

[error] -- [E007] Type Mismatch Error: /Users/oscar/oss/dotty_tests/src/main/scala/Main.scala:30:22                                                                                     
[error] 30 |      case Zero => Odd(Zero)
[error]    |                   ^^^^^^^^^
[error]    |                   Found:    Main.BinNat
[error]    |                   Required: Main.Inc[Main.BinNat(b)]
[error] -- [E007] Type Mismatch Error: /Users/oscar/oss/dotty_tests/src/main/scala/Main.scala:31:25                                                                                     
[error] 31 |      case Odd(n) => Even(n)
[error]    |                     ^^^^^^^
[error]    |                     Found:    Main.BinNat
[error]    |                     Required: Main.Inc[Main.BinNat(b)]
[error] -- [E007] Type Mismatch Error: /Users/oscar/oss/dotty_tests/src/main/scala/Main.scala:34:11                                                                                     
[error] 34 |        Odd(inc(n))
[error]    |        ^^^^^^^^^^^
[error]    |        Found:    Main.BinNat
[error]    |        Required: Main.Inc[Main.BinNat(b)]
[error] three errors found

I have tried several different variants (using manual sealed trait/case classes, matching on _: Zero.type, explicitly adding type annotations in the def inc method... each seemed to trigger different errors and I couldn't find any that worked.

expectation

I'd like it to compile, or suggest a better action to take in the error message

[smarter]

Using enum cases isn't going to work here: the companion objects of enums have an apply method whose result type is the type of the enum, so Odd(Zero) will always have type BinNat, this is the behavior people usually want for ADT (e.g. so that def x = Some(1) return an Option[Int] and not a Some[Int]), but it's clearly not what you want here. You can always get a more precise type by using the class constructor of the enum case instead (new Odd(Zero)), but it isn't in the spirit of enums.

Anyway, if we do this replacement in your code, then we get the following errors:

22 |      case Zero => new Odd(Zero)
   |                   ^^^^^^^^^^^^^
   |                   Found:    Main.BinNat.Odd[Main.BinNat]
   |                   Required: Main.Inc[Main.BinNat(b)]
23 |      case Odd(n) => new Even(n)
   |                     ^^^^^^^^^^^
   |        Found:    Main.BinNat.Even[N$1]
   |        Required: Main.Inc[Main.BinNat(b)]
   |
   |        where:    N$1 is a type in method inc with bounds <: Main.BinNat
26 |        new Odd(inc(n))
   |        ^^^^^^^^^^^^^^^
   |        Found:    Main.BinNat.Odd[Main.BinNat]
   |        Required: Main.Inc[Main.BinNat(b)]

So the compiler isn't able to figure out that Inc[b.type] is equivalent to Inc[Zero.type] in the first case and so on. @AleksanderBG: Should our GADT support be capable of handling this ?

[abgruszecki]

@smarter Not by itself, no, even if we extend it. We could (and at one point wanted to) allow adding GADT constraints to singleton types such as b.type. With this tweak, looking at the second branch of inc, we would know that b.type <: Odd[N] for some pattern-bound type N <: BinNat. At this point, we're trying to return an Even[n.type] when we promised to return an Inc[b.type]. If match types could reduce based on GADT constraints (which I'm not sure they do #6687), we could at this point reduce Inc[b.type] to Even[Inc[N]]. However, this is still not guaranteed to be the same as Even[Inc[n.type]], because N could be BinNat.

I'd say the final missing piece is that we should redefine Even[N <: BinNat] to instead be Even[N <: BinNat & Singleton], and we should know that if n: N and N <: Singleton, then n.type = N (potentially type comparer already knows this?), and we should be able to figure out that A = B implies Inc[A] = Inc[B] even if we cannot reduce either Inc[A] or Inc[B].

To sum up, we need:

1. GADT constraints on singleton types
2. Match types reducing based on GADT constraints (not sure if they do, see Implement memoization #6887)
3. Potentially additional logic in TypeComparer?

/cc @OlivierBlanvillain

[abgruszecki]

Actually: @OlivierBlanvillain, do you see an alternative way forward with the "matching cases" logic that you at one point proposed for typing functions returning match types?