opaque Lean.Meta.coeDeclAttr : Lean.TagAttribute

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

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

Equations

• Lean.Meta.isCoeDecl env declName = Lean.Meta.coeDeclAttr.hasTag env declName

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

Expand coercions occurring in e

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.autoLift : Lean.Option Bool

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

Coerces expr to expectedType using CoeT.

Equations

• One or more equations did not get rendered due to their size.

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

Coerces expr to a function type.

Equations

• One or more equations did not get rendered due to their size.

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

Coerces expr to a type.

Equations

• One or more equations did not get rendered due to their size.

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

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

def Lean.Meta.isMonadApp (type : Lean.Expr) : Lean.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 : Lean.Expr) : Lean.MetaM (Option Lean.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 : Lean.Expr) : Lean.MetaM (Lean.LOption Lean.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.