Generic parser for GADTs with kind-generics (composed with an existential type, in the second half)

GadtRead.hs

{-# LANGUAGE
    QuantifiedConstraints,
    AllowAmbiguousTypes,
    TypeApplications,
    ScopedTypeVariables,
    RankNTypes,
    GADTs,
    DataKinds,
    PolyKinds,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    UndecidableInstances,
    StandaloneDeriving,
    TypeFamilies,
    TypeOperators,
    TemplateHaskell #-}

module GadtRead where

import Data.PolyKinded.Atom
import Generics.Kind
import Generics.Kind.TH
import Data.Kind
import Data.Type.Bool
import Data.Type.Equality (type (==), type (~~))

-- Without existential types
--
-- readFooInt :: String -> Maybe (Foo Int Int)
-- readFooBool :: String -> Maybe (Foo Bool Bool)

data Foo (b :: Type) (a :: Type) where
  Bar :: Foo Int Int
  Baz :: Foo Bool Bool
  Bag :: Foo b a

deriving instance Show (Foo b a)
deriveGenericK ''Foo

-- Read a binary string ("0101...") to choose a constructor.
class GRead f p where
  gread :: String -> Maybe (f p)

instance GRead f p => GRead (M1 i c f) p where
  gread = fmap M1 . gread

instance (GRead f p, GRead g p) => GRead (f :+: g) p where
  gread ('0' : s) = fmap L1 (gread s)
  gread ('1' : s) = fmap R1 (gread s)
  gread _ = Nothing

instance GRead U1 p where
  gread _ = Just U1

instance GReadCon (Sat c) c f p => GRead (c :=>: f) p where
  gread = greadCon @(Sat c)

class GReadCon (b :: Bool) c f p where
  greadCon :: String -> Maybe ((c :=>: f) p)

instance (Interpret c p, GRead f p) => GReadCon 'True c f p where
  greadCon = fmap SuchThat . gread

instance GReadCon 'False c f p where
  greadCon _ = Nothing

-- Whether a constraint is satisfiable
-- Assumed to be a conjunction of type equalities
type family Sat (c :: Atom Type Constraint) :: Bool where
  Sat (c1 ':&: c2) = Sat c1 && Sat c2
  Sat ('Kon (a ~~ b)) = a == b
  {- if you use (~) instead of (~~) here you get a "No instance" error
     that seems to say that, paradoxically, (Sat ('Kon (Int ~ Int))) doesn't
     reduce, but in spite of what's printed that's actually (~~).
   -}

genericRead :: forall a. (GenericK a LoT0, GRead (RepK a) LoT0) => String -> Maybe a
genericRead = fmap toK . gread @(RepK a) @LoT0

readFooInt :: String -> Maybe (Foo Int Int)
readFooInt = genericRead

readFooBool :: String -> Maybe (Foo Bool Bool)
readFooBool = genericRead

example :: [String]
example =
  [ show $ readFooInt  "0"   -- Just Bar
  , show $ readFooInt  "10"  -- Nothing
  , show $ readFooInt  "11"  -- Just Bag
  , show $ readFooBool "0"   -- Nothing
  , show $ readFooBool "10"  -- Just Baz
  , show $ readFooBool "11"  -- Just Bag
  ]

-- With existential types
--
-- readFoo1 :: String -> Ex Foo1

data Foo1 (a :: Type) where
  Bar1 :: Foo1 Int
  Baz1 :: Foo1 Bool
  Bag1 :: Foo1 a

deriving instance Show (Foo1 a)
deriveGenericK ''Foo1

data Ex (f :: k -> Type) where
  Ex :: f a -> Ex f

xmap :: (forall a. f a -> g a) -> Ex f -> Ex g
xmap f (Ex x) = Ex (f x)

deriving instance (forall a. Show (f a)) => Show (Ex f)

data KEx (f :: LoT (k -> Type) -> Type) where
  KEx :: f (p :&&: LoT0) -> KEx f

rxmap :: (forall p. f (p :&&: LoT0) -> g (p :&&: LoT0)) -> KEx f -> KEx g
rxmap f (KEx x) = KEx (f x)

kexToEx :: (forall a. GenericK f (a :&&: LoT0)) => KEx (RepK f) -> Ex f
kexToEx (KEx x) = Ex (toK x)

class GReadEx (f :: LoT (k -> Type) -> Type) where
  greadex :: String -> Maybe (KEx f)

instance GReadEx f => GReadEx (M1 i c f) where
  greadex = fmap (rxmap M1) . greadex

instance (GReadEx f, GReadEx g) => GReadEx (f :+: g) where
  greadex ('0' : s) = fmap (rxmap L1) (greadex s)
  greadex ('1' : s) = fmap (rxmap R1) (greadex s)
  greadex _ = Nothing

instance
  ( Interpret c (TypeIndex c :&&: LoT0)
  , GRead f (TypeIndex c :&&: LoT0)
  ) => GReadEx (c :=>: f) where
  greadex s = fmap (KEx . SuchThat) (gread @f @(TypeIndex c :&&: LoT0) s)

instance GReadEx U1 where
  greadex _ = Just (KEx U1)

type family TypeIndex (c :: Atom (k -> Type) Constraint) :: k where
  TypeIndex (Var0 :~~: 'Kon t) = t

genericReadEx ::
  forall f.
  ((forall a. GenericK f (a :&&: LoT0)), GReadEx (RepK f)) =>
  String -> Maybe (Ex f)
genericReadEx = fmap kexToEx . greadex @_ @(RepK f)

readFoo1 :: String -> Maybe (Ex Foo1)
readFoo1 = genericReadEx

example1 :: [String]
example1 =
  [ show $ readFoo1 "0"   -- Just (Ex Bar1)
  , show $ readFoo1 "10"  -- Just (Ex Baz1)
  , show $ readFoo1 "11"  -- Just (Ex Bag1)
  ]