adding support for inlinable type aliases

src/Agda2Hs/Compile/Term.hs

@@ -8,7 +8,7 @@ import Control.Monad.Reader
 import Data.List ( isPrefixOf )
 import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text ( unpack )
-import qualified Data.Set as Set (singleton)
+import qualified Data.Set as Set ( singleton )
 
 import qualified Language.Haskell.Exts as Hs
 
@@ -20,7 +20,7 @@ import Agda.Syntax.Internal
 
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Pretty
-import Agda.TypeChecking.Reduce ( instantiate, unfoldDefinitionStep )
+import Agda.TypeChecking.Reduce ( unfoldDefinitionStep )
 import Agda.TypeChecking.Substitute ( Apply(applyE), raise, mkAbs )
 
 import Agda.Utils.Lens
@@ -230,14 +230,15 @@ compileTerm v = do
       | Just semantics <- isSpecialTerm f -> do
           reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"
           semantics f es
-      | otherwise -> ifM (isClassFunction f) (compileClassFunApp f es) $ do
-          ifM ((isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f) (compileErasedApp es) $ do
-            ifM (isInlinedFunction f) (compileInlineFunctionApp f es) $ do
-              reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
-              -- Drop module parameters of local `where` functions
-              moduleArgs <- getDefFreeVars f
-              reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
-              (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
+      | otherwise ->
+          ifM (isClassFunction f) (compileClassFunApp f es) $
+          ifM ((isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f) (compileErasedApp es) $
+          ifM (isInlinedFunction f) (compileInlineFunctionApp f es) $ do
+            reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
+            -- Drop module parameters of local `where` functions
+            moduleArgs <- getDefFreeVars f
+            reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
+            (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
     Con h i es -> do
       reportSDoc "agda2hs.compile" 8 $ text "reached constructor:" <+> prettyTCM (conName h)
       -- the constructor may be a copy introduced by module application,

src/Agda2Hs/Compile/Type.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeApplications, NamedFieldPuns #-}
 
 module Agda2Hs.Compile.Type where
 
@@ -8,6 +8,7 @@ import Control.Monad.Trans ( lift )
 import Control.Monad.Reader ( asks )
 import Data.List ( find )
 import Data.Maybe ( mapMaybe, isJust )
+import qualified Data.Set as Set ( singleton )
 
 import qualified Language.Haskell.Exts.Syntax as Hs
 import qualified Language.Haskell.Exts.Extension as Hs
@@ -20,7 +21,7 @@ import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
-import Agda.TypeChecking.Reduce ( reduce )
+import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep )
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
@@ -150,7 +151,8 @@ compileType t = do
          | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics f es
          | Just args <- allApplyElims es ->
              ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
-             ifM (isTransparentFunction f) (compileTransparentType args) $ do
+             ifM (isTransparentFunction f) (compileTransparentType args) $
+             ifM (isInlinedFunction f) (compileInlineType f es) $ do
                vs <- compileTypeArgs args
                f <- compileQName f
                return $ tApp (Hs.TyCon () f) vs
@@ -181,6 +183,25 @@ compileTransparentType args = compileTypeArgs args >>= \case
   []     -> __IMPOSSIBLE__
   (v:vs) -> return $ v `tApp` vs
 
+compileInlineType :: QName -> Elims -> C (Hs.Type ())
+compileInlineType f args = do
+  Function { funClauses = cs } <- theDef <$> getConstInfo f
+
+  let [ Clause { namedClausePats = pats
+               , clauseBody = Just body
+               , clauseTel
+               } ] = filter (isJust . clauseBody) cs
+
+  when (length args < length pats) $ genericDocError =<<
+    text "Cannot compile inlinable type alias" <+> prettyTCM f <+> text "as it must be fully applied."
+
+  r <- liftReduce $ locallyReduceDefs (OnlyReduceDefs $ Set.singleton f)
+                  $ unfoldDefinitionStep (Def f args) f args
+
+  case r of
+    YesReduction _ t -> compileType t
+    _                -> genericDocError =<< text "Could not reduce inline function" <+> prettyTCM f
+
 compileDom :: ArgName -> Dom Type -> C CompiledDom
 compileDom x a
   | usableModality a = case getHiding a of

test/Fail/Inline.agda

@@ -0,0 +1,8 @@
+module Fail.Inline where
+
+open import Haskell.Prelude
+
+tail' : List a → List a
+tail' (x ∷ xs) = xs
+tail' [] = []
+{-# COMPILE AGDA2HS tail' inline #-}

test/Fail/Inline2.agda

@@ -0,0 +1,7 @@
+module Fail.Inline2 where
+
+open import Haskell.Prelude
+
+tail' : (xs : List a) → @0 {{ NonEmpty xs }}  → List a
+tail' (x ∷ xs) = xs
+{-# COMPILE AGDA2HS tail' inline #-}

test/Inlining.agda

@@ -2,6 +2,14 @@ module Inlining where
 
 open import Haskell.Prelude
 
+Alias : Set
+Alias = Bool
+{-# COMPILE AGDA2HS Alias inline #-}
+
+aliased : Alias
+aliased = True
+{-# COMPILE AGDA2HS aliased #-}
+
 record Wrap (a : Set) : Set where
   constructor Wrapped
   field

test/golden/Inline.err

@@ -0,0 +1,2 @@
+test/Fail/Inline.agda:5,1-6
+Cannot make function tail' inlinable. An inline function must have exactly one clause.

test/golden/Inline2.err

@@ -0,0 +1,2 @@
+test/Fail/Inline2.agda:5,1-6
+Cannot make function tail' inlinable. Inline functions can only use variable patterns, dot patterns, or transparent record constructor patterns.

test/golden/Inlining.hs

@@ -1,5 +1,8 @@
 module Inlining where
 
+aliased :: Bool
+aliased = True
+
 test1 :: Int -> Int
 test1 x = 1 + x