nested ReaderT

Stream: lean4

[David Renshaw]

If I'm in the TacticM monad, I get access the Tactic.Context by doing ← read.
But how do I access the inner Term.Context, from the inner TermElabM monad?

[Mario Carneiro]

let termCtx <- readThe Term.Context

[Mario Carneiro]

alternatively <- liftM read

[Mario Carneiro]

Also, many fields of the context are provided as separate functions like getInfoTrees, and those work even if there are more reader layers afterward

[David Renshaw]

Cool, this works.

     let context ← readThe Lean.Elab.Term.Context

[David Renshaw]

But <- liftM read does not seem to work.

[David Renshaw]

ah, need parens

[David Renshaw]

let context (← liftM) read

[Mario Carneiro]

wait that looks wrong

[Mario Carneiro]

let context <- liftM read

[David Renshaw]

oh, right, my liftM thing doesn't work. There's a red squiggle on the next line now...

[Mario Carneiro]

Note that this will just get the second reader in the stack, which is probably the TermElabM context

[Mario Carneiro]

you have to do let context <- liftM <| liftM <| liftM read to go deeper

[David Renshaw]

For yours, I get the error typeclass instance problem is stuck, it is often due to metavariables

[Mario Carneiro]

which typeclass problem? what code?

[Mario Carneiro]

#mwe

[David Renshaw]

import Lean

open Lean Elab.Tactic Parser.Tactic Lean.Meta

def foo : TacticM Unit :=
  do let ctx ← readThe Elab.Term.Context -- works
     let ctx ← liftM read
-- typeclass instance problem is stuck, it is often due to metavariables
--  MonadLiftT (?m.265 ctx) TacticM
--
     pure ()

[Mario Carneiro]

hm, I thought that worked without additional hints. You can do it (even less, in fact) with a type ascription:

import Lean

open Lean Elab.Tactic Elab.Term Parser.Tactic Lean.Meta

def foo : TacticM Unit := do
  let ctx ← (read : TermElabM _)

[David Renshaw]

hah, I had tried this unsuccessfully:

     let (ctx: Elab.Term.Context) ← read

[Mario Carneiro]

yeah you need to use readThe for that version to work

[David Renshaw]

Ah, and I see I can add the liftM if I really want to

  let ctx ← liftM (read : Elab.TermElabM _)

[David Renshaw]

I like readThe. :thumbs_up: