There's a nod given to dependently-typed languages (where types live in the same namespace as values, so they can be passed-into and returned-from functions), but it's useful to note that in those languages this "local coherence" approach doesn't just "look like" lambda calculus, it is lambda calculus. For example, to insert a new element into a sorted list we might define a function like this:

    insert: (t: Type) -> (o: Ord t) -> t -> List t -> List t
    insert t o x xs = case xs of
      Nil _ -> Cons t x (Nil t)
      Cons _ y ys -> case lessThanOrEq t o x y of
        True -> Cons t x xs
        False -> Cons t y (insert t o x ys)

Notice that the first argument `t` is a `Type`, and the second argument `o` is an `Ord t` (where `Ord` must be a function which takes a type as argument and returns another type; presumably for a record of functions). It's literally just lambda calculus.

However, this obviously gets quite tedious; especially when there's so much repetition. For example, the third argument has type `t` and the fourth has type `List t`, so why do we need to pass around `t` itself as a separate argument; can't the computer work it out? Yes we can, and we usually do this with {braces} syntax, e.g.

    insert: {t: Type} -> {o: Ord t} -> t -> List t -> List t
    insert _ _ x xs = case xs of
      Nil _ -> Cons x Nil
      Cons _ y ys -> case lessThanOrEq x y of
        True -> Cons x xs
        False -> Cons y (insert x ys)

This is why the feature is called "implicits", since it's leaving some arguments implicit, for the compiler to fill in using information that's in context. It works quite well for types themselves, but can get a bit iffy for values (as evidenced by this blog post; and I've seen all sorts of footguns in Scala, like defining some implicit String values and hoping the right ones get picked up in the right places...)