Disappearing qualified import

[flupe]

Minimal example of a bug I encountered with qualified imports.

A.agda:

module A where

open import Haskell.Prelude

X : Set
X = ⊤

{-# COMPILE AGDA2HS X #-}

B.agda:

module B where

open import Haskell.Prelude

import A

X : Set
X = A.X

{-# COMPILE AGDA2HS X #-}

---

Compiling file B.agda yields:

module B where

import A (X)

type X = X

A is not imported qualified somehow.

[flupe]

Don't know if this is intended behavior, but the current test case for qualified import does expect the qualification to disappear:

agda2hs/test/QualifiedImports.agda

Lines 7 to 15 in 15314cd

	import Importee
	simpqualBar : Int
	simpqualBar = Importee.foo
	{-# COMPILE AGDA2HS simpqualBar #-}
	simpfoo : Importee.Foo
	simpfoo = Importee.Foo.MkFoo
	{-# COMPILE AGDA2HS simpfoo #-}

agda2hs/test/golden/QualifiedImports.hs

Lines 3 to 12 in 15314cd

	import Importee (Foo(MkFoo), foo)
	import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
	-- ** simple qualification
	simpqualBar :: Int
	simpqualBar = foo
	simpfoo :: Foo
	simpfoo = MkFoo

---

Edit: introduced in #202 , before that things were qualified properly.

[omelkonian]

Maybe worth looking at the "clashing-imports check":

https://github.com/agda/agda2hs/blob/master/test/Fail/ClashingImport.agda#L1-L12

(generally, the whole feature got introduced in PR #136)

This bug might suggest two possible solutions:

1. Extend the check to also account for name clashing with definitions of this module.
2. Treat import M in Agda as import qualified M as M in Haskell.

[flupe]

Gonna investigate. Personally I find your 2nd solution to be the most sensible choice.

[jespercockx]

I agree with solution 2. A non-opened import really should be translated to a qualified import in Haskell.