[Haskell-cafe] (Lazy) SmallCheck and peano numbers

[Levi Stephen]

Hi,

I have the following definitions

type Zero
type Succ a

so that I can muck around with a Vector type that includes its length
encoded in its type.

I was wondering whether it was possible to use SmallCheck (or
QuickCheck) to generate random Peano numbers? Is there an issue here
in that what I actually want to generate is a type rather than a
value?

I do have

reifyInt :: Int -> (forall a. ReflectNum a => a -> b) -> b

but, I'm not sure if this can help me when I need to generate other
values based upon that type (e.g., two vectors with the same size
type)

Thanks,
Levi