From 1ddeb688b32c04b1bf0bcb3619fab6a1c6ea0eaf Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Wed, 27 Mar 2024 15:01:02 +0100
Subject: [PATCH] [ fix #310 ] compile Sigma pattern

---
 src/Agda2Hs/Compile/Function.hs | 1 +
 test/Tuples.agda                | 5 +++++
 test/golden/Tuples.hs           | 5 +++++
 3 files changed, 11 insertions(+)

diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 9f850a54..4d9714df 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -56,6 +56,7 @@ isSpecialCon qn = case prettyShow qn of
   "Haskell.Prim.Tuple._,_"         -> Just tuplePat
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
   "Haskell.Extra.Erase.Erased"     -> Just tuplePat
+  "Haskell.Extra.Sigma._,_"        -> Just tuplePat
   "Agda.Builtin.Int.Int.pos"       -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc"    -> Just negSucIntPat
   _                                -> Nothing
diff --git a/test/Tuples.agda b/test/Tuples.agda
index 4c67555b..5d5eef04 100644
--- a/test/Tuples.agda
+++ b/test/Tuples.agda
@@ -54,3 +54,8 @@ t4 : Σ[ n ∈ Nat ] (Dec (IsTrue (n <= 5)))
 t4 = 3 S., (True ⟨ itsTrue ⟩)
 
 {-# COMPILE AGDA2HS t4 #-}
+
+t5 : Σ[ x ∈ a ] b → a
+t5 p = case p of λ where (x S., y) → x
+
+{-# COMPILE AGDA2HS t5 #-}
diff --git a/test/golden/Tuples.hs b/test/golden/Tuples.hs
index ed6ba07b..d87f1cc8 100644
--- a/test/golden/Tuples.hs
+++ b/test/golden/Tuples.hs
@@ -30,3 +30,8 @@ test2
 t4 :: (Natural, Bool)
 t4 = (3, True)
 
+t5 :: (a, b) -> a
+t5 p
+  = case p of
+        (x, y) -> x
+