Interpreted arithmetic
130 121 bytes

-9 bytes thanks to Ørjan Johansen



type family a+b where s a+b=a+s b;z+b=b
type family a*b where s a*b=a*b+b;z*b=z
class(a#b)c|a b-&gt;c
instance a*b~c=&gt;(a#b)c


Try it online!

This defines closed type families for addition (+) and multiplication (*). Then a type class (#) is defined that uses the (*) type family along with an equality constraint to convert from the world of type familes to the world of typeclass prolog.