Merge remote-tracking branch 'origin/master' into splitOffPartsOfSing…

…lePassCompiler

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

@@ -510,7 +510,7 @@ public abstract partial class SinglePassCodeGenerator {
  var e = (LambdaExpr)expr;
 
  IVariable receiver = null;
- if (enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true }) {
+ if (thisContext != null && (enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true })) {
  var name = ProtectedFreshId("_this");
  var ty = ModuleResolver.GetThisType(e.tok, thisContext);
  receiver = new LocalVariable(RangeToken.NoToken, name, ty, false) {

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -4756,7 +4756,6 @@ private class ArrayLvalueImpl : ILvalue {
  return result;
  }
 
-
  private void CompileTypeTest(TypeTestExpr expr, bool inLetExprBody, ConcreteSyntaxTree wr, ref ConcreteSyntaxTree wStmts) {
  var fromType = expr.E.Type;
  if (fromType.IsSubtypeOf(expr.ToType, false, false)) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5523.dfy

@@ -0,0 +1,14 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+function Loop(xs: seq<()>): ()
+{
+ if |xs| == 0
+ then ()
+ else
+ var _: bool -> bool := e => e;
+ Loop(xs[1..])
+}
+
+method Main(){
+ print Loop([(), ()]), "\n";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5523.dfy.expect

@@ -0,0 +1 @@
+()

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5523.dfy.rs.check

@@ -0,0 +1 @@
+CHECK: error\[E0277\]: the trait bound

docs/dev/news/5524.fix

@@ -0,0 +1 @@
+Only guard `this` when eliminating tail calls, if possible