Can't specify type signature in GHCI when using DataKinds

Question

So, ghci is giving me an interesting error when I try and pin down the type of a polymorphic return value when using DataKinds. I have the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}

data DataKind
    = KindA
    | KindB

data SomeData (a :: DataKind) = forall c. SomeData
    { val :: Int
    , sub :: Maybe (SomeData c)
    }

deriving instance Show (SomeData a)

two :: SomeData 'KindA
two = SomeData 2 Nothing

This code compiles as expected. If I construct SomeData in ghci and don't specify the type it works fine:

> two
SomeData {val = 2, sub = Nothing}

> :t two
two :: SomeData 'KindA

> SomeData 2 Nothing
SomeData 2 Nothing :: SomeData a

But if I try and specify the type it errors:

> SomeData 2 Nothing :: SomeData 'KindA
<interactive>:745:32-37: error:
• Data constructor ‘KindA’ cannot be used here
    (Perhaps you intended to use DataKinds)
• In the first argument of ‘SomeData’, namely ‘KindA’
  In an expression type signature: SomeData KindA
  In the expression: SomeData 1 Nothing :: SomeData KindA

It appears that the quote is not being interpreted by ghci. I started the repl using stack ghci. Has anyone encountered this before? Thanks in advance for any help.

Answer 1

SomeData 2 Nothing :: SomeData 'KindA works if you first :seti -XDataKinds. My thought is that the pragmas in the code files are incorporated when loading the file, but for things evaluated in the REPL you need to enable them inside GHCi explicitly as well.

I would think of this as when in GHCi, the file(s) you load are more like imported modules and any code in the REPL has its own set of language extensions. When loading multiple files in GHCi, you might not necessarily want all language extensions in all loaded files to be enabled/available.