GitLab

Using the solution codes, I got add(S(Z), S(S(Z))) // : S[S[Nat]] = S(S(Z)). It's not right, isn't it?

To figure out this problem, I added a new given instance given succZ: S[Z] = S(Z), and the compiler told me:

ambiguous implicit arguments of type App.this.Sum[App.this.S[App.this.Z.type], 
  App.this.S[App.this.S[App.this.Z.type]]
, App.this.Nat] found for parameter sum of method add in class App.
I found:
    this.sumS[N, App.this.S[App.this.S[App.this.Z.type]], R](
      this.sumZ[App.this.S[App.this.S[App.this.Z.type]]](
        this.succ[App.this.S[App.this.Z.type]](
          /* ambiguous: both given instance succZ in class App and given instance zero in class App match type App.this.S[App.this.Z.type] */
            summon[App.this.S[App.this.Z.type]]
        )
      )
    )
But both given instance succZ in class App and given instance zero in class App match type App.this.S[App.this.Z.type].mdoc

So the compiler regards zero and succZ the same.

Why does it believe Z is the same as S[Z]? And this leads to the wrong answer for add(S(Z), S(S(Z)))?

Thanks in advance.