Reify arbitrary data-kind to a (compile-time known) value

Question

I want to be able to write something like:

reify (Proxy @True)) == True;
reify (Proxy @(Just 5)) == Just 5;

Is it possible by a blanket implementation? I got as far as

class Reify (a :: k) where
  reify :: Proxy a -> k

And I have no idea how to write this except than writing every instance by hand: one instance for True, one instance for False, etc. I don't want to write it all by hand, and I don't want to use template haskell to do it for me. Can I have just one instance to do it?

Or maybe there exists some other approach? The use-case for me is to be able to write:

type DeriveHelper :: Settings -> Type -> Type
newtype DeriveHelper s a = DeriveHelper a

instance (Generic a, GMyClass (Rep a)) => MyClass (DeriveHelper s a) where
  myMethod (DeriveHelper x) = genericMyMethod (reify (Proxy @s)) $ from x

-- and then
data FooBar ...
  deriving MyClass via DeriveHelper SomeSettings FooBar

As for the libraries I've seen in the world that do this, they seem to all have small Settings which I believe is reified by hand.

Answer 1

I would be remiss if I didn't note that the best solution at the moment is still the singletons package, which provides the demote function to do what you want (see example at the end). However, that implementation uses Template Haskell internally to lift existing Prelude types and requires you to use TH explicitly to lift additional types. And, you said you didn't want to do that...

So, I guess it's technically possible with generics. You can use Data.Typeable or Type.Reflection to destruct the type-level t of kind k, and then construct a term t of type k using GHC.Generics (or Data.Data or whatever).

Consider the following proof of concept which uses Data.Typeable for type destruction and Data.Data for term construction:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Reify where

import Data.Typeable
import Data.Data

demote :: forall k t. (Typeable t, Data k) => Proxy (t :: k) -> k
demote pxy
  = let rep = typeRep pxy
    in  fromConstr $ mkConstr (dataTypeOf @k undefined)
                              (removeTick $ tyConName . typeRepTyCon $ rep)
                              []
                              Prefix
  where removeTick ('\'':xs) = xs

This is only a partial implementation, but it will demote arbitrary nullary prefix constructors:

data MyType = A | B Int deriving (Show, Data)

main = do
    print $ (demote (Proxy @'Nothing) :: Maybe Int)
    print $ (demote (Proxy @'False) :: Bool)
    print $ (demote (Proxy @'A) :: MyType)

I don't see any technical barrier to generalizing it to handling constructors of arbitrary arity and adding support for Int#, etc.

Maybe someone's implemented this in a package somewhere, but I don't know where.

Anyway, the singletons solution using TH is ready-to-run and would look something like:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Reify where

import Data.Singletons
import Data.Singletons.TH
import Data.Kind
import GHC.Generics
import GHC.Natural

-- define a new type supporting "demote"
$(singletons [d|
  data MyType = A | B Bool deriving (Show)
  |])

-- add "demote" support to an existing type (e.g., imported from a library)
data LibraryType = C | D Bool deriving (Show)
$(genSingletons [''LibraryType])

main = do
  print $ (demote @('Just 5) :: Maybe Natural)
  print $ (demote @'False :: Bool)
  print $ (demote @'A :: MyType)
  print $ (demote @('D 'False) :: LibraryType)