Abstract module + type parameter crashes Dafny

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

abstract module A {
  opaque predicate Valid<R>(n: int)
  { true }
}

abstract module B refines A {
}

Command to run and resulting output

Paste in VSCode or verify on the command line

Unhandled exception: System.AggregateException: One or more errors occurred. (Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index'))
 ---> System.ArgumentOutOfRangeException: Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index')
   at Microsoft.Dafny.CheckTypeInferenceVisitor.PostVisitOneExpression(Expression expr, TypeInferenceCheckingContext context)
   at Microsoft.Dafny.ASTVisitor`1.VisitExpression(Expression expr, VisitorContext context)
   at Microsoft.Dafny.ASTVisitor`1.<>c__DisplayClass13_0.<VisitExpression>b__0(Expression ee)
   at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable`1 coll, Action`1 action)
   at Microsoft.Dafny.ASTVisitor`1.VisitExpression(Expression expr, VisitorContext context)
   at Microsoft.Dafny.ASTVisitor`1.VisitAttributes(IAttributeBearingDeclaration parent, ModuleDefinition enclosingModule)
   at Microsoft.Dafny.ASTVisitor`1.VisitMethod(Method method)
   at Microsoft.Dafny.ASTVisitor`1.VisitMember(MemberDecl member)
   at System.Collections.Generic.List`1.ForEach(Action`1 action)
   at Microsoft.Dafny.ASTVisitor`1.VisitOneDeclaration(TopLevelDecl decl)
   at Microsoft.Dafny.CheckTypeInferenceVisitor.VisitOneDeclaration(TopLevelDecl decl)
   at System.Collections.Generic.List`1.ForEach(Action`1 action)
   at Microsoft.Dafny.ASTVisitor`1.VisitDeclarations(List`1 declarations)
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleDescription, Boolean isAnExport)
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName)
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass5_0.<Resolve>b__0()
   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)
--- End of stack trace from previous location ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task.Wait(Int32 millisecondsTimeout, CancellationToken cancellationToken)
   at System.Threading.Tasks.Task.Wait()
   at Microsoft.Dafny.DafnyMain.Resolve(Program program)
   at Microsoft.Dafny.CompilerDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId)
   at Microsoft.Dafny.CompilerDriver.RunCompiler(DafnyOptions options)
   at Microsoft.Dafny.DafnyCli.<>c__DisplayClass10_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyCli.<>c__DisplayClass21_0.<<AddDeveloperHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<<UseExceptio

What happened?

Dafny crashed.

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

Windows

[MikaelMayer]

The problem was introduced in 4.3. It did not exist in 4.2

[MikaelMayer]

Removing "opaque" makes things work. It looks like it's related to the creation of the reveal lemma which might be missing type arguments