Absence of control on the order of resolution of implicits

[857b]

When using resolve_implicits, there seems to be no option to control the order in which the different implicits are instantiated. This is needed when interacting with libraries (such as Steel) which rely on resolve_implicits if one also want to use our own implicits. For instance, the following example fails because the second implicit is instantiated before the first one:

module Main
open FStar.Tactics

irreducible let implicit_0 : unit = ()
irreducible let implicit_1 : unit = ()

type dep_on : bool -> Type =
  | DTrue  : dep_on true
  | DFalse : dep_on false

[@@ resolve_implicits; implicit_0]
let build_implicit_0 () : Tac unit =
  print ("build_implicit_0: "^term_to_string (cur_goal ()));
  exact (`false)

[@@ resolve_implicits; implicit_1]
let build_implicit_1 () : Tac unit =
  print ("build_implicit_1: "^term_to_string (cur_goal ()));
  try exact (`DTrue)
  with | _ -> exact (`DFalse)

assume val test_fun (#[@@@ implicit_0] b : bool) (#[@@@ implicit_1] d : dep_on b) : unit -> unit

let () = test_fun ()

[F*] TAC>> build_implicit_1: Main.dep_on (*?u48*) _
[F*] TAC>> build_implicit_0: Prims.bool
[F*] !!!!!!!!!!!! GOAL IS ALREADY SOLVED! (* Instantiating meta argument in application *)
[F*] ( |- ?48 : Prims.bool)	GOAL ALREADY SOLVED!: true
[F*] 
[F*] sol is true
(Error 228) user tactic failed: ‘exact: false does not solve true : bool‘

[TWal]

I'm wondering if #2591 is related to this issue: the test there fails because F* tries to resolve tc2 before resolving tc1.