Crash in new resolver

[keyboardDrummer]

The following program crashes the resolver

ghost function f2(items: set<nat>): (r:nat)
  requires |items| > 0 {
    var item :| item in items;
    item
}

function f(items: set<nat>) : (r:nat)
requires |items| > 0 {
    //assume exists item :: item in items && forall other <- items :: item == other || item < other;
    //assert exists item Smallest()
    var item :| IsSmallest(items, item);
    item
}

predicate IsSmallest(s: set<nat>, item: nat) 
  requires item in s {
  m in s && forall y: nat :: y in s ==> m <= y
}

lemma Smallest(s: set<nat>) returns (m: nat)
  requires s != {}
  ensures m in s && IsSmallest(s, m)
  decreases s
{
  m :| m in s;
  if y: nat :| y in s && y < m {
    ghost var s' := s - {m};
    assert y in s';
    m := ThereIsASmallest(s');
  }
}

function smallest(items: set<nat>): (r: nat)
  requires |items| > 0

method m(items: set<nat>) returns (r:nat)
requires |items| > 0 {
    var item :| item in items;
    return item;
}

results in:

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.UnusedPreType' to type 'Microsoft.Dafny.DPreType'.
   at Microsoft.Dafny.PreTypeConstraints.ConfirmConstraint(CommonConfirmationBag check, PreType preType, DPreType auxPreType)
   at Microsoft.Dafny.PreTypeConstraints.ConfirmTypeConstraints()
   at Microsoft.Dafny.PreTypeConstraints.SolveAllTypeConstraints(String printableContext)
   at Microsoft.Dafny.PreTypeResolver.ResolveFunction(Function f)
   at Microsoft.Dafny.PreTypeResolver.ResolveMember(MemberDecl member)
   at Microsoft.Dafny.PreTypeResolver.ResolveDeclarationBody(Declaration d)
   at Microsoft.Dafny.PreTypeResolver.ResolveDeclarations(List`1 declarations, ModuleResolver resolver, Boolean firstPhaseOnly)
   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.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<Resolve>b__0()
   at Microsoft.Dafny.LanguageServer.Language.CachingResolver.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.<>c__DisplayClass5_0.<<ResolveAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.Compilation.ResolveAsync()