Null-related issues with bounded polymorphism

[RustanLeino]

Dafny version

4.7.0

Code to produce this issue

// Here are four examples that exhibit (the same or related) null problems

// Example 0

trait G {
  const Three := 3
  const Six := Three + Three
}

class E extends G { }

method DoIt<G1 extends G>(g1: G1) {
  var g := g1 as G;
  print g.Six, "\n";
}

method Main() {
  DoIt<E?>(null); // should be an error: E? does not extend G
}

// Example 1

trait G extends object {
  const Three := 3
  const Six := Three + Three
}

class E extends G { }

method DoIt<G1 extends G?>(g1: G1) {
  var g := g1 as G; // should be an error: g1 is a G?, but it might not be a G (because it might be null)
  print g.Six, "\n";
}

method Main() {
  DoIt<E?>(null);
}

// Example 2

trait G extends object {
  const Three := 3
  const Six := Three + Three
}

class E extends G { }

method DoIt<G1 extends G?>(g1: G1) {
  var g := g1 as G?;
  print g.Six, "\n"; // should be an error: this is trying to deference a G?, but it is not known whether or not g is null
}

method Main() {
  DoIt<E?>(null);
}

// Example 3

trait G {
  const Three := 3
  const Six := Three + Three
}

class E extends G { }

trait Thing<G1 extends G> {
  function GetG(): (g: G1)

  method PrintGSix() {
    var g1 := GetG();
    var g := g1 as G;
    print g.Six, "\n";
  }
}

class MyThing extends Thing<E?> { // should be an error: E? does not extend G
  function GetG(): (g: E?) {
    null
  }
}

method Main() {
  var thing := new MyThing;
  thing.PrintGSix();
}

Command to run and resulting output

Each of the programs above passes resolution and verification, but the compiled program causes a crash. For example:

% dafny run test.dfy --type-system-refresh --general-traits=datatype

Dafny program verifier finished with 2 verified, 0 errors
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at _module.__default.DoIt[__G1](__G1 g1) in test.cs:line 5707
   at _module.__default._Main(ISequence`1 __noArgsParameter) in test.cs:line 5712
   at __CallToMain.<>c__DisplayClass0_0.<Main>b__0() in test.cs:line 5742
   at Dafny.Helpers.WithHaltHandling(Action action) in test.cs:line 1673
   at __CallToMain.Main(String[] args) in test.cs:line 5742

What happened?

The compiled program crashes.

What type of operating system are you experiencing the problem on?

Mac