Mode checking works, these were agressive unifications

That should not be allowed

theories/algebra/gmap.v

@@ -49,7 +49,7 @@ Global Instance lookup_ne k :
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
-Global Instance alter_ne f k n :
+Global Instance alter_ne (f : A → A) (k : K) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
 Proof.
   intros ? m m' Hm k'.

theories/algebra/list.v

@@ -340,13 +340,13 @@ Section properties.
     rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
   Qed.
 
-  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
+  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
   Proof.
     rewrite /singletonM /list_singletonM.
     by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
   Qed.
   Lemma list_op_singletonM i (x y : A) :
-    {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
+    {[ i := x ]} ⋅ {[ i := y ]} ≡@{list A} {[ i := x ⋅ y ]}.
   Proof.
     rewrite /singletonM /list_singletonM /=.
     induction i; constructor; rewrite ?left_id; auto.