Parser should not dynamically inject shared builtin program components

[robin-aws]

The advantage of dynamically generating elements such as tuple, array, and arrow types is that there's no maximum arity of such generic types. However, this interferes with being able to compile packages separately, since separate packages may decide to generate the same elements, leading to conflicts when loading or linking.

The easiest fix would be to pre-generate these types up to a maximum arity. Scala currently does this (with a cap of 22) but it looks like Scala 3 will no longer have this limit: scala/scala3#1758. It may be possible to have our cake and eat it too if we borrow some of those techniques.

[robin-aws]

Thinking out loud: to have a robust migration path for this and other future changes, we will likely want to depend on versioning the various target language runtimes. We need to ensure that if Dafny is used to build a DLL (for e.g.) after this change, it will declare a dependency on a version of the runtime that will package the builtins the compiler is now assuming are there already.

[robin-aws]

Note that if you use the dafny.msbuild package to create your DLLs (https://github.com/dafny-lang/dafny.msbuild) then you'll be forced to provide an explicit dependency on DafnyRuntime in your csproj file, so the versioning is under user control. This isn't quite adequate, as a Dafny codebase could get away with too old of a runtime until the code happens to change in a way that fails because of missing builtins. There needs to be tooling support to ensure Dafny can enforce the minimum version of the runtime it is compiling for.

[robin-aws]

I've realized that this is less of a blocking issue for separate compilation than I initially believed, only because many languages allows multiple packages to define the same symbols. For example, if two different jars on your Java classpath both define _System.nat, then it will be loaded from whichever appears earlier on the classpath.

It's still bad practice to allow this state in an application though, since it can lead to very subtle errors when any such ordered lookup behavior is altered (e.g. accidentally reordering the classpath) and the two versions are not actually the identical. Therefore this is still important to fix in the long term, so that packages compiled from Dafny only contain symbols corresponding to the actual Dafny source being compiled.

[cpitclaudel]

Seeing this issue due to your recent comment: another place where I've run into this is reusing the parser (for the REPL), because it forces you to be very careful about the builtins module (but we don't have a way to clone it at the moment)

[robin-aws]

Just to clarify further (as I was briefly confused myself), _System.nat is particularly harmless because that's only a TypeDescriptor for the nat type, and compiled code will generally not use a dedicated "nat" type. That's why the existing Test/comp/separate-compilation/usesTimesTwo.dfy test case doesn't hit any issues despite _System.nat appearing in both projects.

In C# at least, type descriptors are only used in contexts where a default value for a type is needed. If I add this to the usesTimesTwo.dfy source:

method PickANat() returns (n: nat) {
  n := PickSomething();
}

method PickSomething<T(0)>() returns (t: T) {
}

Then the test commands produce this C# code:

  public static BigInteger PickANat()
  {
    BigInteger n = BigInteger.Zero;
    BigInteger _out0;
    _out0 = LibraryModule_Compile.__default.PickSomething<BigInteger>(_System.nat._TypeDescriptor());
    n = _out0;
    return n;
  }
  public static __T PickSomething<__T>(Dafny.TypeDescriptor<__T> _td___T)
  {
    __T t = _td___T.Default();
    return t;
  }

And you see this warning (I've added line breaks):

/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/usesTimesTwo.cs(105,74): warning CS0436: 
The type 'nat' in '/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/usesTimesTwo.cs' conflicts with the imported type 'nat' in 'TimesTwo, Version=3.9.1.41027, Culture=neutral, PublicKeyToken=null'. 
Using the type defined in '/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/usesTimesTwo.cs'. 
[/Users/salkeldr/Documents/GitHub/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj]

Even then it's only a warning and the code still works.

[keyboardDrummer]

Note that the tuple part of this issue was resolved with #2284