Rollback mvar context on try/catch?

[dselsam]

structure Foo (A : Sort _) := (foo : A)
structure Bar (A : Sort _) extends Foo A := (bar : A)
instance {A} : Coe (Bar A) (Foo A) := {coe := Bar.toFoo}
def getFoo {A} (F : Foo A) := F.foo
def bar : Bar Nat := {foo := 0, bar := 1}

#check getFoo bar -- fails with surprising error message

Here is the message:

error: application type mismatch
  getFoo bar
argument
  bar
has type
  Bar Nat : Type
but is expected to have type
  Foo (Bar Nat) : Type

I tracked it down to tryPureCoe? and added a few trace messages:

...
    try
      trace[Elab.term.tryPureCoe.tryCoe.pre] "{← instantiateMVars β}"
      let aNew ← tryCoe errorMsgHeader? β α a none
      trace[Elab.term.tryPureCoe.tryCoe.post] "{← instantiateMVars β}"
      let aNew ← mkPure m aNew
      trace[Elab.term.tryPureCoe.postPure] "{← instantiateMVars β}"
      pure (some aNew)
    catch _ =>
      trace[Elab.term.tryPureCoe.tryCoe.err] "{← instantiateMVars β}"
      pure none
...

Here is the resulting trace:

  [Elab.term.tryPureCoe.tryCoe.pre] ?m.804
  [Elab.term.tryPureCoe.tryCoe.post] Bar Nat
  [Elab.term.tryPureCoe.err] Bar Nat

It looks like tryCoe is assigning β, mkPure is failing, and somehow in the catch branch β still has the assignment found by tryCoe.

I don't understand all the relevant code but I was surprised that the metavariable context does not seem to automatically rollback on try/catch. Is this expected? If so, should tryPureCoe? rollback explicitly?