content: {-# LANGUAGE GADTs #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE ViewPatterns #-}
  module T13750a where
  
  import Data.Kind (Type)
  import Unsafe.Coerce
  
  type family AnyT :: Type where {}
  type family AnyList :: [Type] where {}
  
  newtype NP (xs :: [Type]) = NP [AnyT]
  
  data IsNP (xs :: [Type]) where
    IsNil  :: IsNP '[]
    IsCons :: x -> NP xs -> IsNP (x ': xs)
  
  isNP :: NP xs -> IsNP xs
  isNP (NP xs) =
    if null xs
      then unsafeCoerce IsNil
      else unsafeCoerce (IsCons (head xs) (NP (tail xs)))
  
  pattern Nil :: () => (xs ~ '[]) => NP xs
  pattern Nil <- (isNP -> IsNil)
    where
      Nil = NP []
  
  pattern (:*) :: () => (xs' ~ (x ': xs)) => x -> NP xs -> NP xs'
  pattern x :* xs <- (isNP -> IsCons x xs)
    where
      x :* NP xs = NP (unsafeCoerce x : xs)
  infixr 5 :*
  
  data NS (xs :: [[Type]]) = NS !Int (NP AnyList)
  
  data IsNS (xs :: [[Type]]) where
    IsZ :: NP x -> IsNS (x ': xs)
    IsS :: NS xs -> IsNS (x ': xs)
  
  isNS :: NS xs -> IsNS xs
  isNS (NS i x)
    | i == 0    = unsafeCoerce (IsZ (unsafeCoerce x))
    | otherwise = unsafeCoerce (IsS (NS (i - 1) x))
  
  pattern Z :: () => (xs' ~ (x ': xs)) => NP x -> NS xs'
  pattern Z x <- (isNS -> IsZ x)
    where
      Z x = NS 0 (unsafeCoerce x)
  
  pattern S :: () => (xs' ~ (x ': xs)) => NS xs -> NS xs'
  pattern S p <- (isNS -> IsS p)
  