.#modulename-number in goals of open imported parameterised modules

[GoogleCodeExporter]

I see strange printing of internal names when I open import a parameterised module in a different file, using the latest git version of Agda. To reproduce, create the following files:

-------------- A.agda --------------
module A (X : Set1) where

  data D : Set where
    d : D
------------------------------------

-------------- B.agda --------------
module B where 

open import A Set

open import Relation.Binary.PropositionalEquality

test : (c : D) -> (c ≡ c)
test d = {!!} -- goal ".#A-60005532.d ≡ .#A-60005532.d"
------------------------------------

If I change "open import A Set" into

import A
open A Set

then the printing problem disappears. It also does not occur if A is not parameterised.

Original issue reported on code.google.com by fredrik....@gmail.com on 8 Sep 2014 at 9:20

[GoogleCodeExporter]

My bad. I just hacked the parser (Parser.y) to get the sugar open import A Set. The proper solution is to add a new declaration to Syntax.Concrete and process it properly in the Translation.ConcreteToAbstract.

Parser.y:

    ; unique = hashString $ show $ (Nothing :: Maybe ()) <$ r
         -- turn range into unique id, but delete file path
         -- which is absolute and messes up suite of failing tests
         -- (different hashs on different installations)
         -- TODO: Don't use (insecure) hashes in this way.
    ; fresh = Name mr [ Id $ stringToRawName $ ".#" ++ show m ++ "-" ++ show unique ]

Maybe not too difficult to fix?

Original comment by andreas....@gmail.com on 11 Sep 2014 at 9:11

• Changed state: Accepted

[GoogleCodeExporter]

See issue #481 for the initial feature request open import M args and some discussion.

Original comment by andreas....@gmail.com on 15 Sep 2014 at 12:59

• Added labels: Modules, Syntax

[GoogleCodeExporter]

My bad. I just hacked the parser (Parser.y) to get the sugar open import A Set. ...

Are you sure?

I removed 'unique' from Parser.y and I defined 'Fresh' as it was defined before the commit c370b16 (see the issue-1278 branch).

I was expecting an error on

  open import A Set

but it type-checked without problems.

Original comment by andres.s...@gmail.com on 15 Sep 2014 at 1:19

• Changed state: InfoNeeded

[GoogleCodeExporter]

I think the problem is not about whether it type checks, but how names are printed.

Note that the freshness magic is to ensure that you can write two "open import" statements for the same module without getting an error about duplicate module identifier A and without confusing the two instantiations of the same module, e.g.

open import A Set using ()
open import A Set

Issue #896 seems also related but not quite.

Note that with

open import A Set

A is not in scope, so the expected goal would be

.A.d == .A.d

Original comment by andreas....@gmail.com on 15 Sep 2014 at 3:38

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 15 Sep 2014 at 7:53

• Changed state: Accepted

[GoogleCodeExporter]

Andres, are you planning to take this issue? (Maybe you should set the Owner then.)

Original comment by andreas....@gmail.com on 16 Sep 2014 at 11:37

[GoogleCodeExporter]

I don't dare to answer affirmatively :-)

Original comment by andres.s...@gmail.com on 16 Sep 2014 at 7:42

[GoogleCodeExporter]

I just want to avoid a race to fix this bug. ;-) You can give back ownership.

Original comment by andreas....@gmail.com on 18 Sep 2014 at 6:56

[GoogleCodeExporter]

... at any time, if you choose to.

Original comment by andreas....@gmail.com on 18 Sep 2014 at 6:57

[GoogleCodeExporter]

Please, be my guest :-)

Original comment by andres.s...@gmail.com on 23 Sep 2014 at 2:51

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 29 Sep 2014 at 2:22

• Changed state: Started

[asr]

Note that with

open import A Set

A is not in scope, so the expected goal would be

.A.d == .A.d

@andreasabel, the goal in upstream is

?0 : d ≡ d

isn't it the expected behaviour?

[andreasabel]

That looks fine. I guess we can add the test case and close this issue.

[asr]

I'll do it.