It is possible to omit terms that the type checker can figure out for itself,
replacing them by _. If the type checker cannot infer the value of an
_ it will report an error. For instance, for the polymorphic identity
function
id : (A : Set) -> A -> A
the first argument can be inferred from
the type of the second argument, so we might write id _ zero for the
application of the identity function to zero.
Implicit function spaces are written with curly braces instead of parenthesis. For instance,
_==_ : {A : Set} -> A -> A -> Set
subst : {A : Set}(C : A -> Set){x y : A} -> x == y -> C x -> C y
Note how the first argument to _==_ is left implicit. Similarly we may
leave out the implicit arguments A, x, and y in an application of
subst. To give an implicit argument explicitly, enclose in curly
braces. The following two expressions are equivalent:
subst C eq cx
subst {_} C {_} {_} eq cx
Worth noting is that implicit arguments will be inserted also at the end of an application, so the following is equivalent:
subst C
subst C {_} {_}
To get the function of type {x y : A} -> x == y -> C x -> C y we have to explicitly
abstract over x and y:
\{x}{y} -> subst C
Implicit arguments can also be referred to by name, so if we want to give the
expression e explicitly for y without giving a value for x we can write
subst C {y = e} eq cx
When constructing implicit function spaces the implicit argument can be omitted,
so both expressions below are valid expressions of type
{A : Set} -> A -> A:
\{A} x -> x
\ x -> x
There are no restrictions on when a function space can be implicit. Internally, explicit and implicit function spaces are treated in the same way. This means that there are no guarantees that implicit arguments will be solved. When there are unsolved implicit arguments the type checker will give an error message indicating which application contains the unsolved arguments. The reason for this liberal approach to implicit arguments is that limiting the use of implicit argument to the cases where we guarantee that they are solved rules out many useful cases in practice.