[ re #431 ] Use same strategy for inlining types as for terms

Author: jespercockx

src/Agda2Hs/Compile/Name.hs

@@ -91,6 +91,8 @@ compileName n = hsName . show <$> pretty (nameConcrete n)
 
 compileQName :: QName -> C (Hs.QName ())
 compileQName f = do
+  whenM (isInlinedFunction f) $
+    agda2hsErrorM $ "Failed to inline definition of" <+> prettyTCM f
   whenJustM (getCompileToName f) $ \g ->
     reportSDoc "agda2hs.compile.to" 20 $ text $
       "compiling name " <> prettyShow f <> " to " <> prettyShow g

src/Agda2Hs/Compile/Term.hs

@@ -467,7 +467,6 @@ compileTerm ty v = do
   reduceProjectionLike v >>= \case
 
     v@(Def f es) -> do
-      whenM (isInlinedFunction f) $ bad "inlined function" v
       ty <- defType <$> getConstInfo f
       compileSpined (compileDef f ty) (Def f) ty es
 

src/Agda2Hs/Compile/Type.hs

@@ -87,9 +87,12 @@ compileType t = do
   reportSDoc "agda2hs.compile.type" 12 $ text "Compiling type" <+> prettyTCM t
   reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t
 
+  toInline <- getInlineSymbols
+  t <- locallyReduceDefs (OnlyReduceDefs toInline) $ reduce t
+
   whenM (isErasedBaseType t) fail
 
-  instantiate t >>= \case
+  case t of
     Pi a b -> do
       reportSDoc "agda2hs.compile.type" 13 $ text "Compiling pi type (" <+> prettyTCM (absName b)
         <+> text ":" <+> prettyTCM a <+> text ") -> " <+> underAbstraction a b prettyTCM
@@ -110,10 +113,9 @@ compileType t = do
          | Just args <- allApplyElims es ->
              ifJustM (isUnboxRecord 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
-               vs <- compileTypeArgs (defType def) args
+             ifM (isTransparentFunction f) (compileTransparentType (defType def) args) $ do
                f <- compileQName f
+               vs <- compileTypeArgs (defType def) args
                return $ tApp (Hs.TyCon () f) vs
          | otherwise -> fail
 
@@ -151,10 +153,11 @@ compileType t = do
 compileTypeArgs :: Type -> Args -> C [Hs.Type ()]
 compileTypeArgs ty [] = pure []
 compileTypeArgs ty (x:xs) = do
+  reportSDoc "agda2hs.compile.type" 16 $ text "compileTypeArgs ty =" <+> prettyTCM x
   (a, b) <- mustBePi ty
-  reportSDoc "agda2hs.compile.type" 16 $ text "compileTypeArgs x =" <+> prettyTCM x
-  reportSDoc "agda2hs.compile.type" 16 $ text "                a =" <+> prettyTCM a
-  reportSDoc "agda2hs.compile.type" 16 $ text "         modality =" <+> prettyTCM (getModality a)
+  reportSDoc "agda2hs.compile.type" 16 $ text "                 x =" <+> prettyTCM x
+  reportSDoc "agda2hs.compile.type" 16 $ text "                 a =" <+> prettyTCM a
+  reportSDoc "agda2hs.compile.type" 16 $ text "          modality =" <+> prettyTCM (getModality a)
   let rest = compileTypeArgs (absApp b $ unArg x) xs
   let fail msg = agda2hsErrorM $ (text msg <> text ":") <+> parens (prettyTCM (absName b) <+> text ":" <+> prettyTCM (unDom a))
   compileDom a >>= \case
@@ -204,23 +207,6 @@ compileTransparentType ty args = compileTypeArgs ty args >>= \case
   []     -> __IMPOSSIBLE__
 
 
-compileInlineType :: QName -> Elims -> C (Hs.Type ())
-compileInlineType f args = do
-  Function { funClauses = cs } <- theDef <$> getConstInfo f
-
-  let [ Clause { namedClausePats = pats } ] = filter (isJust . clauseBody) cs
-
-  when (length args < length pats) $ agda2hsErrorM $
-    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
-    _                -> agda2hsErrorM $ text "Could not reduce inline type alias " <+> prettyTCM f
-
-
 data DomOutput = DOInstance | DODropped | DOType | DOTerm
 
 compileDom :: Dom Type -> C DomOutput

test/golden/Inline.err

@@ -1,4 +1,2 @@
 test/Fail/Inline.agda:10.1-5: error: [CustomBackendError]
-agda2hs:
-  cannot compile inlined function:
-    tail'
+agda2hs: Failed to inline definition of tail'

test/golden/Inline2.err

@@ -1,4 +1,2 @@
 test/Fail/Inline2.agda:9.1-5: error: [CustomBackendError]
-agda2hs:
-  cannot compile inlined function:
-    tail'
+agda2hs: Failed to inline definition of tail'