content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  module T18747A where
  
  import Data.Kind
  import Data.Type.Equality
  
  type family Sing :: k -> Type
  data SomeSing :: Type -> Type where
    SomeSing :: Sing (a :: k) -> SomeSing k
  
  data SList :: forall a. [a] -> Type where
    SNil  :: SList '[]
    SCons :: Sing x -> Sing xs -> SList (x:xs)
  type instance Sing = SList
  
  data Univ = U1 | K1 Type | Sum Univ Univ | Product Univ Univ
  
  data SUniv :: Univ -> Type where
    SU1      ::                     SUniv U1
    SK1      :: Sing c           -> SUniv (K1 c)
    SSum     :: Sing a -> Sing b -> SUniv (Sum a b)
    SProduct :: Sing a -> Sing b -> SUniv (Product a b)
  type instance Sing = SUniv
  
  data In :: Univ -> Type where
    MkU1      ::                 In U1
    MkK1      :: c            -> In (K1 c)
    L1        :: In a         -> In (Sum a b)
    R1        ::         In b -> In (Sum a b)
    MkProduct :: In a -> In b -> In (Product a b)
  
  data SIn :: forall u. In u -> Type where
    SMkU1      ::                     SIn MkU1
    SMkK1      :: Sing c           -> SIn (MkK1 c)
    SL1        :: Sing a           -> SIn (L1 a)
    SR1        ::           Sing b -> SIn (R1 b)
    SMkProduct :: Sing a -> Sing b -> SIn (MkProduct a b)
  type instance Sing = SIn
  
  class Generic (a :: Type) where
    type Rep a :: Univ
    from :: a -> In (Rep a)
    to   :: In (Rep a) -> a
  
  class PGeneric (a :: Type) where
    type PFrom (x :: a)          :: In (Rep a)
    type PTo   (x :: In (Rep a)) :: a
  
  class SGeneric k where
    sFrom :: forall (a :: k).          Sing a -> Sing (PFrom a)
    sTo   :: forall (a :: In (Rep k)). Sing a -> Sing (PTo a :: k)
    sTof  :: forall (a :: k).          Sing a -> PTo (PFrom a) :~: a
    sFot  :: forall (a :: In (Rep k)). Sing a -> PFrom (PTo a :: k) :~: a
  
  instance Generic [a] where
    type Rep [a] = Sum U1 (Product (K1 a) (K1 [a]))
    from []     = L1 MkU1
    from (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
    to (L1 MkU1)                           = []
    to (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
  
  instance PGeneric [a] where
    type PFrom '[]    = L1 MkU1
    type PFrom (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
    type PTo (L1 MkU1)                           = '[]
    type PTo (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
  
  instance SGeneric [a] where
    sFrom SNil         = SL1 SMkU1
    sFrom (SCons x xs) = SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))
    sTo (SL1 SMkU1)                             = SNil
    sTo (SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))) = SCons x xs
    sTof SNil    = Refl
    sTof SCons{} = Refl
    sFot (SL1 SMkU1)                        = Refl
    sFot (SR1 (SMkProduct SMkK1{} SMkK1{})) = Refl
  