Example in "Namespaces and Imports" does not type check

[lasarojc]

The following example from the documentation

module Outer {
  var x: int

  def xPlus(z) = x + z

  module Inner {
    val x2 = x + x
  }

  val inv =
    (Inner.x2 - x == x)
}

Does not type check.

[konnov]

Just to better understand what's going on, does not it typecheck in VSCode?

quint typecheck Foo.qnt actually works for me.

[konnov]

As a side problem, it does not work in REPL, as REPL does not support constants yet. The error message is using the outdated syntax:

compile error: <input>:8:5 - error: Assignment <- needs two arguments

[shonfeder]

I am also not able to reproduce on

$ quint --version
0.5.0

[lasarojc]

My bad. I copied the first example by mistake and stuck to it, but it is actually the second example. The issue is updated.

[shonfeder]

thanks for explaining! here's the error:

$  quint typecheck scratch.qnt
/home/sf/Sync/informal-systems/apalache/quint/scratch.qnt:7:14 - error: Failed to resolve name x in definition for x2, in module Inner
7:     val x2 = x + x
                ^

/home/sf/Sync/informal-systems/apalache/quint/scratch.qnt:7:18 - error: Failed to resolve name x in definition for x2, in module Inner
7:     val x2 = x + x
                    ^

error: parsing failed

[konnov]

We should probably ask @bugarela. This may be outdated syntax actually.

[bugarela]

I didn't notice we intended to support that, so this variable visibility is indeed not implemented. The question is: do we still want to support this? The outer module can already access names from the inner modules with namespaces, perhaps it would be too much to allow the other way around as well.

[konnov]

This syntax is probably redundant, if we can import Inner.x2

[shonfeder]

I am slightly confused: it looks to me from the example that the inner module is unable to access the state variables from the surrounding outer module, however your discussion seems to indicate the opposite problem. Am I miss understanding?

[bugarela]

@konnov are you saying that import Inner.x2 would cause conflicts? I'm also having trouble understanding this part

[shonfeder]

To clarify, as far as I understand the error as arising at this point in the spec:

  module Inner {
    val x2 = x + x
  }

In particular, the attempt to refer to the state variable x from within Inner.

If nested submodules are not able to access the values in their parent module, then I don't think I understand what the point of nested modules would be.

[konnov]

I think you are right, @shonfeder. I could not understand this example anymore, though I have written it myself some time ago. I think my motivation was to introduce some form of namespaces. I am not so sure anymore whether we need nested modules at all. And if we need them, I would most likely vote for not having any form of references to outer modules.

[konnov]

I have opened a discussion #496 on the broad issue of nested modules.

[shonfeder]

We decided not to support nested modules!

[lasarojc]

@shonfeder ok. Should I close this?

[shonfeder]

I had meant to close when I commented. Thanks for pointing that out!