Error when guarding nonexistent this

[fabiomadge]

Dafny version

master

Code to produce this issue

function Loop(xs: seq<()>): ()
{
  if |xs| == 0
  then ()
  else
    var _: bool -> bool := e => e;
    Loop(xs[1..])
}

method Main(){
    print Loop([(), ()]), "\n";
}

Command to run and resulting output

dafny -compileTarget:cs -spillTargetCode:3 [file].dfy

What happened?

#5474 introduced a guarding mechanism for this when doing tail call elimination. This change didn't take the case into account when there can be no this, like outside of a class.

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

Mac