In addition to having implicit arguments, Agda lets you omit the value of an explicit argument and replace it with a metavariable, denoted by the _ character, whose value is then determined through the same procedure as implicit resolution.
Does Idris have a similar feature, or are implicit arguments the only way of introducing metavariables into programs?