https://www.haskellforall.com/2024/02/unification-free-keyword-type-checking.html
Unification-free ("keyword") type checking From my perspective, one of the biggest open problems in imple...
The author claims that by removing some type inference (lambdas and generic instantiation) you can reduce the amount of code required to implement type-checking.
@armchair_progamer no mention of (mutual) recursion? It's been a while since I worked on my type checker, but I thought that you needed to separate inference into unification variable generation and constraint solving so that you don't fall into an infinite loop (each function asking the other functions type - forever).
You probably need to annotate recursive function return values. I know in some languages like Swift and Kotlin, at least in some cases this is required; and other languages have you annotate every function’s return value (or at least, every function which isn’t a lambda expression). So IMO it’s not even as much of a drawback as the other two.