Are numbers types and what is "Number"?
So, you have to be very careful to distinguish values, and the types of those values.

We say $v : T$ when $v$ is a value with type $T$.

The type Number

When people say "Number" is a type, usually they're referring to the type of natural numbers. But each number isn't a type, it's a value, and $Number$ is their type. So we can say $1 : Number$, $2 : Number$, etc.

Notation isn't always consistent. Sometimes people will refer to $Number$ as a type class that contains $Nat, Int, Float$ etc. But that's more complicated.

Now, as for each number being a type, in a language like Haskell (or any Hindley-Milner lanugage), this isn't the case, because numbers are values, and types and values are separate.

But there are a few ways we can look at this

Numbers as singletons

But using dependent-types or GADTs, in a Haskell, Agda, Idris, or other languages with advanced types, you can form a type like this (using Agda-like pseudocode):

data TypeNat : Nat -&gt; Set where 
  TZero : TypeNat Zero
  TSucc : {n : Nat} -&gt; TypeNat n -&gt; TypeNat (Succ n)


For any number n, TypeNat n is a type, containing exactly one value, the TypeNat representation of n.

So here, the number isn't the type, but there's a 1:1 correspondence between the numbers and the types.

Numbers to Quantify other things

We can use numbers to quantify things, but in a dependent-type system, usually this is done by indexing types.

So you can have a type like Vec a n, which is the type of Vectors containing exactly n elements of type a. So here, our types are indexed by numbers, but the number itself is not a type.