auto incoherent on goal with evars

[mrhaandi]

Description of the problem

When auto is called on a goal containing an evar, the outcome is difficult to predict and the debug log on exact is misleading.

Create HintDb db1.
Axiom eq_tt : tt = tt.
#[local] Hint Resolve eq_tt : db1.

(* does not use hint, does not instantiate evar *)
Goal exists u, u = tt.
Proof.
  eexists.
  Fail solve [debug auto with nocore db1]. (* says exact eq_tt (in db2). (*fail*) *)
  exact eq_tt. (* the above message was misleading *)
Qed.

(* the above failure is incoherent with the following success *)

Create HintDb db2.
Axiom True_eq_tt : True -> tt = tt.
#[local] Hint Resolve True_eq_tt : db2.

(* uses hypothesis and hint, instantiates evar *)
Goal True -> exists u, u = tt.
Proof.
  intros. eexists.
  solve [auto with nocore db2].
Qed.

Coq Version

The Coq Proof Assistant, version 8.15.2 compiled with OCaml 4.14.0

[mrhaandi]

The reason for the arbitrary behavior is that auto currently uses three different unification procedures for

1. hypotheses with zero arguments
2. hints with zero arguments
3. hypotheses or hints with at least one argument