fix the bug in type checking uninterpreted types

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

@@ -25,6 +25,18 @@ object ModelValueHandler {
    */
   private val matchRegex: Regex = raw"([a-zA-Z0-9_]+)_OF_([A-Z_][A-Z0-9_]*)".r
 
+  /**
+   * Is the supplied string encoding a model value.
+   *
+   * @param text
+   *   a string to test
+   * @return
+   *   true, if the string encodes a model value
+   */
+  def isModelValue(text: String): Boolean = {
+    typeAndIndex(text).isDefined
+  }
+
   /**
    * Returns the type of `s`. If `s` follows the pattern for model values, its type is `ConstT1(_)`, otherwise is is a
    * regular string.

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

@@ -3,9 +3,9 @@ package at.forsyte.apalache.tla.typecheck.etc
 import at.forsyte.apalache.io.annotations.store.{findAnnotation, AnnotationStore}
 import at.forsyte.apalache.io.annotations.{Annotation, AnnotationStr, StandardAnnotations}
 import at.forsyte.apalache.io.typecheck.parser.{DefaultType1Parser, Type1ParseError}
+import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir.values._
-import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.typecheck._
 import com.typesafe.scalalogging.LazyLogging
 
@@ -968,6 +968,12 @@ class ToEtcExpr(
             (SparseTupT1(fieldNo.toInt -> a), IntT1(), a),
         )
 
+      case ValEx(TlaStr(fieldName)) if ModelValueHandler.isModelValue(fieldName) =>
+        // fieldName encodes a constant of an uninterpreted sort
+        val a = varPool.fresh
+        val uninterpretedType = ModelValueHandler.modelValueOrString(fieldName)
+        Seq((FunT1(uninterpretedType, a), uninterpretedType, a))
+
       case ValEx(TlaStr(fieldName)) =>
         // f[s] or [f EXCEPT ![s] = ...], where s is a string literal
         val a = varPool.fresh

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

@@ -400,6 +400,17 @@ class TestToEtcExpr extends AnyFunSuite with BeforeAndAfterEach with ToEtcExprBa
     assert(gen(access).explain(List(), List()).isDefined)
   }
 
+  test("""f["1_OF_A"]""") {
+    // it should always be a function, because A is an uninterpreted type
+    val fun = Seq(parser("((A -> a), A) => a"))
+    val expected = mkUniqApp(fun, mkUniqName("f"), mkUniqConst(ConstT1("A")))
+    val access = tla.appFun(tla.name("f"), tla.str("1_OF_A"))
+    assert(expected == gen(access))
+
+    // Has custom type error message
+    assert(gen(access).explain(List(), List()).isDefined)
+  }
+
   test("DOMAIN f") {
     // DOMAIN is applied to one of the four objects: a function, a sequence, a record, or a sparse tuple
     val types = Seq(parser("(a -> b) => Set(a)"), parser("Seq(c) => Set(Int)"), parser("[] => Set(Str)"),