Many programming languages support implicit programming paradigm. Haskell type classes and C++ templates are the most prominent examples in that regards. Nevertheless, many useful features of implicit programming are omitted in the early stage of language design and the limitations of the initial design have been revealed. For example, in Haskell all type class instances should be declared in the global scope and those are not the first-class values. We propose a core calculus ${lambda}_{Rightarrow}$ for implicit programming. The ${lambda}_{Rightarrow}$ calculus supports all useful features of implicit programming, but it does not suffer from the limitations of the current practice. Furthermore, our calculus supports higher-order and overlapping rules. We present the syntax, operational semantics, polymorphic type system, and type soundness. We also provide a type-directed translation into System F as an efficient compilation technique.