fix: Crash related to the override check for generic functions (#3692)

Fixes #3691.

Source/DafnyCore/Verifier/FunctionCallSubstituter.cs

@@ -19,17 +19,19 @@ public override Expression Substitute(Expression expr) {
  if (expr is FunctionCallExpr e) {
  var receiver = Substitute(e.Receiver);
  var newArgs = SubstituteExprList(e.Args);
+ var typeApplicationAtEnclosingClass = e.TypeApplication_AtEnclosingClass;
  Function function;
  if ((e.Function.EnclosingClass == Tr || Tr.InheritedMembers.Contains(e.Function)) && e.Receiver is ThisExpr && receiver is ThisExpr && Cl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) {
  receiver = new ThisExpr((TopLevelDeclWithMembers)f.EnclosingClass);
  function = (Function)f;
+ typeApplicationAtEnclosingClass = receiver.Type.AsParentType(Cl).TypeArgs.ToList();
  } else {
  function = e.Function;
  }
  return new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel) {
  Function = function,
  Type = e.Type, // TODO: this may not work with type parameters.
- TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass), // resolve here
+ TypeApplication_AtEnclosingClass = SubstituteTypeList(typeApplicationAtEnclosingClass), // resolve here
  TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction), // resolve here
  IsByMethodCall = e.IsByMethodCall
  };

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

@@ -0,0 +1,12 @@
+// RUN: %exits-with 0 %dafny /compile:0 /allocated:4 /functionSyntax:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait A {
+ predicate f()
+ method g() ensures f()
+}
+
+class B<T> extends A {
+ predicate f() { true }
+ method g() ensures f()
+}

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

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

docs/dev/news/3692.fix

@@ -0,0 +1 @@
+Crash related to the override check for generic functions