Do not let 'null' children slip into the AST (#5446)

Fixes #5357

### Description
- Prevent `null` from being returned by `Node.Children`

### How has this been tested?
- Added IDE test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Statements/SkeletonStatement.cs

@@ -1,3 +1,5 @@
+#nullable enable
+
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
@@ -24,11 +26,11 @@ namespace Microsoft.Dafny;
 ///   ConditionOmitted == true && BodyOmitted == false
 /// </summary>
 public class SkeletonStatement : Statement, ICloneable<SkeletonStatement>, ICanFormat {
-  public readonly Statement S;
-  public bool ConditionOmitted { get { return ConditionEllipsis != null; } }
-  public readonly IToken ConditionEllipsis;
-  public bool BodyOmitted { get { return BodyEllipsis != null; } }
-  public readonly IToken BodyEllipsis;
+  public readonly Statement? S;
+  public bool ConditionOmitted => ConditionEllipsis != null;
+  public readonly IToken? ConditionEllipsis;
+  public bool BodyOmitted => BodyEllipsis != null;
+  public readonly IToken? BodyEllipsis;
 
   public SkeletonStatement Clone(Cloner cloner) {
     return new SkeletonStatement(cloner, this);
@@ -52,13 +54,14 @@ public SkeletonStatement(Statement s, IToken conditionEllipsis, IToken bodyEllip
     ConditionEllipsis = conditionEllipsis;
     BodyEllipsis = bodyEllipsis;
   }
+
   public override IEnumerable<Statement> SubStatements {
     get {
       // The SkeletonStatement is really a modification of its inner statement S.  Therefore,
       // we don't consider S to be a substatement.  Instead, the substatements of S are the
       // substatements of the SkeletonStatement.  In the case the SkeletonStatement modifies
       // S by omitting its body (which is true only for loops), there are no substatements.
-      if (!BodyOmitted && S.SubStatements != null) {
+      if (!BodyOmitted && S?.SubStatements != null) {
         foreach (var s in S.SubStatements) {
           yield return s;
         }
@@ -68,7 +71,9 @@ public override IEnumerable<Statement> SubStatements {
 
   public override IEnumerable<Statement> PreResolveSubStatements {
     get {
-      yield return S;
+      if (S != null) {
+        yield return S;
+      }
     }
   }
 

Source/DafnyCore/AST/Types/Types.cs

@@ -1,6 +1,7 @@
 #define TI_DEBUG_PRINT
 using System;
 using System.Collections.Generic;
+using System.Diagnostics;
 using System.Diagnostics.Contracts;
 using System.Linq;
 using System.Threading;
@@ -1946,19 +1947,21 @@ public bool HasTypeArg() {
   }
   public void SetTypeArg(Type arg) {
     Contract.Requires(arg != null);
-    Contract.Requires(1 <= this.TypeArgs.Count);  // this is actually an invariant of all collection types
     Contract.Assume(this.arg == null);  // Can only set it once.  This is really a precondition.
     this.arg = arg;
-    this.TypeArgs[0] = arg;
+
+    Debug.Assert(TypeArgs.Count == 0);
+    TypeArgs.Add(arg);
   }
   public virtual void SetTypeArgs(Type arg, Type other) {
     Contract.Requires(arg != null);
     Contract.Requires(other != null);
-    Contract.Requires(this.TypeArgs.Count == 2);
     Contract.Assume(this.arg == null);  // Can only set it once.  This is really a precondition.
     this.arg = arg;
-    this.TypeArgs[0] = arg;
-    this.TypeArgs[1] = other;
+
+    Debug.Assert(TypeArgs.Count == 0);
+    TypeArgs.Add(arg);
+    TypeArgs.Add(other);
   }
   [ContractInvariantMethod]
   void ObjectInvariant() {
@@ -1971,14 +1974,23 @@ void ObjectInvariant() {
   /// </summary>
   protected CollectionType(Type arg) {
     this.arg = arg;
-    this.TypeArgs = new List<Type> { arg };
+    TypeArgs = new List<Type>(1);
+    if (arg != null) {
+      TypeArgs.Add(arg);
+    }
   }
+
   /// <summary>
   /// This constructor is a collection types with 2 type arguments
   /// </summary>
   protected CollectionType(Type arg, Type other) {
     this.arg = arg;
-    this.TypeArgs = new List<Type> { arg, other };
+    TypeArgs = new List<Type>(2);
+    if (arg != null && other != null) {
+      TypeArgs.Add(arg);
+      TypeArgs.Add(other);
+    }
+    Debug.Assert(arg == null && other == null || arg != null && other != null);
   }
 
   protected CollectionType(Cloner cloner, CollectionType original) {

Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs

@@ -23,6 +23,16 @@ private async Task<List<CompletionItem>> RequestCompletionAsync(TextDocumentItem
       return completionList.OrderBy(completion => completion.Label).ToList();
     }
 
+    [Fact]
+    public async Task CodeCompletionInIncompleteTypeArgumentList() {
+      var source = @"
+function Foo<T>(): seq<".TrimStart();
+      var documentItem = CreateAndOpenTestDocument(source, "CompleteOnThisReturnsClassMembers.dfy");
+
+      var completionList = await RequestCompletionAsync(documentItem, (0, 23));
+      Assert.Empty(completionList);
+    }
+
     [Fact]
     public async Task CompleteOnThisReturnsClassMembers() {
       var source = @"

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -85,6 +85,26 @@ await SetUp(o => {
       Assert.True(hovers.Count > 0, "No hover expression detected.");
     }
 
+    [Fact]
+    public async Task Crash() {
+      var source = @"
+module M {
+  method m()
+}
+module P refines M {
+  method m ... {
+    while true { ...; }
+  }
+}";
+
+      var document = CreateAndOpenTestDocument(source);
+      var hoverResult = await client.RequestHover(new HoverParams() {
+        Position = new Position(0, 20),
+        TextDocument = document
+      }, CancellationToken);
+      Assert.Null(hoverResult);
+    }
+
     [Fact]
     public async Task RecoverableParseErrorTypeRhs() {
       var markup = @"