Can't case split an HitInt with some already existing cases

[ShreckYe]

"HitInt.agda":

{-# OPTIONS --cubical --safe #-}
module HitInt where

open import Cubical.Data.Nat
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude using (subst)

data ℤ : Set where
  pos : (n : ℕ) → ℤ
  neg : (n : ℕ) → ℤ
  posneg : pos 0 ≡ neg 0

-- copied and adapted from Cubical.Data.Int.MoreInts.QuoInt.Base

sucℤ : ℤ → ℤ
sucℤ (pos n)       = pos (suc n)
sucℤ (neg zero)    = pos 1
sucℤ (neg (suc n)) = neg n
sucℤ (posneg _)    = pos 1

predℤ : ℤ → ℤ
predℤ (neg n)       = neg (suc n)
predℤ (pos zero)    = neg 1
predℤ (pos (suc n)) = pos n
predℤ (posneg _)    = neg 1

_+ℤ_ : ℤ → ℤ → ℤ
m +ℤ (pos (suc n)) = sucℤ   (m +ℤ pos n)
m +ℤ (neg (suc n)) = predℤ  (m +ℤ neg n)
m +ℤ _             = m

"SymInt.agda":

{-# OPTIONS --cubical --safe #-}
module SymInt where

open import Cubical.Core.Everything
open import HitInt renaming (_+ℤ_ to _+_; ℤ to Z)

open import Cubical.Foundations.Prelude using (refl; cong)
open import Cubical.Data.Nat using (zero; suc)

0+ : ∀ a → pos zero + a ≡ a
0+ (pos (suc n)) = cong sucℤ (0+ (pos n))
0+ (neg (suc n)) = cong predℤ (0+ (neg n))
0+ a = {!!}

I get this when case splitting a in the hole with the VS Code plugin on Windows:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full\Agda\TypeChecking\Coverage\Match.hs:449:17 in Agda-2.6.2.1-298662f04d83232d4bb339c60ce5d585c6be23bd:Agda.TypeChecking.Coverage.Match

[ice1000]

agda/src/full/Agda/TypeChecking/Coverage/Match.hs

Line 449 in 9428b1d

VarP _ x -> __IMPOSSIBLE__ -- blockedOnConstructor (splitPatVarIndex x) c

🤔🤔

/cc @Saizan