Case-split generates code containing internal module name

[GoogleCodeExporter]

What's the problem?

I have two modules, each in a separate file, as follows:

module Other (parameter : Set) where
  data Foo : Set where
    foo : Foo

module Bug where
  postulate
    something : Set

  open import Other something

  bar : Foo → Foo
  bar x = {!x!}                       -- I do C-c C-c here
  -- bar .#Other-230273218.foo = ?    -- I get this
  -- bar foo = ?                      -- I want this

Problem: If I do a case split in the hole in module Bug, I get some internal 
name instead of just foo. Seems to be related to "open import" vs "open" and 
then "import" as well as importing a module with parameters.

What version of Agda are you using?

Agda HEAD (Agda version 2.3.3).

Original issue reported on code.google.com by ren...@informatik.uni-tuebingen.de on 6 Sep 2013 at 4:08

[GoogleCodeExporter]

For some reason the bug is not triggered if the code above is put in a
single file (under "module M where") and "import" is removed.

Original comment by nils.anders.danielsson on 17 Sep 2013 at 9:09

• Changed title: Case-split generates code containing internal module name
• Changed state: Accepted
• Added labels: CaseSplitting, Milestone-2.3.4, Modules, Priority-High, Type-Defect

[GoogleCodeExporter]

Mmh, one reason is probably that "open import Module parameter" is implemented
at the level of parsing instead at the level of scope checking. See issue #481
for some context concerning the addition of this syntax.

  open import Module parameter

is implemented as

  import Module as .Fresh
  private open module _ = .Fresh parameter

It could be that Agda sees the need to print the constructor as qualified since
it thinks that there are several constructors with name foo in place.

  .Fresh.foo
  ._.foo

(The anon. module). If I do the manual decomposition of open import into

  import Common.Issue481ParametrizedModule as M123

  private
    open module M4711 = M123 Set

  bar : Foo → Foo
  bar x = {! x !}                       -- I do C-c C-c here

then x is replaced by M123.foo instead of foo, clearly not what I want.

Seems that disdisambiguation for constructors is not implemented properly. In
patterns, we could really have ambiguous constructors without problems, so
proper ambiguation should be applied here.

Original comment by andreas....@gmail.com on 29 Oct 2013 at 4:31

• Added labels: Display

[GoogleCodeExporter]

Since I have no clue how constructor QNames are translated from abstract to 
concrete, I should leave this issue to Ulf, or get some tutorial from him about 
this...

Original comment by andreas....@gmail.com on 29 Oct 2013 at 5:29

[GoogleCodeExporter]

Mmh, now I found that inverseScopeLookup does not do its job correctly for 
constructors.  This function is already to blame for issue 719.

Here is the scope for the case above

    * scope (top-level-module)
      private
        names
          Bla --> [M4711.Bla]
          Foo --> [M4711.Foo]
          foo --> [M4711.Foo.foo]
          id --> [M4711.id]
        modules
          Foo --> [M4711.Foo]
          M123 --> [Common.Issue481ParametrizedModule]
          M4711 --> [M4711]
      public
        names
          bar --> [bar]

    * scope M4711
      public
        names
          Bla --> [M4711.Bla]
          Foo --> [M4711.Foo]
          foo --> [M4711.Foo.foo]
          id --> [M4711.id]
        modules
          Foo --> [M4711.Foo]

    * scope M4711.Foo
      public
        names
          foo --> [M4711.Foo.foo]

-- inverse looking up abstract name Common.Issue481ParametrizedModule.Foo.foo
-- yields Just M123.foo

Thus, the original constructor that is stored in the pattern is 
Common.Issue481ParametrizedModule.Foo.foo
but we would like to recover M4711.Foo.foo which is printed as just foo.

Original comment by andreas....@gmail.com on 29 Oct 2013 at 8:41

[GoogleCodeExporter]

We do not even need import or parameterized modules.  It is sufficient to 
trigger a section application by the following code:

module Other where
  data Foo : Set where
    foo : Foo

module M = Other  -- triggers a section application
open M

bar : Foo → Foo
bar x = {!x!}                     -- I do C-c C-c here
-- bar Other.foo = ?              -- I get this
-- bar foo = ?                    -- I want this

after module Issue896b
ScopeInfo
  current = 
  context = TopCtx
  modules
    * scope 
    * scope Issue896b
      private
        names
          Foo --> [Issue896b.M.Foo]
          foo --> [Issue896b.M.Foo.foo]
        modules
          Foo --> [Issue896b.M.Foo]
      public
        names
          bar --> [Issue896b.bar]
        modules
          M --> [Issue896b.M]
          Other --> [Issue896b.Other]
    * scope Issue896b.Other
      public
        names
          Foo --> [Issue896b.Other.Foo]
          foo --> [Issue896b.Other.Foo.foo]
        modules
          Foo --> [Issue896b.Other.Foo]
    * scope Issue896b.Other.Foo
      public
        names
          foo --> [Issue896b.Other.Foo.foo]
    * scope Issue896b.M
      public
        names
          Foo --> [Issue896b.M.Foo]
          foo --> [Issue896b.M.Foo.foo]
        modules
          Foo --> [Issue896b.M.Foo]
    * scope Issue896b.M.Foo
      public
        names
          foo --> [Issue896b.M.Foo.foo]

applying section Other
  ptel =
  tel  =
  tel' =
  tel''=
  eta  =
applySection M = Other
    defs: fromList [(Issue896b.Other.Foo,Issue896b.M.Foo),(Issue896b.Other.Foo.foo,Issue896b.M.Foo.foo)]
    mods: fromList [(Issue896b.Other.Foo,Issue896b.M.Foo)]
inverse looking up abstract name Issue896b.Other.Foo.foo yields Just Other.foo
inverse looking up abstract name Issue896b.M.Foo yields Just Foo

Original comment by andreas....@gmail.com on 29 Oct 2013 at 10:00

[GoogleCodeExporter]

In order to make this work we need type directed pretty printing.
Plan: refactor CheckInternal to make it possible to use it to define arbitrary
type directed traversals, and then implement reify for typed terms (pair of
a term and its type).

Original comment by ulf.nor...@gmail.com on 1 Nov 2013 at 1:37

• Removed labels: CaseSplitting

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 3 Jun 2014 at 10:44

• Added labels: Milestone-2.3.6
• Removed labels: Milestone-2.3.4

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 3 Jun 2014 at 11:34

• Added labels: Milestone-2.4.2
• Removed labels: Milestone-2.3.6

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 20 Aug 2014 at 11:44

• Added labels: Milestone-2.4.4
• Removed labels: Milestone-2.4.2

[andreasabel]

Duplicate of #1635.