(no subject)

In a language enjoying relational parametricity each fresh symbol must immediately obtain either a value (therefore automatically also a type) or at least a type, otherwise it cannot be used in any sensible way. So there are two freshness markers for a symbol: a definition or a type declaration.

x : Type   # that's a type declaration
y: value   # that's a definition

I don't believe in languages where whitespaces can be ignored at random. :-(

P.S. If you want variable type to be inferred, there is a notation n : ¤.