case-split with showimplicits breaks

[jasonhemann]

The following is a seven-line example.

import Data.Vect
data VT : Vect m Nat -> Type where
  Nil  : VT []
  (::) : Vect n t -> VT v -> VT (n :: v)

MatType : (hm : VT v) -> Type
MatType hm = ?MatType_rhs

Steps to Reproduce

First :set showimplicits, then :cs on hm,

Expected Behavior

MatType : (hm : VT v) -> Type
MatType [] = ?MatType_rhs_0
MatType ((::) {v} {t} {n} xs x) = ?MatType_rhs_1

Observed Behavior

Produces

MatType : (hm : VT v) -> Type
MatType [] = ?MatType_rhs_0
MatType (:: {{len:3279} = len} {v} {t} {n} xs x) = ?MatType_rhs_1

or something equivalent. Both the len argument and the :: not being in parens seem incorrect.