One thing that's bad about the notation is not so much the horizontal bar notation, but that the pattern matching leaves so much implicit. You would have exactly the same confusion with pattern matching with sets. The problem is that the names of the variables are semantically significant. For example x can only stand for a program variable, not for a compound expression, e can stand for a compound expression, but not for a program variable. There is nothing except the name to distinguish them, and this is usually not explained. Similarly, τ stands for a monotype, whereas σ stands for a polytype (leaving aside the inst rule, where σ can confusingly also stand for a monotype, and the first rule, which should use τ instead of σ). Additionally a lot is left unexplained by the absence of the square inclusion relation and the free(.) function.
The horizontal bar notation is not ideal however. In my opinion Prolog notation is clearer, because it reads the right way around, and it makes it clear what relation we are defining. In Prolog notation you'd define a typeof(context, term, type) relation:
typeof(C,var(X),T) |- X:T in C
typeof(C,app(X,Y),B) |- typeof(C,X,A -> B), typeof(C,Y,A)
...
In Prolog you should read |- as "if". So the first rule says: "the type of a variable X is T if `X:T` is in the context C".
The horizontal bar notation is not ideal however. In my opinion Prolog notation is clearer, because it reads the right way around, and it makes it clear what relation we are defining. In Prolog notation you'd define a typeof(context, term, type) relation:
In Prolog you should read |- as "if". So the first rule says: "the type of a variable X is T if `X:T` is in the context C".