Resolver crashes on possibly empty subset type of trait

[ssomayyajula]

Dafny version

4.4.0

Code to produce this issue

// Trampoline.dfy

trait ProgramTrait {
  method Compute() returns (r: Result)
}

type Program = ProgramTrait | true

datatype Result =
| Bounce(next: Program)
| Done()

datatype Trivial extends ProgramTrait =
  Trivial()
{
  method Compute() returns (r: Result)
  {
    return Done();
  }
}

Command to run and resulting output

$ dafny verify --type-system-refresh --general-traits:datatype Trampoline.dfy

Unhandled exception: System.AggregateException: One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.InferredTypeProxy' to type 'Microsoft.Dafny.UserDefinedType'.)
 ---> System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.InferredTypeProxy' to type 'Microsoft.Dafny.UserDefinedType'.
   at Microsoft.Dafny.ModuleResolver.CheckCanBeConstructed(Type type, ISet`1 typeParametersUsed) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ModuleResolver.cs:line 2920
   at Microsoft.Dafny.ModuleResolver.CheckCanBeConstructed(Type type, ISet`1 typeParametersUsed) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ModuleResolver.cs:line 2951
   at Microsoft.Dafny.ModuleResolver.ComputeGroundingCtor(IndDatatypeDecl dt) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ModuleResolver.cs:line 2879
   at Microsoft.Dafny.ModuleResolver.SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph`1 dependencies) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ModuleResolver.cs:line 2841
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleDescription, Boolean isAnExport) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1260
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName) in /com.docker.devenvironments.code/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 482
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in /com.docker.devenvironments.code/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 123
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ModuleResolver.cs:line 180
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ProgramResolver.cs:line 175
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in /com.docker.devenvironments.code/Source/DafnyCore/Resolver/ProgramResolver.cs:line 69
   at Microsoft.Dafny.DafnyMain.<>c__DisplayClass8_0.<Resolve>b__0() in /com.docker.devenvironments.code/Source/DafnyCore/DafnyMain.cs:line 87
   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) in /com.docker.devenvironments.code/Source/DafnyCore/DafnyMain.cs:line 87
   at Microsoft.Dafny.DafnyMain.ParseCheck(TextReader stdIn, IReadOnlyList`1 files, String programName, DafnyOptions options, Program& program) in /com.docker.devenvironments.code/Source/DafnyCore/DafnyMain.cs:line 52
   at Microsoft.Dafny.CompilerDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId) in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 295
   at Microsoft.Dafny.CompilerDriver.Run(DafnyOptions options) in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 67
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyDriver/DafnyNewCli.cs:line 114
--- 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.DafnyNewCli.<>c__DisplayClass16_0.<<AddDeveloperHelp>b__0>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyDriver/DafnyNewCli.cs:line 264
--- 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.<<UseExceptionHandler>b__0>d.MoveNext()

What happened?

CheckCanBeConstructed() in ModuleResolver.cs attempts the invalid cast above. Curiously, this program verifies when type Program is annotated with witness Trivial() (but not witness *).

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

Mac