diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index a3ed1fa4..91a84cc3 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE NamedFieldPuns #-}
 module Agda2Hs.Compile.Record where
 
 import Control.Monad ( unless )
@@ -168,7 +169,11 @@ 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} <- def
+  , length (filter keepArg recFields) == 1
+  , not (recRecursive def)
+  = return ()
+
+  | otherwise
+  = genericError "An unboxed type must be a non-recursive record type with exactly one non-erased field."
diff --git a/test/UnboxPragma.agda b/test/UnboxPragma.agda
index 4a2483ca..79ce1be1 100644
--- a/test/UnboxPragma.agda
+++ b/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