More tests.

tests/bi.ref

+The command has indeed failed with message:
+In environment
+PROP : bi
+m : gmap nat nat
+The term "m" has type "gmap nat nat" while it is expected to have type
+ "gmap nat Z" (cannot unify "nat" and "Z").

tests/bi.v

 From iris.bi Require Import bi plainly big_op.
 
+Unset Mangle Names.
+
 (** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
 Lemma test_impl_persistent_1 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
   Persistent (PROP:=PROP) (True → True).
@@ -38,8 +40,23 @@ Definition big_sepM_pattern_both
     {PROP : bi} (m : gmap (nat * nat) (nat * nat)) : PROP :=
   [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.
 
+Definition big_sepM2_pattern {PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP :=
+  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
+
+(** This fails, Coq will infer [x] to have type [Z] due to the equality, and
+then sees a type mismatch with [m : gmap nat nat]. *)
+Fail Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP :=
+  [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.
+
+(** With a cast, we can force Coq to type check the body with [x : nat] and
+thereby insert the [nat] to [Z] coercion in the body. *)
 Definition big_sepM_cast {PROP : bi} (m : gmap nat nat) : PROP :=
   [∗ map] (x:nat) ∈ m, ⌜ 10%Z = x ⌝.
 
-Definition big_sepM2_pattern {PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP :=
-  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
+Section big_sepM_implicit_type.
+  Implicit Types x : nat.
+
+  (** And we can do the same with an [Implicit Type]. *)
+  Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP :=
+    [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.
+End big_sepM_implicit_type.