[GHC] #7352: this type signature in a case alternative does not typecheck and requires ScopedTypeVariables

[GHC]

#7352: this type signature in a case alternative does not typecheck and requires
ScopedTypeVariables
------------------------------+---------------------------------------------
 Reporter:  atnnn             |          Owner:                         
     Type:  bug               |         Status:  new                    
 Priority:  normal            |      Component:  Compiler (Type checker)
  Version:  7.6.1             |       Keywords:                         
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple       
  Failure:  None/Unknown      |       Testcase:                         
Blockedby:                    |       Blocking:                         
  Related:                    |  
------------------------------+---------------------------------------------
 In the following code, E and F are similar data types

 {{{
 {-# LANGUAGE PolyKinds, DataKinds, GADTs #-}

 {-# LANGUAGE ScopedTypeVariables #-}

 data T a = T

 data E a where
   E :: T a -> E '[a]

 data F a where
   F :: T a -> F a

 test1 = case E T :: E '[True] of
   E (T::T True) -> ()

 test2 = case F T of
   F (T::T True) -> ()

 test3 = case E T of  E (T::T True) -> ()
 }}}

 test1 compiles fine with a type signature on E T

 test2 compiles fine with no type signature on F T

 But test3 does not typecheck, it causes this error with 7.6.1

 {{{
     Couldn't match kind `Bool' with `Bool'
     Expected type: a
       Actual type: a0
     Kind incompatibility when matching types:
       a0 :: Bool
       a :: Bool
     In the pattern: E (T :: T True)
     In a case alternative: E (T :: T True) -> ()
 }}}

 And this error with current HEAD

 {{{
     Could not deduce (a ~ 'True)
     from the context ((':) Bool a0 ('[] Bool) ~ (':) Bool a ('[] Bool))
       bound by a pattern with constructor
                  E :: forall (k :: BOX) (a :: k). T k a -> E k ((':) k a
 ('[] k)),
                in a case alternative
       at /home/atnnn/work/bug.hs:20:3-15
       `a' is a rigid type variable bound by
           a pattern with constructor
             E :: forall (k :: BOX) (a :: k). T k a -> E k ((':) k a ('[]
 k)),
           in a case alternative
           at /home/atnnn/work/bug.hs:20:3
     Expected type: T Bool 'True
       Actual type: T Bool a
     In the pattern: T :: T True
     In the pattern: E (T :: T True)
     In a case alternative: E (T :: T True) -> ()
 }}}

 Additionally, removing the ScopedTypeVariables pragma causes an error for
 each test

 {{{
     Illegal type signature: `T True'
       Perhaps you intended to use -XScopedTypeVariables
     In a pattern type-signature
 }}}

 But there are no visible type variables in the type signatures

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