{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Aeson.Schema.Utils.Sum
( SumType(..)
, fromSumType
) where
import Control.Applicative ((<|>))
import Data.Aeson (FromJSON(..), ToJSON(..))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy(..))
import GHC.TypeLits (type (-), ErrorMessage(..), Nat, TypeError)
data SumType (types :: [Type]) where
Here :: forall x xs. x -> SumType (x ': xs)
There :: forall x xs. SumType xs -> SumType (x ': xs)
deriving instance (Show x, Show (SumType xs)) => Show (SumType (x ': xs))
instance Show (SumType '[]) where
show = \case {}
deriving instance (Eq x, Eq (SumType xs)) => Eq (SumType (x ': xs))
instance Eq (SumType '[]) where
_ == _ = True
deriving instance (Ord x, Ord (SumType xs)) => Ord (SumType (x ': xs))
instance Ord (SumType '[]) where
compare _ _ = EQ
instance (FromJSON x, FromJSON (SumType xs)) => FromJSON (SumType (x ': xs)) where
parseJSON v = (Here <$> parseJSON v) <|> (There <$> parseJSON v)
instance FromJSON (SumType '[]) where
parseJSON _ = fail "Could not parse sum type"
instance (ToJSON x, ToJSON (SumType xs)) => ToJSON (SumType (x ': xs)) where
toJSON = \case
Here x -> toJSON x
There xs -> toJSON xs
instance ToJSON (SumType '[]) where
toJSON = \case {}
class FromSumType (n :: Nat) (types :: [Type]) (x :: Type) where
fromSumType' :: 'Just x ~ GetIndex n types => proxy1 n -> SumType types -> Maybe x
instance {-# OVERLAPPING #-} FromSumType 0 (x ': xs) x where
fromSumType' _ = \case
Here x -> Just x
There _ -> Nothing
instance {-# OVERLAPPABLE #-}
( FromSumType (n - 1) xs x
, 'Just x ~ GetIndex (n - 1) xs
) => FromSumType n (_x ': xs) x where
fromSumType' _ = \case
Here _ -> Nothing
There xs -> fromSumType' (Proxy @(n - 1)) xs
fromSumType
:: ( IsInRange n types
, 'Just result ~ GetIndex n types
, FromSumType n types result
)
=> proxy n -> SumType types -> Maybe result
fromSumType = fromSumType'
type family IsInRange (n :: Nat) (xs :: [Type]) :: Constraint where
IsInRange n xs = IsInRange'
( TypeError
( 'Text "Index "
':<>: 'ShowType n
':<>: 'Text " does not exist in list: "
':<>: 'ShowType xs
)
)
n
xs
type family IsInRange' typeErr (n :: Nat) (xs :: [Type]) :: Constraint where
IsInRange' typeErr _ '[] = typeErr
IsInRange' _ 0 (_ ': _) = ()
IsInRange' typeErr n (_ ': xs) = IsInRange' typeErr (n - 1) xs
type family GetIndex (n :: Nat) (types :: [Type]) :: Maybe Type where
GetIndex 0 (x ': xs) = 'Just x
GetIndex _ '[] = 'Nothing
GetIndex n (_ ': xs) = GetIndex (n - 1) xs