{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}
import Unsafe.Coerce (unsafeCoerce)
import GHC.TypeLits
-- class Foo r
-- instance Ord a => Foo a

data D (is :: [Nat]) = D
 deriving Show

type family Count (i :: Nat) (xs :: [Nat]) :: [Nat] where
  Count i '[] = '[]
  Count i (x ': xs) = i ': Count (i+1) xs

class AllElem (is :: [Nat]) (ns :: [Nat])
instance AllElem '[] ns
instance (Elem i ns, AllElem is ns) => AllElem (i ': is) ns
class Elem (i :: Nat) (ns :: [Nat])
instance (Elem' (CmpNat i n) i ns) => Elem i (n : ns)
class Elem' (e :: Ordering) (i :: Nat) (ns :: [Nat])
instance Elem' 'EQ i ns
instance (Elem i ns) => Elem' 'LT i ns
instance (Elem i ns) => Elem' 'GT i ns

class Permutation (is :: [Nat])
instance (AllElem is (Count 0 is)) => Permutation is

f :: Permutation is => D is -> D is
f d = d

g :: D is -> D is
-- g d = unsafeCoerce f d
g d = (unsafeCoerce (f :: forall is. Permutation is => D is -> D is) :: D is -> D is) d
-- g x = (unsafeCoerce (f :: Int -> Int) :: Eq a => a -> a) x

main = print $ show $ g D