{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs #-}
{-# LANGUAGE TypeOperators, NPlusKPatterns #-}
{-# LANGUAGE DeriveFoldable, StandaloneDeriving, TypeApplications #-}
{-# LANGUAGE TemplateHaskell #-} 

import Data.Singletons
import Data.Singletons.TH

import Text.Read (readMaybe)
import Data.Kind (Type)
import qualified Data.Foldable as F

data Nat = Z | S Nat deriving Show

intToNat 0 = Z
intToNat (n + 1) = S (intToNat n)

genSingletons [''Nat]

-- генерирует синглетоны для Nat:

-- data instance Sing (n :: Nat) where
--     SZ :: Sing Z
--     SS :: Sing n -> Sing (S n)

-- instance SingKind Nat where
--     type DemoteRep Nat = Nat

--     fromSing SZ = Z
--     fromSing (SS b) = S (fromSing b)

--     toSing Z = SomeSing SZ
--     toSing (S b) = case toSing b :: SomeSing Nat of
--           SomeSing c -> SomeSing (SS c)

data Vect :: Nat -> Type -> Type where
   V0 :: Vect Z x
   (:>) :: x -> Vect n x -> Vect (S n) x

deriving instance Foldable (Vect n) 

infixr 5 :>

getInt :: IO Int
getInt = do
  resp <- getLine
  case readMaybe @Int resp of
     Just value -> pure value
     Nothing -> do
       putStrLn "error"
       getInt

makeVect :: Sing (size :: Nat) -> a -> Vect size a
makeVect SZ _ = V0
makeVect (SS x) v = v :> makeVect x v

zipVect :: Vect size a -> Vect size b -> Vect size (a, b)
zipVect V0 V0 = V0
zipVect (x1 :> v1) (x2 :> v2) = (x1, x2) :> zipVect v1 v2

main :: IO ()
main = do
  putStrLn "Hello world"
  size <- getInt
  -- нету "голых" экзистенциальных типов, 
  -- работать с синглетоном числа придется только в континьюэйшене
  withSomeSing (intToNat size) $ \ssize -> do
    let vect1 = makeVect ssize size
    let vect2 = makeVect ssize "^_^"
    -- let vect2 = makeVect (SS ssize) "^_^" -- вызовет ошибку
    print . F.toList $ vect1
    print . F.toList $ vect2
    print . F.toList $ zipVect vect1 vect2