added test for proj-like reduction

test/AllTests.agda

@@ -70,6 +70,7 @@ import Issue257
 import Delay
 import Issue273
 import TypeDirected
+import ProjLike
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -139,4 +140,5 @@ import EraseType
 import Delay
 import Issue273
 import TypeDirected
+import ProjLike
 #-}

test/ProjLike.agda

@@ -0,0 +1,22 @@
+module ProjLike where
+
+open import Haskell.Prelude
+
+module M (a : Set) where
+
+  data Scope : Set where
+    Empty : Scope
+    Bind  : a → Scope → Scope
+
+  {-# COMPILE AGDA2HS Scope #-}
+
+  unbind : Scope → Scope
+  unbind Empty      = Empty
+  unbind (Bind _ s) = s
+
+open M Nat public
+
+test : Scope
+test = unbind (Bind 1 (Bind 2 Empty))
+
+{-# COMPILE AGDA2HS test #-}

test/golden/AllTests.hs

@@ -67,4 +67,5 @@ import EraseType
 import Delay
 import Issue273
 import TypeDirected
+import ProjLike
 

test/golden/ProjLike.hs

@@ -0,0 +1,10 @@
+module ProjLike where
+
+import Numeric.Natural (Natural)
+
+data Scope a = Empty
+             | Bind a (Scope a)
+
+test :: Scope Natural
+test = Bind 2 Empty
+