From 21508e15f139b7ee2efff7324c48029c131219c4 Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 20 Feb 2024 17:01:35 +0100
Subject: [PATCH] added test for proj-like reduction

---
 test/AllTests.agda      |  2 ++
 test/ProjLike.agda      | 22 ++++++++++++++++++++++
 test/golden/AllTests.hs |  1 +
 test/golden/ProjLike.hs | 10 ++++++++++
 4 files changed, 35 insertions(+)
 create mode 100644 test/ProjLike.agda
 create mode 100644 test/golden/ProjLike.hs

diff --git a/test/AllTests.agda b/test/AllTests.agda
index d2ebfca6..aeb9e0af 100644
--- a/test/AllTests.agda
+++ b/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
 #-}
diff --git a/test/ProjLike.agda b/test/ProjLike.agda
new file mode 100644
index 00000000..9241eddc
--- /dev/null
+++ b/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 #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index 33276344..82ba1c56 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -67,4 +67,5 @@ import EraseType
 import Delay
 import Issue273
 import TypeDirected
+import ProjLike
 
diff --git a/test/golden/ProjLike.hs b/test/golden/ProjLike.hs
new file mode 100644
index 00000000..57b56502
--- /dev/null
+++ b/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
+