From b3056546a4b644aeff5912cc52430e855fb12ea5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Nov 2021 17:47:40 -0500
Subject: [PATCH] make sure all Instance/Argument have explicit visibility

---
 Makefile.coq.local                    | 11 ++++++++
 coq-lint.sh                           | 12 ++++++++
 theories/lang/adequacy.v              |  2 +-
 theories/lang/heap.v                  |  4 +--
 theories/lang/lang.v                  | 24 ++++++++--------
 theories/lang/lib/arc.v               |  4 +--
 theories/lang/lib/spawn.v             |  2 +-
 theories/lang/lifting.v               | 12 ++++----
 theories/lifetime/lifetime.v          |  2 +-
 theories/lifetime/lifetime_sig.v      |  2 +-
 theories/lifetime/meta.v              |  2 +-
 theories/lifetime/model/definitions.v | 14 +++++-----
 theories/lifetime/model/primitive.v   | 16 +++++------
 theories/typing/function.v            |  4 +--
 theories/typing/lft_contexts.v        | 16 +++++------
 theories/typing/lib/arc.v             |  2 +-
 theories/typing/lib/brandedvec.v      |  2 +-
 theories/typing/lib/ghostcell.v       |  6 ++--
 theories/typing/lib/rc/rc.v           |  2 +-
 theories/typing/lib/refcell/refcell.v |  2 +-
 theories/typing/lib/rwlock/rwlock.v   |  2 +-
 theories/typing/own.v                 |  2 +-
 theories/typing/product.v             |  2 +-
 theories/typing/programs.v            |  4 +--
 theories/typing/soundness.v           |  2 +-
 theories/typing/type.v                | 40 +++++++++++++--------------
 26 files changed, 108 insertions(+), 85 deletions(-)
 create mode 100644 Makefile.coq.local
 create mode 100755 coq-lint.sh

diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 00000000..1c985e35
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,11 @@
+# Run tests interleaved with main build.  They have to be in the same target for this.
+real-all: style
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+.PHONY: style
diff --git a/coq-lint.sh b/coq-lint.sh
new file mode 100755
index 00000000..3bdadfbb
--- /dev/null
+++ b/coq-lint.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+if egrep -n '^\s*((Existing\s+|Program\s+|Declare\s+|)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
+    echo "Please add 'Global' or 'Local' as appropriate."
+    echo
+    exit 1
+fi
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 5f41bde0..ec4b64cd 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -14,7 +14,7 @@ Definition lrustΣ : gFunctors :=
   #[invΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
+Global Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
 Proof. solve_inG. Qed.
 
 Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 2638b7c7..db57e30a 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -67,8 +67,8 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
-Instance: Params (@heap_mapsto) 4 := {}.
-Instance: Params (@heap_freeable) 5 := {}.
+Global Instance: Params (@heap_mapsto) 4 := {}.
+Global Instance: Params (@heap_freeable) 5 := {}.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 0a8dc273..ab1bb8ad 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -59,9 +59,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   end.
 
 Class Closed (X : list string) (e : expr) := closed : is_closed X e.
-Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
+Global Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
 Proof. rewrite /Closed. apply _. Qed.
-Instance closed_decision env e : Decision (Closed env e).
+Global Instance closed_decision env e : Decision (Closed env e).
 Proof. rewrite /Closed. apply _. Qed.
 
 Inductive val :=
@@ -347,10 +347,10 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+Global Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
 Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
 Lemma fill_item_val Ki e :
@@ -404,7 +404,7 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
 Lemma shift_loc_0_nat l : l +â‚— 0%nat = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
-Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
+Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
 Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
 
 Lemma shift_loc_block l n : (l +â‚— n).1 = l.1.
@@ -548,11 +548,11 @@ Lemma stuck_not_head_step σ e' κ σ' ef :
 Proof. inversion 1. Qed.
 
 (** Equality and other typeclass stuff *)
-Instance base_lit_dec_eq : EqDecision base_lit.
+Global Instance base_lit_dec_eq : EqDecision base_lit.
 Proof. solve_decision. Defined.
-Instance bin_op_dec_eq : EqDecision bin_op.
+Global Instance bin_op_dec_eq : EqDecision bin_op.
 Proof. solve_decision. Defined.
-Instance un_op_dec_eq : EqDecision order.
+Global Instance un_op_dec_eq : EqDecision order.
 Proof. solve_decision. Defined.
 
 Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
@@ -597,17 +597,17 @@ Proof.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
 Qed.
-Instance expr_dec_eq : EqDecision expr.
+Global Instance expr_dec_eq : EqDecision expr.
 Proof.
  refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
 Defined.
-Instance val_dec_eq : EqDecision val.
+Global Instance val_dec_eq : EqDecision val.
 Proof.
  refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
 
-Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
-Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
+Global Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
+Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
 
 Canonical Structure stateO := leibnizO state.
 Canonical Structure valO := leibnizO val.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 846d97bd..055bce80 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -110,7 +110,7 @@ Definition arc_stR :=
 Class arcG Σ :=
   RcG :> inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
 Section def.
@@ -161,7 +161,7 @@ Section arc.
   Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
           (P2 : iProp Σ) (N : namespace).
 
-  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+  Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
   Proof using HP1. done. Qed.
 
   Global Instance arc_inv_ne n :
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 4dd4154c..2b120455 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -31,7 +31,7 @@ Definition join : val :=
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
-Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 997ba3f1..2b39093d 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -11,7 +11,7 @@ Class lrustGS Σ := LRustGS {
   lrustGS_heapGS :> heapGS Σ
 }.
 
-Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+Global Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
   iris_invGS := lrustGS_invGS;
   state_interp σ _ κs _ := heap_ctx σ;
   fork_post _ := True%I;
@@ -39,8 +39,8 @@ Local Hint Resolve to_of_val : core.
 
 Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
   as_rec : e = Rec f xl erec.
-Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
-Instance AsRec_rec_locked_val v f xl e :
+Global Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
+Global Instance AsRec_rec_locked_val v f xl e :
   AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
 Proof. by unlock. Qed.
 
@@ -51,13 +51,13 @@ Global Hint Extern 0 (DoSubst _ _ _ _) =>
 
 Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
   do_subst_l : subst_l xl esl e = Some er.
-Instance do_subst_l_nil e : DoSubstL [] [] e e.
+Global Instance do_subst_l_nil e : DoSubstL [] [] e e.
 Proof. done. Qed.
-Instance do_subst_l_cons x xl es esl e er er' :
+Global Instance do_subst_l_cons x xl es esl e er er' :
   DoSubstL xl esl e er' → DoSubst x es er' er →
   DoSubstL (x :: xl) (es :: esl) e er.
 Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
-Instance do_subst_vec xl (vsl : vec val (length xl)) e :
+Global Instance do_subst_vec xl (vsl : vec val (length xl)) e :
   DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
 Proof. by rewrite /DoSubstL subst_v_eq. Qed.
 
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 27874643..3cf40a6b 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -18,7 +18,7 @@ End lifetime.
 
 Notation lft_intersect_list l := (foldr (⊓) static l).
 
-Instance lft_inhabited : Inhabited lft := populate static.
+Global Instance lft_inhabited : Inhabited lft := populate static.
 
 Canonical lftO := leibnizO lft.
 
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index c179f0fa..134e2ba1 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -23,7 +23,7 @@ Module Type lifetime_sig.
   (** * Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Declare Instance lft_intersect : Meet lft.
+  Global Declare Instance lft_intersect : Meet lft.
 
   Parameter lft_ctx : ∀ `{!invGS Σ, !lftGS Σ userE}, iProp Σ.
 
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 8a535061..80ebbcc7 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -11,7 +11,7 @@ Class lft_metaG Σ := LftMetaG {
 }.
 Definition lft_metaΣ : gFunctors :=
   #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
-Instance subG_lft_meta Σ :
+Global Instance subG_lft_meta Σ :
   subG (lft_metaΣ) Σ → lft_metaG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 6c5c38b4..418e1a91 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -66,7 +66,7 @@ Definition lftGpreS' := lftGpreS.
 Definition lftΣ : gFunctors :=
   #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftGpreS Σ :
+Global Instance subG_lftGpreS Σ :
   subG lftΣ Σ → lftGpreS Σ.
 Proof. solve_inG. Qed.
 
@@ -200,12 +200,12 @@ Section defs.
     (∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
 End defs.
 
-Instance: Params (@lft_bor_alive) 4 := {}.
-Instance: Params (@lft_inh) 5 := {}.
-Instance: Params (@lft_vs) 4 := {}.
-Instance idx_bor_params : Params (@idx_bor) 5 := {}.
-Instance raw_bor_params : Params (@raw_bor) 4 := {}.
-Instance bor_params : Params (@bor) 4 := {}.
+Global Instance: Params (@lft_bor_alive) 4 := {}.
+Global Instance: Params (@lft_inh) 5 := {}.
+Global Instance: Params (@lft_vs) 4 := {}.
+Global Instance idx_bor_params : Params (@idx_bor) 5 := {}.
+Global Instance raw_bor_params : Params (@raw_bor) 4 := {}.
+Global Instance bor_params : Params (@bor) 4 := {}.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 140b4d73..080794f6 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -254,14 +254,14 @@ Proof.
 Qed.
 
 (** Basic rules about lifetimes  *)
-Instance lft_inhabited : Inhabited lft := _.
-Instance bor_idx_inhabited : Inhabited bor_idx := _.
-Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
-Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
-Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
-Instance lft_intersect_right_id : RightId eq static (⊓) := _.
+Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Local Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
+Local Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
+Local Instance lft_intersect_right_id : RightId eq static (⊓) := _.
 
 Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
 Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 514d37fc..4111d6e4 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -113,7 +113,7 @@ Section fn.
   Qed.
 End fn.
 
-Arguments fn_params {_ _} _.
+Global Arguments fn_params {_ _} _.
 
 (* We use recursive notation for binders as well, to allow patterns
    like '(a, b) to be used. In practice, only one binder is ever used,
@@ -139,7 +139,7 @@ Notation "'fn(' E ')' '→' R" :=
   (at level 99, R at level 200,
    format "'fn(' E ')'  '→'  R") : lrust_type_scope.
 
-Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
+Global Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
 
 Section typing.
   Context `{!typeGS Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index fd97c826..40f82bf1 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -406,14 +406,14 @@ Section lft_contexts.
   Proof. iIntros (??) "_ !> ?". done. Qed.
 End lft_contexts.
 
-Arguments lctx_lft_incl {_ _} _ _ _ _.
-Arguments lctx_lft_eq {_ _} _ _ _ _.
-Arguments lctx_lft_alive {_ _ _} _ _ _.
-Arguments elctx_sat {_ _} _ _ _.
-Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
-Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
-Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
-Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
+Global Arguments lctx_lft_incl {_ _} _ _ _ _.
+Global Arguments lctx_lft_eq {_ _} _ _ _ _.
+Global Arguments lctx_lft_alive {_ _ _} _ _ _.
+Global Arguments elctx_sat {_ _} _ _ _.
+Global Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
+Global Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
+Global Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
+Global Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
 Lemma elctx_sat_submseteq `{!invGS Σ, !lftGS Σ lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 1c818641..865d1692 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -17,7 +17,7 @@ Section arc.
 
   (* Preliminary definitions. *)
   Let P1 ν q := (q.[ν])%I.
-  Instance P1_fractional ν : Fractional (P1 ν).
+  Local Instance P1_fractional ν : Fractional (P1 ν).
   Proof. unfold P1. apply _. Qed.
   Let P2 l n := († l…(2 + n) ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
   Definition arc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index ef673b5a..1a104e77 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -14,7 +14,7 @@ Class brandidxG Σ := BrandedIdxG {
 
 Definition brandidxΣ : gFunctors
   := #[GFunctor (authR brandidx_stR); lft_metaΣ].
-Instance subG_brandidxΣ {Σ} : subG brandidxΣ Σ → brandidxG Σ.
+Global Instance subG_brandidxΣ {Σ} : subG brandidxΣ Σ → brandidxG Σ.
 Proof. solve_inG. Qed.
 
 Definition brandidxN := lrustN .@ "brandix".
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 6ff1ae07..0caa82fe 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -76,7 +76,7 @@ Class ghostcellG Σ := GhostcellG {
 Definition ghostcellΣ : gFunctors
   := #[GFunctor ghosttoken_stR ; lft_metaΣ].
 
-Instance subG_ghostcellΣ {Σ} : subG ghostcellΣ Σ → ghostcellG Σ.
+Global Instance subG_ghostcellΣ {Σ} : subG ghostcellΣ Σ → ghostcellG Σ.
 Proof. solve_inG. Qed.
 
 (* There are two possible states:
@@ -375,8 +375,6 @@ Section ghostcell.
     eqtype E L (ghostcell κ1 ty1) (ghostcell κ2 ty2).
   Proof. intros. by apply ghostcell_proper. Qed.
 
-  Hint Resolve ghostcell_mono' ghostcell_proper' : lrust_typing.
-
   Global Instance ghostcell_send α ty :
     Send ty → Send (ghostcell α ty).
   Proof. by unfold ghostcell, Send. Qed.
@@ -753,3 +751,5 @@ Section ghostcell.
   Qed.
 
 End ghostcell.
+
+Global Hint Resolve ghostcell_mono' ghostcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 1c186f39..a597e9b3 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -11,7 +11,7 @@ Definition rc_stR :=
 Class rcG Σ :=
   RcG :> inG Σ (authR rc_stR).
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
-Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
+Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
 Proof. solve_inG. Qed.
 
 Definition rc_tok q : authR rc_stR :=
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index e081d017..f50434c7 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -13,7 +13,7 @@ Definition refcell_stR :=
 Class refcellG Σ :=
   RefCellG :> inG Σ (authR refcell_stR).
 Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
-Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
+Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
 
 Definition refcell_st := option ((lft * Datatypes.bool) * frac * positive).
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 5df708e4..f211296c 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -10,7 +10,7 @@ Definition rwlock_stR :=
 Class rwlockG Σ :=
   RwLockG :> inG Σ (authR rwlock_stR).
 Definition rwlockΣ : gFunctors := #[GFunctor (authR rwlock_stR)].
-Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
+Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
 
 Definition Z_of_rwlock_st (st : rwlock_stR) : Z :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 05911b24..abf06d11 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -13,7 +13,7 @@ Section own.
     | _, 0%nat => False
     | sz, n => †{pos_to_Qp (Pos.of_nat sz) / pos_to_Qp (Pos.of_nat n)}l…sz
     end%I.
-  Arguments freeable_sz : simpl never.
+  Global Arguments freeable_sz : simpl never.
 
   Global Instance freeable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index cea73ac8..701bfc65 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -263,7 +263,7 @@ Section typing.
   Qed.
 End typing.
 
-Arguments product : simpl never.
+Global Arguments product : simpl never.
 Global Hint Opaque product : lrust_typing lrust_typing_merge.
 Global Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
   : lrust_typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index c4692f28..abc8515b 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -104,11 +104,11 @@ End typing.
 Definition typed_instruction_ty `{!typeGS Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : iProp Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
-Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
+Global Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
 Definition typed_val `{!typeGS Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
-Arguments typed_val _ _ _%V _%T.
+Global Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
   Context `{!typeGS Σ}.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 294469f0..a2623b75 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -16,7 +16,7 @@ Class typeGpreS Σ := PreTypeG {
 
 Definition typeΣ : gFunctors :=
   #[lrustΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
-Instance subG_typeGpreS {Σ} : subG typeΣ Σ → typeGpreS Σ.
+Global Instance subG_typeGpreS {Σ} : subG typeΣ Σ → typeGpreS Σ.
 Proof. solve_inG. Qed.
 
 Section type_soundness.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5c78ab2c..f197ac81 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,11 +50,11 @@ Global Instance: Params (@ty_size) 2 := {}.
 Global Instance: Params (@ty_own) 2 := {}.
 Global Instance: Params (@ty_shr) 2 := {}.
 
-Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
+Global Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
 Class TyWf `{!typeGS Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
-Arguments ty_lfts {_ _} _ {_}.
-Arguments ty_wf_E {_ _} _ {_}.
+Global Arguments ty_lfts {_ _} _ {_}.
+Global Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> (ty_lfts ty).
@@ -77,7 +77,7 @@ Inductive ListTyWf `{!typeGS Σ} : list type → Type :=
 | list_ty_wf_nil : ListTyWf []
 | list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
 Existing Class ListTyWf.
-Existing Instances list_ty_wf_nil list_ty_wf_cons.
+Global Existing Instances list_ty_wf_nil list_ty_wf_cons.
 
 Fixpoint tyl_lfts `{!typeGS Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
@@ -117,7 +117,7 @@ Record simple_type `{!typeGS Σ} :=
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
-Instance: Params (@st_own) 2 := {}.
+Global Instance: Params (@st_own) 2 := {}.
 
 Program Definition ty_of_st `{!typeGS Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
@@ -157,14 +157,14 @@ Section ofe.
       (∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡ ty2.(ty_shr) κ tid l) →
       type_equiv' ty1 ty2.
-  Instance type_equiv : Equiv type := type_equiv'.
+  Local Instance type_equiv : Equiv type := type_equiv'.
   Inductive type_dist' (n : nat) (ty1 ty2 : type) : Prop :=
     Type_dist :
       ty1.(ty_size) = ty2.(ty_size) →
       (∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ ty2.(ty_own) tid vs) →
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
       type_dist' n ty1 ty2.
-  Instance type_dist : Dist type := type_dist'.
+  Local Instance type_dist : Dist type := type_dist'.
 
   Let T := prodO
     (prodO natO (thread_id -d> list val -d> iPropO Σ))
@@ -225,12 +225,12 @@ Section ofe.
     St_equiv :
       (∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
       st_equiv' ty1 ty2.
-  Instance st_equiv : Equiv simple_type := st_equiv'.
+  Local Instance st_equiv : Equiv simple_type := st_equiv'.
   Inductive st_dist' (n : nat) (ty1 ty2 : simple_type) : Prop :=
     St_dist :
       (∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ (ty2.(ty_own) tid vs)) →
       st_dist' n ty1 ty2.
-  Instance st_dist : Dist simple_type := st_dist'.
+  Local Instance st_dist : Dist simple_type := st_dist'.
 
   Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iPropO Σ :=
     λ tid vl, ty.(ty_own) tid vl.
@@ -399,31 +399,31 @@ Class Copy `{!typeGS Σ} (t : type) := {
       (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
                                   ={E}=∗ na_own tid F ∗ q.[κ])
 }.
-Existing Instances copy_persistent.
-Instance: Params (@Copy) 2 := {}.
+Global Existing Instances copy_persistent.
+Global Instance: Params (@Copy) 2 := {}.
 
 Class ListCopy `{!typeGS Σ} (tys : list type) := lst_copy : Forall Copy tys.
-Instance: Params (@ListCopy) 2 := {}.
+Global Instance: Params (@ListCopy) 2 := {}.
 Global Instance lst_copy_nil `{!typeGS Σ} : ListCopy [] := List.Forall_nil _.
 Global Instance lst_copy_cons `{!typeGS Σ} ty tys :
   Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Send `{!typeGS Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
-Instance: Params (@Send) 2 := {}.
+Global Instance: Params (@Send) 2 := {}.
 
 Class ListSend `{!typeGS Σ} (tys : list type) := lst_send : Forall Send tys.
-Instance: Params (@ListSend) 2 := {}.
+Global Instance: Params (@ListSend) 2 := {}.
 Global Instance lst_send_nil `{!typeGS Σ} : ListSend [] := List.Forall_nil _.
 Global Instance lst_send_cons `{!typeGS Σ} ty tys :
   Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Sync `{!typeGS Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
-Instance: Params (@Sync) 2 := {}.
+Global Instance: Params (@Sync) 2 := {}.
 
 Class ListSync `{!typeGS Σ} (tys : list type) := lst_sync : Forall Sync tys.
-Instance: Params (@ListSync) 2 := {}.
+Global Instance: Params (@ListSync) 2 := {}.
 Global Instance lst_sync_nil `{!typeGS Σ} : ListSync [] := List.Forall_nil _.
 Global Instance lst_sync_cons `{!typeGS Σ} ty tys :
   Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
@@ -536,23 +536,23 @@ Definition type_incl `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
-Instance: Params (@type_incl) 2 := {}.
+Global Instance: Params (@type_incl) 2 := {}.
 (* Typeclasses Opaque type_incl. *)
 
 Definition type_equal `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl ∗-∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
-Instance: Params (@type_equal) 2 := {}.
+Global Instance: Params (@type_equal) 2 := {}.
 
 Definition subtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
-Instance: Params (@subtype) 4 := {}.
+Global Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
 Definition eqtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
-Instance: Params (@eqtype) 4 := {}.
+Global Instance: Params (@eqtype) 4 := {}.
 
 Section subtyping.
   Context `{!typeGS Σ}.
-- 
GitLab