From 80734767d3c1f73037e3d6246d3d2879b65e6801 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 15:21:27 +0200
Subject: [PATCH] [ re #357 ] Erase type arguments of `mapDec`

The types a and b do not appear in Haskell code, so they should be marked as erased
---
 lib/Haskell/Extra/Dec.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
index 5b2bd810..189ab353 100644
--- a/lib/Haskell/Extra/Dec.agda
+++ b/lib/Haskell/Extra/Dec.agda
@@ -35,7 +35,8 @@ Dec : ∀ {ℓ} → @0 Set ℓ → Set ℓ
 Dec P = ∃ Bool (Reflects P)
 {-# COMPILE AGDA2HS Dec inline #-}
 
-mapDec : @0 (a → b)
+mapDec : {@0 a b : Set}
+       → @0 (a → b)
        → @0 (b → a)
        → Dec a → Dec b
 mapDec f g (True  ⟨ x ⟩) = True  ⟨ f x   ⟩