[ fix #340 ] Compile pattern lambda to regular lambda if all proper p…

…atterns are erased

src/Agda2Hs/Compile/Term.hs

@@ -79,14 +79,20 @@ lambdaCase q ty args = compileLocal $ setCurrentRangeQ q $ do
   cs <- mapMaybeM (compileClause' mname (Just q) (hsName "(lambdaCase)") ty') cs
 
   case cs of
-    -- If there is a single clause and all patterns got erased, we
-    -- simply return the body. do
-    [Hs.Match _ _ [] (Hs.UnGuardedRhs _ rhs) _] -> return rhs
+    -- If there is a single clause and all proper patterns got erased,
+    -- we turn the remaining arguments into normal lambdas.
+    [Hs.Match _ _ ps (Hs.UnGuardedRhs _ rhs) _]
+      | null ps -> return rhs
+      | all isVarPat ps -> return $ Hs.Lambda () ps rhs
     _ -> do
       lcase <- hsLCase =<< mapM clauseToAlt cs -- Pattern lambdas cannot have where blocks
       eApp lcase <$> compileArgs ty' rest
       -- undefined -- compileApp lcase (undefined, undefined, rest)
 
+  where
+    isVarPat :: Hs.Pat () -> Bool
+    isVarPat Hs.PVar{} = True
+    isVarPat _ = False
 
 -- | Compile @if_then_else_@ to a Haskell @if ... then ... else ... @ expression.
 ifThenElse :: DefCompileRule

test/AllTests.agda

@@ -85,6 +85,7 @@ import Issue305
 import Issue302
 import Issue309
 import Issue317
+import ErasedPatternLambda
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -167,4 +168,5 @@ import Issue305
 import Issue302
 import Issue309
 import Issue317
+import ErasedPatternLambda
 #-}

test/ErasedPatternLambda.agda

@@ -0,0 +1,18 @@
+open import Haskell.Prelude
+
+Scope = List Bool
+
+data Telescope (@0 α : Scope) : @0 Scope → Set where
+  ExtendTel : ∀ {@0 x β} → Bool → Telescope (x ∷ α) β  → Telescope α (x ∷ β)
+{-# COMPILE AGDA2HS Telescope #-}
+
+caseTelBind : ∀ {@0 x α β} (tel : Telescope α (x ∷ β))
+            → ((a : Bool) (rest : Telescope (x ∷ α) β) → @0 tel ≡ ExtendTel a rest → d)
+            → d
+caseTelBind (ExtendTel a tel) f = f a tel refl
+
+{-# COMPILE AGDA2HS caseTelBind #-}
+
+checkSubst : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) → Bool
+checkSubst t = caseTelBind t λ ty rest → λ where refl → True
+{-# COMPILE AGDA2HS checkSubst #-}

test/golden/AllTests.hs

@@ -80,4 +80,5 @@ import Issue305
 import Issue302
 import Issue309
 import Issue317
+import ErasedPatternLambda
 

test/golden/ErasedPatternLambda.hs

@@ -0,0 +1,10 @@
+module ErasedPatternLambda where
+
+data Telescope = ExtendTel Bool Telescope
+
+caseTelBind :: Telescope -> (Bool -> Telescope -> d) -> d
+caseTelBind (ExtendTel a tel) f = f a tel
+
+checkSubst :: Telescope -> Bool
+checkSubst t = caseTelBind t (\ ty rest -> True)
+