The typechecker and evaluator for this AST would be super simple.
If you want a simple typechecker then you need type annotations. If you want to have type inference then you either need to implement unification or go the bidir route (which still requires top level annotations). You can't have it both ways.
I'm sure the typechecker is as simple as you suggest for GP's language; but not showing it at all makes for an unfair comparison with the article. But the evaluator? Without out the trick of notation that is [x/y] substitution? It's not simple!
You are right that the typechecker gets significantly more complicated if type annotations are optional. But the article and the paper are about real implementations of the language, not arm-chair ones where the burden of type annotations isn't important.
If you want a simple typechecker then you need type annotations. If you want to have type inference then you either need to implement unification or go the bidir route (which still requires top level annotations). You can't have it both ways.