Haskell: Get the value of a DataKinds-type into a function from the type system

Question

I am using DataKinds in Haskell and now I am wondering, if it is possible to get the value from the type system back to work on.

Here is an example:

data MyType = Contructor1 | Constructor2 | ...
    deriving (Show)

f :: IO (Proxy (a :: MyType))
f = do
    -- I want 'x' to be of type 'MyType' being the same value as 'a'.
    let x = #### something ####
    print x
    return Proxy

main = do
    -- Print 'Constructor2' into the console.
    f :: IO (Proxy Constructor2)

    -- Print 'Constructor1' into the console.
    f :: IO (Proxy Constructor1)
    return ()

Answer 1

Turning a type-level value into a plain value (technically called "reification") is not possible, in general. This is because Haskell allows type erasure: all type information is erased during compilation, and none survives at runtime, at least by default.

To keep some type-level information at runtime, one typically changes the types at hand to include a suitably-crafted type class constraint. Below, I changed the type of f accordingly.

{-# LANGUAGE DataKinds, AllowAmbiguousTypes, TypeApplications #-}

import Data.Proxy

data MyType = Constructor1 | Constructor2
    deriving (Show)

class ReifyMyType (a :: MyType) where
   reify :: MyType
instance ReifyMyType 'Constructor1 where
   reify = Constructor1
instance ReifyMyType 'Constructor2 where
   reify = Constructor2

f :: forall a . ReifyMyType a => IO (Proxy (a :: MyType))
f = do
    -- Here we reify @a, turning it into a value x.
    let x = reify @a
    print x
    return Proxy

main = do
    -- Print 'Constructor2' into the console.
    f :: IO (Proxy Constructor2)

    -- Print 'Constructor1' into the console.
    f :: IO (Proxy Constructor1)
    return ()

I believe that there are packages on Hoogle that can help one automate the creation of the boilerplate type classes. I guess singleton is one such package that does that (and much more).

Finally, I see you are using Proxys. In modern Haskell, with the above extensions, they are no longer needed. You should be able to write f :: forall a . ReifyMyType a => IO () and call it using e.g. f @'Constructor1.