also translate Erased to ()

agda · Dec 22, 2023 · 82bed82 · 82bed82
1 parent 59b96f1
commit 82bed82
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 2 deletions.
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
@@ -46,6 +46,7 @@ isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnP
 isSpecialPat qn = case prettyShow qn of
   "Haskell.Prim.Tuple._,_"         -> Just tuplePat
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
+  "Haskell.Extra.Erase.Erased"     -> Just tuplePat
   "Agda.Builtin.Int.Int.pos" -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat
   s | s `elem` badConstructors -> Just $ \ _ _ _ -> genericDocError =<<
@@ -62,7 +63,9 @@ isUnboxCopattern (ProjP _ q) = isJust <$> isUnboxProjection q
 isUnboxCopattern _           = return False
 
 tuplePat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())
-tuplePat cons i ps = mapM (compilePat . namedArg) ps <&> Hs.PTuple () Hs.Boxed
+tuplePat cons i ps =
+  mapM (compilePat . namedArg) (filter keepArg ps) 
+  <&> Hs.PTuple () Hs.Boxed
 
 -- Agda2Hs does not support natural number patterns directly (since
 -- they don't exist in Haskell), however they occur as part of

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

diff --git a/test/golden/EraseType.hs b/test/golden/EraseType.hs
@@ -1,5 +1,11 @@
 module EraseType where
 
+testErase :: ()
+testErase = ()
+
+testMatch :: () -> ()
+testMatch () = ()
+
 testRezz :: Int
 testRezz = 42