opaque Lean.Meta.coeDeclAttr : TagAttribute

def Lean.Meta.isCoeDecl (env : Environment) (declName : Name) : Bool

Return true iff declName is one of the auxiliary definitions/projections used to implement coercions.

def Lean.Meta.expandCoe (e : Expr) : MetaM Expr

Expand coercions occurring in e

opaque Lean.Meta.autoLift : Lean.Option Bool

def Lean.Meta.coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr)

Coerces expr to expectedType using CoeT.

def Lean.Meta.coerceToFunction? (expr : Expr) : MetaM (Option Expr)

Coerces expr to a function type.

def Lean.Meta.coerceToSort? (expr : Expr) : MetaM (Option Expr)

Coerces expr to a type.

def Lean.Meta.isTypeApp? (type : Expr) : MetaM (Option (Expr × Expr))

Return some (m, α) if type can be reduced to an application of the form m α using [reducible] transparency.

def Lean.Meta.isMonadApp (type : Expr) : MetaM Bool

Return true if type is of the form m α where m is a Monad. Note that we reduce type using transparency [reducible].

def Lean.Meta.coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr)

Try coercions and monad lifts to make sure e has type expectedType.

If expectedType is of the form n β, we try monad lifts and other extensions.

Extensions for monads.

1. Try to unify n and m. If it succeeds, then we use

coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β

n must be a Monad to use this one.

2. If there is monad lift from m to n and we can unify α and β, we use

liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α

Note that n may not be a Monad in this case. This happens quite a bit in code such as

def g (x : Nat) : IO Nat := do
  IO.println x
  pure x

def f {m} [MonadLiftT IO m] : m Nat :=
  g 10

3. If there is a monad lift from m to n and a coercion from α to β, we use

liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β

Note that approach 3 does not subsume 1 because it is only applicable if there is a coercion from α to β for all values in α. This is not the case for example for pure $ x > 0 when the expected type is IO Bool. The given type is IO Prop, and we only have a coercion from decidable propositions. Approach 1 works because it constructs the coercion CoeT (m Prop) (pure $ x > 0) (m Bool) using the instance pureCoeDepProp.

Note that, approach 2 is more powerful than tryCoe. Recall that type class resolution never assigns metavariables created by other modules. Now, consider the following scenario

def g (x : Nat) : IO Nat := ...
deg h (x : Nat) : StateT Nat IO Nat := do
v ← g x;
IO.Println v;
...

Let's assume there is no other occurrence of v in h. Thus, we have that the expected of g x is StateT Nat IO ?α, and the given type is IO Nat. So, even if we add a coercion.

instance {α m n} [MonadLiftT m n] {α} : Coe (m α) (n α) := ...

It is not applicable because TC would have to assign ?α := Nat. On the other hand, TC can easily solve [MonadLiftT IO (StateT Nat IO)] since this goal does not contain any metavariables. And then, we convert g x into liftM $ g x.

def Lean.Meta.coerce? (expr expectedType : Expr) : MetaM (LOption Expr)

Coerces expr to the type expectedType. Returns .some coerced on successful coercion, .none if the expression cannot by coerced to that type, or .undef if we need more metavariable assignments.