[Haskell-cafe] Is it possible to do type-level arithmetic without UndeciableInstances?

[Ryan Ingram]

> {-# LANGUAGE TypeFamilies #-}
> module PeanoArith

> data Z = Z
> data S n = S n

So, this type family works just fine:

> type family Plus a b
> type instance Plus Z b = b
> type instance Plus (S a) b = S (Plus a b)

As does this one:

> type family Minus a b
> type instance Minus a Z = Z
> type instance Minus Z (S b) = Z
> type instance Minus (S a) (S b) = Minus a b

But this one doesn't work without UndecidableInstances:

> type family Times a b
> type instance Times Z b = Z
> type instance Times (S a) b = Plus b (Times a b)

I tried several different implementations for Times but I was unable
to come up with one that passed the type family termination checker.
Is there a way to do so?

Some examples of attempts:

> -- (a+1)*(b+1) = ab + a + b + 1
> type family Times1 a b
> type instance Times1 Z Z = Z
> type instance Times1 (S n) Z = Z
> type instance Times1 Z (S n) = Z
> type instance Times1 (S a) (S b) = S (Plus (Times1 a b) (Plus a b))

> -- inline Plus
> type family Times2_H a b acc
> type Times2 a b = Times2_H a b Z
> type instance Times2_H a b (S acc) = S (Times2_H a b acc)
> type instance Times2_H Z b Z = Z
> type instance Times2_H (S a) b Z = Times2_H a b b

Do you have any other ideas?  Is (a*b) too big for the termination
checker to ever accept?

  -- ryan