一句话：提出句法隐式参数与静态重载两个正交机制，以简单实现覆盖隐式参数的常见用法。
隐式参数提供了一种强大的基于项的推理机制，使“显然”的实参可被省略并由类型检查器推断，从而减轻程序员负担并提高表达清晰度。Haskell/Lean 的类型类、Scala 的 implicit 等系统虽实用，但日益复杂且实现成本高。本文重新审视该设计空间，提出两个正交且各自范围有限、实现直接的特征：句法隐式参数与静态重载。两者结合后表达力出乎意料地强，可覆盖实践中隐式参数的许多常见场景。作者形式化了该系统并给出多种示例，证明 elaboration 具有一致性，同时给出推理算法并证明其可靠且完备。系统已在 Koka 语言中完整实现，论文还报告了大规模使用经验并讨论了进一步扩展。
Implicits provide a powerful mechanism for term-based inference, where "obvious" arguments can be omitted and inferred by the type checker. This can greatly reduce the programmer's burden and improve the clarity of expression. As such, many languages support a form of implicits in practice, such as type classes in Haskell or Lean, or implicits in Scala. Unfortunately, many of these systems have become increasingly complex and often require significant implementation effort. In this paper we take a fresh look at the design space with an arguably simpler approach based on two orthogonal features: _syntactic implicit parameters_ and _static overloading_. Each of these features is limited in scope and has a straightforward implementation. Taken together though, they are surprisingly expressive and we believe they can cover many of the common usage scenarios of implicits in practice. We formalize our system and provide various examples, and prove our elaboration is coherent. We also give an inference algorithm and show it is sound and complete. Our system is fully implemented in the Koka language, and we describe our experience with these features at scale, and discuss further extensions.