diff --git a/barrier/client.v b/barrier/client.v
index 1403ea6770a9ab083a80ab492271fbe1fb22b636..89ed8f4ffed3ece9c6c18879f36e2688e28e8e02 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -28,19 +28,10 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: authF (constF heapRA)
+  Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: heapF
                                      .:: (λ _, constF unitRA) : iFunctorG.
   Notation iProp := (iPropG heap_lang Σ).
 
-  Instance: authG heap_lang Σ heapRA.
-  Proof. split; try apply _. by exists 2%nat. Qed.
-
-  Instance: stsG heap_lang Σ barrier_proto.sts.
-  Proof. split; try apply _. by exists 1%nat. Qed.
-
-  Instance: savedPropG heap_lang Σ.
-  Proof. by exists 0%nat. Qed.
-
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
   Proof.
     apply ht_alt. rewrite (heap_alloc ⊤ (ndot nroot "Barrier")); last first.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 5d66586d4b7daa46bd4db0b74ebe0650ed1acee5..2a32e5ffc3955604a0bdfac6bad94d445e1905b1 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -8,6 +8,7 @@ Import uPred.
    predicates over finmaps instead of just ownP. *)
 
 Definition heapRA := mapRA loc (exclRA (leibnizC val)).
+Definition heapF := authF heapRA.
 
 Class heapG Σ := HeapG {
   heap_inG : inG heap_lang Σ (authRA heapRA);
@@ -20,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl.
 Definition of_heap : heapRA → state := omap (maybe Excl).
 
 Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
-  auth_own heap_name {[ l := Excl v ]}.
+  auth_own heap_name ({[ l := Excl v ]} : heapRA).
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).
 Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
@@ -103,7 +104,7 @@ Section heap.
     P ⊑ || Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
-    trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
+    trans (|={E}=> auth_own heap_name (∅ : heapRA) ★ P)%I.
     { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 1a961c2da5d0945625a3ced9c09d3c137988e840..0f8467db59e8cfe3d0557f216c38972d00765068 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -76,12 +76,9 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := λ _, authF (constF heapRA).
+  Definition Σ : iFunctorG := heapF .:: endF.
   Notation iProp := (iPropG heap_lang Σ).
 
-  Instance: authG heap_lang Σ heapRA.
-  Proof. split; try apply _. by exists 1%nat. Qed.
-
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
   Proof.
     apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index fbaae8208e82aaf54cfee250b61da819a784b36b..2e7f75d709503b3c03b5159092918eae8366eb89 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -9,6 +9,13 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_timeless (a : A) :> Timeless a;
 }.
 
+(* TODO: This shadows algebra.auth.authF. *)
+Definition authF (A : cmraT) := constF (authRA A).
+
+Instance authG_inGF (A : cmraT) `{CMRAIdentity A} `{∀ a : A, Timeless a}
+         `{inGF Λ Σ (authF A)} : authG Λ Σ A.
+Proof. split; try apply _. move:(@inGF_inG Λ Σ (authF A)). auto. Qed.
+
 Section definitions.
   Context `{authG Λ Σ A} (γ : gname).
   (* TODO: Once we switched to RAs, it is no longer necessary to remember that a
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index ab156cae7cd6364ee36342077847819e6373c1a4..b42995bf062c3e70b787849de396fce0e74b8c62 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -145,3 +145,22 @@ Proof.
   apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
 Qed.
 End global.
+
+(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
+   the functor breaks badly because Coq is unable to infer the correct
+   typeclasses, it does not unfold the functor. *)
+Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
+  inGF_id : gid;
+  inGF_prf : F = Σ inGF_id;
+}.
+
+Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
+Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.
+
+Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
+Proof. exists 0. done. Qed.
+
+Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
+Proof. exists (S inGF_id). apply inGF_prf. Qed.
+
+Definition endF : gid → iFunctor := const (constF unitRA).
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index c6697b393371c2e1fa612fe23393098ad6febf79..6ab24d6127978ea43810ae94326e220b6a03ee8d 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,6 +5,9 @@ Import uPred.
 Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
+Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
+Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed.
+
 Definition saved_prop_own `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index c794ce2731aee6044ef44afdd4df87d644342eb6..b53c7dcb27ad605e74a8f18b86272fed55ac2fd4 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -8,6 +8,12 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 }.
 Coercion sts_inG : stsG >-> inG.
 
+Definition stsF (sts : stsT) := constF (stsRA sts).
+
+Instance stsG_inGF sts `{Inhabited (sts.state sts)}
+         `{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts.
+Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed.
+
 Section definitions.
   Context `{i : stsG Λ Σ sts} (γ : gname).
   Import sts.