Vars in traits can't be part of extend reveals clauses and it crashes Dafny

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

module TraitContainer {
  trait Trait extends object {
    ghost var traitVar: nat
  }

  export reveals Trait
}

module ImportingModule {
  import opened TraitContainer

  @AssumeCrossModuleTermination // https://github.com/dafny-lang/dafny/issues/1588
  class Implementation extends Trait {
    constructor() {}
  }
}

Command to run and resulting output

dafny verify file.dfy

Process terminated. Assertion failed.
   at Microsoft.Dafny.MemberSelectExpr.MemberSelectCase[A](Func`2 fieldK, Func`2 functionK) in dafny\Source\DafnyCore\AST\Expressions\Applications\MemberSelectExpr.cs:line 282
   at Microsoft.Dafny.BoogieGenerator.ExpressionTranslator.TrExpr(Expression expr) in dafny\Source\DafnyCore\Verifier\BoogieGenerator.ExpressionTranslator.cs:line 466
   at Microsoft.Dafny.BoogieGenerator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\Statements\BoogieGenerator.TrStatement.cs:line 279
   at Microsoft.Dafny.BoogieGenerator.TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables localVariables, ExpressionTranslator etran) in dafny\Source\DafnyCore\Verifier\BoogieGenerator.Methods.cs:line 818

What happened?

So it appears that

• traitVar creates two functions in the trait, a getter and a setter
• The function is not revealed (and I haven't found a way to reveal it in the export set, since it's not displayed as a function)
• The constructor is trying to ensure that this.traitVar == this.traitVar() where the first one is actually a single identifier (dot included), but because the function is not revealed in scope, it crashes the contract assertion.

My instincts tell me that when we reveal a trait, we should also reveal its vars automatically.

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

Windows