Low-level Ltac2 binder API is not low-level enough

[JasonGross]

Description of the problem

The whole point of having Constr.Unsafe (in particular Constr.Unsafe.make) is so that I can build terms without incurring typechecking costs and without having to incur the cost of manipulating the goal evar and pushing things into the context. However, the current binder API makes this effectively impossible because the Constr.Binder.make calls Retyping.relevance_of_type which requires that the term be sufficiently well-typed in the current context.

Require Import Ltac2.Ltac2.
Require Import Ltac2.Notations.
Require Import Ltac2.Constr.
Require Import Ltac2.Array.

Ltac2 b () := (Binder.make None (Unsafe.make (Unsafe.Rel 5))).

Goal True.
  let v := b () in ().
  (* Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
*)

cc @jfehrle @ppedrot

I'm trying to benchmark some code for generating linear-sized proof terms in linear time for rewriting, and this makes it impossible to generate the proof terms I want. (Looking at the code for Retyping.relevance_of_type, it looks like I might be able to get around this by inserting extra cast nodes, but this is still quite unfortunate.)

Coq Version

master / 8.12

[jfehrle]

BTW, kind: ltac2 is not needed. Seems like that label was created by mistake.