{-# LANGUAGE GADTs, DataKinds #-} 

module Main where

import Data.Kind

data Nat = Z | S Nat

data Vec (n :: Nat) (a :: Type) :: Type where 
  VNil :: Vec Z a
  (:::) :: a -> Vec n a -> Vec (S n) a

vToList :: Vec n a -> [a]
vToList VNil = []
vToList (a ::: as) = a : vToList as

data AVec a = forall n. AV (Vec n a)

toList :: AVec a -> [a]
toList (AV v) = vToList v

bad :: AVec Int
bad = case bad of (AV v) -> AV (1 ::: v)

main :: IO ()
main = print (take 10 (toList bad))