From 77c06737fed99e6373bd3e4bfb9d556a52f697dd Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 7 Nov 2023 11:37:38 +0100
Subject: [PATCH] [fix #213] Properly deal with unboxed records, again

---
 src/Agda2Hs/Compile/Type.hs |  8 +++++---
 test/UnboxPragma.agda       | 28 ++++++++++++++++++++--------
 test/golden/UnboxPragma.hs  |  5 +++++
 3 files changed, 30 insertions(+), 11 deletions(-)

diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 8f7e94e0..d2d8d039 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -5,6 +5,7 @@ module Agda2Hs.Compile.Type where
 import Control.Arrow ( (>>>) )
 import Control.Monad ( forM, when )
 import Control.Monad.Reader ( asks )
+import Data.List ( find )
 import Data.Maybe ( mapMaybe )
 
 import qualified Language.Haskell.Exts.Syntax as Hs
@@ -152,9 +153,10 @@ compileTypeArgs args = mapM (compileType . unArg) $ filter keepArg args
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
   def <- theDef <$> getConstInfo r
-  case recTel def `apply` pars of
-    EmptyTel        -> __IMPOSSIBLE__
-    (ExtendTel a _) -> compileType $ unEl $ unDom a
+  let tel = telToList $ recTel def `apply` pars
+  case find keepArg tel of
+    Nothing -> __IMPOSSIBLE__
+    Just t -> compileType $ unEl $ snd (unDom t)
 
 compileTransparentType :: Args -> C (Hs.Type ())
 compileTransparentType args = compileTypeArgs args >>= \case
diff --git a/test/UnboxPragma.agda b/test/UnboxPragma.agda
index 79ce1be1..52f3e50c 100644
--- a/test/UnboxPragma.agda
+++ b/test/UnboxPragma.agda
@@ -1,7 +1,7 @@
 
 open import Haskell.Prelude
 
-record ∃ (A : Set) (P : A → Set) : Set where
+record ∃ (A : Set) (@0 P : A → Set) : Set where
   constructor _[_]
   field
     el : A
@@ -10,13 +10,6 @@ open ∃ public
 
 {-# COMPILE AGDA2HS ∃ unboxed #-}
 
-record Σ0 (A : Set) (P : @0 A → Set) : Set where
-  field
-    @0 el : A
-    pf : P el
-
-{-# COMPILE AGDA2HS Σ0 unboxed #-}
-
 postulate
   IsSorted : List Int → Set
   looksfine : {xs : List Int} → IsSorted xs
@@ -41,3 +34,22 @@ sortAll : List (List Int)
 sortAll = map el (map (λ xs → xs [ looksfine {xs} ]) ((1 ∷ 2 ∷ []) ∷ (3 ∷ []) ∷ []))
 
 {-# COMPILE AGDA2HS sortAll #-}
+
+record Σ0 (A : Set) (P : @0 A → Set) : Set where
+  constructor _[_]
+  field
+    @0 el : A
+    pf : P el
+open Σ0 public
+
+{-# COMPILE AGDA2HS Σ0 unboxed #-}
+
+Scope : (name : Set) → Set
+Scope name = Σ0 (List name) λ xs → ∃ Int λ n → length xs ≡ n
+
+{-# COMPILE AGDA2HS Scope #-}
+
+emptyScope : {name : Set} → Scope name
+emptyScope = [] [ 0 [ refl ] ]
+
+{-# COMPILE AGDA2HS emptyScope #-}
diff --git a/test/golden/UnboxPragma.hs b/test/golden/UnboxPragma.hs
index acfd27d7..1f3370d9 100644
--- a/test/golden/UnboxPragma.hs
+++ b/test/golden/UnboxPragma.hs
@@ -12,3 +12,8 @@ sort3 xs = xs
 sortAll :: [[Int]]
 sortAll = map (\ r -> r) (map (\ xs -> xs) [[1, 2], [3]])
 
+type Scope name = Int
+
+emptyScope :: Scope name
+emptyScope = 0
+