[Haskell-cafe] Type-level naturals & multiplication

[Brad Larsen]

Suppose we implement type-level naturals as so:

data Zero
data Succ a

Then, we can reflect the type-level naturals into a GADT as so (not
sure if ``reflect'' is the right terminology here):

data Nat :: * -> * where
  Zero :: Nat Zero
  Succ :: Nat a -> Nat (Succ a)

Using type families, we can then proceed to define type-level addition:

type family Add a b :: *
type instance Add Zero b = b
type instance Add (Succ a) b = Succ (Add a b)

Is there any way to define type-level multiplication without requiring
undecidable instances?

Sincerely,
Brad