Compute static hover using ast (dafny-lang#4350)

Depends on dafny-lang#4349 ### Changes - Let the statically computed part of hover information also work with project mode - Compute statically part of hover mode using the Dafny AST instead of the `LegacySymbolTable` ### Testing - Turned on project mode in `HoverTest.cs` - Let half of tests in `HoverTest.cs` use a project file <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>
Dargones · Jul 31, 2023 · 25bf208 · 25bf208
1 parent 72410e1
commit 25bf208
Show file tree

Hide file tree

Showing 104 changed files with 585 additions and 447 deletions.
diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs
@@ -191,12 +191,12 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object
     }
   }
 
-  public override IEnumerable<Node> Children => Args.Concat<Node>(
+  public override IEnumerable<INode> Children => Args.Concat<Node>(
     Prev == null
       ? Enumerable.Empty<Node>()
       : new List<Node> { Prev });
 
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
 
 public static class AttributesExtensions {

diff --git a/Source/DafnyCore/AST/Expressions/Applications/ActualBindings.cs b/Source/DafnyCore/AST/Expressions/Applications/ActualBindings.cs
@@ -39,18 +39,18 @@ public void AcceptArgumentExpressionsAsExactParameterList(List<Expression> args
     arguments = args ?? ArgumentBindings.ConvertAll(binding => binding.Actual);
   }
 
-  public override IEnumerable<Node> Children => arguments == null ? ArgumentBindings : arguments;
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => arguments == null ? ArgumentBindings : arguments;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
 
 public class ActualBinding : TokenNode {
   public readonly IToken /*?*/ FormalParameterName;
   public readonly Expression Actual;
   public readonly bool IsGhost;
 
-  public override IEnumerable<Node> Children => new List<Node> { Actual }.Where(x => x != null);
+  public override IEnumerable<INode> Children => new List<Node> { Actual }.Where(x => x != null);
 
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 
   public ActualBinding(IToken /*?*/ formalParameterName, Expression actual, bool isGhost = false) {
     Contract.Requires(actual != null);

diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs
@@ -13,9 +13,9 @@ public class ApplySuffix : SuffixExpr, ICloneable<ApplySuffix>, ICanFormat {
   public readonly ActualBindings Bindings;
   public List<Expression> Args => Bindings.Arguments;
 
-  public override IEnumerable<Node> Children => ResolvedExpression == null
+  public override IEnumerable<INode> Children => ResolvedExpression == null
     ? base.Children.Concat(Bindings == null ? new List<Node>() : Args ?? Enumerable.Empty<Node>()) : new[] { ResolvedExpression };
-  public override IEnumerable<Node> PreResolveChildren => new List<Node> { Lhs, Bindings };
+  public override IEnumerable<INode> PreResolveChildren => new List<Node> { Lhs, Bindings };
 
   [ContractInvariantMethod]
   void ObjectInvariant() {

diff --git a/Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs b/Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs
@@ -14,7 +14,7 @@ public class ExprDotName : SuffixExpr, ICloneable<ExprDotName> {
   /// Because the resolved expression only points to the final resolved declaration,
   /// but not the declaration of the Lhs, we must also include the Lhs.
   /// </summary>
-  public override IEnumerable<Node> Children => ResolvedExpression == null
+  public override IEnumerable<INode> Children => ResolvedExpression == null
     ? new[] { Lhs }
     : new[] { Lhs, ResolvedExpression };
 

diff --git a/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs b/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs
@@ -25,7 +25,7 @@ public NameSegment Clone(Cloner cloner) {
     return new NameSegment(cloner, this);
   }
 
-  public override IEnumerable<Node> PreResolveChildren => OptTypeArguments ?? new List<Type>();
+  public override IEnumerable<INode> PreResolveChildren => OptTypeArguments ?? new List<Type>();
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     formatter.SetTypeLikeIndentation(indentBefore, OwnedTokens);
     foreach (var subType in PreResolveChildren.OfType<Type>()) {

diff --git a/Source/DafnyCore/AST/Expressions/Applications/StaticReceiverExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/StaticReceiverExpr.cs
@@ -97,7 +97,7 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public override IEnumerable<Node> Children =>
+  public override IEnumerable<INode> Children =>
     new[] { ObjectToDiscard, ContainerExpression }.Where(x => x != null).Concat(Type.Nodes);
 
   public new StaticReceiverExpr Clone(Cloner cloner) {

diff --git a/Source/DafnyCore/AST/Expressions/Applications/SuffixExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/SuffixExpr.cs
@@ -49,8 +49,8 @@ public SuffixExpr(IToken tok, Expression lhs)
     Lhs = lhs;
   }
 
-  public override IEnumerable<Node> Children => ResolvedExpression == null ? new[] { Lhs } : base.Children;
-  public override IEnumerable<Node> PreResolveChildren => PreResolveSubExpressions;
+  public override IEnumerable<INode> Children => ResolvedExpression == null ? new[] { Lhs } : base.Children;
+  public override IEnumerable<INode> PreResolveChildren => PreResolveSubExpressions;
 
   public override IEnumerable<Expression> SubExpressions {
     get {

diff --git a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs
@@ -52,9 +52,9 @@ public void AddCustomizedErrorMessage(IToken tok, string s) {
     this.Attributes = new UserSuppliedAttributes(tok, openBrace, closeBrace, args, this.Attributes);
   }
 
-  public override IEnumerable<Node> Children =>
+  public override IEnumerable<INode> Children =>
     (Attributes != null ? new List<Node>() { Attributes } : Enumerable.Empty<Node>()).Concat(
       new List<Node>() { E });
 
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs
@@ -441,8 +441,11 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl
       Bounds = original.Bounds?.Select(b => b?.Clone(cloner)).ToList();
     }
   }
-  public override IEnumerable<Node> Children => (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(SubExpressions);
-  public override IEnumerable<Node> PreResolveChildren =>
+  public override IEnumerable<INode> Children =>
+    (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).
+    Concat(BoundVars).Concat(SubExpressions);
+
+  public override IEnumerable<INode> PreResolveChildren =>
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>())
     .Concat<Node>(Range != null && Range.tok.line > 0 ? new List<Node>() { Range } : new List<Node>())
     .Concat(Term != null && Term.tok.line > 0 ? new List<Node> { Term } : new List<Node>());

diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs
@@ -3,7 +3,7 @@
 
 namespace Microsoft.Dafny;
 
-public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr>, ICanFormat {
+public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr> {
   public override string WhatKind => "lambda";
 
   public Expression Body => Term;

diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs
@@ -73,7 +73,7 @@ public virtual Expression LogicalBody(bool bypassSplitQuantifier = false) {
     throw new cce.UnreachableException(); // This body is just here for the "Requires" clause
   }
 
-  public override IEnumerable<Node> PreResolveChildren => base.SubExpressions;
+  public override IEnumerable<INode> PreResolveChildren => base.SubExpressions;
   public IEnumerable<Expression> PreResolveSubExpressions => base.SubExpressions;
 
   public override IEnumerable<Expression> SubExpressions {

diff --git a/Source/DafnyCore/AST/Expressions/ConcreteSyntaxExpression.cs b/Source/DafnyCore/AST/Expressions/ConcreteSyntaxExpression.cs
@@ -31,7 +31,7 @@ public Expression ResolvedExpression {
   public ConcreteSyntaxExpression(IToken tok)
     : base(tok) {
   }
-  public override IEnumerable<Node> Children => ResolvedExpression == null ? Array.Empty<Node>() : new[] { ResolvedExpression };
+  public override IEnumerable<INode> Children => ResolvedExpression == null ? Array.Empty<Node>() : new[] { ResolvedExpression };
   public override IEnumerable<Expression> SubExpressions {
     get {
       if (ResolvedExpression != null) {
@@ -49,7 +49,7 @@ public override IEnumerable<Expression> TerminalExpressions {
   }
 
   public virtual IEnumerable<Expression> PreResolveSubExpressions => Enumerable.Empty<Expression>();
-  public override IEnumerable<Node> PreResolveChildren => PreResolveSubExpressions;
+  public override IEnumerable<INode> PreResolveChildren => PreResolveSubExpressions;
 
   public override IEnumerable<Type> ComponentTypes => ResolvedExpression.ComponentTypes;
 }
diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs
@@ -16,10 +16,10 @@ public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Att
     this.Attributes = attrs;
   }
 
-  public override IEnumerable<Node> Children =>
+  public override IEnumerable<INode> Children =>
     (Attributes != null ? new Node[] { Attributes } : Enumerable.Empty<Node>()).Concat(new Node[] { Body, Pat });
 
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 
   public void Resolve(ModuleResolver resolver,
     ResolutionContext resolutionContext,

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs
@@ -29,8 +29,8 @@ private NestedMatchCaseStmt(Cloner cloner, NestedMatchCaseStmt original) : base(
   public NestedMatchCaseStmt Clone(Cloner cloner) {
     return new NestedMatchCaseStmt(cloner, this);
   }
-  public override IEnumerable<Node> Children => new[] { Pat }.Concat<Node>(Body).Concat(Attributes?.Args ?? Enumerable.Empty<Node>());
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => new[] { Pat }.Concat<Node>(Body).Concat(Attributes?.Args ?? Enumerable.Empty<Node>());
+  public override IEnumerable<INode> PreResolveChildren => Children;
 
   public void Resolve(
     ModuleResolver resolver,

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs
@@ -50,7 +50,7 @@ public override IEnumerable<Expression> SubExpressions {
     }
   }
 
-  public override IEnumerable<Node> Children => new[] { Source }.Concat<Node>(Cases);
+  public override IEnumerable<INode> Children => new[] { Source }.Concat<Node>(Cases);
 
   public void Resolve(ModuleResolver resolver, ResolutionContext resolutionContext) {
 

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs
@@ -40,7 +40,7 @@ public NestedMatchStmt(Cloner cloner, NestedMatchStmt original) : base(cloner, o
     }
   }
 
-  public override IEnumerable<Node> Children => new[] { Source }.Concat<Node>(Cases);
+  public override IEnumerable<INode> Children => new[] { Source }.Concat<Node>(Cases);
 
   public override IEnumerable<Statement> SubStatements => Cases.SelectMany(c => c.Body);
 

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/DisjunctivePattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/DisjunctivePattern.cs
@@ -11,8 +11,8 @@ public DisjunctivePattern(IToken tok, List<ExtendedPattern> alternatives, bool i
     this.Alternatives = alternatives;
   }
 
-  public override IEnumerable<Node> Children => Alternatives;
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => Alternatives;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 
   public override IEnumerable<Expression> SubExpressions {
     get {

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs
@@ -68,8 +68,8 @@ public override string ToString() {
     }
   }
 
-  public override IEnumerable<Node> Children => Arguments ?? Enumerable.Empty<Node>();
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => Arguments ?? Enumerable.Empty<Node>();
+  public override IEnumerable<INode> PreResolveChildren => Children;
 
   public override IEnumerable<Expression> SubExpressions {
     get {

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/LitPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/LitPattern.cs
@@ -65,8 +65,8 @@ public override string ToString() {
     return Printer.ExprToString(DafnyOptions.DefaultImmutableOptions, OrigLit);
   }
 
-  public override IEnumerable<Node> Children => new[] { OrigLit };
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => new[] { OrigLit };
+  public override IEnumerable<INode> PreResolveChildren => Children;
 
   public override IEnumerable<Expression> SubExpressions {
     get {

diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs
@@ -10,7 +10,7 @@ public class DatatypeValue : Expression, IHasUsages, ICloneable<DatatypeValue>,
   public readonly ActualBindings Bindings;
   public List<Expression> Arguments => Bindings.Arguments;
 
-  public override IEnumerable<Node> Children => new Node[] { Bindings };
+  public override IEnumerable<INode> Children => new Node[] { Bindings };
 
   [FilledInDuringResolution] public DatatypeCtor Ctor;
   [FilledInDuringResolution] public List<Type> InferredTypeArgs = new List<Type>();

diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs
@@ -877,6 +877,6 @@ public string AsStringLiteral() {
     return le == null ? null : le.Value as string;
   }
 
-  public override IEnumerable<Node> Children => SubExpressions;
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => SubExpressions;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
diff --git a/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs b/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs
@@ -49,8 +49,8 @@ public FrameExpression(Cloner cloner, FrameExpression original) {
   }
 
   public IToken NameToken => tok;
-  public override IEnumerable<Node> Children => new[] { E };
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => new[] { E };
+  public override IEnumerable<INode> PreResolveChildren => Children;
   public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
     return new[] { Field }.Where(x => x != null);
   }

diff --git a/Source/DafnyCore/AST/Expressions/Specification.cs b/Source/DafnyCore/AST/Expressions/Specification.cs
@@ -24,6 +24,6 @@ public bool HasAttributes() {
     return Attributes != null;
   }
 
-  public override IEnumerable<Node> Children => Expressions;
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => Expressions;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs
@@ -22,7 +22,7 @@ public StmtExpr(Cloner cloner, StmtExpr original) : base(cloner, original) {
     S = cloner.CloneStmt(original.S);
   }
 
-  public override IEnumerable<Node> Children => new Node[] { S, E };
+  public override IEnumerable<INode> Children => new Node[] { S, E };
 
   public StmtExpr(IToken tok, Statement stmt, Expression expr)
     : base(tok) {

diff --git a/Source/DafnyCore/AST/Expressions/Types/TypeUnaryExpr.cs b/Source/DafnyCore/AST/Expressions/Types/TypeUnaryExpr.cs
@@ -19,7 +19,7 @@ protected TypeUnaryExpr(IToken tok, Expression expr, Type toType)
     ToType = toType;
   }
 
-  public override IEnumerable<Node> Children => base.Children.Concat(ToType.Nodes);
+  public override IEnumerable<INode> Children => base.Children.Concat(ToType.Nodes);
 
   public override IEnumerable<Type> ComponentTypes {
     get {

diff --git a/Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs b/Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs
@@ -102,6 +102,6 @@ public IEnumerable<VT> Vars {
     }
   }
 
-  public override IEnumerable<Node> Children => Arguments ?? Enumerable.Empty<Node>();
-  public override IEnumerable<Node> PreResolveChildren => Children;
+  public override IEnumerable<INode> Children => Var == null ? (Arguments ?? Enumerable.Empty<Node>()) : new[] { Var };
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
diff --git a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs
@@ -4,13 +4,9 @@
 
 namespace Microsoft.Dafny;
 
-public class Formal : NonglobalVariable, ISymbol {
+public class Formal : NonglobalVariable {
   public readonly bool InParam;  // true to in-parameter, false for out-parameter
-  public override bool IsMutable {
-    get {
-      return !InParam;
-    }
-  }
+  public override bool IsMutable => !InParam;
   public readonly bool IsOld;
   public readonly Expression DefaultValue;
   public readonly bool IsNameOnly;
@@ -45,11 +41,10 @@ public bool HasName {
   public override string CompileName =>
     compileName ??= SanitizeName(NameForCompilation);
 
-  public override IEnumerable<Node> Children =>
-    DefaultValue != null ? new List<Node>() { DefaultValue } : Enumerable.Empty<Node>();
+  public override IEnumerable<INode> Children =>
+    (DefaultValue != null ? new List<Node> { DefaultValue } : Enumerable.Empty<Node>()).Concat(base.Children);
 
-  public override IEnumerable<Node> PreResolveChildren => Children;
-  public DafnySymbolKind Kind => DafnySymbolKind.Variable;
+  public override IEnumerable<INode> PreResolveChildren => Children;
 }
 
 /// <summary>

diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariable.cs
@@ -3,7 +3,7 @@
 namespace Microsoft.Dafny;
 
 [ContractClass(typeof(IVariableContracts))]
-public interface IVariable : IDeclarationOrUsage {
+public interface IVariable : ISymbol {
   string Name {
     get;
   }

diff --git a/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs b/Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs
@@ -80,4 +80,8 @@ public string AssignUniqueName(FreshIdGenerator generator) {
   }
 
   public abstract IToken NameToken { get; }
+  public DafnySymbolKind Kind => throw new NotImplementedException();
+  public string GetDescription(DafnyOptions options) {
+    throw new NotImplementedException();
+  }
 }
diff --git a/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs
@@ -57,7 +57,7 @@ public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
   }
 
   public IToken NameToken => tok;
-  public override IEnumerable<Node> Children { get; } = Enumerable.Empty<Node>();
+  public override IEnumerable<INode> Children { get; } = Enumerable.Empty<Node>();
 }
 
 /// <summary>

diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs
@@ -122,7 +122,7 @@ public IEnumerable<BoundVar> BoundVars {
 
   public IEnumerable<BoundVar> AllBoundVars => BoundVars;
 
-  public override IEnumerable<Node> Children =>
+  public override IEnumerable<INode> Children =>
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>())
     .Concat(LHSs)
     .Concat(base.Children);

diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetOrFailExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetOrFailExpr.cs
@@ -31,7 +31,7 @@ public LetOrFailExpr(Cloner cloner, LetOrFailExpr original) : base(cloner, origi
     Body = cloner.CloneExpr(original.Body);
   }
 
-  public override IEnumerable<Node> Children =>
+  public override IEnumerable<INode> Children =>
     (Lhs != null ?
       new List<Node> { Lhs } : Enumerable.Empty<Node>()).Concat(base.Children);
 

diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs
@@ -122,6 +122,10 @@ public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) {
   }
 
   public IToken NameToken => tok;
-  public override IEnumerable<Node> Children => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
-  public override IEnumerable<Node> PreResolveChildren => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
+  public override IEnumerable<INode> Children => IsTypeExplicit ? new List<Node> { Type } : Enumerable.Empty<Node>();
+  public override IEnumerable<INode> PreResolveChildren => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
+  public DafnySymbolKind Kind => DafnySymbolKind.Variable;
+  public string GetDescription(DafnyOptions options) {
+    return this.AsText();
+  }
 }
diff --git a/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs
@@ -24,7 +24,7 @@ public Resolver_IdentifierExpr(Cloner cloner, Resolver_IdentifierExpr original)
     TypeArgs = original.TypeArgs;
   }
 
-  public override IEnumerable<Node> Children => TypeArgs.SelectMany(ta => ta.Nodes);
+  public override IEnumerable<INode> Children => TypeArgs.SelectMany(ta => ta.Nodes);
 
   public abstract class ResolverType : Type {
     public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl>/*?*/ visitedDatatypes) {