[GHC] #11995: Can't infer type

[GHC]

#11995: Can't infer type
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 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

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11995>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler