Generic parser for GADT with kind-generics

GadtRead.hs

{-# LANGUAGE
    AllowAmbiguousTypes,
    TypeApplications,
    ScopedTypeVariables,
    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

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

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  "1"  -- Nothing
  , show $ readFooBool "0"  -- Nothing
  , show $ readFooBool "1"  -- Just Baz
  ]