Remove --overlapping-instances

- In light of a recent issue with `--overlapping-instances`
  (c.f. agda/agda#6895), I removed
  all uses of overlapping in the codebase, which we actually redundant.

- `Foreign.Convertible` no longer relying on `Coercible`.

- `Axiom.Set.List` now exports general decidable equality to avoid ambiguity
  when `Interface.DecEq.DecEq⇒Dec` is also in scope.

src/Axiom/Set/List.agda

@@ -55,9 +55,8 @@ module Decˡ {A : Type} ⦃ _ : DecEq A ⦄ where
   _∈?_ : Dec₂ (_∈ˡ_ {A = A})
   _∈?_ a = Any.any? (a ≟_)
 
-  ≟-∅ : {X : Set A} → Dec (X ≡ ∅)
-  ≟-∅ {[]}    = yes refl
-  ≟-∅ {x ∷ X} = no (λ ())
+  DecEq-Set : DecEq (Set A)
+  DecEq-Set = DecEq-List
 
 List-Modelᵈ : Theoryᵈ
 List-Modelᵈ = record

src/Foreign/Convertible.agda

@@ -1,45 +1,64 @@
-{-# OPTIONS --overlapping-instances #-}
 module Foreign.Convertible where
 
-open import Ledger.Prelude hiding (map)
-
-open import Data.List using (map)
-
-open import Foreign.Haskell
-open import Foreign.Haskell.Coerce
+open import Ledger.Prelude
 
 record Convertible (A B : Set) : Set where
   field to   : A → B
         from : B → A
-
 open Convertible ⦃...⦄ public
 
-private variable A B A' B' K K' V V' : Set
+private variable
+  A B A' B' K K' V V' : Set
+  P Q : Set → Set
+
+Convertible₁ : (Set → Set) → (Set → Set) → Set₁
+Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
+
+Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁
+Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
 
 Convertible-Refl : Convertible A A
 Convertible-Refl = λ where
   .to   → id
   .from → id
 
+-- ** instances
+
+Bifunctor⇒Convertible : ∀ {F : Set → Set → Set} → ⦃ Bifunctor F ⦄
+  → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄
+  → Convertible (F A B) (F A' B')
+Bifunctor⇒Convertible ⦃ _ ⦄ ⦃ ca ⦄ ⦃ cb ⦄ = λ where
+  .to   → bimap (to ⦃ ca ⦄) (to ⦃ cb ⦄)
+  .from → bimap (from ⦃ ca ⦄) (from ⦃ cb ⦄)
+
+open import Foreign.Haskell
+
 instance
-  Coercible⇒Convertible : ⦃ Coercible A B ⦄ → Convertible A B
-  Coercible⇒Convertible = λ where
-    .to   → coerce
-    .from → coerce ⦃ TrustMe ⦄ -- coercibility is symmetric, I promise
+  Convertible-× : Convertible₂ _×_ _×_
+  Convertible-× = Bifunctor⇒Convertible
 
-  Convertible-Pair : ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄
-                   → Convertible (A × B) (Pair A' B')
+  Convertible-Pair : Convertible₂ _×_ Pair
   Convertible-Pair = λ where
-    .to   (a , b) → to a   , to b
+    .to   (a , b) → to   a , to   b
     .from (a , b) → from a , from b
 
-  Convertible-FinSet : ⦃ Convertible A A' ⦄ → Convertible (ℙ A) (List A')
+  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
+  Convertible-⊎ = Bifunctor⇒Convertible
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   (inj₁ a) → left  (to a)
+    .to   (inj₂ b) → right (to b)
+    .from (left a)  → inj₁ (from a)
+    .from (right b) → inj₂ (from b)
+
+  Convertible-FinSet : Convertible₁ ℙ_ List
   Convertible-FinSet = λ where
     .to   s → map to (setToList s)
     .from l → fromList (map from l)
 
   Convertible-Map : ⦃ DecEq K ⦄ → ⦃ Convertible K K' ⦄ → ⦃ Convertible V V' ⦄
-                  → Convertible (K ⇀ V) (List $ Pair K' V')
+    → Convertible (K ⇀ V) (List $ Pair K' V')
   Convertible-Map = λ where
     .to   m → to (proj₁ m)
     .from m → fromListᵐ (map from m)

src/Ledger/Foreign/HSLedger.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --overlapping-instances #-}
-
 module Ledger.Foreign.HSLedger where
 
 open import Ledger.Prelude; open Computational
@@ -12,7 +10,6 @@ open import Data.Nat.Properties using (+-0-commutativeMonoid)
 open import Relation.Binary.Morphism.Structures
 
 open import Foreign.Convertible
-open import Foreign.Haskell.Coerce
 
 import Ledger.Foreign.LedgerTypes as F
 
@@ -166,6 +163,8 @@ open TransactionStructure           HSTransactionStructure
   hiding (PParams)
 
 instance
+  _ = Convertible-Refl
+
   -- Since the foreign address is just a number, we do bad stuff here
   Convertible-Addr : Convertible Addr F.Addr
   Convertible-Addr = λ where
@@ -178,20 +177,20 @@ instance
   Convertible-TxBody : Convertible TxBody F.TxBody
   Convertible-TxBody = λ where
     .to txb → let open TxBody txb in record
-      { txins  = to ⦃ Convertible-FinSet ⦃ Coercible⇒Convertible ⦄ ⦄ txins
+      { txins  = to txins
       ; txouts = to txouts
       ; txfee  = txfee
-      ; txvldt = coerce txvldt
+      ; txvldt = to txvldt
       ; txsize = txsize
       ; txid   = txid
       }
     .from txb → let open F.TxBody txb in record
-      { txins      = from ⦃ Convertible-FinSet ⦃ Coercible⇒Convertible ⦄ ⦄ txins
+      { txins      = from txins
       ; txouts     = from txouts
       ; txcerts    = []
       ; mint       = ε -- since simpleTokenAlgebra only contains ada mint will always be empty
       ; txfee      = txfee
-      ; txvldt     = coerce txvldt
+      ; txvldt     = from txvldt
       ; txwdrls    = ∅ᵐ
       ; txup       = nothing
       ; txADhash   = nothing
@@ -236,7 +235,7 @@ instance
       ; minUTxOValue      = minUTxOValue
       ; poolDeposit       = poolDeposit
       ; Emax              = Emax
-      ; pv                = coerce pv
+      ; pv                = to pv
       ; votingThresholds  = _
       ; govActionLifetime = govActionLifetime
       ; govActionDeposit  = govActionDeposit
@@ -256,7 +255,7 @@ instance
       ; poolDeposit       = poolDeposit
       ; Emax              = Emax
       ; collateralPercent = 0
-      ; pv                = coerce pv
+      ; pv                = from pv
         -- TODO: translate these once they are implemented in F.PParams
       ; drepThresholds    = record
         { P1  = ½ ; P2a = ½ ; P2b = ½ ; P3  = ½ ; P4 = ½
@@ -282,15 +281,13 @@ instance
   Convertible-UTxOState : Convertible UTxOState F.UTxOState
   Convertible-UTxOState = λ where
     .to record { utxo = utxo ; fees = fees } →
-        record { utxo = to ⦃ conv-utxo ⦄ utxo ; fees = fees }
-    .from s → record
-      { utxo      = from ⦃ conv-utxo ⦄ $ F.UTxOState.utxo s
-      ; fees      = F.UTxOState.fees s
+        record { utxo = to utxo ; fees = fees }
+    .from s → let open F.UTxOState s in record
+      { utxo      = from utxo
+      ; fees      = fees
       ; deposits  = ∅ᵐ
       ; donations = ε
       }
-   where conv-utxo : Convertible UTxO F.UTxO
-         conv-utxo = Convertible-Map ⦃ DecEq-Product ⦄ ⦃ Coercible⇒Convertible ⦄
 
 utxo-step : F.UTxOEnv → F.UTxOState → F.TxBody → Maybe F.UTxOState
 utxo-step e s txb = to <$> UTXO-step (from e) (from s) (from txb)

src/Ledger/Prelude.agda

@@ -70,8 +70,9 @@ abstract
   setToList : {A : Set} → ℙ A → List A
   setToList = id
 
-  ≟-∅ : {A : Set} ⦃ _ : DecEq A ⦄ → {X : ℙ A} → Dec (X ≡ ∅)
-  ≟-∅ = L.Decˡ.≟-∅
+  instance
+    DecEq-ℙ : {A : Set} ⦃ _ : DecEq A ⦄ → DecEq (ℙ A)
+    DecEq-ℙ = L.Decˡ.DecEq-Set
 
 open import Axiom.Set.Rel th public
   hiding (_∣'_; _↾'_)
@@ -83,7 +84,7 @@ open import Axiom.Set.TotalMap th public
 open import Axiom.Set.TotalMapOn th
 
 open L.Decˡ public
-  hiding (_∈?_; ≟-∅)
+  hiding (_∈?_; DecEq-Set)
 
 open import Axiom.Set.Sum th public
 open import Axiom.Set.Map.Dec List-Modelᵈ public

src/Ledger/Utxo.lagda

@@ -5,7 +5,6 @@
 
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
-{-# OPTIONS --overlapping-instances #-}
 
 open import Algebra              using (CommutativeMonoid)
 open import Data.Integer.Ext     using (posPart; negPart)
@@ -153,8 +152,6 @@ record UTxOState : Set where
 
 open HasDecPartialOrder ⦃ ... ⦄
 instance
-  _ = ≟-∅
-
   netId? : ∀ {A : Set} {networkId : Network} {f : A → Network}
     → Dec₁ (λ a → f a ≡ networkId)
   netId? {_} {networkId} {f} .Dec₁.P? a = f a ≟ networkId

src/MidnightExample/HSLedger.agda

@@ -1,4 +1,3 @@
-{-# OPTIONS --overlapping-instances #-}
 module MidnightExample.HSLedger where
 
 open import Prelude hiding (_++_)
@@ -28,7 +27,6 @@ instance
 open import MidnightExample.Ledger Hash
 
 open import Foreign.Convertible
-open import Foreign.Haskell.Coerce
 
 instance
   Convertible-Point : Convertible Point F.Point