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?
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