Crash using subset type

[MikaelMayer]

Dafny version

nightly

Code to produce this issue

type seq31<T> = x: seq<T> | |x| <= 31
method TakeThis(
  x: seq31<int> := []
) {
  TakeThis();
}

Command to run and resulting output

Paste in VSCode

What happened?

This code was working in Dafny 4.2.0 but crashes now in latest nightly.

Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.
System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.UserDefinedType' to type 'Microsoft.Dafny.CollectionType'.
   at Microsoft.Dafny.BoogieGenerator.CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, String resultDescription)
   at Microsoft.Dafny.BoogieGenerator.<>c__DisplayClass391_0.<AddMethodImpl>b__6(WFOptions wfo)
   at Microsoft.Dafny.BoogieGenerator.ReadsCheckDelayer.DoWithDelayedReadsChecks(Boolean doOnlyCoarseGrainedTerminationChecks, Action`1 action)
   at Microsoft.Dafny.BoogieGenerator.AddMethodImpl(Method m, Procedure proc, Boolean wellformednessProc)
   at Microsoft.Dafny.BoogieGenerator.AddMethod_Top(Method m, Boolean isByMethod, Boolean includeAllMethods)
   at Microsoft.Dafny.BoogieGenerator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
   at Microsoft.Dafny.BoogieGenerator.AddRevealableTypeDecl(RevealableTypeDecl d)
   at Microsoft.Dafny.BoogieGenerator.DoTranslation(Program p, ModuleDefinition forModule)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.<>c__DisplayClass3_0.<GetVerificationTasksAsync>b__0()
   at System.Threading.Tasks.Task`1.InnerInvoke()
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location ---
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
--- End of stack trace from previous location ---
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine boogieEngine, CompilationAfterResolution compilation, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.<>c__DisplayClass31_1.<<VerifyUnverifiedSymbol>b__2>d.MoveNext()
   at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify verifiable, CompilationAfterResolution compilation)
   at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify verifiable, CompilationAfterResolution compilation)

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

Windows

[stefan-aws]

Was able to reproduce the issue with 4.3.0 and nightly.

[jtristan]

I think the problem is that the type inference used to type [] as seq but now types [] as seq31. It makes the Boogie generator fail as it expects a sequence display expression to have a collection type and not a user defined type.

[jtristan]

Found the source of the issue. PR #4538 modified AST/Expressions/DefaultValueExpression.cs and added this.ResolvedExpression.Type = this.Type; to the method FillIn. Commenting out that line fixes this issue.