Can't infer type

{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
             TypeInType, UnicodeSyntax, GADTs #-}

module T11995 where

import Data.Kind

data NP :: forall k. (ĸ → Type) → ([k] → Type) where
  Nil  :: NP f '[]
  (:*) :: f x → NP f xs → NP f (x:xs)

newtype K a b = K a deriving Show
unK (K a) = a

h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
  Nil     -> []
  K x:*xs -> x : h'collapse xs

if we replace xs by an underscore:

tJN0.hs:13:29-30: error: …
    • Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
      from the context: ((k :: *) ~~ (ĸ :: *),
                         (t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
        bound by a pattern with constructor:
                   :* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
                         f x -> NP k k f xs -> NP k k f ((':) k x xs),
                 in a case alternative
        at /tmp/tJN0.hs:13:3-9
      ‘xs’ is a rigid type variable bound by
        a pattern with constructor:
          :* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
                f x -> NP k k f xs -> NP k k f ((':) k x xs),
        in a case alternative
        at /tmp/tJN0.hs:13:3
      Expected type: NP ĸ k (K ĸ a) t
        Actual type: NP ĸ ĸ (K ĸ a) xs
    • In the first argument of ‘h'collapse’, namely ‘xs’
      In the second argument of ‘(:)’, namely ‘h'collapse xs’
      In the expression: x : h'collapse xs
    • Relevant bindings include
        xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
        h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.

Should it not be able to infer that?

The Glorious Glasgow Haskell Compilation System, version 8.1.20160419