Fix #1693

[janmasrovira]

Closes #1693.

This pr includes:

• fix for Type checking crashes with higher-order functions #1693, including the corresponding test.
• hole ids are now printed when the --show-name-ids flag is provided for Internal syntax.
• moves a bogus positive test to a negative one.

Note that in the test I have:

I : {A : Type} → A → A;
I := S K (K {_} {Bool});

instead of

I : {A : Type} → A → A;
I := S K K;

I could have picked any type instead of Bool, but it needs to be provided explicitly, otherwise inference fails (as expected)