It’s not the prettiest code, but here: https://github.com/evincarofautumn/kitten/blob/8a7e949f1af71384a5fb56693de32474dead492c/new/lib/Kitten/Infer.hs#L123 htt

It’s not the prettiest code, but here: https://github.com/evincarofautumn/kitten/blob/8a7e949f1af71384a5fb56693de32474dead492c/new/lib/Kitten/Infer.hs#L123 https://github.com/evincarofautumn/kitten/blob/8a7e949f1af71... The key line is: (term', t, tenvFinal) <- inferType dictionary tenvFinal' tenv term In “inferType”, I just annotate each term with “Zonk.type_ tenvFinal type_” as I go, in the same pass as generating the type constraints. Since “tenvFinal” is the final type environment, and “zonking” substitutes all type variables with their solved types, everything gets lazily resolved when reading the annotated types later on, e.g., during analysis & codegen.