recall doesn't work in namespaces

Stream: mathlib4

[Mario Carneiro]

MWE:

import Mathlib.Tactic.Recall

namespace Foo
noncomputable def foo := 0
recall Foo.foo : String := ""

[Mario Carneiro]

this is doubly weird:

• You can't use recall foo, you have to write recall Foo.foo even though you are already in the namespace
• The definition does not seem to be checked against the original in any way

[Mario Carneiro]

Also recall doesn't take a doc string. I would like to use it to gloss the declaration, it doesn't have to be stored or validated against the original

[Damiano Testa]

There was also this previous thread about it: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60recall.60.20strangeness

[Mario Carneiro]

oh look at that, past me already filed a bugfix PR

[Mario Carneiro]

seems to be failing though