[ fix #212 ] Be more flexible with unboxed records

src/Agda2Hs/Compile/Record.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE NamedFieldPuns #-}
 module Agda2Hs.Compile.Record where
 
 import Control.Monad ( unless )
@@ -168,7 +169,7 @@ compileRecord target def = setCurrentRange (nameBindingSite $ qnameName $ defNam
       return $ Hs.DataDecl () don Nothing hd [conDecl] ds
 
 checkUnboxPragma :: Defn -> C ()
-checkUnboxPragma def@Record{ recFields = (f:fs) }
-  | keepArg f , all (not . keepArg) fs , not (recRecursive def) = return ()
-checkUnboxPragma _ = genericError $
-  "An unboxed type must be a non-recursive record type with exactly one non-erased field."
+checkUnboxPragma def@Record{recFields} =
+  if length (filter keepArg recFields) == 1 && not (recRecursive def)
+    then return ()
+    else genericError "An unboxed type must be a non-recursive record type with exactly one non-erased field."

test/UnboxPragma.agda

@@ -10,6 +10,13 @@ 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