Sort of reminds me of implementing multiplication in the type system of TypeScript with Peano arithmetic - endless recursion limit errors of Succ<Succ<Succ<Succ

Sort of reminds me of implementing multiplication in the type system of TypeScript with Peano arithmetic - endless recursion limit errors of Succ<Succ<Succ<Succ<Zero>>>>... Never did get it to work properly :(