mkCongrOf

Stream: mathlib4

[Marcus Rossel]

This is probably only a question for @Kyle Miller, but I thought I might as well post it in the open. I'm having trouble with mkCongrOf, in particular when used with proofs by refl. Here's an example:

import Lean
import Mathlib

def Mul.pow [Mul α] [OfNat α 1] (a : α) : Nat → α
  | 0     => 1
  | n + 1 => a * (pow a n)

instance mulPow [Mul α] [OfNat α 1] : Pow α Nat where
  pow := Mul.pow

open Lean Meta Elab Term Tactic Mathlib.Tactic.TermCongr

set_option hygiene false in
elab "does_mk_congr_work?" : tactic => do
  withMainContext do
    -- 1: make refl proof
    let proof ← Tactic.elabTerm (← `((rfl : @HPow.hPow α Nat α (@instHPow α Nat (@mulPow α i₁ i₂)) = @Pow.pow α Nat (@mulPow α i₁ i₂)))) none

    -- 2: make lhs and rhs which will be the target of a rewrite
    let lhs ← Tactic.elabTerm (← `(@HPow.hPow α Nat α (@instHPow α Nat (@mulPow α i₁ i₂)))) none
    let rhs ← Tactic.elabTerm (← `(@Pow.pow α Nat (@mulPow α i₁ i₂))) none

    let c ← liftMetaM do return (← getMCtx).mvarCounter

    -- 3: make cHoles for lhs and rhs
    let lhsHole ← mkCHole (forLhs := true)  lhs proof
    let rhsHole ← mkCHole (forLhs := false) rhs proof

    let a    ← Tactic.elabTerm (← `(a)) none
    let zero ← Tactic.elabTerm (← `((0 : Nat))) none

    -- 4: make complete expressions `l := lhs a 0` and `r := rhs a 0`
    let l ← mkAppM' lhsHole #[a, zero]
    let r ← mkAppM' rhsHole #[a, zero]

    -- 5: try to prove `l = r` by using `mkCongrOf`
    liftMetaM do let _ ← mkCongrOf c 0 l r

set_option pp.explicit true in
example [i₁ : Mul α] [i₂ : OfNat α 1] (a : α) : True := by
  does_mk_congr_work?
/-
function expected
  @x α Nat α
-/

Is this error a result of me using mkCHole/mkCongrOf incorrectly?
This way of using mkCongrOf has worked for me 90% of the time, but on proofs by refl it seems to (almost?) always fail.