added tests for new errors

Author: shazqadeer

Source/Concurrency/LinearDomainCollector.cs

@@ -57,7 +57,7 @@ public LinearDomain(Program program, Type permissionType)
     }
   }
 
-  class LinearDomainCollector : ReadOnlyVisitor
+  class LinearDomainCollector
   {
     private LinearTypeChecker linearTypeChecker;
     private Program program => linearTypeChecker.program;
@@ -137,8 +137,7 @@ private void CreatePermissionCollectors(Dictionary<Type, HashSet<Type>> linearTy
                 [],
                 [collectionTarget],
                 VarHelper.Formal("perm", TypeHelper.MapType(permissionType, Type.Bool), false),
-                null,
-                new QKeyValue(Token.NoToken, "inline", new List<object>(), null));
+                null);
             collectors[ctorType].Add(permissionType, collectorFunction);
             program.AddTopLevelDeclaration(collectorFunction);
           }

Source/Concurrency/LinearTypeCollector.cs

@@ -38,9 +38,24 @@ private void Collect()
       }
     }
 
+    private Type OriginalType(Type type)
+    {
+      if (type is not CtorType ctorType)
+      {
+        return type;
+      }
+      var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(ctorType.Decl);
+      var actualTypeParams = program.monomorphizer.GetTypeInstantiation(ctorType.Decl);
+      if (actualTypeParams == null)
+      {
+        return type;
+      }
+      return new CtorType(Token.NoToken, originalTypeCtorDecl, actualTypeParams.Select(t => OriginalType(t)).ToList());
+    }
+
     private void Check()
     {
-      foreach (var datatypeTypeCtorDecl in linearTypes.Keys.OfType<CtorType>().Select(ctorType => ctorType.Decl).OfType<DatatypeTypeCtorDecl>())
+      foreach (var datatypeTypeCtorDecl in program.TopLevelDeclarations.OfType<DatatypeTypeCtorDecl>())
       {
         var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
         var actualTypeParams = program.monomorphizer.GetTypeInstantiation(datatypeTypeCtorDecl);
@@ -50,15 +65,15 @@ private void Check()
           var innerType = actualTypeParams[0];
           if (linearTypes.ContainsKey(innerType))
           {
-            checkingContext.Error(originalTypeCtorDecl, "One instantiated with a linear type");
+            checkingContext.Error(originalTypeCtorDecl, $"One instantiated with a linear type: {OriginalType(innerType)}");
           }
         }
         else if (typeName == "Map")
         {
           var keyType = actualTypeParams[0];
           if (!IsOneType(keyType) && linearTypes.ContainsKey(keyType))
           {
-            checkingContext.Error(originalTypeCtorDecl, "Map instantiated with a key type that is neither One _ nor ordinary");
+            checkingContext.Error(originalTypeCtorDecl, $"Map instantiated with a key type that is neither One _ nor ordinary: {OriginalType(keyType)}");
           }
         }
       }

Test/civl/regression-tests/type-inst-errors.bpl

@@ -0,0 +1,13 @@
+// RUN: %parallel-boogie -lib:base "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype A<T> { A(x: One T) }
+
+procedure P0(a: A int) returns ({:linear} b: One (A int)) {
+    b := One(a);
+}
+
+procedure P1(a: Map (A int) int) {
+
+}
+

Test/civl/regression-tests/type-inst-errors.bpl.expect

@@ -0,0 +1,3 @@
+base.bpl(285,9): Error: One instantiated with a linear type: A int
+base.bpl(212,9): Error: Map instantiated with a key type that is neither One _ nor ordinary: A int
+2 type checking errors detected in type-inst-errors.bpl