Counterexamples As Assumptions

Source/DafnyCore/CounterExampleGeneration/DafnyModelTypeUtils.cs

@@ -1,5 +1,6 @@
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
+#nullable enable
 
 using System;
 using System.Linq;
@@ -28,7 +29,9 @@ public static Type GetNonNullable(Type type) {
     }
 
     public static Type ReplaceTypeVariables(Type type, Type with) {
-      return ReplaceType(type, t => t.Name.Contains('$'), _ => with);
+      var result = ReplaceType(type, t => t.Name.Contains('$'), _ => with);
+      FillInTypeArgs(result, with);
+      return result;
     }
 
     /// <summary>
@@ -61,6 +64,8 @@ public static Type GetInDafnyFormat(Type type) {
       // The code below converts every "__" to "_":
       newName = UnderscoreRemovalRegex.Replace(newName, "_");
       newName = ConvertTupleName(newName);
+      newName = string.Join(".", newName.Split(".")
+        .Where(part => part != "_module" && part != "_default" && part != "_System"));
       return new UserDefinedType(new Token(), newName,
         type.TypeArgs.ConvertAll(t => TransformType(t, GetInDafnyFormat)));
     }
@@ -82,15 +87,15 @@ private static Type TransformType(Type type, Func<UserDefinedType, Type> transfo
       switch (type) {
         case BasicType:
           return type;
-        case MapType mapType:
+        case MapType mapType when mapType.HasTypeArg():
           return new MapType(mapType.Finite,
             TransformType(mapType.Domain, transform),
             TransformType(mapType.Range, transform));
-        case SeqType seqType:
+        case SeqType seqType when seqType.HasTypeArg():
           return new SeqType(TransformType(seqType.Arg, transform));
-        case SetType setType:
+        case SetType setType when setType.HasTypeArg():
           return new SetType(setType.Finite, TransformType(setType.Arg, transform));
-        case MultiSetType multiSetType:
+        case MultiSetType multiSetType when multiSetType.HasTypeArg():
           return new MultiSetType(TransformType(multiSetType, transform));
         case UserDefinedType userDefinedType:
           return transform(userDefinedType);
@@ -101,5 +106,33 @@ private static Type TransformType(Type type, Func<UserDefinedType, Type> transfo
       }
       return type;
     }
+
+    /// <summary>
+    /// Whenever a collection type does not have an argument, fill it in with the provided arg type
+    /// </summary>
+    private static void FillInTypeArgs(Type type, Type arg) {
+      switch (type) {
+        case BasicType:
+          return;
+        case MapType mapType when !mapType.HasTypeArg():
+          mapType.SetTypeArgs(arg, arg);
+          return;
+        case SeqType seqType when !seqType.HasTypeArg():
+          seqType.SetTypeArg(arg);
+          return;
+        case SetType setType when !setType.HasTypeArg():
+          setType.SetTypeArg(arg);
+          return;
+        case MultiSetType multiSetType when !multiSetType.HasTypeArg():
+          multiSetType.SetTypeArg(arg);
+          return;
+        case UserDefinedType userDefinedType:
+          userDefinedType.TypeArgs.ForEach(typ => FillInTypeArgs(typ, arg));
+          return;
+        case InferredTypeProxy inferredTypeProxy:
+          FillInTypeArgs(inferredTypeProxy.T, arg);
+          return;
+      }
+    }
   }
 }