[ fix #185 ] Only drop module parameter arguments of local where fu…

…nctions

src/Agda2Hs/Compile/Function.hs

@@ -119,27 +119,26 @@ compileFun' withSig def@(Defn {..}) = do
     err = "Not supported: type definition with `where` clauses"
 
 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
+compileClause mod x c = withClauseLocals mod c $ compileClause' mod x c
+
+compileClause' :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))
+compileClause' curModule x c@Clause{ clauseBody = Nothing} = return Nothing
+compileClause' curModule x c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c
   addContext (KeepNames clauseTel) $ do
     ps <- compilePats namedClausePats
-    ls <- asks locals
-    let
-      (children, ls') = partition
-        (   not . isExtendedLambdaName
-         /\ (curModule `isFatherModuleOf`) . qnameModule )
-        ls
-    withLocals ls' $ do
-      body <- compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody
-      whereDecls <- mapM (getConstInfo >=> compileFun' True) children
-      let rhs = Hs.UnGuardedRhs () body
-          whereBinds | null whereDecls = Nothing
-                     | otherwise       = Just $ Hs.BDecls () (concat whereDecls)
-          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 $ Just match
+    body <- compileTerm $ fromMaybe __IMPOSSIBLE__ clauseBody
+    let isWhereDecl = not . isExtendedLambdaName
+          /\ (curModule `isFatherModuleOf`) . qnameModule
+    children <- filter isWhereDecl <$> asks locals
+    whereDecls <- mapM (getConstInfo >=> compileFun' True) children
+    let rhs = Hs.UnGuardedRhs () body
+        whereBinds | null whereDecls = Nothing
+                   | otherwise       = Just $ Hs.BDecls () (concat whereDecls)
+        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 $ 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 (Maybe (Hs.Match ()))
+compileClause' :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))

src/Agda2Hs/Compile/Term.hs

@@ -33,7 +33,7 @@ import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.HsUtils
 
-import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause )
+import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause' )
 
 isSpecialTerm :: QName -> Maybe (QName -> Elims -> C (Hs.Exp ()))
 isSpecialTerm q = case prettyShow q of
@@ -185,8 +185,7 @@ lambdaCase q es = setCurrentRange (nameBindingSite $ qnameName q) $ do
   npars <- size <$> lookupSection mname
   let (pars, rest) = splitAt npars es
       cs           = applyE cls pars
-  ls   <- filter (`extLamUsedIn` cs) <$> asks locals
-  cs   <- withLocals ls $ mapMaybeM (compileClause (qnameModule q) $ hsName "(lambdaCase)") cs
+  cs <- 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.
@@ -239,10 +238,13 @@ compileTerm v = do
         False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case
           True  -> compileErasedApp es
           False -> do
-            -- Drop module parameters (unless projection-like)
-            n <- (theDef <$> getConstInfo f) >>= \case
-              Function{ funProjection = Right{} } -> return 0
-              _ -> size <$> lookupSection (qnameModule f)
+            reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
+            -- Drop module parameters of local `where` functions
+            xs <- asks locals
+            reportSDoc "agda2hs.compile.term" 15 $ text "Locals: " <+> (prettyTCM xs)
+            n <- if
+              | f `elem` xs -> size <$> lookupSection (qnameModule f)
+              | otherwise   -> return 0
             (`app` drop n es) . Hs.Var () =<< compileQName f
     Con h i es
       | Just semantics <- isSpecialCon (conName h) -> semantics h i es

test/AllTests.agda

@@ -59,6 +59,7 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
+import Issue185
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -118,4 +119,5 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
+import Issue185
 #-}

test/Issue185.agda

@@ -0,0 +1,16 @@
+open import Agda.Builtin.Bool
+
+record RecordTest : Set where
+  constructor MkRecord
+  field
+    aBool : Bool
+
+  aBoolAsAFunction : Bool
+  aBoolAsAFunction = aBool
+open RecordTest public
+{-# COMPILE AGDA2HS RecordTest newtype #-}
+{-# COMPILE AGDA2HS aBoolAsAFunction #-}
+
+test : Bool
+test = aBoolAsAFunction (MkRecord true)
+{-# COMPILE AGDA2HS test #-}

test/golden/AllTests.hs

@@ -57,4 +57,5 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
+import Issue185
 

test/golden/Issue185.hs

@@ -0,0 +1,10 @@
+module Issue185 where
+
+newtype RecordTest = MkRecord{aBool :: Bool}
+
+aBoolAsAFunction :: RecordTest -> Bool
+aBoolAsAFunction r = aBool r
+
+test :: Bool
+test = aBoolAsAFunction (MkRecord True)
+