Right, but local inference is also complicated. So the question is how much of it Idris manages to do without manual annotations. It's not even limited to loc

Right, but local inference is also complicated. So the question is how much of it Idris manages to do without manual annotations. It's not even limited to local definitions with names. If you fully annotate "a=b+2" you get something like "a:int = a:int +:(int->int->int) 2:int". The compiler makes an expression tree and every node in the tree has to get an annotation, either from the source text (i.e. manually) or through inference.