diff --git a/tests/bi.ref b/tests/bi.ref
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..3501bc76ecfd2a8f1b503ae9b870dda364b97a14 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -0,0 +1,6 @@
+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").
diff --git a/tests/bi.v b/tests/bi.v
index c68be10a1302c01bc9cb512e3878bebb75cfd5f1..299a8bd3da335b979195624b4babcb3919896555 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -1,5 +1,7 @@
 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.