using `Lean.TSyntax.replaceM` to replace a hole in a type

Stream: metaprogramming / tactics

[Chris Henson]

I am trying to write an elaborator filltype to replace a hole (meant for a type variable) with a given type. E.g. filltype Int (List ?X) to List Int. For a single type, something like this seems to work, but the last result here is unexpected:

import Lean.Elab.Command
open Lean Elab Tactic Command

syntax (name := filltype) "filltype" : term
elab_rules : term
  | `(filltype $tyvar:term $expr:term) => do
        let pattern ← expr.raw.replaceM fun stx =>
          if stx.isOfKind ``Parser.Term.syntheticHole then
            pure tyvar
          else
            pure stx
        Term.elabType pattern

-- these two are as expected
#check filltype Int ?X        -- Int : Type
#check filltype Int Nat       -- Nat : Type

-- but this seems to have no effect
#check filltype Int (List ?X) -- List ?X : Type u_1

[Chris Henson]

In case it is relevant, the fuller scope of what I'd like the elaborator to do is take some type with holes, e.g. List (?X x ?Y), and elaborate to a command that looks something like

instance {X Y : Type} [A X] [A Y] : B (List (X x Y))

where A and B are some existing typeclasses.

[Kyle Miller]

For replaceM, if you return non-none, then it accepts that as the replacement and it does not recurse.

Try doing pure none in the else clause instead

[Chris Henson]

That worked, thanks!