Add implicit arguments required after fix of agda/agda#4174

Author: UlfNorell

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -112,7 +112,7 @@ module _ {a} {A : Set a} where
     x ∷ v ∷ xs ++ ys        <<⟨ refl ⟩
     v ∷ x ∷ xs ++ ys        ∎
 
-  drop-mid-≡ : ∀ {x} ws xs {ys} {zs} →
+  drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
                ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
                ws ++ ys ↭ xs ++ zs
   drop-mid-≡ []       []       eq   with cong tail eq
@@ -291,7 +291,7 @@ module _ {a} {A : Set a} where
     ... | res rewrite ↭-sym-involutive p = res
 
   ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_
-  ∼bag⇒↭ {[]} eq with empty-unique (Inv.sym eq)
+  ∼bag⇒↭ {[]} eq with empty-unique {A = A} (Inv.sym eq)
   ... | refl = refl
   ∼bag⇒↭ {x ∷ xs} eq with ∈-∃++ (to ⟨$⟩ (here ≡.refl))
     where open Inv.Inverse (eq {x})

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -230,7 +230,7 @@ module _ {P : Pred A p} {Q : Pred B q} where
       | lose∘find q
       = refl
 
-    to∘from : ∀ pq → Any-×⁺ (Any-×⁻ pq) ≡ pq
+    to∘from : ∀ pq → Any-×⁺ {xs} (Any-×⁻ pq) ≡ pq
     to∘from pq
       with find pq
         | (λ (f : (proj₁ (find pq) ≡_) ⋐ _) → map∘find pq {f})