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

Question

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.

Answer 1

It's easier to look at your problem without the distraction of JSON.

The real problem is can you define a function

toSomeEnum :: Integer -> SomeEnum xs

Since SomeEnum [] is isomorphic to Void, and -1 is not convertable to SomeEnum xs for any xs, obviously not. We need the ability to fail:

toSomeEnum :: Integer -> Maybe (SomeEnum xs)

And to do anything beyond const Nothing we'll need the ability to compare the elements of xs to the runtime input:

toSomeEnum' :: forall xs. ToSomeEnum xs => Integer -> Maybe (SomeEnum xs)
toSomeEnum' n = do
  SomeNat proxy_n <- someNatVal n
  toSomeEnum proxy_n

class ToSomeEnum (xs :: [Nat]) where
  toSomeEnum :: forall (n :: Nat). KnownNat n => Proxy n -> Maybe (SomeEnum xs)

instance ToSomeEnum '[] where
  toSomeEnum = const Nothing

instance (KnownNat x, ToSomeEnum xs) => ToSomeEnum (x ': xs) where
  toSomeEnum proxy_n = case sameNat proxy_n (Proxy @x) of 
    Just Refl -> Just (SomeEnum proxy_n) -- [1]
    Nothing -> case toSomeEnum proxy_n :: Maybe (SomeEnum xs) of
      Nothing -> Nothing
      Just (SomeEnum proxy_n') -> Just (SomeEnum proxy_n') -- [2]

This didn't quite work as GHC complained

• Could not deduce: Or 'True (IsOneOf n xs) ~ 'True
    arising from a use of ‘SomeEnum’
  from the context: x ~ n
    bound by a pattern with constructor:
               Refl :: forall k (a :: k). a :~: a,
             in a case alternative
    at [1]
...
• Could not deduce: Or (GHC.TypeLits.EqNat n1 x) 'True ~ 'True
    arising from a use of ‘SomeEnum’
  from the context: (KnownNat n1, Member n1 xs)
    bound by a pattern with constructor:
               SomeEnum :: forall (xs :: [Nat]) (n :: Nat).
                           (KnownNat n, Member n xs) =>
                           Proxy n -> SomeEnum xs,
             in a case alternative
    at [2]

Which can be fixed by using a lazier definition of Or:

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

No unsafeCoerce or type witnesses required. Your calling code simply has to know what it expects xs to be.

λ case (toSomeEnum' 1 :: Maybe (SomeEnum '[1,2,3])) of { Just _ -> "ok" ; Nothing -> "nope" }
"ok"
λ case (toSomeEnum' 4 :: Maybe (SomeEnum '[1,2,3])) of { Just _ -> "ok" ; Nothing -> "nope" }
"nope"