Documentation

Lean.Meta.Coe

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

Equations
Instances For

    Expand coercions occurring in e

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

      Coerces expr to expectedType using CoeT.

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

        Coerces expr to a function type.

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

          Coerces expr to a type.

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

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

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

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

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

                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.

                1. 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
                
                
                1. 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.

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

                  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.

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