Peano 数字类型级实现适用于类，但不适用于特征

如何解决Peano 数字类型级实现适用于类，但不适用于特征

以下使用匹配类型对 Peano 数字进行减法的类型级实现有效

sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type _1 = S[O]
type _2 = S[_1]
type _3 = S[_2]

type minus[a <: Nat,b <: Nat] = (a,b) match
  case (O,_) => O
  case (S[n],O) => a
  case (S[n],S[m]) => n minus m

type x = _2 minus _1
summon[x =:= _1]
// val res0: S[O] =:= S[O] = generalized constraint

但是如果类被更改为特征

trait O extends Nat
trait S[N <: Nat] extends Nat

那它为什么not有效

scala> type x = _2 minus _1
// defined alias type x = minus[_2,_1]

scala> summon[x =:= _1]
1 |summon[x =:= _1]
  |                ^
  |                Cannot prove that x =:= _1.