report an error when a type annotation is too general

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

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

src/tla/__rewire_finite_sets_ext_in_apalache.tla

@@ -31,7 +31,7 @@ LOCAL INSTANCE Functions
  *)
 FoldSet(__op(_, _), __base, __set) ==
     \* ApalacheFoldSet accumulates the result in the left argument,
-    \* whereas FinitSetsExt!FoldSet accumulates the result
+    \* whereas FiniteSetsExt!FoldSet accumulates the result
     \* in the right argument.
     LET __OpSwap(__x, __y) == __op(__y, __x) IN
     __ApalacheFoldSet(__OpSwap, __base, __set)
@@ -65,7 +65,7 @@ ProductSet(__set) ==
  * @type: ((a, b) => b, Set(a), b) => b;
  *)
 ReduceSet(__op(_, _), __set, __acc) == 
-   FoldSet(__op, __set, __acc)
+   FoldSet(__op, __acc, __set)
 
 (**
  * Starting from base, apply op to f(x), for all x \in S, in an arbitrary

src/tla/__rewire_sequences_ext_in_apalache.tla

@@ -326,7 +326,7 @@ FoldSeq(__op(_, _), __base, __seq) ==
  *    LET cons(x,y) == <<x,y>>
  *    IN FoldLeft(cons, 0, <<3, 1, 2>>) = << << <<0, 3>>, 1>>, 2>> 
  *
- * @type: ((b, a) => b, a, Seq(a)) => b;
+ * @type: ((b, a) => b, b, Seq(a)) => b;
  *)
 FoldLeft(__op(_, _), __base, __seq) == 
   LET __map(__x, __y) == __op(__x, __y) IN

test/tla/PolyTooGeneral.tla

@@ -0,0 +1,7 @@
+---------------------- MODULE PolyTooGeneral ------------------------------
+\* A library author did not think carefully about the types
+\* and wrote a too general type. The type checker should complain.
+\*
+\* @type: a => b;
+Id(x) == x
+===========================================================================

test/tla/cli-integration-tests.md

@@ -3283,6 +3283,16 @@ $ apalache-mc typecheck TestGetXWithRows.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### typecheck PolyTooGeneral.tla
+
+```sh
+$ apalache-mc typecheck PolyTooGeneral.tla | sed 's/[IEW]@.*//'
+...
+[PolyTooGeneral.tla:6:1-6:10]: Id's type annotation ((c) => b) is too general, inferred: ((a) => a)
+...
+EXITCODE: ERROR (120)
+```
+
 ## configuring the output manager
 
 ### output manager: set out-dir by CLI flag

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

@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.typecheck.etc
 
 import at.forsyte.apalache.tla.lir
-import at.forsyte.apalache.tla.lir.{OperT1, SetT1, TlaType1, TlaType1Scheme, TypingException, VarT1}
+import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.typecheck._
 import at.forsyte.apalache.tla.typecheck.etc.EtcTypeChecker.UnwindException
 import scalaz.unused
@@ -73,21 +73,20 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = true) exten
       case EtcTypeDecl(name: String, declaredType: TlaType1, scopedEx: EtcExpr) =>
         // An inline type annotation.
         // Just propagate the annotated name down the tree. It will be used in a let definition.
-        // All free type variables in the type are considered to be universally quantified,
+        // All free type variables in the type are considered to be universally quantified.
         val polyVars = declaredType.usedNames
         val extCtx = new TypeContext(ctx.types + (name -> TlaType1Scheme(declaredType, polyVars)))
         if (polyVars.isEmpty) {
-          // A non-generic type.
-          // For example, it can be a type of a constant, a state variable, or of a concrete operator.
-          // To register the type with the type listener, add the trivial constraint: a = declaredType.
-          // Importantly, we do not add the callback for parametric types, as their quantified variables may change
-          // in the course of type inference.
-          // This is sound, because parametric types are reported in the case of `EtcLet`.
-          // Yet, we have to report the concrete types here, as they may never appear again down the tree.
+          // For a non-polymorphic type, report it, as it may be the only place, where it is reported.
+          // This is relevant for VARIABLES and CONSTANTS.
+          // Add a trivial constraint: a = declaredType. We need it to place a callback.
           val fresh = varPool.fresh
-          val clause = EqClause(fresh, declaredType)
-            .setOnTypeFound(tt => onTypeFound(ex.sourceRef, tt))
-          solver.addConstraint(clause)
+          val watchClause =
+            EqClause(fresh, declaredType)
+              .setOnTypeFound { inferredType =>
+                onTypeFound(ex.sourceRef, inferredType)
+              }
+          solver.addConstraint(watchClause)
         }
 
         computeRec(extCtx, solver, scopedEx)
@@ -232,7 +231,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = true) exten
         solver.addConstraint(lambdaClause)
         operType
 
-      case EtcLet(name, defEx @ EtcAbs(defBody, binders @ _*), scopedEx) =>
+      case letEx @ EtcLet(name, defEx @ EtcAbs(defBody, binders @ _*), scopedEx) =>
         // Let-definitions that support polymorphism.
         // let name = lambda x \in X, y \in Y, ...: boundEx in scopedEx
         // Before analyzing the operator definition, try to partially solve the equations in the current context.
@@ -318,6 +317,26 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = true) exten
           throw new UnwindException
         }
 
+        // If the operator is annotated, compare the annotation with the inferred type.
+        // If the type annotation is more general than the inferred principal type, report an error.
+        if (ctx.types.contains(name)) {
+          val inferredType = principalDefType
+          val userType = operScheme.principalType
+          new TypeUnifier(varPool).unify(Substitution(), inferredType, userType) match {
+            case None =>
+              val msg = s"Contradiction in the type solver: $inferredType and $userType should be unifiable"
+              throw new TypingException(msg, letEx.sourceRef.tlaId)
+
+            case Some((_, unifiedType)) =>
+              if (unifiedType.usedNames.size < operScheme.principalType.usedNames.size) {
+                // 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
+              }
+          }
+        }
+
         // report the type of the definition
         onTypeFound(defEx.sourceRef, principalDefType)
 

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

@@ -1,14 +1,14 @@
 package at.forsyte.apalache.tla.typecheck.etc
 
-import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, OperT1, SeqT1, SetT1, StrT1, TlaType1, TlaType1Scheme, TupT1, VarT1}
-import at.forsyte.apalache.tla.typecheck._
 import at.forsyte.apalache.io.typecheck.parser.{DefaultType1Parser, Type1Parser}
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.typecheck._
 import org.easymock.EasyMock
 import org.junit.runner.RunWith
-import org.scalatestplus.easymock.EasyMockSugar
-import org.scalatestplus.junit.JUnitRunner
 import org.scalatest.BeforeAndAfterEach
 import org.scalatest.funsuite.AnyFunSuite
+import org.scalatestplus.easymock.EasyMockSugar
+import org.scalatestplus.junit.JUnitRunner
 
 @RunWith(classOf[JUnitRunner])
 class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAfterEach with EtcBuilder {
@@ -521,7 +521,7 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
 
   test("annotated polymorphic let-definition") {
     // The names of type variables may change during type inference
-    // @type: a => b;
+    // @type: a => a;
     // let F == lambda x \in Set(a): ((c, c) => c) x d in F(Int)
     val xDomain = mkUniqConst(parser("Set(c)"))
     val xNameInApp = mkUniqName("x")
@@ -552,8 +552,8 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
       listener.onTypeFound(fName.sourceRef.asInstanceOf[ExactRef], parser("Int => Int"))
     }
     whenExecuting(listener) {
-      // add the type annotation F: \A a: a => b
-      val context = TypeContext("F" -> TlaType1Scheme(parser("a => b"), Set(0, 1)))
+      // add the type annotation F: \A a: a => a
+      val context = TypeContext("F" -> TlaType1Scheme(parser("a => a"), Set(0, 1)))
       val computed = checker.compute(listener, context, letIn)
       assert(computed.contains(parser("Int")))
     }
@@ -565,7 +565,7 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
     // The bug appeared only in the case when using two instances of the constraint solver, so it needed a complex setup.
     //
     // let G ==
-    //   @type: a => b;
+    //   @type: a => a;
     //   let F == lambda x \in Set(a): ((c, c) => c) x d
     //   in F(Int)
     // in
@@ -580,7 +580,8 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
     val fName = mkUniqName("F")
     val fApp = mkUniqAppByName(fName, fArg)
     val letInF = mkUniqLet("F", fBody, fApp)
-    val annotatedLetInF = mkUniqTypeDecl("F", parser("a => b"), letInF)
+    // add the type annotation F: \A a: a => a
+    val annotatedLetInF = mkUniqTypeDecl("F", parser("a => a"), letInF)
     val bool = mkUniqConst(BoolT1)
     val gAbs = mkUniqAbs(annotatedLetInF) // we have to wrap the parameterless body of G with a lambda expression
     val letInG = mkUniqLet("G", gAbs, bool)
@@ -609,7 +610,6 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
       listener.onTypeFound(letInG.sourceRef.asInstanceOf[ExactRef], parser("Bool"))
     }
     whenExecuting(listener) {
-      // add the type annotation F: \A a, b: a => b
       val context = TypeContext.empty
       val computed = checker.compute(listener, context, letInG)
       assert(computed.contains(parser("Bool")))
@@ -899,6 +899,43 @@ class TestEtcTypeChecker extends AnyFunSuite with EasyMockSugar with BeforeAndAf
     }
   }
 
+  test("imprecise annotation") {
+    // Test case for: /~https://github.com/informalsystems/apalache/issues/2102
+
+    // let @type: (a, b) => Bool;
+    //   LET F(x, y) == x = y in TRUE
+    //
+    // 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")
+    val fBody = mkUniqApp(Seq(eq), x, y)
+    // introduce a lambda over the parameters x and y, whose domains are captured with type variables f and g
+    val domX = mkUniqConst(VarT1("f"))
+    val domY = mkUniqConst(VarT1("g"))
+    val lambda = mkUniqAbs(fBody, (x, domX), (y, domY))
+    val underLet = mkUniqConst(BoolT1)
+    val letIn = mkUniqLet("F", lambda, underLet)
+    val annotatedLetInF = mkUniqTypeDecl("F", parser("(a, b) => Bool"), letIn)
+    val bool = mkUniqConst(BoolT1)
+    val gAbs = mkUniqAbs(annotatedLetInF) // we have to wrap the parameterless body of G with a lambda expression
+    val letInG = mkUniqLet("G", gAbs, bool)
+
+    val listener = mock[TypeCheckerListener]
+    expecting {
+      listener.onTypeError(letIn.sourceRef.asInstanceOf[ExactRef],
+          "F's type annotation ((a, b) => Bool) is too general, inferred: ((a, a) => Bool)")
+      // consume all found types
+      for (ex <- Seq(fBody, domX, domY, x, y, lambda, underLet, letIn, annotatedLetInF, bool, gAbs, letInG)) {
+        listener.onTypeFound(EasyMock.eq(ex.sourceRef.asInstanceOf[ExactRef]), EasyMock.anyObject[TlaType1]).anyTimes()
+      }
+    }
+    whenExecuting(listener) {
+      // Notice that the annotation is imprecise! The type checker should complain.
+      checker.compute(listener, TypeContext(), letInG)
+    }
+  }
+
   test("regression for principal types (issue #1259)") {
     val fooType = parser("(a -> b) => Bool")
     // \* @type: (a -> b) => Bool;