From f1a95188b845a236035a443e1be572edcbbff92c Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 6 Aug 2024 18:03:15 +0200
Subject: [PATCH 1/6] basic Singleton type

---
 lib/Haskell/Extra/Singleton.agda | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 lib/Haskell/Extra/Singleton.agda

diff --git a/lib/Haskell/Extra/Singleton.agda b/lib/Haskell/Extra/Singleton.agda
new file mode 100644
index 00000000..1604e5c5
--- /dev/null
+++ b/lib/Haskell/Extra/Singleton.agda
@@ -0,0 +1,21 @@
+module Haskell.Extra.Singleton where
+
+open import Haskell.Prelude
+
+data Singleton (a : Set) : @0 a → Set where
+  MkSingl : ∀ x → Singleton a x
+
+{-# COMPILE AGDA2HS Singleton unboxed #-}
+
+pureSingl : {a : Set} (x : a) → Singleton a x
+pureSingl = MkSingl
+
+{-# COMPILE AGDA2HS pureSingl inline #-}
+
+fmapSingl
+  : {a b : Set} (f : a → b) {@0 x : a}
+  → Singleton a x
+  → Singleton b (f x)
+fmapSingl f (MkSingl x) = MkSingl (f x)
+
+{-# COMPILE AGDA2HS fmapSingl inline #-}

From ff6f65038888215385120ec3a724e7383a200dbf Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Wed, 7 Aug 2024 14:45:15 +0200
Subject: [PATCH 2/6] further work on compiling unboxed datatypes

---
 lib/Haskell/Extra/Singleton.agda |  4 ++--
 src/Agda2Hs/Compile.hs           |  1 +
 src/Agda2Hs/Compile/Function.hs  | 11 ++++++++---
 src/Agda2Hs/Compile/Record.hs    |  7 ++++---
 src/Agda2Hs/Compile/Type.hs      | 29 +++++++++++++++++++++++++----
 src/Agda2Hs/Compile/Utils.hs     | 19 +++++++++++++++++--
 test/Singleton.agda              | 13 +++++++++++++
 7 files changed, 70 insertions(+), 14 deletions(-)
 create mode 100644 test/Singleton.agda

diff --git a/lib/Haskell/Extra/Singleton.agda b/lib/Haskell/Extra/Singleton.agda
index 1604e5c5..94300930 100644
--- a/lib/Haskell/Extra/Singleton.agda
+++ b/lib/Haskell/Extra/Singleton.agda
@@ -8,9 +8,9 @@ data Singleton (a : Set) : @0 a → Set where
 {-# COMPILE AGDA2HS Singleton unboxed #-}
 
 pureSingl : {a : Set} (x : a) → Singleton a x
-pureSingl = MkSingl
+pureSingl x = MkSingl x
 
-{-# COMPILE AGDA2HS pureSingl inline #-}
+{-# COMPILE AGDA2HS pureSingl transparent #-}
 
 fmapSingl
   : {a b : Set} (f : a → b) {@0 x : a}
diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index 22c93619..b3172924 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -89,6 +89,7 @@ compile opts tlm _ def =
         (NoPragma            , _         ) -> return []
         (ExistingClassPragma , _         ) -> return []
         (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
+        (UnboxPragma s       , Datatype{}) -> [] <$ checkUnboxPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
         (TuplePragma b       , Record{}  ) -> return []
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 0fb65335..465095b9 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -399,7 +399,7 @@ checkInlinePragma def@Defn{defName = f} = do
     [c] ->
       unlessM (allowedPats (namedClausePats c)) $ genericDocError =<<
         "Cannot make function" <+> prettyTCM (defName def) <+> "inlinable." <+>
-        "Inline functions can only use variable patterns or transparent record constructor patterns."
+        "Inline functions can only use variable patterns or unboxed constructor patterns."
     _ ->
       genericDocError =<<
         "Cannot make function" <+> prettyTCM f <+> "inlinable." <+>
@@ -408,11 +408,16 @@ checkInlinePragma def@Defn{defName = f} = do
   where allowedPat :: DeBruijnPattern -> C Bool
         allowedPat VarP{} = pure True
         -- only allow matching on (unboxed) record constructors
-        allowedPat (ConP ch ci cargs) =
+        allowedPat (ConP ch ci cargs) = do
+          reportSDoc "agda2hs.compile.inline" 18 $ "Checking unboxing of constructor: "<+> prettyTCM ch
           isUnboxConstructor (conName ch) >>= \case
             Just _  -> allowedPats cargs
             Nothing -> pure False
-        allowedPat _ = pure False
+        -- NOTE(flupe): dot patterns should really only be allowed for *erased* arguments, I think.
+        allowedPat (DotP _ _) = pure True
+        allowedPat p = do
+          reportSDoc "agda2hs.compile.inline" 18 $ "Unsupported pattern"  <+> prettyTCM p
+          pure False
 
         allowedPats :: NAPs -> C Bool
         allowedPats pats = allM pats (allowedPat . dget . dget)
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index b82b0f4a..1045bc59 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -171,9 +171,7 @@ compileRecord target def = do
       return $ Hs.DataDecl () don Nothing hd [conDecl] ds
 
 checkUnboxPragma :: Definition -> C ()
-checkUnboxPragma def = do
-  let Record{..} = theDef def
-
+checkUnboxPragma def | Record{..} <- theDef def = do
   -- recRecursive can be used again after agda 2.6.4.2 is released
   -- see agda/agda#7042
   unless (all null recMutual) $ genericDocError
@@ -197,3 +195,6 @@ checkUnboxPragma def = do
       DOType -> genericDocError =<< text "Type field in unboxed record not supported"
       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):
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 12ac4405..2dd9d8ff 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -9,6 +9,7 @@ import Control.Monad.Trans ( lift )
 import Control.Monad.Reader ( asks )
 import Data.List ( find )
 import Data.Maybe ( mapMaybe, isJust )
+import Data.Foldable ( toList )
 import qualified Data.Set as Set ( singleton )
 
 import qualified Language.Haskell.Exts.Syntax as Hs
@@ -21,6 +22,7 @@ import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
+import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep )
 import Agda.TypeChecking.Substitute
@@ -76,7 +78,7 @@ delayType [] = genericDocError =<< text "Cannot compile unapplied Delay type"
 compileTypeWithStrictness :: Term -> C (Strictness, Hs.Type ())
 compileTypeWithStrictness t = do
   s <- case t of
-    Def f es -> fromMaybe Lazy <$> isUnboxRecord f
+    Def f es -> fromMaybe Lazy <$> isUnboxType f
     _        -> return Lazy
   ty <- compileType t
   pure (s, ty)
@@ -106,7 +108,7 @@ compileType t = do
               <+> text "in Haskell type"
          | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics es
          | Just args <- allApplyElims es ->
-             ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
+             ifJustM (isUnboxType f) (\_ -> compileUnboxType f args) $
              ifJustM (isTupleRecord f) (\b -> compileTupleType f b args) $
              ifM (isTransparentFunction f) (compileTransparentType (defType def) args) $
              ifM (isInlinedFunction f) (compileInlineType f es) $ do
@@ -174,11 +176,31 @@ compileTelSize (ExtendTel a tel) = compileDom a >>= \case
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
   def <- getConstInfo r
-  let tel = recTel (theDef def) `apply` pars
+
+  tel <- case theDef def of
+
+    Record{recTel} -> pure (recTel `apply` pars)
+
+    Datatype{dataCons = [con]} -> do
+      -- NOTE(flupe): con is the *only* constructor of the unboxed datatype
+      Constructor { conSrcCon } <- theDef <$> getConstInfo con
+      -- we retrieve its type
+      Just (_, ty) <- getConType conSrcCon (El (DummyS "some level") (apply (Def r []) pars))
+      theTel <$> telView ty
+
   compileTel tel >>= \case
     [t] -> return t
     _   -> __IMPOSSIBLE__
 
+  where
+    compileTel :: Telescope -> C [Hs.Type ()]
+    compileTel EmptyTel = return []
+    compileTel (ExtendTel a tel) = compileDom a >>= \case
+      DODropped  -> underAbstraction a tel compileTel
+      DOInstance -> __IMPOSSIBLE__
+      DOType     -> __IMPOSSIBLE__
+      DOTerm     -> (:) <$> compileType (unEl $ unDom a) <*> underAbstraction a tel compileTel
+
 compileTupleType :: QName -> Hs.Boxed -> Args -> C (Hs.Type ())
 compileTupleType r b pars = do
   tellUnboxedTuples b
@@ -192,7 +214,6 @@ compileTransparentType ty args = compileTypeArgs ty args >>= \case
   (v:vs) -> return $ v `tApp` vs
   []     -> __IMPOSSIBLE__
 
-
 compileInlineType :: QName -> Elims -> C (Hs.Type ())
 compileInlineType f args = do
   Function { funClauses = cs } <- theDef <$> getConstInfo f
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index a62f80a5..d1649325 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -192,9 +192,24 @@ isUnboxRecord q = do
         _             -> Nothing
     _ -> return Nothing
 
+isUnboxType :: QName -> C (Maybe Strictness)
+isUnboxType q = do
+  getConstInfo q >>= \case
+    Defn{defName = r} ->
+      processPragma r <&> \case
+        UnboxPragma s -> Just s
+        _             -> Nothing
+    -- _ -> return Nothing
+
 isUnboxConstructor :: QName -> C (Maybe Strictness)
-isUnboxConstructor q =
-  caseMaybeM (isRecordConstructor q) (return Nothing) $ isUnboxRecord . fst
+isUnboxConstructor q = do
+  def <- getConstInfo q
+  case theDef def of
+      Constructor {conData = r} -> isUnboxType r
+      _                         -> pure Nothing
+
+  -- caseMaybeM (isRecordConstructor) isUnboxType q
+  -- caseMaybeM (isRecordConstructor q) (return Nothing) $ isUnboxRecord . fst
 
 isUnboxProjection :: QName -> C (Maybe Strictness)
 isUnboxProjection q =
diff --git a/test/Singleton.agda b/test/Singleton.agda
new file mode 100644
index 00000000..3d60d5b4
--- /dev/null
+++ b/test/Singleton.agda
@@ -0,0 +1,13 @@
+open import Haskell.Prelude
+open import Haskell.Extra.Singleton
+
+test1 : (@0 x : ⊤) → Singleton ⊤ x
+test1 x = MkSingl tt
+
+{-# COMPILE AGDA2HS test1 #-}
+
+-- doesn't work because inline functions only reduce because of inline record transformation
+-- test2 : {a b : Set} (f : a → b) {@0 x : a} → Singleton a x → Singleton b (f x)
+-- test2 f sx = fmapSingl f sx
+-- 
+-- {-# COMPILE AGDA2HS test2 #-}

From 97b4897a67d917fe7fea92052c8bce2ff51e23a5 Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Wed, 14 Aug 2024 16:23:12 +0200
Subject: [PATCH 3/6] wip

---
 src/Agda2Hs/Compile/Term.hs | 74 ++++++++++++++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 9 deletions(-)

diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index e283d574..2e7f8373 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -53,13 +53,13 @@ type DefCompileRule = Type -> [Term] -> C (Hs.Exp ())
 
 isSpecialDef :: QName -> Maybe DefCompileRule
 isSpecialDef q = case prettyShow q of
-  _ | isExtendedLambdaName q     -> Just (lambdaCase q)
-  "Haskell.Prim.if_then_else_"   -> Just ifThenElse
-  "Haskell.Prim.case_of_"        -> Just caseOf
-  "Haskell.Prim.the"             -> Just expTypeSig
-  "Haskell.Extra.Delay.runDelay" -> Just compileErasedApp
+  _ | isExtendedLambdaName q            -> Just (lambdaCase q)
+  "Haskell.Prim.if_then_else_"          -> Just ifThenElse
+  "Haskell.Prim.case_of_"               -> Just caseOf
+  "Haskell.Prim.the"                    -> Just expTypeSig
+  "Haskell.Extra.Delay.runDelay"        -> Just compileErasedApp
   "Agda.Builtin.Word.primWord64FromNat" -> Just primWord64FromNat
-  _                              -> Nothing
+  _                                     -> Nothing
 
 
 -- | Compile a @\where@ to the equivalent @\case@ expression.
@@ -153,6 +153,8 @@ compileSpined c tm ty (e@(Proj o q):es) = do
   ty' <- shouldBeProjectible t ty o q
   compileSpined (compileProj q ty t ty') (tm . (e:)) ty' es
 compileSpined c tm ty (e@(Apply (unArg -> x)):es) = do
+  reportSDoc "agda2hs.compile.inline" 18 $ text "spined term" <+> prettyTCM (tm (e:es))
+  reportSDoc "agda2hs.compile.inline" 18 $ text "spined type" <+> prettyTCM ty
   (a, b) <- mustBePi ty
   compileSpined (c . (x:)) (tm . (e:)) (absApp b x) es
 compileSpined _ _ _ _ = __IMPOSSIBLE__
@@ -536,11 +538,64 @@ compileInlineFunctionApp f ty args = do
 
   def <- getConstInfo f
 
-  let ty' = defType def
-  let Function{funClauses = cs} = theDef def
-  let [Clause{namedClausePats = pats}] = filter (isJust . clauseBody) cs
+  let Function{ funClauses = cs } = theDef def
+  let [ Clause { namedClausePats = pats
+               , clauseBody = Just body
+               , clauseTel
+               } ] = filter (isJust . clauseBody) cs
+
+  reportSDoc "agda2hs.compile.inline" 18 $ text "inline function pats " <+> pretty pats
+  reportSDoc "agda2hs.compile.inline" 18 $ text "inline function args " <+> prettyTCM args
+  reportSDoc "agda2hs.compile.inline" 18 $ text "inline function length of tel" <+> prettyTCM (length clauseTel)
+  reportSDoc "agda2hs.compile.inline" 18 $ text "ctxt" <+> (prettyTCM =<< getContextArgs)
 
   ty'' <- piApplyM ty args
+  let ntel = length clauseTel
+
+  -- body' <- addContext clauseTel $ do
+  -- sub <- matchPats pats (raise ntel args)
+    -- reportSDoc "agda2hs.compile.inline" 18 $ text "Generated substitution: " <+> prettyTCM body
+
+
+  addContext (KeepNames clauseTel) $ do
+    body' <- matchPats pats (raise ntel args) body
+    reportSDoc "agda2hs.compile.inline" 18 $ text "function body before substitution: " <+> prettyTCM body
+    reportSDoc "agda2hs.compile.inline" 18 $ text "function body after substitution: "  <+> prettyTCM body'
+    compileTerm (raise ntel ty'') body'
+
+  where
+    matchPats :: NAPs -> [Term] -> Term -> C Term -- Substitution
+    matchPats [] [] tm = pure tm -- pure IdS
+    matchPats (pat:naps) (t:ts) tm -- dot patterns are ignored
+      | DotP _ _ <- namedThing (unArg pat) = matchPats naps ts tm
+    matchPats (pat:naps) (t:ts) tm = do
+      -- each pattern of inlined funtions match a single variable
+      let var = dbPatVarIndex $ extractPatVar (namedThing $ unArg pat)
+      reportSDoc "agda2hs.compile.inline" 18
+        $ text "replacing db var" <+> prettyTCM (Var var []) <+> text "with" <+> prettyTCM t
+
+      -- TODO: improve this
+      matchPats naps ts (applySubst (inplaceS var t) tm)
+      -- composeS (singletonS (dbPatVarIndex var) t) <$> matchPats naps ts
+    matchPats (pat:naps) [] tm = do
+      -- exhausted explicit arguments, yet the inline function is not fully applied.
+      -- we eta-expand with as many missing arguments
+      let name = dbPatVarName (extractPatVar (namedThing $ unArg pat))
+      mkLam (defaultArg name) <$> matchPats naps [] tm
+
+    extractPatVar :: DeBruijnPattern -> DBPatVar
+    extractPatVar (VarP _ v) = v
+    extractPatVar (ConP _ _ args) =
+      let arg = namedThing $ unArg $ head $ filter (usableModality `and2M` visible) args
+      in extractPatVar arg
+    extractPatVar _ = __IMPOSSIBLE__
+
+
+-- NOTE(flupe): for now, we assume that inline functions are fully applied
+--              once this works, we need to add back eta-expansion.
+
+  -- undefined
+  {-
   -- NOTE(flupe): very flimsy, there has to be a better way
   etaExpand (drop (length args) pats) ty' args >>= compileTerm ty''
 
@@ -571,6 +626,7 @@ compileInlineFunctionApp f ty args = do
       (dom, cod) <- mustBePi ty
       let ai = domInfo dom
       Lam ai . mkAbs (extractName p) <$> etaExpand ps (absBody cod) (raise 1 args ++ [ var 0 ])
+      -}
 
 
 compileApp :: Hs.Exp () -> Type -> [Term] -> C (Hs.Exp ())

From 46c3248b1c93750236a617fd7a8129178abac67a Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Wed, 14 Aug 2024 16:34:41 +0200
Subject: [PATCH 4/6] singletons working

---
 src/Agda2Hs/Compile/Term.hs | 25 +++++++++++++------------
 test/Singleton.agda         |  8 ++++----
 test/golden/Inline2.err     |  2 +-
 3 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 2e7f8373..309ad0c6 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -558,30 +558,31 @@ compileInlineFunctionApp f ty args = do
 
 
   addContext (KeepNames clauseTel) $ do
-    body' <- matchPats pats (raise ntel args) body
-    reportSDoc "agda2hs.compile.inline" 18 $ text "function body before substitution: " <+> prettyTCM body
-    reportSDoc "agda2hs.compile.inline" 18 $ text "function body after substitution: "  <+> prettyTCM body'
-    compileTerm (raise ntel ty'') body'
+    matchPats pats (raise ntel args) (compileTerm (raise ntel ty'')) body
+    -- reportSDoc "agda2hs.compile.inline" 18 $ text "function body before substitution: " <+> prettyTCM body
+    -- reportSDoc "agda2hs.compile.inline" 18 $ text "function body after substitution: "  <+> prettyTCM body'
+    -- compileTerm (raise ntel ty'') body'
 
   where
-    matchPats :: NAPs -> [Term] -> Term -> C Term -- Substitution
-    matchPats [] [] tm = pure tm -- pure IdS
-    matchPats (pat:naps) (t:ts) tm -- dot patterns are ignored
-      | DotP _ _ <- namedThing (unArg pat) = matchPats naps ts tm
-    matchPats (pat:naps) (t:ts) tm = do
+    matchPats :: NAPs -> [Term] -> (Term -> C (Hs.Exp ())) -> Term -> C (Hs.Exp ()) -- Substitution
+    matchPats [] [] c tm = c tm -- pure IdS
+    matchPats (pat:naps) (t:ts) c tm -- dot patterns are ignored
+      | DotP _ _ <- namedThing (unArg pat) = matchPats naps ts c tm
+    matchPats (pat:naps) (t:ts) c tm = do
       -- each pattern of inlined funtions match a single variable
       let var = dbPatVarIndex $ extractPatVar (namedThing $ unArg pat)
       reportSDoc "agda2hs.compile.inline" 18
         $ text "replacing db var" <+> prettyTCM (Var var []) <+> text "with" <+> prettyTCM t
 
       -- TODO: improve this
-      matchPats naps ts (applySubst (inplaceS var t) tm)
+      matchPats naps ts c (applySubst (inplaceS var t) tm)
       -- composeS (singletonS (dbPatVarIndex var) t) <$> matchPats naps ts
-    matchPats (pat:naps) [] tm = do
+    matchPats (pat:naps) [] c tm = do
       -- exhausted explicit arguments, yet the inline function is not fully applied.
       -- we eta-expand with as many missing arguments
       let name = dbPatVarName (extractPatVar (namedThing $ unArg pat))
-      mkLam (defaultArg name) <$> matchPats naps [] tm
+      hsLambda name <$> matchPats naps [] c tm
+      -- mkLam (defaultArg name) <$> matchPats naps [] tm
 
     extractPatVar :: DeBruijnPattern -> DBPatVar
     extractPatVar (VarP _ v) = v
diff --git a/test/Singleton.agda b/test/Singleton.agda
index 3d60d5b4..c9232ff2 100644
--- a/test/Singleton.agda
+++ b/test/Singleton.agda
@@ -7,7 +7,7 @@ test1 x = MkSingl tt
 {-# COMPILE AGDA2HS test1 #-}
 
 -- doesn't work because inline functions only reduce because of inline record transformation
--- test2 : {a b : Set} (f : a → b) {@0 x : a} → Singleton a x → Singleton b (f x)
--- test2 f sx = fmapSingl f sx
--- 
--- {-# COMPILE AGDA2HS test2 #-}
+test2 : {a b : Set} (f : a → b) {@0 x : a} → Singleton a x → Singleton b (f x)
+test2 f {x} sx = fmapSingl f {x} sx
+
+{-# COMPILE AGDA2HS test2 #-}
diff --git a/test/golden/Inline2.err b/test/golden/Inline2.err
index e8fb8038..8627624c 100644
--- a/test/golden/Inline2.err
+++ b/test/golden/Inline2.err
@@ -1,2 +1,2 @@
 test/Fail/Inline2.agda:5,1-6
-Cannot make function tail' inlinable. Inline functions can only use variable patterns or transparent record constructor patterns.
+Cannot make function tail' inlinable. Inline functions can only use variable patterns or unboxed constructor patterns.

From d33702feb2c753cc8e3dc776bebd195be17a819c Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Thu, 15 Aug 2024 19:10:03 +0200
Subject: [PATCH 5/6] proper checks for unboxed datatypes

---
 src/Agda2Hs/Compile.hs        |  8 ++---
 src/Agda2Hs/Compile/Data.hs   | 62 ++++++++++++++++++++++++++++-------
 src/Agda2Hs/Compile/Record.hs |  8 ++---
 3 files changed, 59 insertions(+), 19 deletions(-)

diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index b3172924..d363ab55 100644
--- 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
index 3a544a0a..2bccd01b 100644
--- 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
index 1045bc59..8c7ca63d 100644
--- 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):

From 42483a32fd623552035555f9bd4308930c0510bc Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Thu, 15 Aug 2024 19:24:57 +0200
Subject: [PATCH 6/6] trying out idiom brackets

---
 lib/Haskell/Extra/Singleton.agda | 19 +++++++++++++------
 test/Singleton.agda              | 10 ++++++++--
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/lib/Haskell/Extra/Singleton.agda b/lib/Haskell/Extra/Singleton.agda
index 94300930..85863ea2 100644
--- a/lib/Haskell/Extra/Singleton.agda
+++ b/lib/Haskell/Extra/Singleton.agda
@@ -1,21 +1,28 @@
 module Haskell.Extra.Singleton where
 
-open import Haskell.Prelude
+open import Haskell.Prelude hiding (pure; _<*>_)
 
 data Singleton (a : Set) : @0 a → Set where
   MkSingl : ∀ x → Singleton a x
-
 {-# COMPILE AGDA2HS Singleton unboxed #-}
 
-pureSingl : {a : Set} (x : a) → Singleton a x
-pureSingl x = MkSingl x
+module Idiom where
+
+  pure : {a : Set} (x : a) → Singleton a x
+  pure x = MkSingl x
+  {-# COMPILE AGDA2HS pure inline #-}
+
+  _<*>_ : {a b : Set} {@0 f : a → b} {@0 x : a}
+        → Singleton (a → b) f → Singleton a x → Singleton b (f x)
+  MkSingl f <*> MkSingl x = MkSingl (f x)
+  {-# COMPILE AGDA2HS _<*>_ inline #-}
 
-{-# COMPILE AGDA2HS pureSingl transparent #-}
+open Idiom public renaming (pure to pureSingl; _<*>_ to apSingl)
 
 fmapSingl
   : {a b : Set} (f : a → b) {@0 x : a}
   → Singleton a x
   → Singleton b (f x)
 fmapSingl f (MkSingl x) = MkSingl (f x)
-
 {-# COMPILE AGDA2HS fmapSingl inline #-}
+
diff --git a/test/Singleton.agda b/test/Singleton.agda
index c9232ff2..79ffae45 100644
--- a/test/Singleton.agda
+++ b/test/Singleton.agda
@@ -1,5 +1,5 @@
-open import Haskell.Prelude
-open import Haskell.Extra.Singleton
+open import Haskell.Prelude hiding (pure; _<*>_)
+open import Haskell.Extra.Singleton as Singleton
 
 test1 : (@0 x : ⊤) → Singleton ⊤ x
 test1 x = MkSingl tt
@@ -11,3 +11,9 @@ test2 : {a b : Set} (f : a → b) {@0 x : a} → Singleton a x → Singleton b (
 test2 f {x} sx = fmapSingl f {x} sx
 
 {-# COMPILE AGDA2HS test2 #-}
+
+test3 : {@0 x y : Nat} → Singleton Nat x → Singleton Nat y → Singleton Nat (x + y)
+test3 x y = (| x + y |)
+  where open Singleton.Idiom
+
+{-# COMPILE AGDA2HS test3 #-}