[ fix #200 ] Handle absurd clauses in compileClause

src/Agda2Hs/Compile/ClassInstance.hs

@@ -3,6 +3,7 @@ module Agda2Hs.Compile.ClassInstance where
 import Control.Monad ( when, filterM, unless )
 import Control.Monad.Reader ( local )
 
+import Data.Foldable ( toList )
 import Data.List ( nub )
 import Data.Maybe ( isNothing, mapMaybe )
 import qualified Data.HashMap.Strict as HMap
@@ -186,7 +187,7 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do
          -- No minimal dictionary used, proceed with compiling as a regular clause.
          | otherwise
          -> do ms <- disableCopatterns $ compileClause curModule uf c'
-               return ([Hs.InsDecl () (Hs.FunBind () [ms]) | keepArg arg], [])
+               return ([Hs.InsDecl () (Hs.FunBind () (toList ms)) | keepArg arg], [])
 
 fieldArgInfo :: QName -> C ArgInfo
 fieldArgInfo f = do

src/Agda2Hs/Compile/Function.hs

@@ -106,7 +106,7 @@ compileFun' withSig def@(Defn {..}) = do
         pars <- getContextArgs
         reportSDoc "agda2hs.compile" 10 $ "applying clauses to parameters: " <+> prettyTCM pars
         let clauses = filter keepClause funClauses `apply` pars
-        cs <- mapM (compileClause (qnameModule defName) x) clauses
+        cs <- mapMaybeM (compileClause (qnameModule defName) x) clauses
         return $ [Hs.TypeSig () [x] ty | withSig ] ++ [Hs.FunBind () cs]
   where
     Function{..} = theDef
@@ -118,7 +118,8 @@ compileFun' withSig def@(Defn {..}) = do
       addContext tel $ ifIsSort b (\_ -> return True) (return False)
     err = "Not supported: type definition with `where` clauses"
 
-compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Hs.Match ())
+compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))
+compileClause curModule x c@Clause{ clauseBody = Nothing} = return Nothing
 compileClause curModule x c@Clause{..} = withClauseLocals curModule c $ do
   reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c
   addContext (KeepNames clauseTel) $ do
@@ -138,7 +139,7 @@ compileClause curModule x c@Clause{..} = withClauseLocals curModule c $ do
           match = case (x, ps) of
             (Hs.Symbol{}, p : q : ps) -> Hs.InfixMatch () p x (q : ps) rhs whereBinds
             _                         -> Hs.Match () x ps rhs whereBinds
-      return match
+      return $ Just match
 
 noAsPatterns :: DeBruijnPattern -> C ()
 noAsPatterns = \case

src/Agda2Hs/Compile/Function.hs-boot

@@ -4,4 +4,4 @@ import qualified Language.Haskell.Exts.Syntax as Hs ( Match, Name )
 import Agda.Syntax.Internal ( Clause, ModuleName )
 import Agda2Hs.Compile.Types ( C )
 
-compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Hs.Match ())
+compileClause :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))

src/Agda2Hs/Compile/Term.hs

@@ -167,7 +167,7 @@ lambdaCase q es = setCurrentRange (nameBindingSite $ qnameName q) $ do
   let (pars, rest) = splitAt npars es
       cs           = applyE cls pars
   ls   <- filter (`extLamUsedIn` cs) <$> asks locals
-  cs   <- withLocals ls $ mapM (compileClause (qnameModule q) $ hsName "(lambdaCase)") cs
+  cs   <- withLocals ls $ mapMaybeM (compileClause (qnameModule q) $ hsName "(lambdaCase)") cs
   case cs of
     -- If there is a single clause and all patterns got erased, we
     -- simply return the body.

test/AllTests.agda

@@ -57,6 +57,7 @@ import TypeOperatorExport
 import TypeOperatorImport
 import IOFile
 import IOInput
+import Issue200
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -114,4 +115,5 @@ import TypeOperatorExport
 import TypeOperatorImport
 import IOFile
 import IOInput
+import Issue200
 #-}

test/Issue200.agda

@@ -0,0 +1,11 @@
+open import Haskell.Prelude
+
+data Void : Set where
+
+test : Maybe Void → Maybe Void
+test = λ
+    { Nothing → Nothing
+    }
+
+{-# COMPILE AGDA2HS Void #-}
+{-# COMPILE AGDA2HS test #-}

test/golden/AllTests.hs

@@ -55,4 +55,5 @@ import TypeOperatorExport
 import TypeOperatorImport
 import IOFile
 import IOInput
+import Issue200