fix recursive record check

agda · Dec 26, 2023 · daf6fe1 · daf6fe1
1 parent 07c9d3d
commit daf6fe1
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 2 deletions.
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
@@ -170,9 +170,12 @@ compileRecord target def = do
 
 checkUnboxPragma :: Defn -> C ()
 checkUnboxPragma def
-  | Record{recFields} <- def
+  | Record{recFields, recMutual} <- def
   , length (filter keepArg recFields) == 1
-  , not (recRecursive def)
+  -- , not (recRecursive def)
+  --     can be used again after agda 2.6.4.2 is released
+  --     see: agda/agda#7042
+  , all null recMutual -- see agda/agda#7042
   = return ()
 
   | otherwise

diff --git a/test/AllTests.agda b/test/AllTests.agda
@@ -65,6 +65,7 @@ import ModuleParametersImports
 import Coerce
 import Inlining
 import EraseType
+import Issue257
 
 {-# FOREIGN AGDA2HS
 import Issue14

diff --git a/test/Issue257.agda b/test/Issue257.agda
@@ -0,0 +1,7 @@
+module Issue257 where
+
+open import Haskell.Prelude
+
+record Wrap : Set where
+  field int : Integer
+{-# COMPILE AGDA2HS Wrap unboxed #-}