Exercise Session 8, question 2
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.