Is there a way to print/debug value from `getOptions`

Stream: lean4

[Shubham Kumar 🦀 (he/him)]

I am trying to write a single function that can manage multiple trace classes. I want the trace class to be enabled in the environment of my lean project.

So I created a small project to see how to go about. In the Trace.lean file (in the lean prelude) registerTraceClass registers a Name type with trace tag. So I thought - "Ok, I should look inside the getOptions value"

The function to inspect the value inside getOptions looks like this -

def f {m : Type -> Type} {α : Type} [Monad m] [MonadLiftT IO m]  [MonadOptions m] [MonadOptions (IO m)] [Inhabited α] : m α := do
  let opts ← getOptions
  let s := toString opts
  IO.eprintln s!"{s}"
  pure (default : α)

Now that is the current bachground I have about the problem at hand. If I missed something please let me know.

When I try the above code I get the following error.

Application type mismatch: The argument
  m
has type
  Type → Type
but is expected to have type
  Type
in the application
  IO m

But when I change it to

def f {m : Type -> Type} {α : Type} [Monad m] [MonadLiftT IO m]  [MonadOptions m] [MonadOptions (IO (m α))] [Inhabited α] : m α := do
  let opts ← getOptions
  let s := toString opts
  IO.eprintln s!"{s}"
  pure (default : α)

to satisfy the type signature I get the inverse of the previous requirement

Application type mismatch: The argument
  IO (m α)
has type
  Type
but is expected to have type
  Type → Type
in the application
  MonadOptions (IO (m α))

I don't know what to do to see inside options. Any way to get through this would be helpful :pray:

[Henrik Böving]

The constraint [MonadOptions (IO m)] (and also [MonadOptions (IO (m a))] doesn't make sense, you need to provide MonadOptions with a monad and only IO or m on their own are monads. I don't see why you'd even want to have that constraint in the first place though, the function should just work without it.

[Shubham Kumar 🦀 (he/him)]

I did try without that constraint but it didn't work
I get the following error when I try to #eval f

Error :

failed to synthesize
  MonadOptions IO

[Shubham Kumar 🦀 (he/him)]

the complete snippet

def f {m : Type -> Type} {α : Type} [Monad m] [MonadLiftT IO m]  [MonadOptions m] [Inhabited α] : m α := do
  let opts ← getOptions
  let s := toString opts
  IO.eprintln s!"{s}"
  pure (default : α)

#eval f

[Henrik Böving]

Sure, because the system decided to operate with m = IO as you didn't tell it any better and IO is not a MonadOptions, if you want it to work you need to operate in a monad that implements MonadOptions.

[Henrik Böving]

For example like so:

import Lean

open Lean

def f {m : Type -> Type} [Monad m] [MonadLiftT IO m]  [MonadOptions m]: m Unit := do
  let opts ← getOptions
  let s := toString opts
  IO.eprintln s!"{s}"

#eval f (m := MetaM)

[Shubham Kumar 🦀 (he/him)]

I see, is there a way to inline MetaM as the implicit the function definition? I don't want user to bear the burden

[Henrik Böving]

If you write a function that is already in MetaM and call f from that function the system is going to infer MetaM on its own. You need to annotate it in #eval because there is no additional information.

[Shubham Kumar 🦀 (he/him)]

but there is no way to make it explicit in an IO context?

Also I see that we cannot use a type that is constrained by inhabited. Is there a specific reason for it?
(This is not needed right now but I was curious :D)

Thanks either way, it works now :rocket:

[Henrik Böving]

but there is no way to make it explicit in an IO context?

That doesn't make sense, IO is not a MonadOptions so you cannot run this function in IO

Also I see that we cannot use a type that is constrained by inhabited. Is there a specific reason for it?
(This is not needed right now but I was curious :D)

there is no need for it here, it's generally possible

[Shubham Kumar 🦀 (he/him)]

Right I should have looked at the instances implemented for MonadOptions. Thanks!