Crash on reads with different datatype ordering

[txiang61]

Dafny version

4.5.0

Code to produce this issue

class S { }

datatype A = A(s: S) {}

datatype C = C(b: B) {

  static ghost const f := (x: C) 
    reads x.b.a.s => x.ToSpec()
  
  ghost function ToSpec(): bool
    reads b.a.s
}

datatype B = B(a: A) {}

Command to run and resulting output

dafny verify --warn-shadowing --relax-definite-assignment=false --isolate-assertions --general-traits=datatype --type-system-refresh

What happened?

Crashes. Verifies if switch the order of datatype B and datatype C.

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

Mac

[stefan-aws]

A more refined example that crashes with --type-system-refresh and verifies without:

class S {}

class C {
  const f := (x: B') reads x.s => true // doesn't fail
  const g := (x: B) reads x.s => true // fails
}

datatype C' = C'() {
  const f := (x: B') reads x.s => true // doesn't fail
  const g := (x: B) reads x.s => true // fails
}

datatype B = B(s: S) {}

class B' {
  const s: S
  constructor B'(s: S) {
    this.s := s;
  }
}