diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 8df020a7aa3..b60787eb9ae 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/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;