[ fix #443 ] Disallow anything that's not a function in where blocks

Author: jespercockx

src/Agda2Hs/Compile/Function.hs

@@ -236,7 +236,7 @@ compileClause'' curModule projName x ty c@Clause{..} = do
     let withWhereModule = case children of
           []    -> id
           (c:_) -> addWhereModule $ qnameModule c
-    whereDecls <- withWhereModule $ compileLocal $ mapM (getConstInfo >=> compileFun' True) children
+    whereDecls <- withWhereModule $ compileLocal $ mapM compileWhereDef children
 
     let Just body            = clauseBody
         Just (unArg -> typ)  = clauseType
@@ -250,6 +250,13 @@ compileClause'' curModule projName x ty c@Clause{..} = do
           (Hs.Symbol{}, p : q : ps) -> Hs.InfixMatch () p x (q : ps) rhs whereBinds
           _                         -> Hs.Match () x ps rhs whereBinds
     return $ Just match
+  where
+    compileWhereDef f = do
+      def <- getConstInfo f
+      case theDef def of
+        Function{} -> compileFun' def
+        def -> agda2hsErrorM $
+          "Cannot compile" <+> prettyTCM f <+> "in a `where` block"
 
 keepClause :: Clause -> C Bool
 keepClause c@Clause{..} = case (clauseBody, clauseType) of

test/Fail/Issue443.agda

@@ -0,0 +1,9 @@
+open import Haskell.Prelude
+
+module Fail.Issue443 where
+
+test : ⊤
+test = local
+  where postulate local : ⊤
+
+{-# COMPILE AGDA2HS test #-}

test/golden/Issue443.err

@@ -0,0 +1,2 @@
+test/Fail/Issue443.agda:5.1-5: error: [CustomBackendError]
+agda2hs: Cannot compile Fail.Issue443.local in a `where` block