Fix for issue #443

src/Agda2Hs/Compile.hs

@@ -58,6 +58,7 @@ initCompileEnv genv tlm rewrites = CompileEnv
   , rewrites          = rewrites
   , writeImports      = True
   , checkNames        = True
+  , genSignature      = True
   }
 
 initCompileState :: CompileState
@@ -133,7 +134,7 @@ compile genv tlm _ def =
         (DefaultPragma _     , Axiom{}   ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def
         (DefaultPragma _     , _         ) | isInstance -> pure <$> compileInstance ToDefinition def
         (DefaultPragma _     , Axiom{}   ) -> compilePostulate def
-        (DefaultPragma _     , Function{}) -> compileFun True def
+        (DefaultPragma _     , Function{}) -> compileFun def
         (DefaultPragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord False ds) def
 
         _ -> agda2hsErrorM $ text "Don't know how to compile" <+> prettyTCM (defName def)

src/Agda2Hs/Compile/Function.hs

@@ -95,20 +95,21 @@ compileLitNatPat = \case
 
 
 compileFun, compileFun'
-  :: Bool -- ^ Whether the type signature should also be generated
-  -> Definition -> C [Hs.Decl ()]
+  :: Definition -> C [Hs.Decl ()]
 
-compileFun withSig def@Defn{..} =
+compileFun def@Defn{..} =
   setCurrentRangeQ defName
     $ maybePrependFixity defName (defName ^. lensFixity)
     -- initialize locals when first stepping into a function
     $ withFunctionLocals defName
-    $ compileFun' withSig def
+    $ compileFun' def
 
 -- inherit existing (instantiated) locals
-compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
+compileFun' def@Defn{..} = inTopContext $ withCurrentModule m $ do
   reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
 
+  withSig <- shouldGenerateSignature
+
   whenM ((withSig &&) <$> inRecordMod defName) $
     agda2hsError "not supported: functions inside a record module"
 
@@ -235,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
@@ -249,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
@@ -407,7 +415,7 @@ withClauseLocals curModule c@Clause{..} k = do
 
 -- | Ensure a definition can be defined as transparent.
 checkTransparentPragma :: Definition -> C ()
-checkTransparentPragma def = compileFun False def >>= \case
+checkTransparentPragma def = withoutSignature (compileFun def) >>= \case
     [Hs.FunBind _ cls] ->
       mapM_ checkTransparentClause cls
     [Hs.TypeDecl _ hd b] ->
@@ -461,8 +469,8 @@ checkCompileToFunctionPragma def s = noCheckNames $ do
     "does not match the type" <+> text (Hs.pp rtype) <+> "of" <+> prettyTCM r
   -- Check that clauses match
   reportSDoc "agda2hs.compileto" 20 $ "Checking that clauses of" <+> ppd <+> "matches those of" <+> ppr
-  [Hs.FunBind _ dcls] <- compileFun False def
-  [Hs.FunBind _ rcls] <- compileFun False rdef
+  [Hs.FunBind _ dcls] <- withoutSignature $ compileFun def
+  [Hs.FunBind _ rcls] <- withoutSignature $ compileFun rdef
   unless (length dcls == length rcls) $ fail $
     "they have a different number of clauses"
   forM_ (zip dcls rcls) $ \(dcl , rcl) -> do

src/Agda2Hs/Compile/Record.hs

@@ -51,8 +51,8 @@ compileMinRecord fieldNames m = withMinRecord m $ do
   -- We can't simply compileFun here for two reasons:
   -- * it has an explicit dictionary argument
   -- * it's using the fields and definitions from the minimal record and not the parent record
-  compiled <- addContext (defaultDom rtype) $ compileLocal $
-    fmap concat $ traverse (compileFun False) defaults
+  compiled <- addContext (defaultDom rtype) $ compileLocal $ withoutSignature $
+    fmap concat $ traverse compileFun defaults
   let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ]
   reportSDoc "agda2hs.record.min" 20 $
     text "Done compiling minimal record" <+> pretty m <+>

src/Agda2Hs/Compile/Types.hs

@@ -102,6 +102,8 @@ data CompileEnv = CompileEnv
   -- ^ whether we should add imports of compiled names
   , checkNames :: Bool
   -- ^ whether we should check validity of compiled names
+  , genSignature :: Bool
+  -- ^ whether we should generate type signatures for functions
   }
 
 type Qualifier = Maybe (Maybe (Hs.ModuleName ()))

src/Agda2Hs/Compile/Utils.hs

@@ -451,3 +451,9 @@ noCheckNames = local $ \e -> e { checkNames = False }
 
 doNameCheck :: C Bool
 doNameCheck = reader checkNames
+
+withoutSignature :: C a -> C a
+withoutSignature = local $ \e -> e { genSignature = False }
+
+shouldGenerateSignature :: C Bool
+shouldGenerateSignature = reader genSignature

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