report an error when a type annotation is too general

.unreleased/features/2102-polytypes-precision.md

@@ -1,2 +1,2 @@
 From now on, the type checker reports an error, when the inferred type
-is less specific than the type annotation, see #2109.
+is more specific than the annotated type, see #2109.

tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala

@@ -329,7 +329,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = true) exten
 
             case Some((_, unifiedType)) =>
               if (unifiedType.usedNames.size < operScheme.principalType.usedNames.size) {
-                // The number of free variables has decreased. The annotation by the user is imprecise.
+                // The number of free variables has decreased. The annotation by the user is to general.
                 val msg = s"$name's type annotation $userType is too general, inferred: $inferredType"
                 onTypeError(letEx.sourceRef, msg)
                 throw new UnwindException

tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestEtcTypeChecker.scala

@@ -905,7 +905,7 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
     // let @type: (a, b) => Bool;
     //   F(x, y) == x = y in TRUE
     //
-    // The principal type of F is (c, c) => Bool, which is more concrete than (a, b) => Bool.
+    // The principal type of F is (c, c) => Bool, which is more specific than (a, b) => Bool.
     val eq = parser("(c, c) => Bool")
     val x = mkUniqName("x")
     val y = mkUniqName("y")