Dafny crash (possibly related to default values for arguments)

[fzaiser]

Dafny version

4.3.0

Code to produce this issue

function SumFromTo(sequence: nat -> real, start: nat := 0, end: nat): real

function PartialSums(sequence: nat -> real): nat -> real {
  (n: nat) => SumFromTo(sequence, n)
}

Command to run and resulting output

$ dafny verify Test.dfy
Process terminated. Assertion failed.
   at Microsoft.Dafny.ModuleResolver.ResolveActualParameters(ActualBindings bindings, List`1 formals, IToken callTok, Object context, ResolutionContext resolutionContext, Dictionary`2 typeMap, Expression receiver) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 3347
   at Microsoft.Dafny.ModuleResolver.ResolveApplySuffix(ApplySuffix e, ResolutionContext resolutionContext, Boolean allowMethodCall) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 6010
   at Microsoft.Dafny.ModuleResolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 548
   at Microsoft.Dafny.ModuleResolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 1117
   at Microsoft.Dafny.Function.Resolve(ModuleResolver resolver) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/AST/Members/Function.cs:line 443
   at Microsoft.Dafny.ModuleResolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 2776
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 155
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypes(List`1 declarations, Boolean initialRound) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs:line 62
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleName, Boolean isAnExport) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1097
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, Boolean isAnExport) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 466
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 123
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/ModuleResolver.cs:line 184
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/ProgramResolver.cs:line 174
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/Resolver/ProgramResolver.cs:line 68
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.<Resolve>b__0() in /private/tmp/dafny-20230929-6545-bad9x4/dafny-4.3.0/Source/DafnyCore/DafnyMain.cs:line 89
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   at System.Threading.Tasks.Task.ExecuteEntry()
   at System.Threading.Tasks.TaskScheduler.TryExecuteTask(Task task)
   at Microsoft.Boogie.CustomStackSizePoolTaskScheduler.WorkLoop()
   at System.Threading.Thread.StartCallback()
[1]    27001 abort      dafny verify Test.dfy

What happened?

Dafny crashed. I didn't expect Dafny to crash.

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

Mac