MetaCoq: what's the `term` equivalent of `_`?

Using Coq
1

Writing reified MetaCoq terms by hand can get tedious sometimes, is there a placeholder of the type term in MetaCoq that could be used for things that can be inferred by the type checker? And if it cannot be inferred then the unquoting would fail. I’m essentially looking for a reified version of _. (I realize _ isn’t a term but a type checking convenience, but still)

I thought maybe tEvar could be used for this but I couldn’t figure out how. The documentation doesn’t help much with tEvar.

Idris has a way to achieve this. Idris has two equivalents of term, one is called TT , for typed core language terms, and Raw , for unchecked core language terms. TT has a constructor named Erased and in Raw you can do something like this: https://github.com/joom/hezarfen/blob/master/Hezarfen/Prover.idr#L8-L10

Agda has an unknown constructor in their Term type: https://agda.readthedocs.io/en/v2.6.0.1/language/reflection.html#terms

2

At the moment we don’t have such a feature. tEvar might be a way to go indeed, but the lack of documentation in this case is simply a witness of a lack of feature.
We don’t support them basically.

Right now, for something like this we would call inference manually to fill the hole but I agree this is not ideal.