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.