The filtering of parameters for builtin definitions happens after the computation of the implicit parameters

[sonmarcho]

First reported on the Zulip: https://aeneas-verif.zulipchat.com/#narrow/channel/349819-general/topic/Bugs.3A.20SHA1.20in.20Aeneas/near/493428308
This can lead to issues with external, non-builtin definitions, like here:

axiom alloc.vec.Vec.extend_from_slice
  {T : Type} {A : Type} (corecloneCloneInst : core.clone.Clone T) :
  --          ^^^^^^^^ This type parameter can't actually be infered from the inputs
  alloc.vec.Vec T → Slice T → Result (alloc.vec.Vec T)

[Nadrieril]

Imo we should remove that parameter in a micro-pass instead. I saw a TODO to this effect somewhere recently.

[sonmarcho]

Yes, this is what I have in mind: remove in a micro-pass, then compute the information about the explicit parameters.
The reason why I didn't do that in the first place is that for a very long time I didn't have visitors to explore a whole crate (because of typing issues involving polymorphic definitions which were specialized for different types). But now I have those visitors for Charon-ML, so it should be straightforward.