Fix C# codegen for tail-recursive member functions

Closes #2173.

RELEASE_NOTES.md

@@ -4,6 +4,7 @@
 - fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142)
 - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942)
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
+- fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (https://github.com/dafny-lang/dafny/pull/2205)
 
 # 3.6.0
 

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -1331,7 +1331,9 @@ public bool ProcessDllImport(MemberDecl decl, ConcreteSyntaxTree wr) {
     protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, ConcreteSyntaxTree wr) {
       Contract.Assume((member is Method m0 && m0.IsTailRecursive) || (member is Function f0 && f0.IsTailRecursive)); // precondition
       if (!member.IsStatic && !NeedsCustomReceiver(member)) {
-        wr.WriteLine("var _this = this;");
+        var receiverType =  member.EnclosingClass is DatatypeDecl dt ?
+          "_I" + dt.CompileName + TypeParameters(SelectNonGhost(dt, dt.TypeArgs)) : "var";
+        wr.WriteLine($"{receiverType} _this = this;");
       }
       wr.Fork(-1).WriteLine("TAIL_CALL_START: ;");
       return wr;

Test/git-issues/git-issue-2173.dfy

@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:4 /compileTarget:cs "%s" >> "%t"
+
+datatype T = Leaf(x: int) | T(t: T) {
+  function method {:tailrecursion} TR() : int {
+    if Leaf? then 0
+    else t.TR()
+  }
+}
+
+method Main() {
+  print Leaf(0).TR();
+}

Test/git-issues/git-issue-2173.dfy.expect

@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+Running...
+
+0