Non-reference type parameter in extending type causes malformed Boogie

[RustanLeino]

Dafny version

4.8.1

Code to produce this issue

trait Parent {
  function F(): nat
}

datatype Dt<K(!new)> extends Parent = Dt {
  function F(): nat {
    0
  }
}

Command to run and resulting output

% dafny verify test.dfy --type-system-refresh --general-traits=datatype --bprint=d.bpl && boogie d.bpl

Dafny program verifier finished with 2 verified, 0 errors
d.bpl(3025,173): error: where clause not allowed on the 'implementation' copies of formals
1 parse errors detected in d.bpl

What happened?

The program gives rise to an override check, which is described by a Boogie procedure/implementation. What's currently generated is

procedure {:verboseName "Dt.F (override check)"} OverrideCheck$$_module.Dt.F(
    _module.Dt$K: Ty where $AlwaysAllocated(_module.Dt$K),
    this: DatatypeType
       where $Is(this, Tclass._module.Dt(_module.Dt$K))
         && $IsAlloc(this, Tclass._module.Dt(_module.Dt$K), $Heap));
 ...

implementation {:smt_option "smt.arith.solver", "2"} {:verboseName "Dt.F (override check)"} OverrideCheck$$_module.Dt.F(
    _module.Dt$K: Ty where $AlwaysAllocated(_module.Dt$K),
    this: DatatypeType)
{ ... }

In Boogie, the parameters of a procedure can have where clauses. Each implementation of the procedure inherits those where clauses, but is not allowed to repeat them. The example shows that the this parameter adheres to this restriction, but the _module.Dt$K does not.

Note, Boogie enforces this rule in its parser. But since Dafny usually just passes a Boogie AST to the Boogie verifier, this problem is detected only by using the --bprint option and passing the resulting .bpl file directly to the boogie tool.

The fix is simply to omit this where clause for the implementation.

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

Mac