Example of HF Zipper breaking on Nat

hf_zipper_nat.idr

%default total
ℕ : Type
ℕ = Nat

data D : ℕ -> Type where
  K0 : D Z
  K1 : {k : ℕ} -> D k -> D (S k)
  K2 : {k : ℕ} -> D k -> D Z

data Ctx : ℕ -> Type where
  Root        : {m : ℕ} -> Ctx m
  K1Hole      : {k : ℕ} -> Ctx (S k)  -> Ctx k
  K2Hole      : {k : ℕ} -> Ctx Z -> Ctx n

data Zipper : Nat -> Type where
  ▷ : {m : ℕ} -> D m -> Ctx m -> Zipper m
  Fail : {m : ℕ} -> Zipper m

downFromK1 : {k : ℕ} -> Zipper (S k) -> Zipper k
downFromK1 (▷ (K1 d) ctx) = ▷ d (K1Hole ctx)
downFromK1 Fail = Fail

upFromK1 : {k : ℕ} -> Zipper k -> Zipper (S k)
upFromK1 (▷ e ctx@(K1Hole pc)) = ▷ (K1 e) pc
upFromK1 (▷ _ _) = Fail
upFromK1 Fail = Fail

downFromK2 : {k : ℕ} -> Zipper Z -> Zipper k
downFromK2 (▷ (K2 d) ctx) = ▷ d (K2Hole ctx)
downFromK2 (▷ _ _) = Fail
downFromK2 Fail = Fail