Coercion from `List a` to `List (Option a)`?

Stream: new members

[Justus Springer]

Not really a new member, but I have a very basic question. The following code confuses me:

import Mathlib

variable (α : Type) (l : List α)

#check (l : List (Option α)) -- works, displays the following:
-- do
--   let a ← l
--   pure (some a) : List (Option α)

#synth Coe (List α) (List (Option α)) -- failed to synthesize

Somehow Lean is able to interpret l as a List (Option α), even though it can't find a Coe instance (I wouldn't have expected there to be one either). Even weirder, it displays it using do-notation.

[David Ledvinka]

Is this a MWE? In Lean 4 Web I get an error...

[David Ledvinka]

It works after import Mathlib

[Justus Springer]

You're right, it only works with Mathlib. #min_imports is giving nothing though.

[Justus Springer]

Edited the example to include Mathlib

[Eric Wieser]

I think this is using MonadLift not Coe

[David Ledvinka]

Yeah Monad List instance is in Mathlib but not in Core or Batteries

[Justus Springer]

I don't know how MonadLift works. I naively assumed that whenever you do variable (x : A) and then #check (x : B) works, there must be a coercion from A to B, which is why I got confused. In the docs about MonadLift, it says "Computations in the monad m can be run in the monad n. These translations are inserted automatically by the compiler." So I guess that automatic insertion is what's causing this, correct?

[Ruben Van de Velde]

Yeah, it is - monads are used for do notation, that's also why it's printing like that

[Eric Wieser]

I suppose you could argue that automated MonadLift insertion should not happen outside of do notation

[Kyle Miller]

@Eric Wieser It's used frequently when passing monadic values to various combinators. I suppose Lean could require do to signal intent to coerce, but that'd be a disruptive change.

[Eric Wieser]

Is it easy for you to find an example that doesn't use do?

[Kyle Miller]

You could also argue that Monad List shouldn't be an instance, to prevent this coercion insertion. It's a bit uneasy to have List represent both data and a computational context. (Option is in a similar situation, but so far it's too useful to require using a monad-specific OptionM.)

[Eric Wieser]

I guess another option (which I think I started exploring in a PR) is to have the MonadLift instance be some <$> l instead of the bind that is currently inserted

[Ruben Van de Velde]

Should core Monad be called MonadForComputation instead?

[Eric Wieser]

Or a [EnableDoNotation m] that is orthogonal to Monad, which is required by do and MonadLift auto-insertion

[Kyle Miller]

@Eric Wieser I don't have any immediately accessible examples, but monad lifting occurs frequently enough between all the metaprogramming monads that I'm sure removing monad lifting from the term coercion system would break many things.

[Eric Wieser]

I suppose the easiest way to find the examples (which is not particularly easy) is to make the change and see what breaks