You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
[Error - 11:58:32 AM] Request textDocument/documentSymbol failed.
Message: Internal Error - System.InvalidOperationException: Sequence contains no elements
at System.Linq.ThrowHelper.ThrowNoElementsException()
at System.Linq.Enumerable.Last[TSource](IEnumerable`1 source)
at Microsoft.Dafny.ArrowType.PrettyArrowTypeName(String arrow, List`1 typeArgs, Type result, ModuleDefinition context, Boolean parseAble)
at Microsoft.Dafny.UserDefinedType.TypeName(ModuleDefinition context, Boolean parseAble)
at Microsoft.Dafny.Type.<>c__DisplayClass21_0.<TypeArgsToString>b__0(Type ty)
at Microsoft.Dafny.Util.<>c__DisplayClass3_0`1.<Comma>b__0(T element, Int32 index)
at Microsoft.Dafny.Util.Comma[T](String comma, IEnumerable`1 l, Func`3 f)
at Microsoft.Dafny.Util.Comma[T](IEnumerable`1 l, Func`2 f)
at Microsoft.Dafny.Type.TypeArgsToString(ModuleDefinition context, List`1 typeArgs, Boolean parseAble)
at Microsoft.Dafny.Type.TypeArgsToString(ModuleDefinition context, Boolean parseAble)
at Microsoft.Dafny.MapType.TypeName(ModuleDefinition context, Boolean parseAble)
at Microsoft.Dafny.Type.ToString()
at Microsoft.Dafny.TypeConstraint.ErrorMsg.<Reporting>g__RemoveAmbiguity|5_0(Object[] msgArgs)
at Microsoft.Dafny.TypeConstraint.ErrorMsg.Reporting(ErrorReporter reporter, String suffix)
at Microsoft.Dafny.TypeConstraint.ErrorMsg.ReportAsError(ErrorReporter reporter)
at Microsoft.Dafny.TypeConstraint.ReportErrors(ErrorReporter reporter)
at Microsoft.Dafny.Resolver.SolveAllTypeConstraints()
at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport)
at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(TextDocumentItem document, Program program) in `dafny\Source\DafnyLanguageServer\Language\Symbols\DafnyLangSymbolResolver.cs:line 49
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(TextDocumentItem textDocument, Program program, Boolean& canDoVerification, CancellationToken cancellationToken) in `dafny\Source\DafnyLanguageServer\Language\Symbols\DafnyLangSymbolResolver.cs:line 31
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(DocumentTextBuffer textDocument, CancellationToken cancellationToken) in `dafny\Source\DafnyLanguageServer\Workspace\TextDocumentLoader.cs:line 95
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.<>c__DisplayClass12_0.<<LoadAsync>b__0>d.MoveNext() in `dafny\Source\DafnyLanguageServer\Workspace\TextDocumentLoader.cs:line 78
--- End of stack trace from previous location ---
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken) in `dafny\Source\DafnyLanguageServer\Workspace\TextDocumentLoader.cs:line 77
at Microsoft.Dafny.LanguageServer.Workspace.Compilation.ResolveAsync() in `dafny\Source\DafnyLanguageServer\Workspace\Compilation.cs:line 85
at Microsoft.Dafny.LanguageServer.Workspace.DocumentManager.GetSnapshotAfterResolutionAsync() in `dafny\Source\DafnyLanguageServer\Workspace\DocumentManager.cs:line 177
at Microsoft.Dafny.LanguageServer.Handlers.DafnyDocumentSymbolHandler.Handle(DocumentSymbolParams request, CancellationToken cancellationToken) in `dafny\Source\DafnyLanguageServer\Handlers\DafnyDocumentSymbolHandler.cs:line 34
at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.<RouteRequest>g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(IRequestDescriptor`1 descriptors, Request request, CancellationToken token)
at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__Displ
The text was updated successfully, but these errors were encountered:
This PR used to fix#2833, but I am no longer able to reproduce the problem in the latest master anyway, so I cannot add a test that this PR would solve at this point.
Still, I think it's safer to have a safeguard. Otherwise, when `result` is `null` and `typeArgs` is empty, it will continue to throw an exception
Failing code
I cannot post minimal code.
Steps to reproduce the issue
Expected behavior
No error should appear
Actual behavior
The text was updated successfully, but these errors were encountered: