missing MonadLift IO CommandElabM

Stream: lean4

[Tomas Skrivan]

Why is there no instance for MonadLift IO CommandElabM? There is an instance for its transitive closure MonadLiftT IO CommandElabM.

I want to write a function that recursively visits all files in the specified path and the lack of the above instance gives me trouble using the function visitFiles. To circumvent that I have to convert an instance of MonadLiftT to an instance MonadLift.

mwe:

import Lean
open Lean Elab Command System

partial def visitFiles {m} [Monad m] [MonadLift IO m] (fp : FilePath) (f : FilePath → m Unit) :
    m Unit := do
  if ← fp.isDir then
    for dirEntry in ← fp.readDir do
      visitFiles dirEntry.path f
  else
    f fp

partial def visitFilesT {m} [Monad m] [inst : MonadLiftT IO m] (fp : FilePath) (f : FilePath → m Unit) :
    m Unit := do
  have _ : MonadLift IO m := ⟨inst.monadLift⟩
  if ← fp.isDir then
    for dirEntry in ← fp.readDir do
      visitFiles dirEntry.path f
  else
    f fp


def command : CommandElabM Unit := do
  let dir ← IO.currentDir
  -- visitFiles dir (λ p => IO.println p) -- failed to synthesize instance MonadLift IO CommandElabM
  visitFilesT dir (λ p => IO.println p)

#eval command

[Jannis Limperg]

This works:

import Lean
open Lean Elab Command System

#check inferInstanceAs $ MonadLift BaseIO IO

partial def visitFiles {m} [Monad m] [MonadLiftT IO m] (fp : FilePath) (f : FilePath → m Unit) :
    m Unit := do
  have : MonadLiftT BaseIO m := ⟨λ x => liftM (liftM (m := BaseIO) (n := IO) x)⟩
  if ← liftM fp.isDir then
    for dirEntry in ← fp.readDir do
      visitFiles dirEntry.path f
  else
    f fp

#eval show CommandElabM _ from do
  let dir ← IO.currentDir
  visitFiles dir (λ p => IO.println p)

In general:

• MonadLift does one step of monad lifting, so e.g. we have MonadLift m (ReaderT α m) but not MonadLift m (ReaderT α (ReaderT β m))).
• MonadLiftT is the multi-step version (transitive closure) of MonadLift, so we have both MonadLiftT m (ReaderT α m) andMonadLiftT m (ReaderT α (ReaderT β m))).

The strange thing with this example is that Lean does not infer MonadLiftT BaseIO m from MonadLift BaseIO IO and MonadLiftT IO m. This seems to be a limitation of the way the MonadLiftT instances are constructed: Lean can infer MonadLiftT m o from MonadLiftT m n and MonadLift n o (extending the chain on the right), but not from MonadLift m n and MonadLiftT n o (extending the chain on the left). Not sure if anything can be done about this.

[Tomas Skrivan]

Nice observations, just one step lifting with MonadLift makes sense.

Also the transitivity seems to behave the same as with coercion. CoeTC A B and Coe B C implies CoeTC A C but Coe A B and CoeTC B C does not imply CoeTC A C.

But as a solution I like my approach have _ : MonadLift IO m := ⟨inst.monadLift⟩ more as it is simpler and there is no need for liftM in ← fp.isDir.

[Gabriel Ebner]

As a general rule, always accept MonadLiftT and provide MonadLift. My suggested solution:

import Lean
open Lean Elab Command System

partial def visitFiles [Monad m] [MonadLiftT IO m] (fp : FilePath) (f : FilePath → m Unit) :
    m Unit := do
  have : MonadLift IO m := ⟨(·)⟩
  if ← fp.isDir then
    for dirEntry in ← fp.readDir do
      visitFiles dirEntry.path f
  else
    f fp

#eval show CommandElabM _ from do
  visitFiles (← IO.currentDir) (IO.println ·)