To explain these concepts in more detail, you want a Sigma type
(n :: Nat, Vect (n :: Nat) a)
But we don’t have those in Haskell. Instead you can have a second class existential type by writing it as a GADT:
data SomeVect a where
SomeVect :: (n :: Nat) -> Vect (n :: Nat) a -> SomeNat a
-- ^ This is not yet valid Haskell!
But we don’t have dependent types either! Instead there is a singleton type SNat :: Nat -> Type that does a similar job. It’s called a “singleton” because there is one value of type SNat n for each literal type n :: Natural. Using SNat we can write the desired Sigma type equivalent as
data SomeVect a where
SomeVect :: SNat (n :: Nat) -> Vect (n :: Nat) a -> SomeNat a
-- ^ This is now valid Haskell
For convenience there is a class KnownNat (n :: Nat) where natSing :: SNat n. This makes the above type equivalent to
data SomeVect a where
SomeVect :: KnownNat (n :: Nat) => Vect (n :: Nat) a -> SomeNat a
In order to reify a value level Nat (or Integer) to a type level Nat we need to use reifyNat. That is we pass in an i :: Integer (actually I should have put a guard that it is non-negative) and we “get out” a type level n :: Nat.
I’ve never used Agda, but I guess in Agda SNat vanishes and reifyNat is roughly just function application.