[Haskell] Type-Level Naturals Like Prolog?

[Jared Warren]

Haskell's type checking language is a logical programming language.
The canonical logical language is Prolog. However, Idealised Prolog
does not have data structures, and does Peano numbers like:

  natural(zero).
  natural(x), succ(x,y) :- natural(y)

And I believe (but cannot confirm):

  succ(zero,y).
  succ(x,y) :- succ(y,z)

Why can't Haskell (with extensions) do type-level Peano naturals in
the same fashion? The code would be something like:

> data Zero
>
> class Natural x where
> 	toInt :: x -> Integer
> instance Natural Zero where
> 	toInt _ = 0
> instance (Natural x, Succ x y) => Natural y where
> 	toInt y = undefined + 1
>
> class Succ x y
> instance Succ Zero y
> instance Succ x y => Succ y z
>
> zero = toInt (undefined :: Zero) -- THIS SUCCEEDS
>
> one = toInt (undefined :: (Succ Zero x) => x) -- THIS FAILS

Thanks,
Jared Warren