Singletons, type families, and existential types for a FromJSON instance

Question

It's probably easier to briefly outline my general problem first and then show where I get stuck.

I want to receive a JSON list of some singleton indexed type where the indexing type also has an associated type family. In code:

data MyType = MyValue1 | MyValue2
type family MyFamily (mt :: MyType) where
    MyFamily MyValue1 = Int
    MyFamily MyValue2 = Double
data InputType (mt :: MyType) = InputNoFamily | InputWithFamily (MyFamily mt)
data OutputType (mt :: MyType) = OutputNoFamily | OutputWithFamily (MyFamily mt)

With existential quantification I should be able to hide the varying index and still be able to get at the values (with some continuation-like higher ranked type function - there may be a better name for this). I'd end up with my program flowing along the lines of

JSON -> [Some InputType] -> [Some OutputType] -> JSON

where Some is from exinst package, but also redefined below. I can parse the JSON in the case that I don't parse the MyFamily mt, but I can't work out the best way to enable parsing that from the JSON as well.

What I have so far is below:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}

module SO where

import Data.Aeson
import Data.Singletons.TH
import GHC.Generics

$(singletons [d|
  data MyType
    = MyValue1
    | MyValue2
    | MyValue3
    deriving (Show, Eq, Generic)
  |])
instance FromJSON MyType

type family MyFamily (mt :: MyType) :: * where
  MyFamily 'MyValue1 = Double
  MyFamily 'MyValue2 = Double
  MyFamily 'MyValue3 = Int

-- stolen from exinst package
data Some (f :: k -> *) =
    forall a. Some (Sing a) (f a)

some :: forall (f :: k -> *) a. SingI a => f a -> Some f
some = Some (sing :: Sing a)

withSome :: forall (f :: k -> *) (r :: *). Some f -> (forall a. SingI a => f a -> r) -> r
withSome (Some s x) g = withSingI s (g x)

data MyCompoundType (mt :: MyType)
    = CompoundNoIndex
    | CompoundWithIndex (MyFamily mt)

deriving instance (Show (SMyType mt), Show (MyFamily mt)) => Show (MyCompoundType mt)

-- instance with no parsing of `MyFamily`
instance
  forall (mt :: MyType).
  ( SingKind (KindOf mt)
  , FromJSON (DemoteRep (KindOf mt))
  ) => FromJSON (Some MyCompoundType) where
    parseJSON = withObject "MyCompoundType" $ \o -> do
      mt :: MyType <- o .: "myType"
      case toSing mt of
        SomeSing (smt :: SMyType mt') -> case smt of
          SMyValue1 -> return $ some (CompoundNoIndex :: MyCompoundType mt')
          SMyValue2 -> return $ some (CompoundNoIndex :: MyCompoundType mt')
          SMyValue3 -> return $ some (CompoundNoIndex :: MyCompoundType mt')

I obviously need to add a FromJSON (MarketIndex mt) constraint, but I also need to be able to tie it to the Some CompoundType that I'm generating the instance for.

The simple addition of a FromJSON (MyFamily mt) constaint

instance
  forall (mt :: MyType).
  ( SingKind (KindOf mt)
  , FromJSON (DemoteRep (KindOf mt))
  , FromJSON (MyFamily mt)
  ) => FromJSON (Some MyCompoundType) where
    parseJSON = undefined

gives ambiguous types errors

Could not deduce (FromJSON (MyFamily mt0))
  arising from the ambiguity check for an instance declaration
from the context (SingKind (KindOf mt),
                  FromJSON (DemoteRep (KindOf mt)),
                  FromJSON (MyFamily mt))
  bound by an instance declaration:
             (SingKind (KindOf mt), FromJSON (DemoteRep (KindOf mt)),
              FromJSON (MyFamily mt)) =>
             FromJSON (Some MyCompoundType)
  at SO.hs:(57,3)-(61,39)
The type variable ‘mt0’ is ambiguous
In the ambiguity check for:
  forall (mt :: MyType).
  (SingKind (KindOf mt), FromJSON (DemoteRep (KindOf mt)),
   FromJSON (MyFamily mt)) =>
  FromJSON (Some MyCompoundType)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘FromJSON (Some (MyCompoundType))’

I can see that the typechecker talking about mt0 rather than mt is a big problem, but I don't know how to cajole it into expecing a mt type on the right hand side of the constraint.

(I also realise that I haven't included FromJSON (MyFamily mt) instances but if the typechecker can't figure out mt ~ mt0 I don't think that currently matters).

Hopefully, there's a fix?

I've spent a reasonable amount of time trying out different things but there's a quite a few different things going on (singletons, existentials, etc.). I'm slowly getting myself up to some level of proficiency, but I just don't have enough knowledge or experience to be certain how they are (or aren't) contributing to the problem.

Answer 1

(My prior answer to a prior question of yours is largely applicable here).

You're free to parse any type you want, you just have to demonstrate that a particular type has a FromJSON instance. In this case, you should parse concrete result types of MyFamily, because they all have appropriate instances.

instance FromJSON (Some MyCompoundType) where
    parseJSON = withObject "MyCompoundType" $ \o -> do
      cons :: String <- o .: "constructor"
      mt :: MyType <- o .: "myType"
      case toSing mt of
        SomeSing smt ->
          case cons of
            "CompoundNoIndex" -> pure $ Some smt CompoundNoIndex
            "CompoundWithIndex" -> case smt of
              SMyValue1 -> Some SMyValue1 . CompoundWithIndex <$> o .: "field"
              SMyValue2 -> Some SMyValue2 . CompoundWithIndex <$> o .: "field"
              SMyValue3 -> Some SMyValue3 . CompoundWithIndex <$> o .: "field"

Here I assumed that there's something that indicates the encoded constructor. There are many alternative formats for encoding and decoding, of course.

Alternatively, we can throw together an approximation of quantified constraints, and make more use of the singleton tag parsed from the "myType" field:

import Data.Constraint -- from "constraints"
import Data.Proxy

data MyFamilySym :: TyFun MyType * -> *
type instance Apply MyFamilySym a = MyFamily a  

class ForallInst (f :: TyFun k * -> *) (c :: * -> Constraint) where
  allInst :: Proxy '(f, c) -> Sing x -> Dict (c (f @@ x))

instance ForallInst MyFamilySym FromJSON where
  allInst _ SMyValue1 = Dict
  allInst _ SMyValue2 = Dict
  allInst _ SMyValue3 = Dict  

instance FromJSON (Some MyCompoundType) where
    parseJSON = withObject "MyCompoundType" $ \o -> do
      cons :: String <- o .: "constructor"
      SomeSing smt <- toSing <$> o .: "myType"
      case cons of
        "CompoundNoIndex" -> pure (Some smt CompoundNoIndex)
        "CompoundWithIndex" ->
          case allInst (Proxy :: Proxy '(MyFamilySym, FromJSON)) smt of
            Dict -> Some smt . CompoundWithIndex <$> o .: "field" 

The key point here is the defunctionalization with MyFamilySym and Apply. It enables us to effectively put MyFamily into instance heads, which would be otherwise outlawed by GHC. See this blog post for more on defunctionalization in singletons.

With quantified instances over type families, there's one thing we can never avoid: writing out all the cases of the type family and demonstrating an instance for each case. The ForallInst solution also does this, but at least it requires us to write out the cases only once.

Answer 2

I am not very familiar with singletons, but I still spot a possible misunderstanding here:

In your current instance, the part

forall (mt :: MyType).
  ( SingKind (KindOf mt)
  , FromJSON (DemoteRep (KindOf mt))
  ) =>

is not used at all. The file compiles just as well if you remove it.

It looks to me like you are trying to have a constraint that says that "For all types of kind MyType, these instances should exist." Unfortunately, such a feature (sometimes called "quantified constraints" or "rank n constraints") is not currently supported by GHC (and Simon PJ, who was coauthor on the paper that first suggested it, is on record as saying he has no idea how to implement the type inference for it.)

I assume the reason your modified version doesn't work is that there you actually do need quantified constraints for the FromJSON (MyFamily mt) part.

I have a hunch that I hope might help, though. (Unfortunately I don't understand enough about using singletons to write an actual solution attempt.) What if you replace some of your types by GADTs? e.g.:

data MyCompoundType (mt :: MyType) where
    CompoundNoIndex :: MyCompoundType mt
    CompoundWithIndex :: FromJSON (MyFamily mt) => MyCompoundType mt

That way, MyCompoundType can carry around the required instance itself.