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.

Goldofpleasure

I believe its a GHCi thing. Try writing :set -XDataKinds to manually enable the extension. For some reason the interpreter doesn't load it automatically when you load a file. – Illustrative

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.

Figurant

Thanks! That makes sense. I was reading a similar question and one of the answers mentioned that you only need the DataKinds extension when you use the promoted constructors, which seems to be equivalent of needing to enable the extension in the repl. – Goldofpleasure

It's often better to use :seti instead of :set – using :set will also cause extensions to be enabled in all loaded files, as though you'd run ghc with those options. The :seti command just sets the extensions for interactive use. For example, GHCi behaves as though the user had specified :seti -XNoMonomorphismRestriction by default – GHCi-bound variables aren't monomorphized, but variables bound in loaded files are left alone. – Thoma

@AntalSpector-Zabusky I've edited the answer to reference :seti. I had not been aware of that option and looking it up I agree that its behavior would be less surprising in this case. – Figurant