GADTs-Typeable.hs

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}

import qualified Data.Dependent.Map as DM
import           Data.Dependent.Sum (DSum (..))
import           Data.GADT.Compare
import           Data.Kind
import           Data.Typeable
import           Unsafe.Coerce


------------------------------------------
-- 1. The types of our problem.

-- Some arbitrary enum value.
data Label = Foo | Bar | Baz
  deriving (Show, Eq, Ord, Bounded, Enum, Typeable)

-- A GADT that defines "singletons" (kinda): one constructor for each label.
data Tag (l :: Label) where
  FooTag :: Tag Foo
  BarTag :: Tag Bar
  BazTag :: Tag Baz

deriving instance Show (Tag l)


------------------------------------------
-- 2. Example usage

-- Mapping from label to type (à la Trees That Grow).
class Show (ValueType l) => Representation (l :: Label) where
  type ValueType l :: Type

instance Representation 'Foo where type ValueType 'Foo = Int
instance Representation 'Bar where type ValueType 'Bar = String
instance Representation 'Baz where type ValueType 'Baz = ()

-- Example use case: a value whose representation is parametric over the label.
data Value l where
  Value :: Representation l =>
    { vName  :: String
    , vValue :: ValueType l
    } -> Value l
deriving instance Show (Value l)

-- We want to use Tag as the key in a dependent map; the value thing is just an example.
type LabeledValueMap = DM.DMap Tag Value

-- Example usage: create a map, print its content
main :: IO ()
main = do
  let dmap = DM.fromList [ FooTag :=> Value "answer" 42
                         , BarTag :=> Value "answer" "42"
                         , BazTag :=> Value "answer" ()
                         ]
  sequence_ $ do
    (tag :=> value) <- DM.toList dmap
    pure $ putStrLn $ show tag ++ ": " ++ show value



------------------------------------------
-- 3. Tthe Problem ™

-- How to write instances of GEq and GCompare for Tag?

#if 1
-- This works: we explictly reify, and use unsafe coerce.

reify :: Tag l -> Label
reify FooTag = Foo
reify BarTag = Bar
reify BazTag = Baz

instance GEq Tag where
  geq b1 b2
    | reify b1 == reify b2 = unsafeCoerce $ Just Refl
    | otherwise            = Nothing

instance GCompare Tag where
  gcompare b1 b2 = case compare (reify b1) (reify b2) of
    EQ -> unsafeCoerce GEQ
    LT -> GLT
    GT -> GGT
#endif

#if 0
-- But THIS DOESN'T!
-- No suitable instance of Tyepable is found?

deriving instance Typeable (Tag l)
deriving instance Typeable 'Foo
deriving instance Typeable 'Bar
deriving instance Typeable 'Baz

instance GEq Tag where
  geq (_ :: Tag l1) (_ :: Tag l2)
    | Just Refl <- eqT @l1 @l2 = Just Refl
    | otherwise                = Nothing

instance GCompare Tag where
  gcompare b1 b2 = undefined
#endif

#if 0
-- This works, but is horrible?
-- And what about gcompare?

deriving instance Typeable (Tag l)

instance GEq Tag where
  geq FooTag FooTag = Just Refl
  geq BarTag BarTag = Just Refl
  geq BazTag BazTag = Just Refl
  geq _ _           = Nothing

instance GCompare Tag where
  gcompare b1 b2 = undefined
#endif