Systematise use of Relation.Binary.Definitions.DecidableEquality (#2354)

* systematic use of `DecidableEquality`

* tweak

Author: jamesmckinna

src/Algebra/Solver/Monoid.agda

@@ -20,7 +20,7 @@ open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 import Relation.Binary.Reflection
@@ -114,7 +114,7 @@ open module R = Relation.Binary.Reflection
 
 infix 5 _≟_
 
-_≟_ : ∀ {n} → Decidable {A = Normal n} _≡_
+_≟_ : ∀ {n} → DecidableEquality (Normal n)
 nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
   where open ListEq Fin._≟_
 

src/Axiom/UniquenessOfIdentityProofs.agda

@@ -60,7 +60,7 @@ module Constant⇒UIP
 -- proof produced by the decision procedure.
 
 module Decidable⇒UIP
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+  {a} {A : Set a} (_≟_ : DecidableEquality A)
   where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_

src/Data/Bool/Properties.agda

@@ -25,7 +25,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Poset; Preorder; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
 open import Relation.Binary.Definitions
-  using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
+  using (Decidable; DecidableEquality; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness)
@@ -48,7 +48,7 @@ private
 
 infix 4 _≟_
 
-_≟_ : Decidable {A = Bool} _≡_
+_≟_ : DecidableEquality Bool
 true  ≟ true  = yes refl
 false ≟ false = yes refl
 true  ≟ false = no λ()

src/Data/Char/Properties.agda

@@ -23,7 +23,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
 open import Relation.Binary.Definitions
-  using (Decidable; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
+  using (Decidable; DecidableEquality; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
 import Relation.Binary.Construct.On as On
 import Relation.Binary.Construct.Subst.Equality as Subst
 import Relation.Binary.Construct.Closure.Reflexive as Refl
@@ -55,7 +55,7 @@ open import Agda.Builtin.Char.Properties
 -- Properties of _≡_
 
 infix 4 _≟_
-_≟_ : Decidable {A = Char} _≡_
+_≟_ : DecidableEquality Char
 x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y)
 
 setoid : Setoid _ _

src/Data/List/Membership/DecPropositional.agda

@@ -6,12 +6,12 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality using (_≡_)
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 module Data.List.Membership.DecPropositional
-  {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where
+  {a} {A : Set a} (_≟_ : DecidableEquality A) where
+
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 ------------------------------------------------------------------------
 -- Re-export contents of propositional membership

src/Data/List/Membership/Propositional/Properties.agda

@@ -259,7 +259,7 @@ module _ {r} {R : Rel A r} (R? : Binary.Decidable R) where
   ∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
   ∈-deduplicate⁻ xs z∈dedup[R,xs] = Membership.∈-deduplicate⁻ (≡.setoid A) R? xs z∈dedup[R,xs]
 
-module _ (_≈?_ : Binary.Decidable {A = A} _≡_) where
+module _ (_≈?_ : DecidableEquality A) where
 
   ∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs
   ∈-derun⁺ z∈xs = Membership.∈-derun⁺ (≡.setoid A) _≈?_ (flip trans) z∈xs

src/Data/List/Relation/Binary/Equality/DecPropositional.agda

@@ -10,16 +10,16 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 module Data.List.Relation.Binary.Equality.DecPropositional
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where
+  {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
 open import Data.List.Base using (List)
 open import Data.List.Properties using (≡-dec)
 import Data.List.Relation.Binary.Equality.Propositional as PropositionalEq
 import Data.List.Relation.Binary.Equality.DecSetoid as DecSetoidEq
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 ------------------------------------------------------------------------
 -- Publically re-export everything from decSetoid and propositional
@@ -34,5 +34,5 @@ open DecSetoidEq (decSetoid _≟_) public
 
 infix 4 _≡?_
 
-_≡?_ : Decidable (_≡_ {A = List A})
+_≡?_ : DecidableEquality (List A)
 _≡?_ = ≡-dec _≟_

src/Data/List/Relation/Binary/Sublist/DecPropositional.agda

@@ -8,19 +8,18 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Bundles using (DecPoset)
-open import Relation.Binary.Structures using (IsDecPartialOrder)
-open import Relation.Binary.Definitions using (Decidable)
-open import Agda.Builtin.Equality using (_≡_)
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 module Data.List.Relation.Binary.Sublist.DecPropositional
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+  {a} {A : Set a} (_≟_ : DecidableEquality A)
   where
 
 open import Data.List.Relation.Binary.Equality.DecPropositional _≟_
   using (_≡?_)
 import Data.List.Relation.Binary.Sublist.DecSetoid as DecSetoidSublist
 import Data.List.Relation.Binary.Sublist.Propositional as PropositionalSublist
+open import Relation.Binary.Bundles using (DecPoset)
+open import Relation.Binary.Structures using (IsDecPartialOrder)
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------

src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda

@@ -7,13 +7,12 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
-       {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+       {a} {A : Set a} (_≟_ : DecidableEquality A)
        where
 
-import Relation.Binary.PropositionalEquality.Properties as P
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
-open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (P.decSetoid _≟_) public
+open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (decSetoid _≟_) public

src/Data/Maybe/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (_∋_; id; _∘_; _∘′_)
 open import Function.Definitions using (Injective)
 open import Level using (Level)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
@@ -35,7 +35,7 @@ private
 just-injective : ∀ {x y} → (Maybe A ∋ just x) ≡ just y → x ≡ y
 just-injective refl = refl
 
-≡-dec : Decidable _≡_ → Decidable {A = Maybe A} _≡_
+≡-dec : DecidableEquality A → DecidableEquality (Maybe A)
 ≡-dec _≟_ nothing  nothing  = yes refl
 ≡-dec _≟_ (just x) nothing  = no λ()
 ≡-dec _≟_ nothing  (just y) = no λ()

src/Data/Nat/Binary/Properties.agda

@@ -67,7 +67,7 @@ infix 4  _<?_ _≟_ _≤?_
 1+[2_]-injective : Injective _≡_ _≡_ 1+[2_]
 1+[2_]-injective refl = refl
 
-_≟_ : Decidable {A = ℕᵇ} _≡_
+_≟_ : DecidableEquality ℕᵇ
 zero     ≟ zero     =  yes refl
 zero     ≟ 2[1+ _ ] =  no λ()
 zero     ≟ 1+[2 _ ] =  no λ()

src/Data/Record.agda

@@ -16,15 +16,14 @@ open import Data.Product.Base hiding (proj₁; proj₂)
 open import Data.Unit.Polymorphic
 open import Function.Base using (id; _∘_)
 open import Level
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
 -- The module is parametrised by the type of labels, which should come
 -- with decidable equality.
 
-module Data.Record {ℓ} (Label : Set ℓ) (_≟_ : Decidable {A = Label} _≡_) where
+module Data.Record {ℓ} (Label : Set ℓ) (_≟_ : DecidableEquality Label) where
 
 ------------------------------------------------------------------------
 -- A Σ-type with a manifest field

src/Data/String/Properties.agda

@@ -23,7 +23,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsDecPartialOrder; IsDecTotalOrder)
 open import Relation.Binary.Definitions
-  using (Reflexive; Symmetric; Transitive; Substitutive; Decidable)
+  using (Reflexive; Symmetric; Transitive; Substitutive; Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core
 import Relation.Binary.Construct.On as On
 import Relation.Binary.PropositionalEquality.Properties as PropEq
@@ -89,7 +89,7 @@ x ≈? y = Pointwise.decidable Char._≟_ (toList x) (toList y)
 
 infix 4 _≟_
 
-_≟_ : Decidable _≡_
+_≟_ : DecidableEquality String
 x ≟ y = map′ ≈⇒≡ ≈-reflexive $ x ≈? y
 
 ≡-setoid : Setoid _ _

src/Data/Sum/Properties.agda

@@ -12,7 +12,7 @@ open import Level
 open import Data.Sum.Base
 open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (mk↔ₛ′; _↔_)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
@@ -34,10 +34,10 @@ inj₁-injective refl = refl
 inj₂-injective : ∀ {x y} → (A ⊎ B ∋ inj₂ x) ≡ inj₂ y → x ≡ y
 inj₂-injective refl = refl
 
-module _ (dec₁ : Decidable {A = A} {B = A} _≡_)
-         (dec₂ : Decidable {A = B} {B = B} _≡_) where
+module _ (dec₁ : DecidableEquality A)
+         (dec₂ : DecidableEquality B) where
 
-  ≡-dec : Decidable {A = A ⊎ B} _≡_
+  ≡-dec : DecidableEquality (A ⊎ B)
   ≡-dec (inj₁ x) (inj₁ y) = map′ (cong inj₁) inj₁-injective (dec₁ x y)
   ≡-dec (inj₁ x) (inj₂ y) = no λ()
   ≡-dec (inj₂ x) (inj₁ y) = no λ()

src/Data/These/Properties.agda

@@ -11,7 +11,7 @@ module Data.These.Properties where
 open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry)
 open import Data.These.Base
 open import Function.Base using (_∘_)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 
@@ -35,7 +35,7 @@ module _ {a b} {A : Set a} {B : Set b} where
   these-injective : ∀ {x y : A} {a b : B} → these x a ≡ these y b → x ≡ y × a ≡ b
   these-injective = < these-injectiveˡ , these-injectiveʳ >
 
-  ≡-dec : Decidable _≡_ → Decidable _≡_ → Decidable {A = These A B} _≡_
+  ≡-dec : DecidableEquality A → DecidableEquality B → DecidableEquality (These A B)
   ≡-dec dec₁ dec₂ (this x)    (this y) =
     map′ (cong this) this-injective (dec₁ x y)
   ≡-dec dec₁ dec₂ (this x)    (that y)    = no λ()

src/Data/Unit/Polymorphic/Properties.agda

@@ -21,7 +21,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder)
 open import Relation.Binary.Definitions
-  using (Decidable; Antisymmetric; Total)
+  using (DecidableEquality; Antisymmetric; Total)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; trans; decSetoid; setoid; isEquivalence)
 
@@ -35,7 +35,7 @@ private
 
 infix 4 _≟_
 
-_≟_ : Decidable {A = ⊤ {ℓ}} _≡_
+_≟_ : DecidableEquality (⊤ {ℓ})
 _ ≟ _ = yes refl
 
 ≡-setoid : ∀ ℓ → Setoid ℓ ℓ

src/Data/Unit/Properties.agda

@@ -16,7 +16,7 @@ open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Poset; DecTotalOrder)
 open import Relation.Binary.Structures
   using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder)
-open import Relation.Binary.Definitions using (Decidable; Total; Antisymmetric)
+open import Relation.Binary.Definitions using (DecidableEquality; Total; Antisymmetric)
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
@@ -30,7 +30,7 @@ open import Relation.Binary.PropositionalEquality
 
 infix 4 _≟_
 
-_≟_ : Decidable {A = ⊤} _≡_
+_≟_ : DecidableEquality ⊤
 _ ≟ _ = yes refl
 
 ≡-setoid : Setoid 0ℓ 0ℓ

src/Data/Vec/Membership/DecPropositional.agda

@@ -6,12 +6,12 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_)
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 module Data.Vec.Membership.DecPropositional
-  {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where
+  {a} {A : Set a} (_≟_ : DecidableEquality A) where
+
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 ------------------------------------------------------------------------
 -- Re-export contents of propositional membership

src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda

@@ -6,14 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 module Data.Vec.Relation.Binary.Equality.DecPropositional
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where
+  {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
 import Data.Vec.Relation.Binary.Equality.Propositional as PEq
 import Data.Vec.Relation.Binary.Equality.DecSetoid as DSEq
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 ------------------------------------------------------------------------
 -- Publicly re-export everything from decSetoid and propositional

src/Effect/Monad/Partiality.agda

@@ -21,7 +21,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core as B hiding (Rel; _⇔_)
 open import Relation.Binary.Definitions
-  using (Decidable; Reflexive; Symmetric; Transitive)
+  using (DecidableEquality; Reflexive; Symmetric; Transitive)
 open import Relation.Binary.Structures
   using (IsPreorder; IsEquivalence)
 open import Relation.Binary.Bundles
@@ -115,7 +115,7 @@ data Kind : Set where
 
 infix 4 _≟-Kind_
 
-_≟-Kind_ : Decidable (_≡_ {A = Kind})
+_≟-Kind_ : DecidableEquality Kind
 _≟-Kind_ strong       strong       = yes ≡.refl
 _≟-Kind_ strong       (other k)    = no λ()
 _≟-Kind_ (other k)    strong       = no λ()

src/Reflection/AST/Term.agda

@@ -141,8 +141,8 @@ _≟-Clause_   : DecidableEquality Clause
 _≟-Clauses_  : DecidableEquality Clauses
 _≟_          : DecidableEquality Term
 _≟-Sort_     : DecidableEquality Sort
-_≟-Patterns_ : Decidable (_≡_ {A = Args Pattern})
-_≟-Pattern_  : Decidable (_≡_ {A = Pattern})
+_≟-Patterns_ : DecidableEquality (Args Pattern)
+_≟-Pattern_  : DecidableEquality Pattern
 
 -- Decidable equality 'transformers'
 -- We need to inline these because the terms are not sized so

src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda

@@ -17,7 +17,7 @@ open import Relation.Binary.Core using (Rel; REL; _=[_]⇒_)
 open import Relation.Binary.Structures
   using (IsPreorder; IsStrictPartialOrder; IsPartialOrder; IsDecStrictPartialOrder; IsDecPartialOrder; IsStrictTotalOrder; IsTotalOrder; IsDecTotalOrder)
 open import Relation.Binary.Definitions
-  using (Symmetric; Transitive; Reflexive; Asymmetric; Antisymmetric; Trichotomous; Total; Decidable; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects_; _Respects₂_)
+  using (Symmetric; Transitive; Reflexive; Asymmetric; Antisymmetric; Trichotomous; Total; Decidable; DecidableEquality; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects_; _Respects₂_)
 open import Relation.Binary.Construct.Closure.Reflexive
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as ≡
@@ -78,7 +78,7 @@ module _ {_~_ : Rel A ℓ} where
   ... | tri≈ _ refl _ = inj₁ refl
   ... | tri> _ _    c = inj₂ [ c ]
 
-  dec : Decidable {A = A} _≡_ → Decidable _~_ → Decidable _~ᵒ_
+  dec : DecidableEquality A → Decidable _~_ → Decidable _~ᵒ_
   dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b ⊎-dec ~-dec a b)
 
   decidable : Trichotomous _≡_ _~_ → Decidable _~ᵒ_

src/Relation/Binary/PropositionalEquality/Properties.agda

@@ -19,7 +19,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence; IsPreorder; IsPartialOrder)
 open import Relation.Binary.Definitions
-  using (Decidable; DecidableEquality)
+  using (DecidableEquality)
 import Relation.Binary.Properties.Setoid as Setoid
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Unary using (Pred)
@@ -157,7 +157,7 @@ isEquivalence = record
   ; trans = trans
   }
 
-isDecEquivalence : Decidable _≡_ → IsDecEquivalence {A = A} _≡_
+isDecEquivalence : DecidableEquality A → IsDecEquivalence _≡_
 isDecEquivalence _≟_ = record
   { isEquivalence = isEquivalence
   ; _≟_           = _≟_