Quadratic Micropass Type Inference

Summary

2026.03.27 [Updated: 2026.03.27] :: 7 min read Introduction# Languages that allow plentiful of type inference can often produce confusing error messages. Type inference makes assumptions about what the user intends types to be, and if there’s a type error, there’s a high risk one of those assumptions were wrong. When the compiler then creates an error message it’ll use those types that may have been inferred from false assumptions. I propose a new kind of type inference algorithm that always prioritises the type unifications the end-user is most likely to care about, independent from the types order in source code. The goal being to not have the end-user need to reverse engineer what causes the compiler to infer an incorrect type, and instead work with the users pre-existing assumptions. Background# Languages with simpler inference such as Go can infer inside-out. Meaning we can figure out the type of an expression/statement by looking at its kind plus the types of its subexpressions. func main() { x := someFunction() // the type of the right-hand side is always known } func someFunction() string {...} But this approach quickly falls apart. fn main() { let f = |x| { // we don't know the type of `y` as the type of `x` is not yet known let y = (x, x); return y; }; // we don't know the type of `f` either. f("Hello!"); // it's not until here we know the type of `x`, `y` and f`. } A more powerful form of inference is type variable unification. With such a system we can leave types partially uninferred, and have later expressions/statements fill in the gaps. Lets take the same example but use type variable unification this time. We start inferring types inside-out like in the first example. But; for the types that are not yet known we put a type variable. (annotated as ’N) fn main() { let f: fn(ˈ1) -> ˈ2 = |x| { let y: (ˈ1, ˈ1) = (x, x); return y; // '2 = ('1, '1) }; ... } As the name “type variable” suggests, they are variables and thus can be re-assigned. ... f("Hello!"...