{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T15725 where

import Data.Functor.Identity (Identity(..))
import Data.Kind (Type)
import GHC.Exts (Any)

-----
-- The important bits
-----

type instance Meth (x :: Identity a) = GenericMeth x
instance SC Identity

-------------------------------------------------------------------------------

data family Sing :: forall k. k -> Type
data instance Sing :: forall a. Identity a -> Type where
  SIdentity :: Sing x -> Sing ('Identity x)

newtype Par1 p = Par1 p
data instance Sing :: forall p. Par1 p -> Type where
  SPar1 :: Sing x -> Sing ('Par1 x)

type family Rep1 (f :: Type -> Type) :: Type -> Type

class PGeneric1 (f :: Type -> Type) where
  type From1 (z :: f a)      :: Rep1 f a
  type To1   (z :: Rep1 f a) :: f a

class SGeneric1 (f :: Type -> Type) where
  sFrom1 :: forall (a :: Type) (z :: f a).      Sing z -> Sing (From1 z)
  sTo1   :: forall (a :: Type) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)

type instance Rep1 Identity = Par1

instance PGeneric1 Identity where
  type From1 ('Identity x) = 'Par1 x
  type To1   ('Par1 x)     = 'Identity x

instance SGeneric1 Identity where
  sFrom1 (SIdentity x) = SPar1 x
  sTo1 (SPar1 x) = SIdentity x

type family GenericMeth (x :: f a) :: f a where
  GenericMeth x = To1 (Meth (From1 x))

type family Meth (x :: f a) :: f a

class SC f where
  sMeth         :: forall a (x :: f a).
                   Sing x -> Sing (Meth x)
  default sMeth :: forall a (x :: f a).
                   ( SGeneric1 f, SC (Rep1 f)
                   , Meth x ~ GenericMeth x
                   )
                => Sing x -> Sing (Meth x)
  sMeth sx = sTo1 (sMeth (sFrom1 sx))

  dummy :: f a -> ()
  dummy _ = ()

type instance Meth (x :: Par1 p) = x
instance SC Par1 where
  sMeth x = x