Interpreted arithmetic A little known fact is that if you turn on enough language extensions (ghc) Haskell becomes a dynamically typed interpreted language!  For example the following program implements addition.

{-# Language MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}

data Zero
data Succ a

class Add a b c | a b -&gt; c
instance Add Zero a a
instance (Add a b c) =&gt; Add (Succ a) b (Succ c)


This doesn't really look like Haskell any more.  For one instead of operating over objects, we operate over types.  Each number is it's own type.  Instead of functions we have type classes. The functional dependencies allows us to use them as functions between types.

So how do we invoke our code? We use another class

class Test a | -&gt; a
 where test :: a
instance (Add (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) a)
  =&gt; Test a


This sets the type of test to the type 4 + 3.  If we open this up in ghci we will find that test is indeed of type 7:

Ok, one module loaded.
*Main&gt; :t test
test :: Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))




Task

I want you to implement a class that multiplies two Peano numerals (non-negative integers).  The Peano numerals will be constructed using the same data types in the example above:

data Zero
data Succ a


And your class will be evaluated in the same way as above as well.  You may name your class whatever you wish.

You may use any ghc language extensions you want at no cost to bytes.

Test Cases

These test cases assume your class is named M, you can name it something else if you would like.

class Test1 a| -&gt;a where test1::a
instance (M (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) a)=&gt;Test1 a

class Test2 a| -&gt;a where test2::a
instance (M Zero (Succ (Succ Zero)) a)=&gt;Test2 a

class Test3 a| -&gt;a where test3::a
instance (M (Succ (Succ (Succ (Succ Zero)))) (Succ Zero) a)=&gt;Test3 a

class Test4 a| -&gt;a where test4::a
instance (M (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))) (Succ (Succ (Succ Zero))) a)=&gt;Test4 a




Results

*Main&gt; :t test1
test1
  :: Succ
       (Succ
          (Succ
             (Succ
                (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))
*Main&gt; :t test2
test2 :: Zero
*Main&gt; :t test3
test3 :: Succ (Succ (Succ (Succ Zero)))
*Main&gt; :t test4
test4
  :: Succ
       (Succ
          (Succ
             (Succ
                (Succ
                   (Succ
                      (Succ
                         (Succ
                            (Succ
                               (Succ
                                  (Succ
                                     (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))


Draws inspiration from Typing the technical interview
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.