Proofs involving conversion from and to length-indexed vectors

FromToVec.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module FromToVec where

import Data.Kind
import Data.Type.Equality

type Sing :: k -> Type
type family Sing

type SList :: [a] -> Type
data SList l where
  SNil :: SList '[]
  (:%) :: Sing x -> SList xs -> SList (x : xs)
type instance Sing @[a] = SList

type Nat :: Type
data Nat where
  Z :: Nat
  S :: Nat -> Nat

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

type SVec :: Vec a n -> Type
data SVec v where
  SVNil :: SVec VNil
  (:%>) :: Sing x -> SVec xs -> SVec (x :> xs)
type instance Sing @(Vec a n) = SVec

type FromVec :: Vec a n -> [a]
type family FromVec v where
  FromVec VNil      = '[]
  FromVec (x :> xs) = x : FromVec xs

type Len :: [a] -> Nat
type family Len l where
  Len '[]      = Z
  Len (_ : xs) = S (Len xs)

type ToVec :: forall a. forall (l :: [a]) -> Vec a (Len l)
type family ToVec l where
  ToVec '[]      = VNil
  ToVec (x : xs) = x :> ToVec xs

fromToVec :: forall a (l :: [a]).
             SList l -> FromVec (ToVec l) :~: l
fromToVec SNil = Refl
fromToVec (_ :% sxs)
  | Refl <- fromToVec sxs
  = Refl

toFromVec :: forall a n (v :: Vec a n).
             SVec v -> ToVec (FromVec v) :~~: v
toFromVec SVNil = HRefl
toFromVec (_ :%> sxs)
  | HRefl <- toFromVec sxs
  = HRefl