quint icon indicating copy to clipboard operation
quint copied to clipboard

Name resolution has issues when qualifiers conflict with modules

Open bugarela opened this issue 1 year ago • 2 comments

This case results in [QNT406] Instantiation error: 'N' is not a constant in 'A'

module A {
  const N: int
  val a = N
}

module B {
  import A(N=1) as A
  import A(N=2).*
  val b = A::a + a
}

In this one, bar can't be found:

module A {
  val a = 1
}

module Foo {
  val bar = 5
}

module B {
  import A as Foo
  import Foo.*
  val test = bar
}


The problem is that, after processing the first import, the name resolution overwrites the table for the name A or Foo with the table for the qualified module.

We might be able to support this if we really want, but I tested and typescript doesn't allow conflicting qualifiers: image

So it might be a matter of raising a proper error.

bugarela avatar Aug 08 '23 12:08 bugarela

Related issue: This goes through name resolution, but then fails at flattening

import intN(BITWIDTH=64) as int64 from "intN"
type Int64 = int64::IntN
import int64.*

The intended behavior was such that the following solution satisfied it:

import intN(BITWIDTH=64).* from "intN"
type Int64 = IntN

import uintN(BITWIDTH=64) as uint64 from "uintN"
type Uint64 = uint64::UintN

bugarela avatar Oct 05 '23 11:10 bugarela

The first example in the issue description is working now! But not the second.

shonfeder avatar Jan 09 '24 17:01 shonfeder