module Type.Promotion where
import Prelude
import Data.Typeable
import GHC.TypeLits
class Known (t :: k) (val :: *) where typeVal :: Proxy t -> val
instance (Num i, KnownNat t) => Known (t :: Nat) i where typeVal = fromIntegral . natVal
instance val ~ Bool => Known True val where typeVal _ = True
instance val ~ Bool => Known False val where typeVal _ = False
instance val ~ Maybe a => Known 'Nothing val where typeVal _ = Nothing
instance (val ~ Maybe a, Known t a) => Known ('Just t) val where typeVal _ = Just $ typeVal (Proxy :: Proxy t)
instance (val ~ Either l r, Known t l) => Known ('Left t) val where typeVal _ = Left $ typeVal (Proxy :: Proxy t)
instance (val ~ Either l r, Known t r) => Known ('Right t) val where typeVal _ = Right $ typeVal (Proxy :: Proxy t)
instance Known ('[]) [a] where typeVal _ = []
instance (Known t a, Known ts [a]) => Known (t ': ts) [a] where typeVal _ = typeVal (Proxy :: Proxy t) : typeVal (Proxy :: Proxy ts)