[fix #213] Properly deal with unboxed records, again

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

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 #-}

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
+