Imported constructor is qualified with internal module when normalizing

[jespercockx]

I have one file Test1.agda

module Test1 (A : Set₁) where
data Foo : Set where
  foo : Foo

and another file Test2.agda

module Test2 where
open import Test1 Set

When I load Test2 and ask Agda to normalize foo, I would expect to get foo but I get .#Test1-137587325.foo instead.

The following attempt at a workaround also doesn't work:

module Test2 where
open import Test1 Set hiding (foo)
open Foo

but this one does:

module Test2 where
import Test1
open Test1 Set hiding (foo)
open Test1.Foo

This could be a duplicate of #896, but I'm not sure.

[andreasabel]

I closed #896, let's continue the work on this issue here.