Fix arity checker bug

[janmasrovira]

Depends on #1538.

The following fails to arity check:

inductive Box (A : Type) {
  b : A → Box A;
};

x : Box ((A : Type) → A → A);
x := b λ {A a := a};

The issue is that when arity checking an application, we were first checking the arguments and then adding the holes. As an unwanted consequence, the arguments could be assigned an incorrect arity. Now this is fixed

The pr also includes pretty printing for arities, which was useful during the debugging.