{-# LANGUAGE RankNTypes, GADTs, ConstraintKinds, FlexibleInstances #-}

module Data.Dyn where

import Type.Reflection

data Dyn ctx where
  Dyn :: ctx a => TypeRep a -> a -> Dyn ctx

toDyn :: (Typeable a, ctx a) => a -> Dyn ctx
toDyn :: a -> Dyn ctx
toDyn a
val = TypeRep a -> a -> Dyn ctx
forall (ctx :: * -> Constraint) a.
ctx a =>
TypeRep a -> a -> Dyn ctx
Dyn (a -> TypeRep a
forall a. Typeable a => a -> TypeRep a
typeOf a
val) a
val

withDyns :: Dyn ctx -> Dyn ctx ->
            (forall a. ctx a => a -> a -> b) ->
            (SomeTypeRep -> SomeTypeRep -> b) -> b
withDyns :: Dyn ctx
-> Dyn ctx
-> (forall a. ctx a => a -> a -> b)
-> (SomeTypeRep -> SomeTypeRep -> b)
-> b
withDyns (Dyn TypeRep a
ty1 a
v1) (Dyn TypeRep a
ty2 a
v2) forall a. ctx a => a -> a -> b
f SomeTypeRep -> SomeTypeRep -> b
def = case TypeRep a -> TypeRep a -> Maybe (a :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
ty1 TypeRep a
ty2 of
  Maybe (a :~~: a)
Nothing -> SomeTypeRep -> SomeTypeRep -> b
def (TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep a
ty1) (TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep a
ty2)
  Just a :~~: a
HRefl -> a -> a -> b
forall a. ctx a => a -> a -> b
f a
v1 a
a
v2

instance Eq (Dyn Ord) where
  Dyn Ord
d1 == :: Dyn Ord -> Dyn Ord -> Bool
== Dyn Ord
d2 = Dyn Ord
-> Dyn Ord
-> (forall a. Ord a => a -> a -> Bool)
-> (SomeTypeRep -> SomeTypeRep -> Bool)
-> Bool
forall (ctx :: * -> Constraint) b.
Dyn ctx
-> Dyn ctx
-> (forall a. ctx a => a -> a -> b)
-> (SomeTypeRep -> SomeTypeRep -> b)
-> b
withDyns Dyn Ord
d1 Dyn Ord
d2 forall a. Eq a => a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(==) (\SomeTypeRep
_ SomeTypeRep
_ -> Bool
False)

instance Ord (Dyn Ord) where
  compare :: Dyn Ord -> Dyn Ord -> Ordering
compare Dyn Ord
d1 Dyn Ord
d2 = Dyn Ord
-> Dyn Ord
-> (forall a. Ord a => a -> a -> Ordering)
-> (SomeTypeRep -> SomeTypeRep -> Ordering)
-> Ordering
forall (ctx :: * -> Constraint) b.
Dyn ctx
-> Dyn ctx
-> (forall a. ctx a => a -> a -> b)
-> (SomeTypeRep -> SomeTypeRep -> b)
-> b
withDyns Dyn Ord
d1 Dyn Ord
d2 forall a. Ord a => a -> a -> Ordering
compare SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare