This is all true, although nothing about the reading "x has type t" implies that "x" can only have one type. It is a separate metatheorem about your system of inference rules that terms have unique types -- and not even one that is always true, e.g. in the presence of subtyping.
> for example, numeric literals in Haskell can have several types
Technically, numeric literals in Haskell have precisely one type: `(Num a) => a`. The literal `42` is actually interpreted as the expression `fromInteger (42 :: Integer)`, where `fromInteger` is a function on the `Num` typeclass. In turn, the `Num` typeclass constraint desugars to a function taking a dictionary of functions, `NumDict a -> a`. The typeclass machinery just means GHC will infer the appropriate instance whose dictionary should be provided.
(technically technically, GHC can be even cleverer if it knows statically which dictionary will be used, avoiding using the dictionary entirely; but this desugaring to dictionaries is ground truth, semantically.)
> for example, numeric literals in Haskell can have several types
Technically, numeric literals in Haskell have precisely one type: `(Num a) => a`. The literal `42` is actually interpreted as the expression `fromInteger (42 :: Integer)`, where `fromInteger` is a function on the `Num` typeclass. In turn, the `Num` typeclass constraint desugars to a function taking a dictionary of functions, `NumDict a -> a`. The typeclass machinery just means GHC will infer the appropriate instance whose dictionary should be provided.
(technically technically, GHC can be even cleverer if it knows statically which dictionary will be used, avoiding using the dictionary entirely; but this desugaring to dictionaries is ground truth, semantically.)