I had some unexpected behaviour of type class inference when using a function that used `mguard`

in its definition. Below I have tried to condense it to a minimal example.

In the unexpected case, type-inference looks for an instance of `elem_of`

and yields `fun x y => False`

instead of the expected `@elem_of_list nat`

.

```
From stdpp Require Import gmap.
Ltac solve_unexpected :=
intros (? & ?); case_option_guard;
[unfold elem_of in *; tauto |
congruence].
Ltac solve_expected x :=
exists [x]; case_option_guard;
match goal with
| H : _ |- Some _ <> None => congruence
| H : _ ∉ _ |- _ => contradict H; eapply elem_of_cons; eauto
end.
(* In my original code [mguard] was part of some function I defined.
As the below examples show, type class inference will give different
results depending on how the statement is elaborated. *)
(* Set Printing All *)
Example unexpected1 (x: nat) :
¬ (∃ sl: list nat, mguard (x ∈ sl) (λ _ : x ∈ sl, Some x) <> None).
Proof. solve_unexpected. Qed.
(* We get the expected result just by adding some type annotation *)
Example expected1 (x: nat) :
∃ sl: list nat, mguard (x ∈ (sl: list nat)) (λ _ : x ∈ sl, Some x) <> None.
Proof. solve_expected x. Qed.
(* But also by removing parts *)
Example expected2 (x: nat) :
∃ sl: list nat, mguard (x ∈ sl) (λ _, Some x) <> None.
Proof. solve_expected x. Qed.
(* For better visual comparisons:
*)
Example unexpected (x: nat) :
¬ (∃ sl: list nat, mguard (x ∈ sl) (λ _ : x ∈ sl, Some x) <> None) /\
¬ (∃ sl: list nat, mguard (x ∈ sl) (λ _ : x ∈ (sl: list nat), Some x) <> None).
Proof. split; solve_unexpected. Qed.
Example expected (x: nat) :
(∃ sl: list nat, mguard (0 ∈ sl) (λ _ : 0 ∈ sl, Some x) <> None) /\
(∃ sl: list nat, mguard (x ∈ (sl: list nat)) (λ _ : x ∈ sl, Some x) <> None) /\
(∃ sl: list nat, mguard (x ∈ sl) (λ _, Some x) <> None).
Proof. repeat split; [solve_expected 0|..]; solve_expected x. Qed.
(* If [mguard] is replaced by [decide] to give similar code the problem
does not appear. So it seems to me that this problem is more specific to [mguard],
or at least I was not able to minimize [mguard] out of this. *)
Example expected_decide (x: nat) :
(∃ sl: list nat, (if (decide (x ∈ sl)) then Some x else None) <> None).
Proof.
Set Printing All.
exists [x]. destruct (decide _) as [|H].
- congruence.
- contradict H. eapply elem_of_cons. eauto.
Qed.
```