make Erase interface inlinable

lib/Haskell/Extra/Erase.agda

@@ -3,7 +3,10 @@ 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
@@ -41,24 +44,34 @@ module Haskell.Extra.Erase where
     rezz-id = rezz _
 
   rezzCong : {@0 a : Set} {@0 x : a} (f : a → b) → Rezz a x → Rezz b (f x)
-  rezzCong f (rezz x) = rezz (f x)
-  {-# COMPILE AGDA2HS rezzCong #-}
+  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 (rezz x) (rezz y) = rezz (f x y)
-  {-# COMPILE AGDA2HS rezzCong2 #-}
+  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 (rezz (x ∷ xs)) = rezz x
-  {-# COMPILE AGDA2HS rezzHead #-}
+  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 (rezz (x ∷ xs)) = rezz xs
-  {-# COMPILE AGDA2HS rezzTail #-}
+  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 #-}
+  {-# COMPILE AGDA2HS rezzErase inline #-}
 
   erase-injective : Erased x ≡ Erased y → x ≡ y
   erase-injective refl = refl

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
 

test/EraseType.agda

@@ -17,3 +17,13 @@ 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/EraseType.hs

@@ -1,10 +1,14 @@
 module EraseType where
 
-import Haskell.Extra.Erase (rezzErase)
-
 testRezz :: Int
 testRezz = 42
 
 testRezzErase :: ()
-testRezzErase = rezzErase
+testRezzErase = ()
+
+testCong :: Int
+testCong = 1 + testRezz
+
+rTail :: [Int] -> [Int]
+rTail = \ ys -> tail ys