[fix #219] always qualify unopened imports

src/Agda2Hs/Compile/Name.hs

@@ -150,10 +150,10 @@ compileQName f
         (C.Qual as C.QName{} : _) -> liftTCM $ do
           let qual = hsModuleName $ prettyShow as
           lookupModuleInCurrentModule as >>= \case
-            (x:_) | qual /= mod -> isDatatypeModule (amodName x) >>= \case
-              Just{} -> return $ QualifiedAs Nothing
-              Nothing -> return $ QualifiedAs $ Just qual
-            _ -> return Nothing
+            (x:_) | qual /= mod -> do
+              isDataMod <- isJust <$> isDatatypeModule (amodName x)
+              return $ QualifiedAs (if isDataMod then Nothing else Just qual)
+            _ -> return $ QualifiedAs Nothing
           `catchError` \_ -> return $ QualifiedAs Nothing
         _ -> return $ QualifiedAs Nothing
 

test/QualifiedImports.agda

@@ -35,3 +35,7 @@ qualFooable = Qually.doTheFoo
 qualDefaultBar : Qually.Foo
 qualDefaultBar = Qually.defaultFoo
 {-# COMPILE AGDA2HS qualDefaultBar #-}
+
+Foo : Set
+Foo = Importee.Foo
+{-# COMPILE AGDA2HS Foo #-}

test/golden/QualifiedImports.hs

@@ -1,15 +1,15 @@
 module QualifiedImports where
 
-import Importee (Foo(MkFoo), foo)
+import qualified Importee (Foo(MkFoo), foo)
 import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
 
 -- ** simple qualification
 
 simpqualBar :: Int
-simpqualBar = foo
+simpqualBar = Importee.foo
 
-simpfoo :: Foo
-simpfoo = MkFoo
+simpfoo :: Importee.Foo
+simpfoo = Importee.MkFoo
 
 -- ** qualified imports
 
@@ -25,3 +25,5 @@ qualFooable = Qually.doTheFoo
 qualDefaultBar :: Qually.Foo
 qualDefaultBar = Qually.defaultFoo
 
+type Foo = Importee.Foo
+