[ re agda#357 ] Make Erase type play nice with instance search

jespercockx · Sep 7, 2024 · 59cfe72 · 59cfe72
1 parent 1078344
commit 59cfe72
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
@@ -14,8 +14,8 @@ module Haskell.Extra.Erase where
     @0 xs  : List a
 
   record Erase (@0 a : Set ℓ) : Set ℓ where
-    constructor Erased
-    field @0 get : a
+    instance constructor Erased
+    field @0 {{get}} : a
   open Erase public
   {-# COMPILE AGDA2HS Erase tuple #-}
 
@@ -69,11 +69,11 @@ module Haskell.Extra.Erase where
                    ne = subst NonEmpty p itsNonEmpty
   {-# COMPILE AGDA2HS rezzTail inline #-}
 
-  rezzErase : {@0 a : Set} {@0 x : a} → Rezz (Erased x)
-  rezzErase {x = x} = Erased x ⟨ refl ⟩
+  rezzErase : {@0 a : Set} {@0 x : a} → Rezz (Erased {{x}})
+  rezzErase {x = x} = Erased {{x}} ⟨ refl ⟩
   {-# COMPILE AGDA2HS rezzErase inline #-}
 
-  erase-injective : Erased x ≡ Erased y → x ≡ y
+  erase-injective : Erased {{x}} ≡ Erased {{y}} → x ≡ y
   erase-injective refl = refl
 
   inspect_by_ : (x : a) → (Rezz x → b) → b

diff --git a/test/EraseType.agda b/test/EraseType.agda
@@ -4,12 +4,12 @@ open import Haskell.Prelude
 open import Haskell.Extra.Erase
 
 testErase : Erase Int
-testErase = Erased 42
+testErase = Erased {{42}}
 
 {-# COMPILE AGDA2HS testErase #-}
 
 testMatch : Erase Int → Erase Int
-testMatch (Erased x) = Erased (x + 1)
+testMatch (Erased {{x}}) = Erased {{x + 1}}
 
 {-# COMPILE AGDA2HS testMatch #-}