this type signature in a case alternative does not typecheck and requires ScopedTypeVariables

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

Trac metadata

Trac field	Value
Version	7.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture