Compile Erase to ()

lib/Haskell/Extra/Erase.agda

@@ -13,7 +13,6 @@ module Haskell.Extra.Erase where
     constructor Erased
     field @0 get : a
   open Erase public
-  {-# COMPILE AGDA2HS Erase #-}
 
   infixr 4 ⟨_⟩_
   record Σ0 (@0 a : Set) (b : @0 a → Set) : Set where

src/Agda2Hs/Compile/Term.hs

@@ -57,6 +57,7 @@ isSpecialCon :: QName -> Maybe (ConHead -> ConInfo -> Elims -> C (Hs.Exp ()))
 isSpecialCon = prettyShow >>> \case
   "Haskell.Prim.Tuple._,_"         -> Just tupleTerm
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tupleTerm
+  "Haskell.Extra.Erase.Erased"     -> Just (\_ _ _ -> erasedTerm)
   _ -> Nothing
 
 tupleTerm :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())
@@ -160,6 +161,9 @@ sequ q (e:es) = do
     vs -> return $ hsVar "_>>_" `eApp` vs
 sequ q [] = return $ hsVar "_>>_"
 
+erasedTerm :: C (Hs.Exp ())
+erasedTerm = return $ Hs.Tuple () Hs.Boxed []
+
 caseOf :: QName -> Elims -> C (Hs.Exp ())
 caseOf _ es = compileElims es >>= \case
   -- applied to pattern lambda

src/Agda2Hs/Compile/Type.hs

@@ -43,6 +43,7 @@ isSpecialType :: QName -> Maybe (QName -> Elims -> C (Hs.Type ()))
 isSpecialType = prettyShow >>> \case
   "Haskell.Prim.Tuple._×_"   -> Just tupleType
   "Haskell.Prim.Tuple._×_×_" -> Just tupleType
+  "Haskell.Extra.Erase.Erase" -> Just erasedType
   _ -> Nothing
 
 tupleType :: QName -> Elims -> C (Hs.Type ())
@@ -51,6 +52,9 @@ tupleType q es = do
   ts <- mapM (compileType . unArg) as
   return $ Hs.TyTuple () Hs.Boxed ts
 
+erasedType :: QName -> Elims -> C (Hs.Type ())
+erasedType _ _ = return $ Hs.TyTuple () Hs.Boxed []
+
 -- | Add a class constraint to a Haskell type.
 constrainType
   :: Hs.Asst () -- ^ The class assertion.

test/AllTests.agda

@@ -64,6 +64,7 @@ import ModuleParameters
 import ModuleParametersImports
 import Coerce
 import Inlining
+import EraseType
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -128,4 +129,5 @@ import ModuleParameters
 import ModuleParametersImports
 import Coerce
 import Inlining
+import EraseType
 #-}

test/EraseType.agda

@@ -0,0 +1,19 @@
+module EraseType where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Erase
+
+testErase : Erase Int
+testErase = Erased 42
+
+{-# COMPILE AGDA2hs testErase #-}
+
+testRezz : Rezz Int (get testErase)
+testRezz = rezz 42
+
+{-# COMPILE AGDA2HS testRezz #-}
+
+testRezzErase : Rezz (Erase Int) testErase
+testRezzErase = rezzErase
+
+{-# COMPILE AGDA2HS testRezzErase #-}

test/golden/AllTests.hs

@@ -62,4 +62,5 @@ import ModuleParameters
 import ModuleParametersImports
 import Coerce
 import Inlining
+import EraseType
 

test/golden/EraseType.hs

@@ -0,0 +1,10 @@
+module EraseType where
+
+import Haskell.Extra.Erase (rezzErase)
+
+testRezz :: Int
+testRezz = 42
+
+testRezzErase :: ()
+testRezzErase = rezzErase
+

test/golden/Haskell/Extra/Erase.hs

@@ -0,0 +1,17 @@
+module Haskell.Extra.Erase where
+
+rezzCong :: (a -> b) -> a -> b
+rezzCong f x = f x
+
+rezzCong2 :: (a -> b -> c) -> a -> b -> c
+rezzCong2 f x y = f x y
+
+rezzHead :: [a] -> a
+rezzHead (x : xs) = x
+
+rezzTail :: [a] -> [a]
+rezzTail (x : xs) = xs
+
+rezzErase :: ()
+rezzErase = ()
+