Internal error when reavealing in subset type witness clause

[racko]

Dafny version

4.9.0+25fa1000744d8d8a9a6a84c0712149daeda6f67e

Code to produce this issue

type T = x: int | true witness (reveal f(); 0)

Command to run and resulting output

$ dafny verify bug.dfy
Encountered internal compilation exception: Specified method is not supported.
Unhandled exception: System.NotSupportedException: Specified method is not supported.
   at Microsoft.Dafny.TypeSynonymDeclBase.get_ContainsHide()
   at Microsoft.Dafny.CodeContextWrapper.get_ContainsHide()
   at Microsoft.Dafny.HideRevealStmt.GenResolve(INewOrOldResolver resolver, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveStatement(Statement stmt, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext)
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd)
   at Microsoft.Dafny.ModuleResolver.ResolveNamesAndInferTypes(List`1 declarations, Boolean initialRound)
   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.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.Compilation.ResolveAsync()
   at Microsoft.Dafny.VerifyCommand.HandleVerification(DafnyOptions options)
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_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.DafnyNewCli.<>c__DisplayClass17_0.<<AddDeveloperHelp>b__1>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.<<UseExceptionHandler>b__0>d.MoveNext()

Seems to be a regression from 4.8.1:

$ dafny --version
4.8.1+d15eef77080d3262d783bbed92b285bf148cce6b
$ dafny verify bug.dfy 
bug.dfy(1,39): Error: cannot reveal 'f' because no revealable constant, function, assert label, or requires label in the current scope is named 'f'
  |
1 | type T = x: int | true witness (reveal f(); 0)
  |                                        ^

1 resolution/type errors detected in bug.dfy

Providing an opaque definition for f,

opaque function f(): int { 0 }

type T = x: int | true witness (reveal f(); 0)

the less minimal example verifies with 4.8.1 but I get the same error with 4.9.0

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

Linux