{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}
 
import Data.List
 
data Peano = Zero | Successor Peano
 
data Vector peanoNum someType where
    Nil :: Vector Zero someType
    (:+) :: someType -> Vector num someType -> Vector (Successor num) someType
 
infixr 5 :+ 
 
type family Iterate peanoNum constructor someType where
    Iterate Zero cons typ = typ
    Iterate (Successor pn) cons typ = 
        cons (Iterate pn cons typ)
 
showIter :: Vector n a -> Iterate n [] Double -> String
showIter  Nil      d  = show d
showIter (x :+ xs) ds = "[" ++ intercalate ", " (map (showIter xs) ds) ++ "]"
 
main = print $ showIter (undefined :+ undefined :+ Nil) [[1, 2], [4, 5, 6], [7]]

ey0jIExBTkdVQUdFIEdBRFRzLCBEYXRhS2luZHMsIFR5cGVGYW1pbGllcyAjLX0KCmltcG9ydCBEYXRhLkxpc3QKCmRhdGEgUGVhbm8gPSBaZXJvIHwgU3VjY2Vzc29yIFBlYW5vCgpkYXRhIFZlY3RvciBwZWFub051bSBzb21lVHlwZSB3aGVyZQogICAgTmlsIDo6IFZlY3RvciBaZXJvIHNvbWVUeXBlCiAgICAoOispIDo6IHNvbWVUeXBlIC0+IFZlY3RvciBudW0gc29tZVR5cGUgLT4gVmVjdG9yIChTdWNjZXNzb3IgbnVtKSBzb21lVHlwZQogICAgCmluZml4ciA1IDorIAoKdHlwZSBmYW1pbHkgSXRlcmF0ZSBwZWFub051bSBjb25zdHJ1Y3RvciBzb21lVHlwZSB3aGVyZQogICAgSXRlcmF0ZSBaZXJvIGNvbnMgdHlwID0gdHlwCiAgICBJdGVyYXRlIChTdWNjZXNzb3IgcG4pIGNvbnMgdHlwID0gCiAgICAgICAgY29ucyAoSXRlcmF0ZSBwbiBjb25zIHR5cCkKICAgICAgICAKc2hvd0l0ZXIgOjogVmVjdG9yIG4gYSAtPiBJdGVyYXRlIG4gW10gRG91YmxlIC0+IFN0cmluZwpzaG93SXRlciAgTmlsICAgICAgZCAgPSBzaG93IGQKc2hvd0l0ZXIgKHggOisgeHMpIGRzID0gIlsiICsrIGludGVyY2FsYXRlICIsICIgKG1hcCAoc2hvd0l0ZXIgeHMpIGRzKSArKyAiXSIKCm1haW4gPSBwcmludCAkIHNob3dJdGVyICh1bmRlZmluZWQgOisgdW5kZWZpbmVkIDorIE5pbCkgW1sxLCAyXSwgWzQsIDUsIDZdLCBbN11d