Why this typecheck fails? (scala.compiletime.ops.int)

Question

I was making a own fixed-size vector class and this code was rejected

import scala.compiletime.ops.int._

enum Tensor1[Dim <: Int, +T]:
  case Empty extends Tensor1[0, Nothing]
  case Cons[N <: Int, A](head: A, tail: Tensor1[N, A]) extends Tensor1[S[N], A]

  def ::[SuperT >: T](operand: SuperT): Tensor1[Dim + 1, SuperT] = Cons(operand, this)

with this message:

[error] Tree: Tensor1.Cons.apply[Dim, SuperT](operand, this)
[error] I tried to show that
[error]   Tensor1.Cons[Dim, SuperT]
[error] conforms to
[error]   Tensor1[Dim + (1 : Int), SuperT]
[error] but the comparison trace ended with `false`:

but when I changed Dim + 1 to S[Dim] in definition of ::, it works.

  def ::[SuperT >: T](operand: SuperT): Tensor1[S[Dim], SuperT] = Cons(operand, this)

Why this happens? Are S and + 1 different?

Answer 1

Yes, S and + 1 are indeed different.

type S[N <: Int] <: Int

type +[X <: Int, Y <: Int] <: Int

They are implemented in compiler internals.

Scala is not an actual theorem prover. It allows you to prove theorems but doesn't prove theorems for you. Scala knows that 10 + 1 or 1 + 10 are S[10] but doesn't know that n + 1 or 1 + n are S[n]

summon[10 + 1 =:= S[10]] //compiles
summon[1 + 10 =:= S[10]] //compiles

type n <: Int
//summon[n + 1 =:= S[n]] // doesn't compile
//summon[1 + n =:= S[n]] // doesn't compile

Even when S and + are implemented inductively

sealed trait Nat
class S[N <: Nat] extends Nat
object _0 extends Nat
type _0 = _0.type
type _1 = S[_0]

type +[N <: Nat, M <: Nat] = N match
  case _0 => M
  case S[n] => S[n + M]

it's obvious that _1 + n =:= S[n] but not obvious that n + _1 =:= S[n] (this is a theorem to be proved)

type n <: Nat
summon[_1 + n =:= S[n]] // compiles
//summon[n + _1 =:= S[n]] // doesn't compile

If you define addition inductively with respect to the 2nd argument

type +[N <: Nat, M <: Nat] = M match
  case _0 => N
  case S[m] => S[N + m]

then vice versa n + _1 =:= S[n] becomes obvious but _1 + n =:= S[n] has to be proved

//summon[_1 + n =:= S[n]] // doesn't compile
summon[n + _1 =:= S[n]] // compiles

How to define induction on natural numbers in Scala 2.13?