Spurious failure of SSReflect's assumption interpretation

[silene]

Description of the problem

Assumption interpretation (i.e., move => /foo) fails on trivial examples. The equivalent construction in vanilla Ltac (i.e., intros H%foo) works fine, as does the fully instantiated variant in SSReflect (i.e., move => /(foo _ _ _ _ _)).

Small Coq file to reproduce the bug

From Coq Require Import ssreflect.

Definition bind {A B} (o : option A) (f : A -> option B) :=
  match o with
  | Some o => f o
  | None => None
  end.

Lemma bind_inv A B o f v : @bind A B o f = Some v -> exists w, o = Some w /\ f w = Some v.
Proof. intros H. destruct o as [o|]. now exists o. easy. Qed.

Goal forall x y, bind x (fun t => Some (S t)) = Some y -> y <> O.
Proof.
Fail move => x y /bind_inv H. (* Failure: __view_subject__ is used in hypothesis H. *)
move => x y /(bind_inv _ _ _ _ _) H. (* OK. Also OK: intros x y H%bind_inv. *)
by move: H => [w [_ [<-]]].
Qed.

Version of Coq where this bug occurs

8.13.1, 8.17.1, 8.19.1

Last version of Coq where the bug did not occur

No response

[CohenCyril]

This is a perfectly valid behaviour of forward views. The problem is A and B being of type Type they are "catchall sort" arguments of bind_inv, and v is a general catchall... hence they can be instanciated with bind x (fun t => Some (S t)) = Some y, which causes the issue. The error message is not helpful though (@gares can we make it better?)

There are two standard solutions to this problem,

• make A, B and v maximally implicit in the def of bind_inv, or
• or tag A and B as "non prop" by typing them as nonPropType (from ssreflect.v)

[CohenCyril]

Maybe the behaviour where Type arguments get instanciated is actually never used and should be excluded by the view mechanism.

[silene]

make A, B and v maximally implicit in the def of bind_inv,

No, it does not work. It fails with the exact same message.

By the way, did you really mean A, B, and v? Why would v change anything?

Anyway, unless all the arguments are maximally implicit, which is the same as the full manual instantiation, it seems to fail.

[CohenCyril]

Lemma bind_inv {A B v} o f : @bind A B o f = Some v -> exists w, o = Some w /\ f w = Some v.
Proof. intros H. destruct o as [o|]. now exists o. easy. Qed.

works.

So does

Lemma bind_inv (A B : nonPropType) o f v : @bind A B o f = Some v -> exists w, o = Some w /\ f w = Some v.
Proof. intros H. destruct o as [o|]. now exists o. easy. Qed.

[CohenCyril]

Indeed if you do not put v first it stops working, and this is likely to be a bug.

[CohenCyril]

By the way, did you really mean A, B, and v? Why would v change anything?

Because v has type variable B, so v := @bind A B o f = Some v and B := Prop is a valid instanciation.

EDIT: B := @bind A B o f = Some v and v := __top__ indeed!

[silene]

I guess you meant B := (bind x (fun t => Some (S t)) = Some y) and v := __top__, but I get your point about v being the issue here. Unfortunately, the bind_inv lemma actually comes from a third-party library, so that means I would have to define my own variant (either that or I keep using the Ltac version).

[silene]

Maybe the behaviour where Type arguments get instanciated is actually never used and should be excluded by the view mechanism.

Actually, it might be sufficient to just never instantiate a dependent argument with the "view subject". Indeed, even if this resulting instance were to be well-typed by sheer luck (as it is here), the process would then necessarily fail with "__view_subject__ is used", since the argument is dependent. Am I missing something?

[gares]

Your suggestion makes sense, but I don't have cycles to implement it.
The code is not that simple since we call the pretyper that works on glob terms but some pieces are econstr, so we stash them into ltac variables...

coq/plugins/ssr/ssrview.ml

Lines 286 to 288 in 98a2533

	guess_max_implicits ist v >>= fun n ->
	Ssrcommon.tclFIRSTi (fun n ->
	interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n

So v may not be trivially a global reference with a type we can analyze... In particular see the guess_max_implicits kludge. But I believe it can be implemented, but it may be harder than it seems.