Adding to this, there's a set of language features which use the type system to generate code. So, things like traits in Rust or Typeclasses in Haskell use the

Adding to this, there's a set of language features which use the type system to generate code. So, things like traits in Rust or Typeclasses in Haskell use the type system to infer which instance is being used and insert a dictionary of trait method implementations as the first argument to your polymorphic function. You can't really do this kind of thing if the compiler can't do `Type -> code` and is only verifying the types are consistent. A pseudocode example is something like: trait ToString for T { fn toString(self: T) -> String; } impl ToString for number { fn toString(self: number) -> String { // implementation here } } impl ToString for Point { fn toString(self: Point) -> String { return f"({self.x.toString()}, {self.y.toString()})"; } } fn printString<T: ToString>(t: T) { print(t.toString()); } Then when it generates code, it uses the inferred type information to generate different code: let p = Point(1.0, 2.0); printString(p); // translated into printString(implToStringForPoint, p); let n = 2.0; printString(n); // translated into printString(implToStringForNumber, n); And then type inference becomes implementation inference, which is really powerful