Null pointer exception on underconstrained closures

[MikaelMayer]

method m() {
  var f := st => set x | x in st;
}

To test it on the command-line:

echo "method m() { var f := st => set x | x in st; }" | ./Binaries/Dafny.exe -stdin

(1,17): Error: the type of this variable is underspecified
(1,36): Error: the type of this variable is underspecified
(1,32): Error: type of bound variable 'x' could not be determined; please
specify the type explicitly
Unhandled exception. System.AggregateException: One or more errors occurred. (Ob
ject reference not set to an instance of an object.)
---> System.NullReferenceException: Object reference not set to an instance of
an object.
at Microsoft.Dafny.Resolver.DiscoverAllBounds_Aux_SingleVar[VT](List1 bvars, Int32 j, Expression expr, Boolean polarity, List1 knownBounds) in dafny\Source\Dafny\Resolver\BoundsDiscovery.cs:line 197

The error is here:

          case BinaryExpr.ResolvedOpcode.InSeq:
            if (whereIsBv == 0) {
              bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1, e0.Type, e1.Type.AsSeqType.Arg));
            }                                     //AsSeqType seems to return null ^^

After this crash, the IDE extension no longer processes any other Dafny code and crashes until the IDE is restarted

[MikaelMayer]

Good news, since recent changes, the issue is still there, but the LSP server is no longer stuck. I only displays the error in the diagnostics window, making it possible for the user to identify what is wrong by dissecting.