[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 (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by thomie):

 * keywords:   => TypeInType


@@ -2,0 +2,5 @@
+ {-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
+              TypeInType, UnicodeSyntax, GADTs #-}
+
+ module T11995 where
+

New description:

 {{{#!hs
 {-# 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

--

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