Use refresh resolver by default

Source/DafnyCore/AST/Cloner.cs

@@ -260,6 +260,9 @@ public virtual Type CloneType(Type t) {
       } else if (t is TypeRefinementWrapper typeRefinementWrapper) {
         // don't bother keeping TypeRefinementWrapper wrappers
         return CloneType(typeRefinementWrapper.T);
+      } else if (t is BottomTypePlaceholder bottomTypePlaceholder) {
+        // don't bother keeping BottomTypePlaceholder wrappers
+        return CloneType(bottomTypePlaceholder.T);
       } else {
         Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
         return null; // to please compiler

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -315,6 +315,14 @@ public static IEnumerable<Field> AllFields(IEnumerable<TopLevelDecl> declaration
     }
   }
 
+  public static IEnumerable<MemberDecl> AllMembers(IEnumerable<TopLevelDecl> declarations) {
+    foreach (var decl in declarations.OfType<TopLevelDeclWithMembers>()) {
+      foreach (var member in decl.Members) {
+        yield return member;
+      }
+    }
+  }
+
   public static IEnumerable<TopLevelDeclWithMembers> AllTypesWithMembers(List<TopLevelDecl> declarations) {
     foreach (var d in declarations) {
       if (d is TopLevelDeclWithMembers cl) {
@@ -905,7 +913,9 @@ public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useIm
               }
             }
 
-            ctor.Destructors.Add(dtor);
+            if (!localDuplicate) {
+              ctor.Destructors.Add(dtor);
+            }
           }
 
           foreach (var duplicate in duplicates) {

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -72,6 +72,7 @@ public byte[] MyHash {
   public readonly ISet<int> Bitwidths = new HashSet<int>();
   [FilledInDuringResolution] public SpecialField ORDINAL_Offset;  // used by the translator
 
+  public readonly TypeSynonymDecl StringDecl;
   public readonly SubsetTypeDecl NatDecl;
   public UserDefinedType Nat() { return new UserDefinedType(Token.NoToken, "nat", NatDecl, new List<Type>()); }
   public readonly TraitDecl ObjectDecl;
@@ -92,10 +93,10 @@ public SystemModuleManager(DafnyOptions options) {
     this.Options = options;
     SystemModule.Height = -1;  // the system module doesn't get a height assigned later, so we set it here to something below everything else
     // create type synonym 'string'
-    var str = new TypeSynonymDecl(SourceOrigin.NoToken, new Name("string"),
+    StringDecl = new TypeSynonymDecl(SourceOrigin.NoToken, new Name("string"),
       new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false),
       new List<TypeParameter>(), SystemModule, new SeqType(new CharType()), null);
-    SystemModule.SourceDecls.Add(str);
+    SystemModule.SourceDecls.Add(StringDecl);
     // create subset type 'nat'
     var bvNat = new BoundVar(Token.NoToken, "x", Type.Int);
     var natConstraint = Expression.CreateAtMost(Expression.CreateIntLiteral(Token.NoToken, 0), Expression.CreateIdentExpr(bvNat));

Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

@@ -16,6 +16,10 @@ void ObjectInvariant() {
   public IOrigin BodyStartTok = Token.NoToken;
   public Name NameNode;
 
+  public string GetNameRelativeToModule() {
+    return this is ICallable iCallable ? iCallable.NameRelativeToModule : ToString();
+  }
+
   public virtual IOrigin NavigationToken => NameNode.Origin;
 
   public string Name => NameNode.Value;
@@ -150,4 +154,4 @@ public override string ToString() {
 
   // For Compilation
   internal CodeGenIdGenerator CodeGenIdGenerator = new();
-}
+}

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -3366,7 +3366,8 @@ protected override void EmitConversionExpr(Expression fromExpr, Type fromType, T
       } else if (fromType.Equals(toType) || fromType.AsNewtype != null || toType.AsNewtype != null) {
         wr.Append(Expr(fromExpr, inLetExprBody, wStmts));
       } else {
-        Contract.Assert(false, $"not implemented for C#: {fromType} -> {toType}");
+        wr = EmitDowncast(fromType, toType, fromExpr.Origin, wr);
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -3794,7 +3794,8 @@ protected override void EmitConversionExpr(Expression fromExpr, Type fromType, T
       } else if (fromType.Equals(toType) || fromType.AsNewtype != null || toType.AsNewtype != null) {
         wr.Append(Expr(fromExpr, inLetExprBody, wStmts));
       } else {
-        Contract.Assert(false, $"not implemented for go: {fromType} -> {toType}");
+        wr = EmitCoercionIfNecessary(fromType, toType, fromExpr.Origin, wr);
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -4249,7 +4249,8 @@ protected override void EmitConversionExpr(Expression fromExpr, Type fromType, T
       } else if (fromType.Equals(toType) || fromType.AsNewtype != null || toType.AsNewtype != null) {
         wr.Append(Expr(fromExpr, inLetExprBody, wStmts));
       } else {
-        Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}");
+        wr = EmitDowncast(fromType, toType, fromExpr.Origin, wr);
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -2464,7 +2464,7 @@ protected override void EmitConversionExpr(Expression fromExpr, Type fromType, T
       } else if (fromType.Equals(toType) || fromType.AsNewtype != null || toType.AsNewtype != null) {
         wr.Append(Expr(fromExpr, inLetExprBody, wStmts));
       } else {
-        Contract.Assert(false, $"not implemented for javascript: {fromType} -> {toType}");
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -4547,9 +4547,9 @@ protected virtual void TrCallStmt(CallStmt s, string receiverReplacement, Concre
           if (!p.IsGhost) {
             wr.Write(sep);
             var fromType = s.Args[i].Type;
-            var toType = s.Method.Ins[i].Type;
-            var instantiatedToType = toType.Subst(s.MethodSelect.TypeArgumentSubstitutionsWithParents());
-            var w = EmitCoercionIfNecessary(fromType, instantiatedToType, s.Origin, wr, toType);
+            var origToType = s.Method.Original.Ins[i].Type;
+            var instantiatedToType = origToType.Subst(s.MethodSelect.TypeArgumentSubstitutionsWithParents());
+            var w = EmitCoercionIfNecessary(fromType, instantiatedToType, s.Origin, wr, origToType);
             w = EmitDowncastIfNecessary(fromType, instantiatedToType, s.Origin, w);
             EmitExpr(s.Args[i], false, w, wStmts);
             sep = ", ";
@@ -5325,7 +5325,7 @@ protected virtual void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSynta
           wr.Write(sep);
           var fromType = e.Args[i].Type;
           var instantiatedToType = e.Function.Ins[i].Type.Subst(e.TypeArgumentSubstitutionsWithParents());
-          var w = EmitCoercionIfNecessary(fromType, instantiatedToType, tok: e.Origin, wr: wr, e.Function.Ins[i].Type);
+          var w = EmitCoercionIfNecessary(fromType, instantiatedToType, tok: e.Origin, wr: wr, e.Function.Original.Ins[i].Type);
           w = EmitDowncastIfNecessary(fromType, instantiatedToType, e.Origin, w);
           tr(e.Args[i], w, inLetExprBody, wStmts);
           sep = ", ";

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

@@ -160,12 +160,12 @@ private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDis
         return pat;
       case IdPattern p:
         if (inDisjunctivePattern && p.ResolvedLit == null && p.Arguments == null && !p.IsWildcardPattern) {
-          return new IdPattern(p.Origin, FreshTempVarName("_", null), null, p.IsGhost);
+          return new IdPattern(p.Origin, "_", null, p.IsGhost);
         }
         var args = p.Arguments?.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern));
         return new IdPattern(p.Origin, p.Id, p.Type, args, p.IsGhost) { ResolvedLit = p.ResolvedLit, BoundVar = p.BoundVar };
       case DisjunctivePattern p:
-        return new IdPattern(p.Origin, FreshTempVarName("_", null), null, p.IsGhost);
+        return new IdPattern(p.Origin, "_", null, p.IsGhost);
       default:
         Contract.Assert(false);
         return null;

Source/DafnyCore/DafnyMain.cs

@@ -87,10 +87,6 @@ public static string Resolve(Program program) {
         return null;
       }
 
-      if (program.Options.Get(CommonOptionBag.GeneralNewtypes) && !program.Options.Get(CommonOptionBag.TypeSystemRefresh)) {
-        return "use of --general-newtypes requires --type-system-refresh";
-      }
-
       var programResolver = new ProgramResolver(program);
 #pragma warning disable VSTHRD002
       LargeStackFactory.StartNew(() => programResolver.Resolve(CancellationToken.None)).Wait();

Source/DafnyCore/Generic/ErrorReporter.cs

@@ -70,7 +70,7 @@ public void Error(MessageSource source, Enum errorId, IOrigin tok, string format
     Contract.Requires(tok != null);
     Contract.Requires(format != null);
     Contract.Requires(args != null);
-    Error(source, errorId.ToString(), tok, string.Format(format, args));
+    Error(source, errorId.ToString(), tok, Format(format, args));
   }
 
   public void Error(MessageSource source, Enum errorId, IOrigin tok, string msg) {
@@ -139,7 +139,7 @@ public void Warning(MessageSource source, Enum errorId, IOrigin tok, string form
     Contract.Requires(tok != null);
     Contract.Requires(format != null);
     Contract.Requires(args != null);
-    Warning(source, errorId, tok, String.Format(format, args));
+    Warning(source, errorId, tok, Format(format, args));
   }
 
   public void Warning(MessageSource source, Enum errorId, IOrigin tok, string msg) {
@@ -179,7 +179,7 @@ public void Deprecated(MessageSource source, Enum errorId, IOrigin tok, string f
     Contract.Requires(format != null);
     Contract.Requires(args != null);
     if (Options.DeprecationNoise != 0) {
-      Warning(source, errorId, tok, String.Format(format, args));
+      Warning(source, errorId, tok, Format(format, args));
     }
   }
 
@@ -189,14 +189,22 @@ public void Info(MessageSource source, IOrigin tok, string msg, object errorId =
     Message(source, ErrorLevel.Info, errorId?.ToString(), tok, msg);
   }
 
-  public void Info(MessageSource source, IOrigin tok, string msg, params object[] args) {
+  public void Info(MessageSource source, IOrigin tok, string format, params object[] args) {
     Contract.Requires(tok != null);
-    Contract.Requires(msg != null);
+    Contract.Requires(format != null);
     Contract.Requires(args != null);
-    Info(source, tok, String.Format(msg, args));
+    Info(source, tok, Format(format, args));
+  }
+
+  private string Format(string format, object[] args) {
+    // In some cases, the "format" isn't actually a (Dafny-generated) format string, but a (user-defined) literal string.
+    // Such a user-defined literal may contain format information, like the "{0}" in the "ensures x in {0} <==> x in {1}".
+    // To prevent such string from going to string.Format, we first check if "args" has any arguments at all.
+    // This solves all known issues.
+    return args.Length == 0 ? format : string.Format(format, args);
   }
 
   public string ErrorToString(ErrorLevel header, IOrigin tok, string msg) {
     return $"{tok.TokenToString(Options)}: {header.ToString()}: {msg}";
   }
-}
+}

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -210,10 +210,10 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
     "Prevents a warning from being generated for axioms, such as assume statements and functions or methods without a body, that don't have an {:axiom} attribute.") {
   };
 
-  public static readonly Option<bool> TypeSystemRefresh = new("--type-system-refresh", () => false,
+  public static readonly Option<bool> TypeSystemRefresh = new("--type-system-refresh", () => true,
     @"
 false - The type-inference engine and supported types are those of Dafny 4.0.
-true - Use an updated type-inference engine.".TrimStart()) {
+true (default) - Use an updated type-inference engine.".TrimStart()) {
     IsHidden = true
   };
 
@@ -223,18 +223,18 @@ public enum GeneralTraitsOptions {
     Full
   }
 
-  public static readonly Option<GeneralTraitsOptions> GeneralTraits = new("--general-traits", () => GeneralTraitsOptions.Legacy,
+  public static readonly Option<GeneralTraitsOptions> GeneralTraits = new("--general-traits", () => GeneralTraitsOptions.Datatype,
     @"
 legacy - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits.
-datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
+datatype (default) - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
 full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.".TrimStart()) {
     IsHidden = true
   };
 
-  public static readonly Option<bool> GeneralNewtypes = new("--general-newtypes", () => false,
+  public static readonly Option<bool> GeneralNewtypes = new("--general-newtypes", () => true,
     @"
 false - A newtype can only be based on numeric types or another newtype.
-true - (requires --type-system-refresh) A newtype case be based on any non-reference, non-trait, non-arrow, non-ORDINAL type.".TrimStart()) {
+true (default) - (requires --type-system-refresh) A newtype case be based on any non-reference, non-trait, non-arrow, non-ORDINAL type.".TrimStart()) {
     IsHidden = true
   };
 
@@ -434,15 +434,16 @@ datatype with a single non-ghost constructor that has a single
 0 - The char type represents any UTF-16 code unit.
 1 (default) - The char type represents any Unicode scalar value.".TrimStart(), defaultValue: true);
     DafnyOptions.RegisterLegacyUi(TypeSystemRefresh, DafnyOptions.ParseBoolean, "Language feature selection", "typeSystemRefresh", @"
-0 (default) - The type-inference engine and supported types are those of Dafny 4.0.
-1 - Use an updated type-inference engine. Warning: This mode is under construction and probably won't work at this time.".TrimStart(), defaultValue: false);
+0 - The type-inference engine and supported types are those of Dafny 4.0.
+1 (default) - Use an updated type-inference engine.".TrimStart(), defaultValue: true);
     DafnyOptions.RegisterLegacyUi(GeneralTraits, DafnyOptions.ParseGeneralTraitsOption, "Language feature selection", "generalTraits", @"
-legacy (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits.
-datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
-full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.".TrimStart());
+legacy - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits.
+datatype (default) - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
+full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.".TrimStart(),
+      defaultValue: GeneralTraitsOptions.Datatype);
     DafnyOptions.RegisterLegacyUi(GeneralNewtypes, DafnyOptions.ParseBoolean, "Language feature selection", "generalNewtypes", @"
-0 (default) - A newtype can only be based on numeric types or another newtype.
-1 - (requires /typeSystemRefresh:1) A newtype case be based on any non-reference, non-trait, non-arrow, non-ORDINAL type.".TrimStart(), false);
+0 - A newtype can only be based on numeric types or another newtype.
+1 (default) - (requires /typeSystemRefresh:1) A newtype case be based on any non-reference, non-trait, non-arrow, non-ORDINAL type.".TrimStart(), true);
     DafnyOptions.RegisterLegacyUi(TypeInferenceDebug, DafnyOptions.ParseBoolean, "Language feature selection", "titrace", @"
 0 (default) - Don't print type-inference debug information.
 1 - Print type-inference debug information.".TrimStart(), defaultValue: false);

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1127,6 +1127,11 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
 
       int prevErrorCount = reporter.Count(ErrorLevel.Error);
 
+      if (Options.Get(CommonOptionBag.GeneralNewtypes) && !Options.Get(CommonOptionBag.TypeSystemRefresh)) {
+        reporter.Error(MessageSource.Resolver, Token.NoToken, "use of --general-newtypes requires --type-system-refresh");
+        return;
+      }
+
       // ---------------------------------- Pass 0 ----------------------------------
       // This pass:
       // * resolves names, introduces (and may solve) type constraints
@@ -1477,6 +1482,17 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
         }
       }
 
+      foreach (var member in ModuleDefinition.AllMembers(declarations)) {
+        if (member.HasUserAttribute("only", out var attribute)) {
+          reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_assumes_other.ToString(), attribute.Origin,
+            "Members with {:only} temporarily disable the verification of other members in the entire file");
+          if (attribute.Args.Count >= 1) {
+            reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_has_no_before_after.ToString(), attribute.Args[0].Origin,
+              "{:only} on members does not support arguments");
+          }
+        }
+      }
+
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // Check that class constructors are called when required.
         new ObjectConstructorChecker(reporter).VisitDeclarations(declarations);
@@ -2159,7 +2175,7 @@ public void RegisterInheritedMembers(TopLevelDeclWithMembers cl, [CanBeNull] DPr
       if (cl is NewtypeDecl newtypeDecl) {
         if (Options.Get(CommonOptionBag.TypeSystemRefresh)) {
           baseTypeDecl = basePreType?.Decl as TopLevelDeclWithMembers;
-          baseTypeArguments = basePreType?.Arguments.ConvertAll(preType => PreType2TypeUtil.PreType2Type(preType, false, TypeParameter.TPVariance.Co));
+          baseTypeArguments = basePreType?.Arguments.ConvertAll(preType => PreType2TypeUtil.PreType2Type(preType, false));
         } else {
           // ignore any subset types, since they have no members and thus we don't need their type-parameter mappings
           var baseType = newtypeDecl.BaseType.NormalizeExpand();

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -5151,7 +5151,7 @@ private Expression DesugarDatatypeUpdate(IOrigin tok, Expression root, DatatypeD
       if (candidateResultCtors.Count == 0) {
         return root;
       }
-      Expression rewrite = null;
+
       // Create a unique name for d', the variable we introduce in the let expression
       var dName = FreshTempVarName("dt_update_tmp#", resolutionContext.CodeContext);
       var dVar = new BoundVar(new AutoGeneratedOrigin(tok), dName, root.Type);
@@ -5160,7 +5160,6 @@ private Expression DesugarDatatypeUpdate(IOrigin tok, Expression root, DatatypeD
       candidateResultCtors.Reverse();
       foreach (var crc in candidateResultCtors) {
         // Build the arguments to the datatype constructor, using the updated value in the appropriate slot
-        var ctorArguments = new List<Expression>();
         var actualBindings = new List<ActualBinding>();
         foreach (var f in crc.Formals) {
           Expression ctorArg;
@@ -5169,7 +5168,6 @@ private Expression DesugarDatatypeUpdate(IOrigin tok, Expression root, DatatypeD
           } else {
             ctorArg = new ExprDotName(tok, d, f.NameNode, null);
           }
-          ctorArguments.Add(ctorArg);
           var bindingName = new Token(tok.line, tok.col) {
             Uri = tok.Uri,
             val = f.Name
@@ -5191,7 +5189,7 @@ private Expression DesugarDatatypeUpdate(IOrigin tok, Expression root, DatatypeD
       Contract.Assert(body != null); // because there was at least one element in candidateResultCtors
 
       // Wrap the let's around body
-      rewrite = body;
+      var rewrite = body;
       foreach (var entry in rhsBindings) {
         if (entry.Value.Item1 != null) {
           var lhs = new CasePattern<BoundVar>(tok, entry.Value.Item1);