fix module application

src/Agda2Hs/AgdaUtils.hs

@@ -21,6 +21,7 @@ import Agda.Syntax.TopLevelModuleName
 import Agda.TypeChecking.Monad ( topLevelModuleName )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Substitute
+import Agda.TypeChecking.Reduce ( reduceDefCopy )
 
 import Agda.Utils.Either ( isRight )
 import Agda.Utils.List ( initMaybe )
@@ -101,3 +102,18 @@ getTopLevelModuleForQName = getTopLevelModuleForModuleName . qnameModule
 lookupModuleInCurrentModule :: C.Name -> TCM [AbstractModule]
 lookupModuleInCurrentModule x =
   List1.toList' . Map.lookup x . nsModules . thingsInScope [PublicNS, PrivateNS] <$> getCurrentScope
+
+-- | Try to unfold a definition if introduced by module application.
+maybeUnfoldCopy
+  :: PureTCM m
+  => QName -- ^ Name of the definition.
+  -> Elims
+  -> (Term -> m a)
+  -- ^ Callback if the definition is indeed a copy.
+  -> (QName -> Elims -> m a)
+  -- ^ Callback if the definition isn't a copy.
+  -> m a
+maybeUnfoldCopy f es onTerm onDef =
+  reduceDefCopy f es >>= \case
+    NoReduction ()   -> onDef f es
+    YesReduction _ t -> onTerm t

src/Agda2Hs/Compile/Term.hs

@@ -230,25 +230,29 @@ compileTerm v = do
       hsVar s `app` es
     -- v currently we assume all record projections are instance
     -- args that need attention
-    Def f es
+    Def f es -> maybeUnfoldCopy f es compileTerm $ \f es -> if
       | Just semantics <- isSpecialTerm f -> do
-        reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"
-        semantics f es
+          reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"
+          semantics f es
       | otherwise -> isClassFunction f >>= \case
-        True  -> compileClassFunApp f es
-        False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case
-          True  -> compileErasedApp es
-          False -> do
-            reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
-            -- Drop module parameters of local `where` functions
-            moduleArgs <- getDefFreeVars f
-            reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
-            (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
-    Con h i es
-      | Just semantics <- isSpecialCon (conName h) -> semantics h i es
-    Con h i es -> isUnboxConstructor (conName h) >>= \case
-      Just _  -> compileErasedApp es
-      Nothing -> (`app` es) . Hs.Con () =<< compileQName (conName h)
+          True  -> compileClassFunApp f es
+          False -> (isJust <$> isUnboxProjection f) `or2M` isTransparentFunction f >>= \case
+            True  -> compileErasedApp es
+            False -> do
+              reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function"
+              -- Drop module parameters of local `where` functions
+              moduleArgs <- getDefFreeVars f
+              reportSDoc "agda2hs.compile.term" 15 $ text "Module arguments for" <+> (prettyTCM f <> text ":") <+> prettyTCM moduleArgs
+              (`app` drop moduleArgs es) . Hs.Var () =<< compileQName f
+    Con h i es -> do
+      reportSDoc "agda2hs.compile" 8 $ text "reached constructor:" <+> prettyTCM (conName h)
+      -- the constructor may be a copy introduced by module application,
+      -- therefore we need to find the original constructor
+      info <- getConstInfo (conName h)
+      if not (defCopy info)
+        then compileCon h i es
+        else let Constructor{conSrcCon = c} = theDef info in
+             compileCon c ConOSystem es
     Lit l -> compileLiteral l
     Lam v b | usableModality v, getOrigin v == UserWritten -> do
       when (patternInTeleName `isPrefixOf` absName b) $ genericDocError =<< do
@@ -272,7 +276,16 @@ compileTerm v = do
     t -> genericDocError =<< text "bad term:" <?> prettyTCM t
   where
     app :: Hs.Exp () -> Elims -> C (Hs.Exp ())
-    app hd es = eApp <$> pure hd <*> compileElims es
+    app hd es = eApp hd <$> compileElims es
+
+    compileCon :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())
+    compileCon h i es
+      | Just semantics <- isSpecialCon (conName h)
+      = semantics h i es
+    compileCon h i es =
+      isUnboxConstructor (conName h) >>= \case
+        Just _  -> compileErasedApp es
+        Nothing -> (`app` es) . Hs.Con () =<< compileQName (conName h)
 
 -- `compileErasedApp` compiles an application of an erased constructor
 -- or projection.

src/Agda2Hs/Compile/Type.hs

@@ -150,6 +150,8 @@ compileType' t = do
 compileType :: Term -> C (Hs.Type ())
 compileType t = do
   reportSDoc "agda2hs.compile.type" 12 $ text "Compiling type" <+> prettyTCM t
+  reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t
+
   case t of
     Pi a b -> compileDom (absName b) a >>= \case
       DomType _ hsA -> do
@@ -159,7 +161,7 @@ compileType t = do
         hsB <- underAbstraction a b (compileType . unEl)
         return $ constrainType hsA hsB
       DomDropped -> underAbstr a b (compileType . unEl)
-    Def f es -> do
+    Def f es -> maybeUnfoldCopy f es compileType $ \f es -> do
       def <- getConstInfo f
       if | not (usableModality def) ->
             genericDocError

test/AllTests.agda

@@ -61,6 +61,7 @@ import Issue200
 import Issue169
 import Issue210
 import ModuleParameters
+import ModuleParametersImports
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -122,4 +123,5 @@ import Issue200
 import Issue169
 import Issue210
 import ModuleParameters
+import ModuleParametersImports
 #-}

test/ModuleParametersImports.agda

@@ -0,0 +1,10 @@
+module ModuleParametersImports where
+
+open import Haskell.Prelude
+open import ModuleParameters Bool (λ _ → Nat)
+
+scope : Scope
+scope = unbind (Bind True 3 (Bind False 2 Empty))
+{-# COMPILE AGDA2HS scope #-}
+
+

test/golden/AllTests.hs

@@ -59,4 +59,5 @@ import Issue200
 import Issue169
 import Issue210
 import ModuleParameters
+import ModuleParametersImports
 

test/golden/ModuleParametersImports.hs

@@ -0,0 +1,11 @@
+module ModuleParametersImports where
+
+import qualified ModuleParameters (Scope(Bind, Empty), unbind)
+import Numeric.Natural (Natural)
+
+scope :: ModuleParameters.Scope Natural
+scope
+  = ModuleParameters.unbind
+      (ModuleParameters.Bind 3
+         (ModuleParameters.Bind 2 ModuleParameters.Empty))
+