A length-indexed list where the length is ad-hoc polymorphic (using singletons)

my-ghc-8.6.2.nix

let
  nixpkgsTarball = builtins.fetchTarball {
    name = "nixos-unstable-2018-11-09";
    url = https://github.com/nixos/nixpkgs/archive/1c49226176d248129c795f4a654cfa9d434889ae.tar.gz;
    sha256 = "0v8vp38lh6hqazfwxhngr5j96m4cmnk1006kh5shx0ifsphdip62";
  };

  nixpkgs = import nixpkgsTarball { };
in

with nixpkgs;

let
  ghc862 =
    haskell.packages.ghc862.override {
      overrides = self: super: {

        singletons = haskell.lib.overrideCabal super.singletons (drv: {
          version = "2.5";
          sha256 = "0bk1ad4lk4vc5hw2j4r4nzs655k43v21d2s66hjvp679zxkvzz44";
        });

        th-desugar = self.callHackage "th-desugar" "1.9" {};
      };
    };

  ghcWithPkgs =
    ghc862.ghcWithPackages (pkgs: with pkgs; [ singletons ]);
in

pkgs.mkShell {
  buildInputs = [ ghcWithPkgs ];
}

polymorphic-length-index.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Coerce
import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits
import Numeric.Natural (Natural)
import Unsafe.Coerce

-- Define a Peano datatype and some helper functions.

$(singletons [d|

  data Peano = Z | S Peano deriving (Eq, Ord, Show)

  addPeano :: Peano -> Peano -> Peano
  addPeano Z a = a
  addPeano (S a) b = S (addPeano a b)

  subtractPeano :: Peano -> Peano -> Peano
  subtractPeano Z _ = Z
  subtractPeano a Z = a
  subtractPeano (S a) (S b) = subtractPeano a b

  multPeano :: Peano -> Peano -> Peano
  multPeano Z _ = Z
  multPeano (S a) b = addPeano (multPeano a b) b

  n0 :: Peano
  n0 = Z

  n1 :: Peano
  n1 = S n0

  n2 :: Peano
  n2 = S n1

  n3 :: Peano
  n3 = S n2

  n4 :: Peano
  n4 = S n3

  n5 :: Peano
  n5 = S n4

  n6 :: Peano
  n6 = S n5

  n7 :: Peano
  n7 = S n6

  n8 :: Peano
  n8 = S n7

  n9 :: Peano
  n9 = S n8

  n10 :: Peano
  n10 = S n9

  instance Num Peano where
    (+) = addPeano

    (-) = subtractPeano

    (*) = multPeano

    abs = id

    signum Z = Z
    signum (S _) = S Z

    fromInteger n = if n == 0 then Z else S (fromInteger (n - 1))

  |])

-- | Create a kind-class for defining the 'ToNat' type family.  This gives us a way
-- to convert an @(n :: k)@ to a Nat.
--
-- Below, we create an instance of it for 'Nat' and 'Peano'.
class (SDecide k, SNum k, PNum k) => PToNat k where
  type family ToNat (n :: k) :: Nat

instance PToNat Nat where
  type ToNat n = n

instance PToNat Peano where
  type ToNat 'Z = 0
  type ToNat ('S n) = 1 + ToNat n

-- | This is quite a complicated kind-class.  It declares the 'VecIdxZero' and
-- 'VecIdxSucc' type families.  These let you figure out what types to use for
-- the \"zero\" and \"succ\" elements for a 'Vec' parameterized by the kind
-- @k@.
--
-- There are instances of this for 'Nat' and 'Peano'.
class
  ( VecIdxZero k ~ FromInteger 0
  , ToNat (VecIdxZero k) ~ 0
  , PToNat k
  , forall (n :: k). (FromInteger 0 + n) ~ n
  ) => VecIdx k where
  type family VecIdxZero k :: k
  type family VecIdxSucc k :: k ~> k

instance VecIdx Nat where
  type VecIdxZero Nat = 0
  -- This is the defunctionalization version of @(+ 1)@.
  type VecIdxSucc Nat = ((+@#@$$) 1)

instance VecIdx Peano where
  type VecIdxZero Peano = 'Z
  -- This is the defunctionalization version of @'S@.
  type VecIdxSucc Peano = TyCon 'S

-- A length-indexed list where the index is polymorphic over the 'VecIdx'
-- kind-class.
data Vec (k :: Type) (n :: k) :: Type -> Type where
  EmptyVec :: Vec k (VecIdxZero k) a
  ConsVec :: a -> Vec k n a -> Vec k (VecIdxSucc k @@ n) a

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

-- Singleton function for 'Vec' indexed by either 'Peano' or 'Nat'.

singletonVecPeano' :: a -> Vec Peano N1 a
singletonVecPeano' a = ConsVec a EmptyVec

singletonVecNat' :: a -> Vec Nat 1 a
singletonVecNat' a = ConsVec a EmptyVec

-- | Super-unsafe axiom that could prove anything.  Use with care.
axiom :: forall a b. a :~: b
axiom = unsafeCoerce (Refl :: Int :~: Int)

-- | This is a proof.  It can be read as follows:
--
-- Given that @n@ is not zero, then @Succ (n - 1) == n@.
proofSubtract1Succ
  :: forall k (n :: k)
   . Refuted (n :~: VecIdxZero k)
  -> ((VecIdxSucc k) @@ (n - FromInteger 1)) :~: n
proofSubtract1Succ _ = axiom

-- These are some simple proofs that say adding 0 to any 'PNum' is the same as
-- doing nothing.

zeroPlusLL :: forall k (n :: k). (PNum k) => (FromInteger 0 + n) :~: n
zeroPlusLL = axiom

zeroPlusLR :: forall k (n :: k). (PNum k) => (n + FromInteger 0) :~: n
zeroPlusLR = axiom

-- | This says that if we know that @Succ n'@ is @n@, then we know that @Succ
-- (n' + m)@ is the same as @n + m@.
succPlus1 :: forall k n n' m. (n ~ (VecIdxSucc k @@ n')) => (VecIdxSucc k @@ (n' + m)) :~: (n + m)
succPlus1 = axiom

-- | This is a proof that addition commutes.
additionCommute :: forall n m. (n + m) :~: (m + n)
additionCommute = axiom

-- | Just like 'replicate' for lists.
replicateVec :: forall k n a. VecIdx k => Sing n -> a -> Vec k n a
replicateVec sn a =
  case sFromInteger (sing @0) of
    zeron ->
      case sn %~ zeron of
        Proved Refl -> EmptyVec
        Disproved notZeroProof ->
          case sFromInteger (sing @1) of
            (onen :: Sing (FromInteger 1 :: k)) ->
              case proofSubtract1Succ notZeroProof of
                Refl -> a `ConsVec` replicateVec (sn %- onen) a

-- | Append two vectors.
appendVec :: forall k n m a. VecIdx k => Vec k n a -> Vec k m a -> Vec k (n + m) a
appendVec EmptyVec vec =
  case zeroPlusLL @k @m of
    Refl -> vec
appendVec vec EmptyVec =
  case zeroPlusLR @k @n of
    Refl -> vec
appendVec (ConsVec a (vecA :: Vec k n' a)) vecB =
  case succPlus1 @k @n @n' @m of
    Refl -> ConsVec a (appendVec vecA vecB)

-- | Zero-cost coercion from one vector type to another.
--
-- In order for this to work, @'ToNat' n@ has to be the same as @'ToNat' m@.
coerceVec
  :: forall (k :: Type) (j :: Type) (n :: k) (m :: j) (a :: Type)
   . ( VecIdx k
     , VecIdx j
     , ToNat n ~ ToNat m
     )
  => Vec k n a
  -> Vec j m a
coerceVec = unsafeCoerce

-- | Test that coercion actually works.
testCoerce :: forall (a :: Type). Vec Peano N5 a -> Vec Nat 5 a
testCoerce = coerceVec

-- | A vector that is polymorphic over the index kind.  We know it is length 3.
testVec1 :: (SingI (FromInteger 3 :: k), VecIdx k) => Vec k (FromInteger 3) String
testVec1 = replicateVec sing "foo"

-- | A vector that is polymorphic over the index kind.  We know it is length 4.
testVec2 :: (SingI (FromInteger 4 :: k), VecIdx k) => Vec k (FromInteger 4) String
testVec2 = replicateVec sing "bar"

-- | Test appending 'testVec1' and 'testVec2' together.
testAppVec :: Vec Peano N7 String
testAppVec = appendVec testVec1 testVec2

-- | Show how we can polymorphically append one element to a vec.
test
  :: forall k n
   . (VecIdx k, SingI (FromInteger 1 :: k))
  => Vec k n String
  -> Vec k (n + FromInteger 1) String
test =
  case additionCommute @(FromInteger 1) @n of
    Refl ->
      appendVec
        (replicateVec
          (sing @(FromInteger 1) :: Sing (FromInteger 1 :: k))
          "hello"
        )

This can be run in ghci like the following:

$ nix-shell my-ghc-8.6.2.nix --command 'ghci polymorphic-length-index.hs'
> testAppVec
ConsVec "foo" (ConsVec "foo" (ConsVec "foo" (ConsVec "bar" (ConsVec "bar" (ConsVec "bar" (ConsVec "bar" EmptyVec))))))