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

jespercockx · Sep 9, 2024 · 2d085c1 · 2d085c1
1 parent 03c9aae
commit 2d085c1
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
@@ -14,11 +14,13 @@ module Haskell.Extra.Erase where
     @0 xs  : List a
 
   record Erase (@0 a : Set ℓ) : Set ℓ where
-    constructor Erased
-    field @0 get : a
+    instance constructor iErased
+    field @0 {{get}} : a
   open Erase public
   {-# COMPILE AGDA2HS Erase tuple #-}
 
+  pattern Erased x = iErased {{x}}
+
   infixr 4 ⟨_⟩_
   record Σ0 (@0 a : Set) (b : @0 a → Set) : Set where
     constructor ⟨_⟩_