Type inference woes

CONSIDER this Rust code that a reasonable human being might try to write:

fn add<T>(a: T, b: T) -> T {
return a + b;
}
If you try to compile that, you’ll get an error like this:

:1:25: 1:30 error: binary operation `+` cannot be applied to type `T`
What you actually have to write is something like this:

use std::ops::Add;
fn add<T: Add>(a: T, b: T) -> T::Output {
return a + b;
}
Now it typechecks correctly.

This seems a little ridiculous. The compiler already knew that T had to be a type that supports addition — it just told me that. So why am I spelling it out?

>>1
This has nothing to do with type inference - it only has to do with you giving it an incorrect type. \((t : *) \to Add\ t \to t \to t \to t\) is not the same as \((t : *) \to t \to t \to t\).
Type inference is about the types being inferred without having to write any types at all - for example if you could write fn add(a, b) { return a + b; }.
In any case, you should not be using rust. Consider Coq instead.