Improve: unification message in case of disallowed variable

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3126
From: ruibaptista@live.com
Reported version: 8.4
CC: @aspiwack, @herbelin, @JasonGross

See also: #3823
See also: #5264

[coqbot]

Comment author: ruibaptista@live.com

Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.

(* For this goal the following series of tactics fails. *)

(*

intros T1 P1 H1.
eexists.
destruct H1 as [x1 H1].
apply H1.

*)

(* But it's possible to get them to work simply by reordering them. *)

intros T1 P1 H1.
destruct H1 as [x1 H1].
eexists.
apply H1.

[coqbot]

Comment author: @aspiwack

This is not a bug: an existential variable cannot be instantiated using variables introduced later. It would create ill-typed proof terms.

In fact it would allow proofs of False along the lines of:

Definition Top {A} (x:A) := True.

Goal exists x:False, Top x -> False -> False.
Proof.
  eexists.
  intros x y.
  instantiate (1:=y) in x.
  exact y.
Qed.

The error message of instanciate is much better :

Error: Instance is not well-typed in the environment of ?9

The apply tactic fails with:

Error: Impossible to unify "?9" with "x1".

I'm leaving this bug as a request for a better error message. (and changing the title along these lines)

[coqbot]

Comment author: @herbelin

Backtracking on setting the bug as invalid (I was too quick on reading Arnaud's comment).

Actually, the error message improved and shows that there is a solution:

Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
intros T1 P1 H1.
eexists ?[x].
destruct H1 as [x1 H1].
Fail apply H1.
(* Unable to unify "?x@ {H1:=existT P1 x1 H1}" with "x1" (cannot instantiate 
"?x" because "x1" is not in its scope: available arguments are "T1" "P1"
"existT P1 x1 H1"). *)
(* The diagnosis of Coq is wrong, since x1 can be extracted from "existT P1 x1 H1". But the unification is not strong enough to do it. *)
(* Indeed, the following, which renounces to use x1 but redoes a case on the initial H1, works: *)
instantiate (x:=projT1 H1).
apply H1.
Qed.

In any case, my conclusions at this time are the following:

• The error message bug is fixed, in the sense that it is enough informative, and hence I'm formally closing the bug as resolved.
• The unification is too weak, in the sense that it does not see that a copy of x1 can be re-extracted from "existT P1 x1 H1"; thus it implicitly remains a feature request for unification, as in There should be a variant of [destruct] that destructs the relevant term in all evars which the current goal depends on #3823, which I add to a collection of unification weaknesses at "https://coq.inria.fr/cocorico/CoqDevelopment/UnificationProblems".
• It is not impossible that it remains a misunderstanding on the fact that the x1 coming from the destruct cannot be used to instantiate ?[x], only a new projection from H1 can be done.