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/Grammar/Printer/Printer.Expression.cs

@@ -1198,6 +1198,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
       } else if (expr is Resolver_IdentifierExpr) {
         wr.Write("[Resolver_IdentifierExpr]");  // we can get here in the middle of a debugging session
       } else if (expr is DecreasesToExpr decreasesToExpr) {
+        wr.Write("(");
         var comma = false;
         foreach (var oldExpr in decreasesToExpr.OldExpressions) {
           if (comma) {
@@ -1219,6 +1220,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
           PrintExpression(newExpr, false);
           comma = true;
         }
+        wr.Write(")");
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -311,6 +311,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) {

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -3347,7 +3347,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.tok, wr);
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -3767,7 +3767,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.tok, wr);
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -4293,7 +4293,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.tok, wr);
+        EmitExpr(fromExpr, inLetExprBody, wr, wStmts);
       }
     }
 

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -2462,7 +2462,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

@@ -4507,9 +4507,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.Tok, wr, toType);
+            var origToType = s.Method.Original.Ins[i].Type;
+            var instantiatedToType = origToType.Subst(s.MethodSelect.TypeArgumentSubstitutionsWithParents());
+            var w = EmitCoercionIfNecessary(fromType, instantiatedToType, s.Tok, wr, origToType);
             w = EmitDowncastIfNecessary(fromType, instantiatedToType, s.Tok, w);
             EmitExpr(s.Args[i], false, w, wStmts);
             sep = ", ";
@@ -5287,7 +5287,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.tok, wr: wr, e.Function.Ins[i].Type);
+          var w = EmitCoercionIfNecessary(fromType, instantiatedToType, tok: e.tok, wr: wr, e.Function.Original.Ins[i].Type);
           w = EmitDowncastIfNecessary(fromType, instantiatedToType, e.tok, w);
           tr(e.Args[i], w, inLetExprBody, wStmts);
           sep = ", ";

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

@@ -159,12 +159,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.Tok, FreshTempVarName("_", null), null, p.IsGhost);
+          return new IdPattern(p.Tok, "_", null, p.IsGhost);
         }
         var args = p.Arguments?.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern));
         return new IdPattern(p.Tok, p.Id, p.Type, args, p.IsGhost) { ResolvedLit = p.ResolvedLit, BoundVar = p.BoundVar };
       case DisjunctivePattern p:
-        return new IdPattern(p.Tok, FreshTempVarName("_", null), null, p.IsGhost);
+        return new IdPattern(p.Tok, "_", null, p.IsGhost);
       default:
         Contract.Assert(false);
         return null;

Source/DafnyCore/DafnyMain.cs

@@ -86,10 +86,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, IToken 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, IToken tok, string msg) {
@@ -139,7 +139,7 @@ public void Warning(MessageSource source, Enum errorId, IToken tok, string forma
     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, IToken tok, string msg) {
@@ -179,21 +179,29 @@ public void Deprecated(MessageSource source, Enum errorId, IToken tok, string fo
     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));
     }
   }
 
-  public void Info(MessageSource source, IToken tok, string msg, object errorId = null) {
+  public void Info(MessageSource source, IToken tok, string format, object errorId = null) {
     Contract.Requires(tok != null);
-    Contract.Requires(msg != null);
-    Message(source, ErrorLevel.Info, errorId?.ToString(), tok, msg);
+    Contract.Requires(format != null);
+    Message(source, ErrorLevel.Info, errorId?.ToString(), tok, format);
   }
 
-  public void Info(MessageSource source, IToken tok, string msg, params object[] args) {
+  public void Info(MessageSource source, IToken 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, IToken tok, string msg) {

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -208,10 +208,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
   };
 
@@ -221,18 +221,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
   };
 
@@ -414,15 +414,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
@@ -1471,6 +1476,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.RangeToken.ToToken(),
+            "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].RangeToken.ToToken(),
+              "{: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);

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -2771,14 +2771,6 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) {
       currentClass = cl;
       foreach (MemberDecl member in cl.Members) {
         Contract.Assert(VisibleInScope(member));
-        if (member.HasUserAttribute("only", out var attribute)) {
-          reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_assumes_other.ToString(), attribute.RangeToken.ToToken(),
-            "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].RangeToken.ToToken(),
-              "{:only} on members does not support arguments");
-          }
-        }
         if (member is Field) {
           var resolutionContext = new ResolutionContext(new NoContext(currentClass.EnclosingModuleDefinition), false);
           scope.PushMarker();

Source/DafnyCore/Resolver/PreType/PreType.cs

@@ -402,6 +402,17 @@ public override PreType Substitute(Dictionary<TypeParameter, PreType> subst) {
       return new DPreType(Decl, newArguments ?? Arguments, printablePreType);
     }
 
+    public TopLevelDecl DeclWithMembersBypassInternalSynonym() {
+      if (Decl is InternalTypeSynonymDecl isyn) {
+        var udt = UserDefinedType.FromTopLevelDecl(isyn.tok, isyn);
+        if (isyn.RhsWithArgumentIgnoringScope(udt.TypeArgs) is UserDefinedType { ResolvedClass: { } decl }) {
+          return decl is NonNullTypeDecl nntd ? nntd.Class : decl;
+        }
+      }
+
+      return Decl;
+    }
+
     /// <summary>
     /// Returns the pre-type "parent<X>", where "X" is a list of type parameters that makes "parent<X>" a supertype of "this".
     /// Requires "this" to be some pre-type "C<Y>" and "parent" to be among the reflexive, transitive parent traits of "C".
@@ -426,7 +437,6 @@ public DPreType AsParentType(TopLevelDecl parent, PreTypeResolver preTypeResolve
         Contract.Assert(isyn.TypeArgs.Count == cl.TypeArgs.Count);
         for (var i = 0; i < isyn.TypeArgs.Count; i++) {
           var typeParameter = isyn.TypeArgs[i];
-          Contract.Assert(typeParameter == cl.TypeArgs[i]);
           Contract.Assert(rhsType.TypeArgs[i] is UserDefinedType { ResolvedClass: var tpDecl } && tpDecl == typeParameter);
         }