[ re #185 ] Don't drop data/record module parameters + introduce help…

…er function `moduleParametersToDrop`
agda · Oct 12, 2023 · 3037b1a · 3037b1a
1 parent 42f83e2
commit 3037b1a
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 5 deletions.
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
@@ -89,9 +89,9 @@ qualifyType s = \case
 -- arguments bound.
 compileTopLevelType :: Bool -> Type -> (Hs.Type () -> C a) -> C a
 compileTopLevelType keepType t cont = do
-    ctxArgs <- getContextArgs
-    modTel <- lookupSection =<< currentModule
-    go (modTel `apply` ctxArgs) cont
+    reportSDoc "agda2hs.compile.type" 12 $ text "Compiling top-level type" <+> prettyTCM t
+    modTel <- moduleParametersToDrop =<< currentModule
+    go modTel cont
   where
     go :: Telescope -> (Hs.Type () -> C a) -> C a
     go EmptyTel cont = do

diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
@@ -18,7 +18,7 @@ import qualified Agda.Syntax.Concrete.Name as C
 import Agda.Syntax.Internal
 import Agda.Syntax.Position ( noRange )
 import Agda.Syntax.Scope.Base
-import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName )
+import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName, isDatatypeModule )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import qualified Agda.Syntax.Common.Pretty as P
 
@@ -32,7 +32,7 @@ import Agda.TypeChecking.Monad.SizedTypes ( isSizeType )
 import Agda.TypeChecking.Pretty ( Doc, (<+>), text, PrettyTCM(..) )
 import Agda.TypeChecking.Records ( isRecordConstructor, getRecordOfField )
 import Agda.TypeChecking.Reduce ( instantiate, reduce )
-import Agda.TypeChecking.Substitute ( Subst, TelV(TelV) )
+import Agda.TypeChecking.Substitute ( Subst, TelV(TelV), Apply(..) )
 import Agda.TypeChecking.Telescope ( telView )
 
 import Agda.Utils.Lens ( (<&>) )
@@ -157,6 +157,15 @@ dropClassModule m@(MName ns) = isClassModule m >>= \case
   True  -> dropClassModule $ MName $ init ns
   False -> return m
 
+moduleParametersToDrop :: ModuleName -> C Telescope
+moduleParametersToDrop mod = do
+   reportSDoc "agda2hs.moduleParameters" 25 $ text "Getting telescope for" <+> prettyTCM mod
+   isDatatypeModule mod >>= \case
+     Just _ -> return EmptyTel
+     Nothing -> do
+       ctxArgs <- getContextArgs
+       (`apply` ctxArgs) <$> lookupSection mod
+
 isUnboxRecord :: QName -> C (Maybe Strictness)
 isUnboxRecord q = do
   getConstInfo q >>= \case