Using a structural type (type level Peano numbers) to try to simplify the replicateVec function.

singleton-vec-proofs.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

module VectStuff3 where

import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import Data.Singletons.Decide (Decision(Disproved, Proved), Refuted, (:~:)(Refl), (%~))
import Data.Singletons.Prelude
       (PNum((+), (-)), SNum((%-)), SingI, SingKind(Demote, fromSing, toSing),
        SomeSing(SomeSing), sing, withSomeSing)
import Data.Singletons.TypeLits (KnownNat, Nat, SNat, Sing(SNat), natVal)
-- import GHC.TypeLits (Nat {-CmpNat, KnownNat, Nat, natVal-})
import GHC.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)

newtype MyNat = MyNatCon Nat

data instance Sing (z :: MyNat) where
  SZ :: Sing ('MyNatCon 0)
  SSucc :: KnownNat n => Sing ('MyNatCon n) -> Sing ('MyNatCon (1 + n))

deriving instance Show (Sing (z :: MyNat))

axiom :: Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))

plusMinusNM :: forall n m. Dict ((m + (n - m)) ~ n)
plusMinusNM = axiom

nMinus1isSNatProof :: forall n. Refuted (n :~: 0) -> SNat n -> SNat (n - 1)
nMinus1isSNatProof _ SNat = (sing @_ @n) %- (sing @_ @1)

singNatToMyNatCon :: forall n. Sing n -> Sing ('MyNatCon n)
singNatToMyNatCon snat =
  case snat %~ (sing @_ @0) of
    Proved Refl -> SZ
    Disproved f ->
      case plusMinusNM @n @1 of
        Dict ->
          case nMinus1isSNatProof f snat of
            snat'@SNat -> SSucc (singNatToMyNatCon snat')

mPlus1IsKnownNat :: forall n m o. ('MyNatCon n ~ 'MyNatCon (o + m), KnownNat m, KnownNat o) :- KnownNat n
mPlus1IsKnownNat =
  Sub $
    let int = natVal (Proxy @m) + natVal (Proxy @o)
    in
    case toSing int of
      SomeSing (SNat :: Sing x) ->
        unsafeCoerce (Dict :: Dict (KnownNat x)) int

myNatConToSingNat :: forall n. Sing ('MyNatCon n) -> Sing n
myNatConToSingNat SZ = sing @_ @0
myNatConToSingNat (SSucc (_ :: Sing ('MyNatCon m))) =
  case mPlus1IsKnownNat @n @m @1 of
    Sub Dict -> sing @_ @(1 + m)

instance SingI n => SingI ('MyNatCon n) where
  sing :: Sing ('MyNatCon n)
  sing = singNatToMyNatCon $ sing @_ @n

data Vect n a where
  VNil :: Vect 0 a
  VCons :: a -> Vect n a -> Vect (1 + n) a

newtype MyNatural = MyNatural Natural deriving (Num, Show)

instance SingKind MyNat where
  type Demote MyNat = MyNatural

  fromSing :: forall (a :: MyNat). Sing a -> MyNatural
  fromSing SZ = MyNatural . fromSing $ myNatConToSingNat SZ -- fromSing . myNatConToSingNat
  fromSing x@(SSucc _) = MyNatural . fromSing $ myNatConToSingNat x

  toSing :: MyNatural -> SomeSing MyNat
  toSing (MyNatural n) = withSomeSing n $ SomeSing . singNatToMyNatCon

replicateVec :: Sing ('MyNatCon n) -> a -> Vect n a
replicateVec SZ _ = VNil
replicateVec (SSucc s) a = VCons a $ replicateVec s a

This can be loaded into GHCI with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package classy-prelude  --package singletons --package containers --package typelits-witnesses --package constraints