frob.hs

{-# LANGUAGE KindSignatures, DataKinds, GADTs, FlexibleInstances, FlexibleContexts #-}
main = return ()

-- Problem: I want to (de)serialize a GADT with multiple constructors.
-- Any given type will only have a single valid constructor, so there should be no need to serialize a tag.
-- However, it is difficult to convince GHC that for all `n`, `Foo n` is deserializable.
-- This is presumably because the instances for `n ~ Z` and `n ~ S m` are in separate places and GHC
-- doesn't have logic in place to realized that that covers all possibilities.
-- However, I can't figure out a good way to combine the two instances so GHC is happy.

data Nat = Z | S Nat

data Foo (n :: Nat) where
    FooZ :: Foo 'Z
    FooN :: Int -> Foo n -> Foo ('S n)

-- This is a stand-in for the deserialize function of e.g. "Store"
class Frob a where
    frob :: Int -> Maybe a

-- I tried to combine these two instances by pattern matching on singleton types,
-- but I ran into issues with the recursive step.
instance Frob (Foo 'Z) where
    frob 0 = Just FooZ
    frob _ = Nothing

instance Frob (Foo n) => Frob (Foo ('S n)) where
    frob i = FooN i <$> frob (i-1)

data Blah n = Blah Int (Foo n)

-- GHC complains:
--    No instance for (Frob (Foo n)) arising from a use of ‘frob’
-- But of course, we know there is an instance, for all n.
instance Frob (Blah n) where
    frob i = Blah i <$> frob (i-1)