Is it possible to write a function Int -> NatSing n, where NatSing is a singleton type of peano numbers?

Question 1

No, you cannot write such a function.

A function of type

Int -> NatSing n

says that it can transform any integer into a polymorphic NatSing. But there is no polymorphic NatSing.

What you seem to want here is to have n determined by the incoming Int. That'd be a dependent type:

(n :: Int) -> NatSing n

Such a thing isn't possible in Haskell. You'd have to use Agda or Idris or another dependently typed language. The hack with singletons is exactly Haskell's way to get around this. If you want to make a distinction based on a value, you have to lift the value to the type level, which is what NatSing is.

You could write a function that returns a NatSing for some n, by wrapping the n up in an existential type:

data ExNatSing where
  ExNatSing :: NatSing n -> ExNatSing

But this wouldn't give you much benefit in practice. By wrapping the n up, you lose all information about it, and cannot make decisions based on it later.

By exactly the same argument, you can also not hope to define a function

list :: [a] -> List n a

The only approach you can use to save yourself some typing work is to define a type class that construct the NatSing value automatically:

class CNatSing (n :: Nat) where
  natSing :: NatSing n

instance CNatSing Zero where
  natSing = ZeroSing

instance CNatSing n => CNatSing (Succ n) where
  natSing = SuccSing natSing

Then, you can say:

list :: CNatSing n => [a] -> List n a
list xs = list' xs natSing
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but still partial

Here, the type context you use this in makes GHC fill in the right NatSing. However, this function is still partial, because still the caller of the function can choose at what n to use this. If I want to use a [Int] of length 3 as a List (Succ Zero) Int it's going to crash.

Again, you could wrap this up in an existential instead:

data SomeList a where
  SomeList :: NatSing n -> List n a -> SomeList a

Then you could write

list :: [a] -> SomeList a
list []       = SomeList ZeroSing Nil
list (x : xs) = case list xs of
                  SomeList n xs -> SomeList (SuccSing n) (x : xs')

Again, the benefit is small, but in contrast to ExNatSing, there at least is one: you now can temporarily unwrap a SomeList and pass it to functions that operate on a List n a, getting type-system guarantees on how the length of the list is transformed by these functions.

Question 2

What you want looks something like (Int -> (exists n . NatSing n)), where n is unknown ahead of time. You could do that with something like (untested):

data AnyNatSing where
  AnyNatSing :: NatSing n -> AnyNatSing

toNatSing :: Int -> AnyNatSing
toNatSing n
  | n > 0 = case toNatSing (n - 1) of
      AnyNatSing n -> AnyNatSing (SuccSing n)
  | otherwise = AnyNatSing ZeroSing

Question 3

As said by Louis Wassermann, the closest match to what you want is an existential wrapper that makes NatSing monomorphic from the outside.

I consider that pretty useless though, since it basically just throws away the type-checking of lengths and you're left with a dumb standard integer type. There are easier ways to to that, like, using a dumb standard integer type and ordinary Haskell lists...

But there's one alternative that's perhaps not quite so useless. Remember that it's pretty much equivalent if you return some value x from a function, or instead pass a higher-order and call that with x; I think lisps particularly like such continuation-passing tricks.

For your example, you need a function that's able to accept any length-type of lists. Well, such functions certainly exist, e.g. a scalar product that requires two lists of equal length, but doesn't care what the length is. And it then returns a simple monomorphic number. For simplicity's sake, let's consider an even simpler sum on your list type:

sumSing :: Num a => List (n::Nat) a -> a
sumSing Nil = 0
sumSing (Cons x ls) = x + sumSing ls

Then you can do:

{-# LANGUAGE RankNTypes     #-}

onList :: (forall n . CNatSing n => List n a -> b) -> [a] -> b
f`onList`l = f (list l)

(list being kosmicus' variant with the CNatSing class constraint) and call it like

sumSing `onList` [1,2,3]

...which is of course in itself no more useful than the existential solution (which, I think, actually desugars to something similar to this RankN stuff). But you can do more here, like the scalar product example – providing two lists and actually ensuring through the type system they have the same length. This would be far uglier with existentials: you'd basically need a seperate TwoEqualLenLists type.