proper checks for unboxed datatypes

agda · Aug 15, 2024 · d33702f · d33702f
1 parent 46c3248
commit d33702f
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 19 deletions.
diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
@@ -20,10 +20,10 @@ import Agda.Utils.Monad ( whenM, anyM, when )
 import qualified Language.Haskell.Exts.Extension as Hs
 
 import Agda2Hs.Compile.ClassInstance ( compileInstance )
-import Agda2Hs.Compile.Data ( compileData )
+import Agda2Hs.Compile.Data ( compileData, checkUnboxedDataPragma )
 import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma )
 import Agda2Hs.Compile.Postulate ( compilePostulate )
-import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
+import Agda2Hs.Compile.Record ( compileRecord, checkUnboxedRecordPragma )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName )
 import Agda2Hs.Pragma
@@ -88,8 +88,8 @@ compile opts tlm _ def =
       case (p , theDef def) of
         (NoPragma            , _         ) -> return []
         (ExistingClassPragma , _         ) -> return []
-        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
-        (UnboxPragma s       , Datatype{}) -> [] <$ checkUnboxPragma def
+        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxedRecordPragma def
+        (UnboxPragma s       , Datatype{}) -> [] <$ checkUnboxedDataPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
         (TuplePragma b       , Record{}  ) -> return []

diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs
@@ -2,7 +2,7 @@ module Agda2Hs.Compile.Data where
 
 import qualified Language.Haskell.Exts.Syntax as Hs
 
-import Control.Monad ( when )
+import Control.Monad ( unless, when )
 import Agda.Compiler.Backend
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -14,8 +14,9 @@ import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
+import Agda.Utils.Monad ( mapMaybeM )
 
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.HsUtils
@@ -46,15 +47,15 @@ compileData newtyp ds def = do
     when newtyp (checkNewtype d cs)
 
     return [Hs.DataDecl () target Nothing hd cs ds]
-  where
-    allIndicesErased :: Type -> C ()
-    allIndicesErased t = reduce (unEl t) >>= \case
-      Pi dom t -> compileDomType (absName t) dom >>= \case
-        DomDropped      -> allIndicesErased (unAbs t)
-        DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
-        DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
-        DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
-      _ -> return ()
+
+allIndicesErased :: Type -> C ()
+allIndicesErased t = reduce (unEl t) >>= \case
+  Pi dom t -> compileDomType (absName t) dom >>= \case
+    DomDropped      -> allIndicesErased (unAbs t)
+    DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
+    DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
+    DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
+  _ -> return ()
 
 compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
 compileConstructor params c = do
@@ -77,3 +78,42 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c
   DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints"
   DomDropped        -> underAbstraction a tel compileConstructorArgs
   DomForall{}       -> __IMPOSSIBLE__
+
+
+checkUnboxedDataPragma :: Definition -> C ()
+checkUnboxedDataPragma def = do
+  let Datatype{..} = theDef def
+
+  -- unboxed datatypes shouldn't be recursive
+  unless (all null dataMutual) $ genericDocError
+    =<< text "Unboxed datatype" <+> prettyTCM (defName def)
+    <+> text "cannot be recursive"
+
+  TelV tel t <- telViewUpTo dataPars (defType def)
+  let params :: [Arg Term] = teleArgs tel
+
+  allIndicesErased t
+
+  case dataCons of
+    [con] -> do
+      info <- getConstInfo con
+      let Constructor {..} = theDef info
+      ty <- defType info `piApplyM` params
+      TelV conTel _ <- telView ty
+      args <- nonErasedArgs conTel
+      unless (length args == 1) $ genericDocError
+        =<< text "Unboxed datatype" <+> prettyTCM (defName def)
+        <+> text "should have a single constructor with exactly one non-erased argument."
+
+    _     -> genericDocError =<< text "Unboxed datatype" <+> prettyTCM (defName def)
+                             <+> text "must have exactly one constructor."
+
+  where
+    nonErasedArgs :: Telescope -> C [String]
+    nonErasedArgs EmptyTel = return []
+    nonErasedArgs (ExtendTel a tel) = compileDom a >>= \case
+      DODropped  -> underAbstraction a tel nonErasedArgs
+      DOType     -> genericDocError =<< text "Type argument in unboxed datatype not supported"
+      DOInstance -> genericDocError =<< text "Instance argument in unboxed datatype not supported"
+      DOTerm     -> (absName tel:) <$> underAbstraction a tel nonErasedArgs
+
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
@@ -29,6 +29,7 @@ import Agda2Hs.Compile.Function ( compileFun )
 import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
+import Agda2Hs.Compile.Data ( allIndicesErased )
 import Agda2Hs.HsUtils
 
 -- | Primitive fields and default implementations
@@ -170,8 +171,9 @@ compileRecord target def = do
       let conDecl = Hs.QualConDecl () Nothing Nothing $ Hs.RecDecl () cName fieldDecls
       return $ Hs.DataDecl () don Nothing hd [conDecl] ds
 
-checkUnboxPragma :: Definition -> C ()
-checkUnboxPragma def | Record{..} <- theDef def = do
+checkUnboxedRecordPragma :: Definition -> C ()
+checkUnboxedRecordPragma def = do
+  let Record{..} = theDef def
   -- recRecursive can be used again after agda 2.6.4.2 is released
   -- see agda/agda#7042
   unless (all null recMutual) $ genericDocError
@@ -196,5 +198,3 @@ checkUnboxPragma def | Record{..} <- theDef def = do
       DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported"
       DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields
 
-checkUnboxPragma def | Datatype{..} <- theDef def = do
-  pure () -- TOOD(flupe):