match_expr + do notation: (kernel) decl has metavars

Stream: lean4

[Siddharth Bhat]

Consider the MWE that mixes match_expr with do notation elaboration:

import Lean
open Lean

variable {e' : Expr}

partial def MemPairwiseSeparateProof.ofExpr? : Option Unit :=
  go ()
  where
    /-
    (kernel) declaration has metavariables 'MemPairwiseSeparateProof.ofExpr?.go'
    -/
    go (_ : Unit) : Option Unit := do
      match_expr e' with
      | _ => none

A slightly different MWE:

/-
application type mismatch
  bind (instantiateMVarsIfMVarApp e)
argument
  instantiateMVarsIfMVarApp e
has type
  MetaM Expr : Type
but is expected to have type
  Option Expr : Type
-/
partial def k (e : Expr) : Option Unit := do
  match_expr e with
  | _ => none

The do notation seems important to reproduce this. I guess this is a bug?