fix: Unary - to resolve to base type (like “int”, not “nat”)

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -40,7 +40,9 @@ public partial class PreTypeResolver {
  } else if (expr is NegationExpression) {
  var e = (NegationExpression)expr;
  ResolveExpression(e.E, resolutionContext);
- e.PreType = e.E.PreType;
+ e.PreType = CreatePreTypeProxy("result of unary -");
+ AddSubtypeConstraint(e.PreType, e.E.PreType, e.E.tok,
+ $"type of argument to unary - ({{1}}) must agree with the result type ({{0}})");
  AddConfirmation(PreTypeConstraints.CommonConfirmationBag.NumericOrBitvector, e.E.PreType, e.E.tok, "type of unary - must be of a numeric or bitvector type (instead got {0})");
  // Note, e.ResolvedExpression will be filled in during CheckTypeInference, at which time e.PreType has been determined
 

Source/DafnyCore/Resolver/PreType/PreTypeToType.cs

@@ -174,7 +174,7 @@ class PreTypeToTypeVisitor : ASTVisitor<IASTVisitorContext> {
  }
 
  // Case: fixed pre-type type
- if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr) {
+ if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr or NegationExpression) {
  // Note, for the LiteralExpr "null", we expect to get a possibly-null type, whereas for a reference-type ThisExpr, we expect
  // to get the non-null type. The .PreType of these two distinguish between those cases, because the latter has a .PrintablePreType
  // field that gives the non-null type.