Implicit Arguments

To explain the use of implicit arguments, let's define a function that takes an argument and simply returns it, without doing anything.
Wait a second!
It seems, in the chapter Built-in Types, we already have a function just like this.
Remind the definition of the.
It takes a type and an argument of that type, then simply returns the second argument.
It already looks good, but there is one problem -- it takes two arguments.
Is it possible to take only one argument, like the original requirement?
This is where implicit can be helpful.
Now id can be applied to one argument.
First, implicit Pi type is a Type.
If we omit an implicit argument in a function application, the type checker will infer the type of the next non-implicit argument, and use this information to resolve the implicit argument, and insert it.
Suppose I am the type checker, when I see id("abc"),
  1. I infer id to be (implicit T: Type, x: T) -> T;
  2. I infer the argument "abc" to be String;
  3. Now I know T = String;
  4. I insert the implicit argument for id("abc"), to get id(implicit String, "abc").
Thus the following expressions are the same.
We can use the implicit value in function body.
An example would be a function that can return the type of its argument.
We can use multiple implicit arguments to find the car type of a Pair.
We do not support implicit argument over implicit argument.
The following is a counterexample.
counterexample
function k(
  implicit A: Type,
  implicit B: Type,
  x: A,
  y: B,
): A {
  return x
}
Nor do we support implicit argument over one normal argument.
The following is a counterexample.
counterexample
function k(
  implicit A: Type,
  Trivial,
  x: A,
): A {
  return x
}