Peano arithmetic at compile time Peano numbers represent nonnegative integers as zero or successors of other Peano numbers. For example, 1 would be represented as Succ(Zero) and 3 would be Succ(Succ(Succ(Zero))).
Task
Implement the following operations on Peano numbers, at compile time:

Addition
Subtraction - You will never be required to subtract a greater number from a smaller one.
Multiplication
Division - You will never be required to divide two numbers if the result will not be an integer.

Input/Output
The input and output formats do not have to be the same, but they should be one of these:

A type constructor of kind * -&gt; * to represent S and a type of kind * to represent Z, e.g. S&lt;S&lt;Z&gt;&gt; to represent 2 in Java or int[][] (int for 0, [] for S).
A string with a Z at the middle and 0 or more S(s and )s around it, e.g. &quot;S(S(Z))&quot; to represent 2.
Any other format resembling Peano numbers, where there is a value representing zero at the bottom, and another wrapper that can contain other values.

Rules

You may use type members, implicits, type constructors, whatever you want, as long as a result can be obtained at compile time.
For the purposes of this challenge, any execution phase before runtime counts as compile time.
Since answers must work at compile-time, answers must be in compiled languages. This includes languages like Python, provided you can show that the bytecode contains the result of your computation before you even run the code.
This is code-golf, so shortest code in bytes wins!

Example for just addition in Scala
sealed trait Num {
  //This is like having a method `abstract Num plus(Num n);`
  type Plus[N &lt;: Num] &lt;: Num
}
object Zero extends Num {
  //When we add any n to zero, it's just that n again
  type Plus[N &lt;: Num] = N
}
final class Succ[N &lt;: Num](n: N) extends Num {
  //In Java: `Num plus(Num x) { return new Succ(n.plus(x)) }
  type Plus[X &lt;: Num] = Succ[N#Plus[X]]
}

Usage (Scastie):
//This is just for sugar
type +[A &lt;: Num, B &lt;: Num] = A#Plus[B]

type Zero = Zero.type
type Two = Succ[Succ[Zero]]
type Three = Succ[Two]
type Five = Succ[Succ[Three]]
val five: Five = null
val threePlusTwo: Three + Two = five
val notFivePlusTwo: Five + Two = five //should fail
val zeroPlusFive: Zero + Five = five

Test cases
S is used for successors and Z is used for zero.
S(S(S(Z))) + Z = S(S(S(Z)))                 | 3 + 0 = 3
S(S(Z)) + S(S(S(Z))) = S(S(S(S(S(Z)))))     | 2 + 3 = 5
S(S(S(Z))) - S(S(S(Z))) = Z                 | 3 - 3 = 0
S(S(Z)) * S(S(S(Z))) = S(S(S(S(S(S(Z))))))  | 2 * 3 = 6
S(S(S(S(Z)))) / S(S(Z)) = S(S(Z))           | 4 / 2 = 2
Z / S(S(Z)) = Z                             | 0 / 2 = 0

Some links to help you get started

Type-Level Programming in Scala (a bunch of articles, including ones about Peano arithmetic) (for Scala)
Multiplication at compile time (for Scala)
Peano arithmetic in C++ type system (for C++)
Type arithmetic (for Haskell)
CP-1610 assembly, 37 bytes
This is simply using macro expansion.
Z EQU 0
MACRO S(n)
(%n%+1)
ENDM
 DCW [expression]

Example
With the expression S(S(Z)) * S(S(S(Z))), this gets compiled as:
00000000 Z                          
0x0                             Z EQU 0
                                MACRO S(n)
                                (%n%+1)
                                ENDM
                                ;DCW S(S(Z)) * S(S(S(Z)))
                                ;DCW (S(Z)+1) * S(S(S(Z)))
                                ;DCW ((Z+1)+1) * S(S(S(Z)))
                                ;DCW ((Z+1)+1) * (S(S(Z))+1)
                                ;DCW ((Z+1)+1) * ((S(Z)+1)+1)
0000   0006                      DCW ((Z+1)+1) * (((Z+1)+1)+1)
 ERROR SUMMARY - ERRORS DETECTED 0
               -  WARNINGS       0

(compiled with as1600 from the SDK included with jzIntv)