Единични елементи, семейства от типове и екзистенциални типове за екземпляр на FromJSON

Вероятно е по-лесно първо да очертая накратко общия си проблем и след това да покажа къде съм заседнал.

Искам да получа списък с JSON на някакъв единично индексиран тип, където типът на индексиране също има свързано семейство типове. В код:

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)

С екзистенциалното количествено определяне би трябвало да мога да скрия променливия индекс и пак да мога да получа стойностите (с някаква подобна на продължение тип функция с по-висок ранг - може да има по-добро име за това). В крайна сметка програмата ми ще върви по линията на

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

където Some е от exinst пакет, но също така предефиниран по-долу. Мога да анализирам JSON в случай, че не анализирам MyFamily mt, но не мога да намеря най-добрия начин да активирам анализирането и на това от JSON.

Това, което имам досега, е по-долу:

{-# 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')

Очевидно трябва да добавя ограничение FromJSON (MarketIndex mt), но също така трябва да мога да го свържа с Some CompoundType, за което генерирам екземпляра.

Простото добавяне на FromJSON (MyFamily mt) containt

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

дава двусмислени типове грешки

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))’

Виждам, че инструментът за проверка на типа говори за mt0, а не за mt, е голям проблем, но не знам как да го убедя да очаква тип mt от дясната страна на ограничението.

(Осъзнавам също, че не съм включил FromJSON (MyFamily mt) екземпляри, но ако програмата за проверка на типа не може да разбере mt ~ mt0, не мисля, че това в момента има значение).

Надяваме се, че има поправка?

Прекарах доста време в изпробване на различни неща, но се случват доста различни неща (единични, екзистенциални и т.н.). Бавно достигам до някакво ниво на владеене, но просто нямам достатъчно знания или опит, за да съм сигурен как те допринасят (или не) за проблема.