[ re #357 ] Rewrite \x -> (a -> x) to (->) a and \x -> ((->) x)…

… to `(->)`

src/Agda2Hs/Compile/Type.hs

@@ -128,12 +128,21 @@ compileType t = do
 
     Sort s -> return (Hs.TyStar ())
 
-    -- TODO: we should also drop lambdas that can be erased based on their type
-    -- (e.g. argument is of type Level/Size or in a Prop) but currently we do
-    -- not have access to the type of the lambda here.
-    Lam argInfo restAbs
-      | hasQuantity0 argInfo -> underAbstraction_ restAbs compileType
-      | otherwise -> genericDocError =<< text "Not supported: type-level lambda" <+> prettyTCM t
+    Lam argInfo restAbs -> do
+      (body , x0) <- underAbstraction_ restAbs $ \b ->
+        (,) <$> compileType b <*> (hsName <$> compileDBVar 0)
+
+      -- TODO: we should also drop lambdas that can be erased based on their type
+      -- (e.g. argument is of type Level/Size or in a Prop) but currently we do
+      -- not have access to the type of the lambda here.
+      if | hasQuantity0 argInfo -> return body
+         -- Rewrite `\x -> (a -> x)` to `(->) a`
+         | Hs.TyFun _ a (Hs.TyVar _ y) <- body
+         , y == x0 -> return $ Hs.TyApp () (Hs.TyCon () $ Hs.Special () $ Hs.FunCon ()) a
+         -- Rewrite `\x -> ((->) x)` to `(->)`
+         | Hs.TyApp _ (Hs.TyCon _ (Hs.Special _ (Hs.FunCon _))) (Hs.TyVar _ y) <- body
+         , y == x0 -> return $ Hs.TyCon () $ Hs.Special () $ Hs.FunCon ()
+         | otherwise -> genericDocError =<< text "Not supported: type-level lambda" <+> prettyTCM t
 
     _ -> fail
   where fail = genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t

test/AllTests.agda

@@ -88,6 +88,7 @@ import Issue317
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
+import FunCon
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -173,4 +174,5 @@ import Issue317
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
+import FunCon
 #-}

test/FunCon.agda

@@ -0,0 +1,22 @@
+
+open import Haskell.Prelude
+
+data D1 (t : Set → Set) : Set where
+  C1 : t Bool → D1 t
+
+{-# COMPILE AGDA2HS D1 #-}
+
+f1 : D1 (λ a → Int → a)
+f1 = C1 (_== 0)
+
+{-# COMPILE AGDA2HS f1 #-}
+
+data D2 (t : Set → Set → Set) : Set where
+  C2 : t Int Int → D2 t
+
+{-# COMPILE AGDA2HS D2 #-}
+
+f2 : D2 (λ a b → a → b)
+f2 = C2 (_+ 1)
+
+{-# COMPILE AGDA2HS f2 #-}

test/golden/AllTests.hs

@@ -83,4 +83,5 @@ import Issue317
 import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
+import FunCon
 

test/golden/FunCon.hs

@@ -0,0 +1,12 @@
+module FunCon where
+
+data D1 t = C1 (t Bool)
+
+f1 :: D1 ((->) Int)
+f1 = C1 (== 0)
+
+data D2 t = C2 (t Int Int)
+
+f2 :: D2 (->)
+f2 = C2 (+ 1)
+