## 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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information