> Except for function definitions, where the types could be inferred from the function bodies, but are not:

That's an interface boundary, as I mentioned. You would have to write the types in many cases anyway for separate compilation to work. In languages where you have whole-program type inference like ML and Haskell, people frequently end up writing the types for functions because of this issue.

> Plus (and this is more related to the complete lack of implicit type conversions), there are types everywhere in the program. I frequently can't write a number without having to append a type, even when the type has been explicitly defined previously.

This has nothing to do with implicit type conversions, but is rather because numeric literals have no type. It is not a type inference problem; it is just the way that numeric literals are defined.

> let mut s: Vec3<f64> = Vec3{x: 0f64, y: 0f64, z: 0f64, w: 0f64};

That much explicitness is not necessary. It could be written:

    let mut s: Vec3<f64> = Vec3 { x: 0.0, y: 0.0, z: 0.0, w: 0.0 };

Or:

    let mut s = Vec3 { x: 0f64, y: 0.0, z: 0.0, w: 0.0 };

The default types for bare literals is described in RFC #212 (https://github.com/rust-lang/rfcs/pull/212)

To summarize: bare FP literals default to f64, bare integral literals default to isize. (NOTE: isize is recently renamed from int. It is a pointer-sized integer.)

(EDIT: The default for integer literals may be superseded by a later RFC. I seem to recall that the default is actually i32 now, but I can't find a PR to back up that claim.)

So you could easily get a Vec3<f64> like so:

    let mut s = Vec3 { x: 0.0,  y: 0.0, z: 0.0, w: 0.0 };
    let mut t = Vec3 { x: 0f64, y: 0.0, z: 0.0, w: 0.0 };

The key here is that integral literals and floating point literals are distinct.

A bare literal of the form `0` is an unconstrained integral literal.

Whereas a literal of the form `0.0` or `.0` is an unconstrained float literal.

In practice it is very rare for me to annotate my numeric literals. If the variable escapes the stack frame it will be constrained by the signature of the function anyways. If not I constrain the type inline (`let x: T = ...`) and use the appropriate bare literals.