Pattern matching breaks injective type families

{-# LANGUAGE TypeFamilyDependencies, TypeOperators, DataKinds, GADTs, TypeApplications #-}

data HList xs where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x:xs)

type family ListId xs = ys | ys -> xs
  where
    ListId '[] = '[]
    ListId (x:xs) = (x : ListId xs)

f :: HList (ListId ts) -> ()
f a =
  case a of
    HNil -> ()
--  z@(HCons _ _) -> f z   -- uncomment to break
    z -> f z

While z -> f z works, pattern matching on HCons breaks it:

A.hs:16:24: error:
    • Could not deduce: ListId xs ~ xs1
      from the context: ListId ts ~ (x : xs1)
        bound by a pattern with constructor:
                   HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
                 in a case alternative
        at A.hs:16:8-16
      ‘xs1’ is a rigid type variable bound by
        a pattern with constructor:
          HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
        in a case alternative
        at A.hs:16:8-16
      Expected type: HList (ListId (x : xs))
        Actual type: HList (ListId ts)
    • In the first argument of ‘f’, namely ‘z’
      In the expression: f z
      In a case alternative: z@(HCons _ _) -> f z
   |
16 |     z@(HCons _ _) -> f z
   |                        ^