Internalizing a genarg discard the internalization env #21639
Description
Description of the problem
The code which internalizes a genarg (here) discards the internalization env env.impls.
This leads to errors related to implicit arguments when using e.g. ltac quotations (or any other code which internalizes gen args):
Fail Fixpoint f {A} (a : A) (n : nat) : nat :=
match n with
| 0 => 0
| S n => ltac:(exact (f a n))
end.
(* The term "a" has type "A" while it is expected to have type "Type".*)The error above only appears if A is an implicit argument.
IMO the fix is to change Genintern.intern_fun to receive an extra argument ?impls:internalization_env (and check there aren't any other pieces of information which are discarded when internalizing a genarg).
Small Rocq / Coq file to reproduce the bug
Version of Rocq / Coq where this bug occurs
9.1.0 (and AFAICT also master)
Interface of Rocq / Coq where this bug occurs
No response
Last version of Rocq / Coq where the bug did not occur
No response