Type inference deduces omitted expression and variable types from program context. One useful model treats the problem as unification: represent types, generic parameters, arguments, and return values as terms containing holes, then find substitutions that make the terms agree. section 10.3
The method signature and the call become two structured terms. Unifying them fills the holes: the argument fixes a type, the lambda constrains its parameter, and those constraints propagate through nested generic types to determine the return type. section 10.3
Inferring a nested generic result
For `Frob<A, B>(A a, Func<A, B> f)`, the call `var v = Frob(1.5, x => [x]);` yields `T -> double`, `U -> List<double>`, `V -> List<List<double>>`, and `X -> double`. Written explicitly, the call returns `List<List<double>>` and uses `Frob<double, List<double>>`; the lambda parameter is `double`.
A unification-based treatment emphasizes these working ideas:
- Encode types and signatures as binary terms built from constants, symbols, and holes. section 10.3
- Build a substitution that fills holes, while rejecting contradictions and preventing infinite self-containing substitutions with an occurs check. section 10.7
- Use aliasing between holes when multiple constraints refer to the same unknown type. section 10.7
- Treat the result as a general deduction technique: unification also supports logic programming when combined with backtracking search. section 10.3
