Is it possible to declare FromJSON instance for my weird enum-like type?

Viewed 122

I'm trying to define a type that can be restricted to a subset of Nat's. While I realise a simple solution would be to use a regular ADT I'm still curious if such type could be defined with an accompanying FromJSON instance. Here's what I have so far:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test where

import Control.Monad
import Data.Aeson
import Data.Kind (Constraint)
import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits
import Prelude


type family Or (a :: Bool) (b :: Bool) :: Bool where
  Or 'False 'False = 'False
  Or 'True 'False = 'True
  Or 'False 'True = 'True
  Or 'True 'True = 'True

type family IsOneOf (n :: Nat) (xs :: [Nat]) :: Bool where
  IsOneOf n '[] = 'False
  IsOneOf n (x ': xs) = Or (n == x) (IsOneOf n xs)

type family Member n xs :: Constraint where
  Member n xs = 'True ~ IsOneOf n xs

data SomeEnum (xs :: [Nat]) where
        SomeEnum :: (KnownNat n, Member n xs) => Proxy n -> SomeEnum xs

This can be then used as follows:

λ> SomeEnum (Proxy :: Proxy 1) :: SomeEnum [1,2]

I was able to define a ToJSON instance:

instance ToJSON (SomeEnum xs) where
  toJSON (SomeEnum n) = Number (fromIntegral . natVal $ n)

However it doesn't seem declaring a FromJSON instance is possible as I can't figure out how to convince the compiler that whatever number I might get out of a JSON document is indeed a member of the set of accepted values of SomeEnum.

My question then is - is it possible to declare that instance at all with the current formulation of the data type? Could perhaps the type itself be adjusted somehow to allow for such instance while preserving the behaviour of being restricted to specific set of Nats?

I'm not very familiar with Haskell's type level features so perhaps what I'm asking doesn't make sense in its current form. I would appreciate any comments.

1 Answers
Related