diff --git a/integration-tests/aqua/examples/abilitiesClosure.aqua b/integration-tests/aqua/examples/abilitiesClosure.aqua
index d5b2b165e..7b16c9b5d 100644
--- a/integration-tests/aqua/examples/abilitiesClosure.aqua
+++ b/integration-tests/aqua/examples/abilitiesClosure.aqua
@@ -7,7 +7,7 @@ ability WorkerJob:
 
 func disjoint_run{WorkerJob}() -> -> string:
   run = func () -> string:
-      r <- WorkerJob.runOnSingleWorker()
+      r <- WorkerJob.runOnSingleWorker("worker")
       <- r
   <- run
 
diff --git a/semantics/src/main/scala/aqua/semantics/rules/ValuesAlgebra.scala b/semantics/src/main/scala/aqua/semantics/rules/ValuesAlgebra.scala
index 12cbf8d4c..ca12c51a1 100644
--- a/semantics/src/main/scala/aqua/semantics/rules/ValuesAlgebra.scala
+++ b/semantics/src/main/scala/aqua/semantics/rules/ValuesAlgebra.scala
@@ -53,29 +53,38 @@ class ValuesAlgebra[S[_], Alg[_]: Monad](using
   private def resolveSingleProperty(rootType: Type, op: PropertyOp[S]): Alg[Option[PropertyRaw]] =
     op match {
       case op: IntoField[S] =>
-        T.resolveField(rootType, op)
-      case op: IntoArrow[S] =>
-        for {
-          maybeArgs <- op.arguments.traverse(valueToRaw)
-          arrowProp <- maybeArgs.sequence.flatTraverse(
-            T.resolveArrow(rootType, op, _)
+        OptionT(T.resolveIntoField(op, rootType))
+          .map(
+            _.fold(
+              field = t => IntoFieldRaw(op.value, t),
+              property = t => FunctorRaw(op.value, t)
+            )
           )
-        } yield arrowProp
+          .value
+      case op: IntoArrow[S] =>
+        (for {
+          args <- op.arguments.traverse(arg => OptionT(valueToRaw(arg)))
+          argTypes = args.map(_.`type`)
+          arrowType <- OptionT(T.resolveIntoArrow(op, rootType, argTypes))
+        } yield IntoArrowRaw(op.name.value, arrowType, args)).value
       case op: IntoCopy[S] =>
         (for {
           _ <- OptionT.liftF(
             reportNamedArgsDuplicates(op.args)
           )
-          fields <- op.args.traverse(arg => OptionT(valueToRaw(arg.argValue)).map(arg -> _))
-          prop <- OptionT(T.resolveCopy(op, rootType, fields))
-        } yield prop).value
-      case op: IntoIndex[S] =>
-        for {
-          maybeIdx <- op.idx.fold(LiteralRaw.Zero.some.pure)(valueToRaw)
-          idxProp <- maybeIdx.flatTraverse(
-            T.resolveIndex(rootType, op, _)
+          args <- op.args.traverse(arg =>
+            OptionT(valueToRaw(arg.argValue)).map(
+              arg.argName.value -> _
+            )
           )
-        } yield idxProp
+          argsTypes = args.map { case (_, raw) => raw.`type` }
+          structType <- OptionT(T.resolveIntoCopy(op, rootType, argsTypes))
+        } yield IntoCopyRaw(structType, args.toNem)).value
+      case op: IntoIndex[S] =>
+        (for {
+          idx <- OptionT(op.idx.fold(LiteralRaw.Zero.some.pure)(valueToRaw))
+          valueType <- OptionT(T.resolveIntoIndex(op, rootType, idx.`type`))
+        } yield IntoIndexRaw(idx, valueType)).value
     }
 
   def valueToRaw(v: ValueToken[S]): Alg[Option[ValueRaw]] =
diff --git a/semantics/src/main/scala/aqua/semantics/rules/types/TypesAlgebra.scala b/semantics/src/main/scala/aqua/semantics/rules/types/TypesAlgebra.scala
index b4eb4dbd8..e28a0313d 100644
--- a/semantics/src/main/scala/aqua/semantics/rules/types/TypesAlgebra.scala
+++ b/semantics/src/main/scala/aqua/semantics/rules/types/TypesAlgebra.scala
@@ -40,21 +40,74 @@ trait TypesAlgebra[S[_], Alg[_]] {
 
   def defineAlias(name: NamedTypeToken[S], target: Type): Alg[Boolean]
 
-  def resolveIndex(rootT: Type, op: IntoIndex[S], idx: ValueRaw): Alg[Option[PropertyRaw]]
+  /**
+   * Resolve `IntoIndex` property on value with `rootT` type
+   *
+   * @param op property to resolve
+   * @param rootT type of the value to which property is applied
+   * @param idxType type of the index
+   * @return type of the value at given index if property application is valid
+   */
+  def resolveIntoIndex(
+    op: IntoIndex[S],
+    rootT: Type,
+    idxType: Type
+  ): Alg[Option[DataType]]
 
-  def resolveCopy(
-    token: IntoCopy[S],
+  /**
+   * Resolve `IntoCopy` property on value with `rootT` type
+   *
+   * @param op property to resolve
+   * @param rootT type of the value to which property is applied
+   * @param types types of arguments passed
+   * @return struct type if property application is valid
+   * @note `types` should correspond to `op.args`
+   */
+  def resolveIntoCopy(
+    op: IntoCopy[S],
     rootT: Type,
-    fields: NonEmptyList[(NamedArg[S], ValueRaw)]
-  ): Alg[Option[PropertyRaw]]
+    types: NonEmptyList[Type]
+  ): Alg[Option[StructType]]
 
-  def resolveField(rootT: Type, op: IntoField[S]): Alg[Option[PropertyRaw]]
+  enum IntoFieldRes(`type`: Type) {
+    case Field(`type`: Type) extends IntoFieldRes(`type`)
+    case Property(`type`: Type) extends IntoFieldRes(`type`)
 
-  def resolveArrow(
-    rootT: Type,
+    def fold[A](field: Type => A, property: Type => A): A =
+      this match {
+        case Field(t) => field(t)
+        case Property(t) => property(t)
+      }
+  }
+
+  /**
+   * Resolve `IntoField` property on value with `rootT` type
+   *
+   * @param op property to resolve
+   * @param rootT type of the value to which property is applied
+   * @return if property application is valid, return
+   *         Field(type) if it's a field of rootT (fields of structs or abilities),
+   *         Property(type) if it's a property of rootT (functors of collections)
+   */
+  def resolveIntoField(
+    op: IntoField[S],
+    rootT: Type
+  ): Alg[Option[IntoFieldRes]]
+
+  /**
+   * Resolve `IntoArrow` property on value with `rootT` type
+   *
+   * @param op property to resolve
+   * @param rootT type of the value to which property is applied
+   * @param types types of arguments passed
+   * @return arrow type if property application is valid
+   * @note `types` should correspond to `op.arguments`
+   */
+  def resolveIntoArrow(
     op: IntoArrow[S],
-    arguments: List[ValueRaw]
-  ): Alg[Option[PropertyRaw]]
+    rootT: Type,
+    types: List[Type]
+  ): Alg[Option[ArrowType]]
 
   def ensureValuesComparable(token: Token[S], left: Type, right: Type): Alg[Boolean]
 
diff --git a/semantics/src/main/scala/aqua/semantics/rules/types/TypesInterpreter.scala b/semantics/src/main/scala/aqua/semantics/rules/types/TypesInterpreter.scala
index 24e41526b..c609821e3 100644
--- a/semantics/src/main/scala/aqua/semantics/rules/types/TypesInterpreter.scala
+++ b/semantics/src/main/scala/aqua/semantics/rules/types/TypesInterpreter.scala
@@ -1,5 +1,6 @@
 package aqua.semantics.rules.types
 
+import aqua.errors.Errors.internalError
 import aqua.parser.lexer.*
 import aqua.raw.value.*
 import aqua.semantics.Levenshtein
@@ -17,6 +18,7 @@ import cats.syntax.apply.*
 import cats.syntax.flatMap.*
 import cats.syntax.foldable.*
 import cats.syntax.functor.*
+import cats.syntax.monad.*
 import cats.syntax.option.*
 import cats.syntax.traverse.*
 import cats.{Applicative, ~>}
@@ -187,132 +189,177 @@ class TypesInterpreter[S[_], X](using
           .as(true)
     }
 
-  override def resolveField(rootT: Type, op: IntoField[S]): State[X, Option[PropertyRaw]] = {
+  override def resolveIntoField(
+    op: IntoField[S],
+    rootT: Type
+  ): State[X, Option[IntoFieldRes]] = {
     rootT match {
       case nt: NamedType =>
-        nt.fields(op.value)
-          .fold(
+        nt.fields(op.value) match {
+          case Some(t) =>
+            locations
+              .pointFieldLocation(nt.name, op.value, op)
+              .as(Some(IntoFieldRes.Field(t)))
+          case None =>
+            val fields = nt.fields.keys.map(k => s"`$k`").toList.mkString(", ")
             report
               .error(
                 op,
-                s"Field `${op.value}` not found in type `${nt.name}`, available: ${nt.fields.toNel.toList.map(_._1).mkString(", ")}"
+                s"Field `${op.value}` not found in type `${nt.name}`, available: $fields"
               )
               .as(None)
-          ) { t =>
-            locations.pointFieldLocation(nt.name, op.value, op).as(Some(IntoFieldRaw(op.value, t)))
-          }
+        }
       case t =>
         t.properties
-          .get(op.value)
-          .fold(
+          .get(op.value) match {
+          case Some(t) =>
+            State.pure(Some(IntoFieldRes.Property(t)))
+          case None =>
             report
               .error(
                 op,
-                s"Expected data type to resolve a field '${op.value}' or a type with this property. Got: $rootT"
+                s"Property `${op.value}` not found in type `$t`"
               )
               .as(None)
-          )(t => State.pure(Some(FunctorRaw(op.value, t))))
-
+        }
     }
   }
 
-  override def resolveArrow(
-    rootT: Type,
+  override def resolveIntoArrow(
     op: IntoArrow[S],
-    arguments: List[ValueRaw]
-  ): State[X, Option[PropertyRaw]] = {
+    rootT: Type,
+    types: List[Type]
+  ): State[X, Option[ArrowType]] = {
+    /* Safeguard to check condition on arguments */
+    if (op.arguments.length != types.length)
+      internalError(s"Invalid arguments, lists do not match: ${op.arguments} and $types")
+
+    val opName = op.name.value
+
     rootT match {
       case ab: GeneralAbilityType =>
-        val name = ab.name
-        val fields = ab.fields
-        lazy val fieldNames = fields.toNel.toList.map(_._1).mkString(", ")
-        fields(op.name.value)
-          .fold(
-            report
-              .error(
-                op,
-                s"Arrow `${op.name.value}` not found in type `$name`, " +
-                  s"available: $fieldNames"
-              )
-              .as(None)
-          ) {
-            case at @ ArrowType(_, _) =>
-              locations
-                .pointFieldLocation(name, op.name.value, op)
-                .as(Some(IntoArrowRaw(op.name.value, at, arguments)))
-            case _ =>
+        val abName = ab.fullName
+
+        ab.fields.lookup(opName) match {
+          case Some(at: ArrowType) =>
+            val reportNotEnoughArguments =
+              /* Report at position of arrow application */
               report
                 .error(
                   op,
-                  s"Unexpected. `${op.name.value}` must be an arrow."
+                  s"Not enough arguments for arrow `$opName` in `$abName`, " +
+                    s"expected: ${at.domain.length}, given: ${op.arguments.length}"
                 )
-                .as(None)
-          }
-      case t =>
-        t.properties
-          .get(op.name.value)
-          .fold(
-            report
-              .error(
-                op,
-                s"Expected type to resolve an arrow '${op.name.value}' or a type with this property. Got: $rootT"
+                .whenA(op.arguments.length < at.domain.length)
+            val reportTooManyArguments =
+              /* Report once at position of the first extra argument */
+              op.arguments.drop(at.domain.length).headOption.traverse_ { arg =>
+                report
+                  .error(
+                    arg,
+                    s"Too many arguments for arrow `$opName` in `$abName`, " +
+                      s"expected: ${at.domain.length}, given: ${op.arguments.length}"
+                  )
+              }
+            val checkArgumentTypes =
+              op.arguments
+                .zip(types)
+                .zip(at.domain.toList)
+                .forallM { case ((arg, argType), expectedType) =>
+                  ensureTypeMatches(arg, expectedType, argType)
+                }
+
+            locations.pointFieldLocation(abName, opName, op) *>
+              reportNotEnoughArguments *>
+              reportTooManyArguments *>
+              checkArgumentTypes.map(typesMatch =>
+                Option.when(
+                  typesMatch && at.domain.length == op.arguments.length
+                )(at)
               )
-              .as(None)
-          )(t => State.pure(Some(FunctorRaw(op.name.value, t))))
 
+          case Some(t) =>
+            report
+              .error(op, s"Field `$opName` has non arrow type `$t` in `$abName`")
+              .as(None)
+          case None =>
+            val available = ab.arrowFields.keys.map(k => s"`$k`").mkString(", ")
+            report
+              .error(op, s"Arrow `$opName` not found in `$abName`, available: $available")
+              .as(None)
+        }
+      case t =>
+        /* NOTE: Arrows are only supported on services and abilities,
+           (`.copy(...)` for structs is resolved by separate method) */
+        report
+          .error(op, s"Arrow `$opName` not found in `$t`")
+          .as(None)
     }
   }
 
-  // TODO actually it's stateless, exists there just for reporting needs
-  override def resolveCopy(
-    token: IntoCopy[S],
+  override def resolveIntoCopy(
+    op: IntoCopy[S],
     rootT: Type,
-    args: NonEmptyList[(NamedArg[S], ValueRaw)]
-  ): State[X, Option[PropertyRaw]] =
+    types: NonEmptyList[Type]
+  ): State[X, Option[StructType]] = {
+    if (op.args.length != types.length)
+      internalError(s"Invalid arguments, lists do not match: ${op.args} and $types")
+
     rootT match {
       case st: StructType =>
-        args.forallM { case (arg, value) =>
-          val fieldName = arg.argName.value
-          st.fields.lookup(fieldName) match {
-            case Some(t) =>
-              ensureTypeMatches(arg.argValue, t, value.`type`)
-            case None =>
-              report.error(arg.argName, s"No field with name '$fieldName' in $rootT").as(false)
+        op.args
+          .zip(types)
+          .forallM { case (arg, argType) =>
+            val fieldName = arg.argName.value
+            st.fields.lookup(fieldName) match {
+              case Some(fieldType) =>
+                ensureTypeMatches(arg.argValue, fieldType, argType)
+              case None =>
+                report
+                  .error(
+                    arg.argName,
+                    s"No field with name '$fieldName' in `$st`"
+                  )
+                  .as(false)
+            }
           }
-        }.map(
-          Option.when(_)(
-            IntoCopyRaw(
-              st,
-              args.map { case (arg, value) =>
-                arg.argName.value -> value
-              }.toNem
-            )
+          .map(Option.when(_)(st))
+      case t =>
+        report
+          .error(
+            op,
+            s"Non data type `$t` does not support `.copy`"
           )
-        )
-
-      case _ =>
-        report.error(token, s"Expected $rootT to be a data type").as(None)
+          .as(None)
     }
+  }
 
-  // TODO actually it's stateless, exists there just for reporting needs
-  override def resolveIndex(
-    rootT: Type,
+  override def resolveIntoIndex(
     op: IntoIndex[S],
-    idx: ValueRaw
-  ): State[X, Option[PropertyRaw]] =
-    if (!ScalarType.i64.acceptsValueOf(idx.`type`))
-      report.error(op, s"Expected numeric index, got $idx").as(None)
-    else
-      rootT match {
-        case ot: OptionType =>
-          op.idx.fold(
-            State.pure(Some(IntoIndexRaw(idx, ot.element)))
-          )(v => report.error(v, s"Options might have only one element, use ! to get it").as(None))
-        case rt: CollectionType =>
-          State.pure(Some(IntoIndexRaw(idx, rt.element)))
-        case _ =>
-          report.error(op, s"Expected $rootT to be a collection type").as(None)
-      }
+    rootT: Type,
+    idxType: Type
+  ): State[X, Option[DataType]] =
+    ensureTypeOneOf(
+      op.idx.getOrElse(op),
+      ScalarType.integer,
+      idxType
+    ) *> (rootT match {
+      case ot: OptionType =>
+        op.idx.fold(State.pure(Some(ot.element)))(v =>
+          // TODO: Is this a right place to report this error?
+          // It is not a type error, but rather a syntax error
+          report.error(v, s"Options might have only one element, use ! to get it").as(None)
+        )
+      case rt: CollectionType =>
+        State.pure(Some(rt.element))
+      case t =>
+        report
+          .error(
+            op,
+            s"Non collection type `$t` does not support indexing"
+          )
+          .as(None)
+    })
 
   override def ensureValuesComparable(
     token: Token[S],
@@ -423,7 +470,7 @@ class TypesInterpreter[S[_], X](using
   ): State[X, Boolean] = for {
     /* Check that required fields are present
        among arguments and have correct types */
-    enough <- expected.fields.toNel.traverse { case (name, typ) =>
+    enough <- expected.fields.toNel.forallM { case (name, typ) =>
       arguments.lookup(name) match {
         case Some(arg -> givenType) =>
           ensureTypeMatches(arg.argValue, typ, givenType)
@@ -435,7 +482,7 @@ class TypesInterpreter[S[_], X](using
             )
             .as(false)
       }
-    }.map(_.forall(identity))
+    }
     expectedKeys = expected.fields.keys.toNonEmptyList
     /* Report unexpected arguments */
     _ <- arguments.toNel.traverse_ { case (name, arg -> typ) =>
diff --git a/semantics/src/test/scala/aqua/semantics/ValuesAlgebraSpec.scala b/semantics/src/test/scala/aqua/semantics/ValuesAlgebraSpec.scala
index 5fce10b0d..85ce9a149 100644
--- a/semantics/src/test/scala/aqua/semantics/ValuesAlgebraSpec.scala
+++ b/semantics/src/test/scala/aqua/semantics/ValuesAlgebraSpec.scala
@@ -65,12 +65,30 @@ class ValuesAlgebraSpec extends AnyFlatSpec with Matchers with Inside {
   def stream(values: ValueToken[Id]*): CollectionToken[Id] =
     CollectionToken[Id](CollectionToken.Mode.StreamMode, values.toList)
 
+  def serviceCall(
+    srv: String,
+    method: String,
+    args: List[ValueToken[Id]] = Nil
+  ): PropertyToken[Id] =
+    PropertyToken(
+      variable(srv),
+      NonEmptyList.of(
+        IntoArrow(
+          Name[Id](method),
+          args
+        )
+      )
+    )
+
   def allPairs[A](list: List[A]): List[(A, A)] = for {
     a <- list
     b <- list
   } yield (a, b)
 
-  def genState(vars: Map[String, Type] = Map.empty) = {
+  def genState(
+    vars: Map[String, Type] = Map.empty,
+    types: Map[String, Type] = Map.empty
+  ) = {
     val init = RawContext.blank.copy(
       parts = Chain
         .fromSeq(ConstantRaw.defaultConstants())
@@ -88,6 +106,10 @@ class ValuesAlgebraSpec extends AnyFlatSpec with Matchers with Inside {
           ) :: _
         )
       )
+      .focus(_.types)
+      .modify(types.foldLeft(_) { case (st, (name, t)) =>
+        st.defineType(NamedTypeToken(name), t)
+      })
   }
 
   def valueOfType(t: Type)(
@@ -626,4 +648,72 @@ class ValuesAlgebraSpec extends AnyFlatSpec with Matchers with Inside {
       value.`type` shouldBe OptionType(BottomType)
     }
   }
+
+  it should "type check service calls" in {
+    val srvName = "TestSrv"
+    val methodName = "testMethod"
+    val methodType = ArrowType(
+      ProductType(ScalarType.i8 :: ScalarType.string :: Nil),
+      ProductType(Nil)
+    )
+
+    def test(args: List[ValueToken[Id]], vars: Map[String, Type] = Map.empty) = {
+      val state = genState(
+        vars,
+        types = Map(
+          srvName -> ServiceType(
+            srvName,
+            NonEmptyMap.of(
+              methodName -> methodType
+            )
+          )
+        )
+      )
+
+      val call = serviceCall(srvName, methodName, args)
+
+      val alg = algebra()
+      val (st, res) = alg
+        .valueToRaw(call)
+        .run(state)
+        .value
+
+      res shouldBe None
+      atLeast(1, st.errors.toList) shouldBe a[RulesViolated[Id]]
+    }
+
+    // not enough arguments
+    // TestSrv.testMethod()
+    test(List.empty)
+    // TestSrv.testMethod(42)
+    test(literal("42", LiteralType.unsigned) :: Nil)
+    // TestSrv.testMethod(var)
+    test(variable("var") :: Nil, Map("var" -> ScalarType.i8))
+
+    // wrong argument type
+    // TestSrv.testMethod([42, var])
+    test(
+      array(literal("42", LiteralType.unsigned), variable("var")) :: Nil,
+      Map("var" -> ScalarType.i8)
+    )
+    // TestSrv.testMethod(42, var)
+    test(
+      literal("42", LiteralType.unsigned) :: variable("var") :: Nil,
+      Map("var" -> ScalarType.i64)
+    )
+    // TestSrv.testMethod("test", var)
+    test(
+      literal("test", LiteralType.string) :: variable("var") :: Nil,
+      Map("var" -> ScalarType.string)
+    )
+
+    // too many arguments
+    // TestSrv.testMethod(42, "test", var)
+    test(
+      literal("42", LiteralType.unsigned) ::
+        literal("test", LiteralType.string) ::
+        variable("var") :: Nil,
+      Map("var" -> ScalarType.string)
+    )
+  }
 }
diff --git a/types/src/main/scala/aqua/types/Type.scala b/types/src/main/scala/aqua/types/Type.scala
index 1ddd8058a..25fd11994 100644
--- a/types/src/main/scala/aqua/types/Type.scala
+++ b/types/src/main/scala/aqua/types/Type.scala
@@ -370,6 +370,11 @@ sealed trait NamedType extends Type {
 
   def fields: NonEmptyMap[String, Type]
 
+  def arrowFields: Map[String, ArrowType] =
+    fields.toSortedMap.collect { case (name, at: ArrowType) =>
+      name -> at
+    }
+
   /**
    * Get all fields defined in this type and its fields of named type.
    * Paths to fields are returned **without** type name