Implicits checked twice?

[mtzguido]

trafficstars

The query length l == 10 does not work via SMT due to lack of fuel. So we can attempt to use meta-args to solve the squash via normalization, which should work fine, but does not.

I would have expected the implicit to be solved by the tactic, and not need any re-checking, but apparently some re-checking is done and so this fails. At least, the rechecking should be done on the rewritten type..?

open FStar.Tactics.V2

let solve_trivial () : Tac unit =
  compute ();
  trefl()

let func (p : Type0) (#[solve_trivial()] prf : squash p) : unit = ()

let l = [1;2;3;4;5;6;7;8;9;10]

let test = func (List.length l == 10)

This seems to be previous to all the #3134 stuff.