Vec.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Main where

import Data.Kind
import Data.Nat
import Data.Singletons
import Data.Type.Equality
import Unsafe.Coerce
import Prelude hiding (reverse)

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

infixr 5 :>

deriving stock instance Show a => Show (Vec n a)

mPlusZero :: forall (m :: Nat). Sing m -> m `NatPlus` Z :~: m
mPlusZero SZ = Refl
mPlusZero (SS n) = case mPlusZero n of Refl -> Refl

mPlusSucc :: forall (n :: Nat) (m :: Nat). Sing m -> (m `NatPlus` S n) :~: S (m `NatPlus` n)
mPlusSucc SZ = Refl
mPlusSucc (SS m') = case mPlusSucc @n m' of Refl -> Refl

reverse :: Vec n a -> Vec n a
reverse ys = go SZ Nil ys
  where
    go :: forall m p a. Sing m -> Vec m a -> Vec p a -> Vec (m `NatPlus` p) a
    go m acc Nil = case mPlusZero m of Refl -> acc
    go m acc (x :> (xs :: Vec p_pred a)) = case mPlusSucc @p_pred m of Refl -> go (SS m) (x :> acc) xs

main :: IO ()
main = print $ reverse $ 'a' :> 'b' :> 'c' :> Nil