{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE LambdaCase              #-}
{-# LANGUAGE PatternSynonyms         #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}
module T15517a () where

import Data.Kind (Type)
import Data.Proxy

newtype Rep (ki :: kon -> Type) (phi :: Nat -> Type) (code :: [[Atom kon]])
  = Rep (NS (PoA ki phi) code)

data NA  :: (kon -> Type) -> (Nat -> Type) -> Atom kon -> Type where
  NA_I :: (IsNat k) => phi k -> NA ki phi (I k)
  NA_K ::              ki  k -> NA ki phi (K k)

data NP :: (k -> Type) -> [k] -> Type where
  NP0  :: NP p '[]
  (:*) :: p x -> NP p xs -> NP p (x : xs)

class IsNat (n :: Nat) where
  getSNat :: Proxy n -> SNat n
instance IsNat Z where
  getSNat _ = SZ
instance IsNat n => IsNat (S n) where
  getSNat p = SS (getSNat $ proxyUnsuc p)

proxyUnsuc :: Proxy (S n) -> Proxy n
proxyUnsuc _ = Proxy

type PoA (ki :: kon -> Type) (phi :: Nat -> Type) = NP (NA ki phi)

data Atom kon
  = K kon
  | I Nat

data Nat = S Nat | Z
data SNat :: Nat -> Type where
  SZ ::           SNat Z
  SS :: SNat n -> SNat (S n)

data Kon = KInt
data Singl (kon :: Kon) :: Type where
  SInt :: Int -> Singl KInt

type family Lkup (n :: Nat) (ks :: [k]) :: k where
  Lkup Z     (k : ks) = k
  Lkup (S n) (k : ks) = Lkup n ks

data El :: [Type] -> Nat -> Type where
  El :: IsNat ix => Lkup ix fam -> El fam ix

data NS :: (k -> Type) -> [k] -> Type where
  There :: NS p xs -> NS p (x : xs)
  Here  :: p x     -> NS p (x : xs)

class Family (ki :: kon -> Type) (fam :: [Type]) (codes :: [[[Atom kon]]])
      | fam -> ki codes , ki codes -> fam where
    sfrom' :: SNat ix -> El fam ix -> Rep ki (El fam) (Lkup ix codes)

data Rose a = a :>: [Rose a]
            | Leaf a

type FamRoseInt = '[Rose Int, [Rose Int]]

type CodesRoseInt =
    '[ '[ '[K KInt, I (S Z)], '[K KInt]], '[ '[], '[I Z, I (S Z)]]]

pattern IdxRoseInt = SZ
pattern IdxListRoseInt = SS SZ

pat1 :: PoA Singl (El FamRoseInt) '[I Z, I (S Z)]
     -> NS (PoA Singl (El FamRoseInt)) '[ '[], '[I Z, I (S Z)]]
pat1 d = There (Here d)

pat2 :: PoA Singl (El FamRoseInt) '[]
     -> NS (PoA Singl (El FamRoseInt)) '[ '[], '[I Z, I (S Z)]]
pat2 d = Here d

pat3 :: PoA Singl (El FamRoseInt) '[K KInt]
     -> NS (PoA Singl (El FamRoseInt)) '[ '[K KInt, I (S Z)], '[K KInt]]
pat3 d = There (Here d)

pat4 :: PoA Singl (El FamRoseInt) '[K KInt, I (S Z)]
     -> NS (PoA Singl (El FamRoseInt)) '[ '[K KInt, I (S Z)], '[K KInt]]
pat4 d = Here d

instance Family Singl FamRoseInt CodesRoseInt where
  sfrom' = \case IdxRoseInt     -> \case El (x :>: xs) -> Rep (pat4 (NA_K (SInt x) :* (NA_I (El xs) :* NP0)))
                                         El (Leaf x)   -> Rep (pat3 (NA_K (SInt x) :* NP0))
                 IdxListRoseInt -> \case El []     -> Rep (pat2 NP0)
                                         El (x:xs) -> Rep (pat1 (NA_I (El x) :* (NA_I (El xs) :* NP0)))