singletonArith.hs

data Counter :: Nat -> Type where
  Counter :: (KnownNat s) => Sing s -> Counter s

data ACounter :: Type where
  ACounter :: (KnownNat s, KnownNat (s + 1)) => Counter s -> ACounter

incCounter :: forall a. (KnownNat a, KnownNat (a + 1)) => Counter a -> Counter (a + 1) 
incCounter _ = Counter $ sing @(a + 1)

zero :: Counter 0 
zero = Counter (sing @0)

-- incCounter works...
-- > (\(Counter x) -> fromSing x)  $ incCounter (incCounter zero) 
-- 2

--existential version doesn't...
incCounterS :: ACounter -> ACounter
incCounterS (ACounter c) = ACounter $  incCounter c -- Could not deduce
                                      -- (KnownNat((s GHC.TypeNats.+ 1) GHC.TypeNats.+ 1))
                                      -- arising from a use of 'ACounter' (...)