diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index 0ecf54c5513173efdbdb0a6a6eee4d86c53c701a..63114e83bfa4efdce0604a90f8edbaeb5ea434a2 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 (** A general interface for a lock.
 All parameters are implicit, since it is expected that there is only one
 [heapGS_gen] in scope that could possibly apply. *)
-Structure lock `{!heapGS_gen hlc Σ} := Lock {
+Class lock `{!heapGS_gen hlc Σ} := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
@@ -18,11 +18,11 @@ Structure lock `{!heapGS_gen hlc Σ} := Lock {
   is_lock (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
   locked (γ: name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_lock_ne γ lk : Contractive (is_lock γ lk);
-  is_lock_persistent γ lk R : Persistent (is_lock γ lk R);
+  is_lock_ne γ lk :> Contractive (is_lock γ lk);
+  is_lock_persistent γ lk R :> Persistent (is_lock γ lk R);
   is_lock_iff γ lk R1 R2 :
     is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2;
-  locked_timeless γ : Timeless (locked γ);
+  locked_timeless γ :> Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
   (** * Program specs *)
   newlock_spec (R : iProp Σ) :
@@ -34,7 +34,5 @@ Structure lock `{!heapGS_gen hlc Σ} := Lock {
 }.
 Global Hint Mode lock + + + : typeclass_instances.
 
-Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
-
 Global Instance is_lock_proper hlc Σ `{!heapGS_gen hlc Σ} (L : lock) γ lk :
   Proper ((≡) ==> (≡)) (L.(is_lock) γ lk) := ne_proper _.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 7f3f6270b15aa9e56386f2deb505146664019bf2..e0c23c96401cf99fa39a9288be5672bda0966641 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation lib.lock.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
 From iris.prelude Require Import options.
@@ -515,3 +515,31 @@ Proof.
   iIntros (?) "_". rewrite /heap_e /=.
   wp_alloc l. wp_load. wp_store. wp_load. auto.
 Qed.
+
+(** Just making sure the lock typeclass actually works. *)
+(** Sadly the [lang] import reexports the [ssreflect.lock] so we have to
+re-import the library we really want to use... *)
+Import heap_lang.lib.lock.
+Section lock.
+  Context `{!heapGS Σ, !lock}.
+
+  Definition lock_client : val :=
+    λ: "loc" "lock",
+      acquire "lock";;
+      "loc" <- #42;;
+      release "lock".
+
+  Lemma wp_lock_client loc lock γ :
+    is_lock γ lock (∃ v, loc ↦ v) -∗
+    WP lock_client #loc lock {{ _, True }}.
+  Proof.
+    iIntros "#Hislock".
+    wp_lam. wp_smart_apply (acquire_spec with "Hislock") as "[Hlocked [%v Hloc]]".
+    wp_store.
+    wp_smart_apply (release_spec with "[$Hlocked Hloc]").
+    { iFrame "Hislock". eauto. }
+    eauto.
+  Qed.
+
+End lock.
+