Formatter unfolds unnamed function parameter with refinements weirdly

[chandradeepdey]

type vec (a: Type) : n: nat -> Type =
  | Nil : vec a 0
  | Cons : #n: nat -> hd: a -> tl: vec a n -> vec a (n + 1)

let pconv_vec_z' (#a: Type) (#n: nat) (_:unit{equals n 0}) (v: vec a n) : vec a 0 = Nil

the last line becomes

let pconv_vec_z'
      (#a: Type)
      (#n: nat)
      (_:
          (_:
            unit
              { match _ with
//                    ^
// Failed to resolve implicit argument ?5 of type (*?u4*)
                | _ -> equals n 0
                | _ -> False }))
      (v: vec a n)
    : vec a 0 = Nil

(which also has an error)