Attempt to promote a value to a type results in an internal error

Trying to compile

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

data Nat = Zero | Succ Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a 'Zero
  Cons :: a -> Vec a n -> Vec a ('Succ n)

data Bad = Bad {
  a :: Nat,
  b :: Vec Int a}

results in error: Not in scope: type variable ‘a’.

Change the last structure to

data Bad = Bad {
  a :: Nat,
  b :: Vec Int 'a}

and the result is

    • GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [r15Y :-> ATcTyCon Bad,
                               r17P :-> APromotionErr RecDataConPE]
    • In the second argument of ‘Vec’, namely ‘a’
      In the type ‘Vec Int a’
      In the definition of data constructor ‘Bad’

The user is attempting to promote a value to a type, which cannot be done, but the error message should be more informative.

Reproduces in 8.0.1 and 8.1.20161010.