New module Erase for dealing with erased and resurrected values

lib/Haskell/Extra/Erase.agda

@@ -0,0 +1,80 @@
+module Haskell.Extra.Erase where
+
+  open import Agda.Primitive
+  open import Agda.Builtin.Sigma
+  open import Agda.Builtin.Equality
+
+  open import Haskell.Prim
+  open import Haskell.Prim.List
+  open import Haskell.Law.Equality
+
+  private variable 
+    @0 x y : a
+    @0 xs  : List a
+
+  record Erase (@0 a : Set ℓ) : Set ℓ where
+    constructor Erased
+    field @0 get : a
+  open Erase public
+
+  infixr 4 ⟨_⟩_
+  record Σ0 (@0 a : Set) (b : @0 a → Set) : Set where
+    constructor ⟨_⟩_
+    field
+      @0 proj₁ : a
+      proj₂ : b proj₁
+  open Σ0 public
+  {-# COMPILE AGDA2HS Σ0 unboxed #-}
+
+  pattern <_> x = record { proj₁ = _ ; proj₂ = x }
+
+  -- Resurrection of erased values
+  record Rezz (a : Set ℓ) (@0 x : a) : Set ℓ where
+    constructor Rezzed
+    field
+      rezzed    : a
+      @0 isRezz : rezzed ≡ x
+  open Rezz public
+  {-# COMPILE AGDA2HS Rezz unboxed #-}
+
+  pattern rezz x = Rezzed x refl
+
+  instance
+    rezz-id : {x : a} → Rezz a x
+    rezz-id = rezz _
+
+  rezzCong : {@0 a : Set} {@0 x : a} (f : a → b) → Rezz a x → Rezz b (f x)
+  rezzCong f (Rezzed x p) = Rezzed (f x) (cong f p)
+  {-# COMPILE AGDA2HS rezzCong inline #-}
+
+  rezzCong2 : (f : a → b → c) → Rezz a x → Rezz b y → Rezz c (f x y)
+  rezzCong2 f (Rezzed x p) (Rezzed y q) = Rezzed (f x y) (cong₂ f p q)
+  {-# COMPILE AGDA2HS rezzCong2 inline #-}
+
+  rezzHead : Rezz (List a) (x ∷ xs) → Rezz a x
+  rezzHead {x = x} (Rezzed ys p) =
+    Rezzed (head ys)
+           (subst (λ ys → ⦃ @0 _ : NonEmpty ys ⦄ → head ys ≡ x)
+              (sym p) refl)
+    where instance @0 ne : NonEmpty ys
+                   ne = subst NonEmpty (sym p) itsNonEmpty
+  {-# COMPILE AGDA2HS rezzHead inline #-}
+
+  rezzTail : Rezz (List a) (x ∷ xs) → Rezz (List a) xs
+  rezzTail {xs = xs} (Rezzed ys p) =
+    Rezzed (tail ys)
+           (subst (λ ys → ⦃ @0 _ : NonEmpty ys ⦄ → tail ys ≡ xs)
+              (sym p) refl)
+    where instance @0 ne : NonEmpty ys
+                   ne = subst NonEmpty (sym p) itsNonEmpty
+  {-# COMPILE AGDA2HS rezzTail inline #-}
+
+  rezzErase : Rezz (Erase a) (Erased x)
+  rezzErase {x = x} = Rezzed (Erased x) refl
+  {-# COMPILE AGDA2HS rezzErase inline #-}
+
+  erase-injective : Erased x ≡ Erased y → x ≡ y
+  erase-injective refl = refl
+
+  inspect_by_ : (x : a) → (Rezz a x → b) → b
+  inspect x by f = f (rezz x)

lib/Haskell/Law/Equality.agda

@@ -24,6 +24,9 @@ sym refl = refl
 trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans refl refl = refl
 
+subst : ∀ {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y
+subst P refl z = z
+
 --------------------------------------------------
 -- Scary Things
 

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

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,34 @@
+module EraseType where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Erase
+
+testErase : Erase Int
+testErase = Erased 42
+
+{-# 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
+
+{-# COMPILE AGDA2HS testRezz #-}
+
+testRezzErase : Rezz (Erase Int) testErase
+testRezzErase = rezzErase
+
+{-# COMPILE AGDA2HS testRezzErase #-}
+
+testCong : Rezz Int (1 + get testErase)
+testCong = rezzCong (1 +_) testRezz
+
+{-# COMPILE AGDA2HS testCong #-}
+
+rTail : ∀ {@0 x xs} → Rezz (List Int) (x ∷ xs) → Rezz (List Int) xs
+rTail = rezzTail
+
+{-# COMPILE AGDA2HS rTail #-}

test/HeightMirror.agda

@@ -1,6 +1,6 @@
 
 open import Haskell.Prelude hiding (max)
-open import Haskell.Law.Equality
+open import Haskell.Law.Equality hiding (subst)
 
 subst : {p : @0 a → Set} {@0 m n : a} → @0 m ≡ n → p m → p n
 subst refl t = t

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,20 @@
+module EraseType where
+
+testErase :: ()
+testErase = ()
+
+testMatch :: () -> ()
+testMatch () = ()
+
+testRezz :: Int
+testRezz = 42
+
+testRezzErase :: ()
+testRezzErase = ()
+
+testCong :: Int
+testCong = 1 + testRezz
+
+rTail :: [Int] -> [Int]
+rTail = \ ys -> tail ys
+