Do not filter implicit args in internal to core translation

[paulcadman]

The internal to core translation was removing implicit arguments from function definitions and applications. This is incorrect as the implicit bindings are required when translating the following (in csuc, the binding of the implicit argument is required in an application on the rhs):

Num : Type;
Num := {A : Type} → (A → A) → A → A;

csuc : Num → Num;
csuc n {_} f := f ∘ n {_} f;

Apart from removing this filter from function and application translation, this required the following changes:

ConstructorInfo:
The _constructorArgsNum field must include the number of type parameters of its inductive type.

PatternConstructorApp:
The pattern arguments must include wildcards for the implicit type parameters passed to the constructor.

BuiltinIf:
The BuiltinIf expression is passed an implicit type argument that must be removed when translating to Core if.

LitString:
A literal string is a function with an implcit type argument. So this must be a translated to a lambda where the type argument is ignored.

• Fixes The translation from Internal to Core doesn't work with type synonyms #1714