Show how implicit arguments can be inferred in Lean 4 meta code

MetaElab.lean

import Lean

namespace Lean

  open Meta Elab Tactic


  -- Although `α` is completely superfluous, we can use it to infer arguments.
  @[reducible] def TypedExpr (α : Expr) := Expr

  -- For `α : Expr`, introduce `a : α` as a shorthand for `a : TypedExpr α`.
  scoped instance : CoeSort Expr Type := ⟨TypedExpr⟩

  namespace TypedExpr

    -- These infer `α` from the target type.

    def mkFreshMVar {α : Expr} : MetaM α :=
      mkFreshExprMVar α

    def instantiate {α : Expr} : α → MetaM α :=
      instantiateMVars

    def synthesize {α : Expr} : MetaM α :=
      synthInstance α

    def synthesize? {α : Expr} : MetaM (Option α) :=
      synthInstance? α

    def elaborate {α : Expr} (a : Syntax) : TacticM α :=
      elabTerm a α

  end TypedExpr



  -- Can be used like `mkEq`, but figures out `u` and `α` by elaboration
  -- on the meta level, instead of at run time.
  def mkEq' {u : Level} {α : mkSort u} (a b : α) : mkSort levelZero :=
    mkApp3 (mkConst ``Eq [u]) α a b

  def mkEqRefl' {u : Level} {α : mkSort u} (a : α) : mkEq' a a :=
    mkApp2 (mkConst ``Eq.refl [u]) α a

  -- Not a particularly convincing example yet; just shows how the
  -- inference works in principle.
  example : MetaM Expr := do
    let u ← mkFreshLevelMVar
    let α : mkSort u ← TypedExpr.mkFreshMVar
    let a : α ← TypedExpr.mkFreshMVar
    mkEqRefl' a



  -- Reflect the type class `Inhabited` as a type class on the meta level.
  class _Inhabited {u : Level} (α : mkSort u) where
  (s : mkApp (mkConst ``Inhabited [u]) α)

  -- Make an instance of `_Inhabited` directly usable as an expression.
  instance {u : Level} (α : mkSort u) : Coe (_Inhabited α) Expr :=
    ⟨λ s => s.s⟩

  -- Reflect `Inhabited.default`.
  def _Inhabited.mkDefault {u : Level} (α : mkSort u) [s : _Inhabited α] : α :=
    mkApp2 (mkConst ``Inhabited.default [u]) α s


  -- An example how `mkEq'` and `_Inhabited` might be used.
  -- Note how the instance of `_Inhabited α` is automatically passed on
  -- to `_Inhabited.mkDefault` (of course), and especially how the two
  -- implicit arguments of `mkEq` are inferred automatically because
  -- `_Inhabited.mkDefault` is defined to return `α` (i.e. `TypedExpr α`).
  def example_defaultEqSelf {u : Level} (α : mkSort u) [_Inhabited α] :=
    mkEq' (_Inhabited.mkDefault α) (_Inhabited.mkDefault α)

  -- This example shows how a synthesized instance of `Inhabited` is
  -- automatically passed to `example_defaultEqSelf` by type class inference.
  example {u : Level} (α : mkSort u) : MetaM (mkSort levelZero) := do
    let s : _Inhabited α := ⟨← TypedExpr.synthesize⟩
    example_defaultEqSelf α

end Lean