{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Nub where

import Data.Proxy
import Data.Type.Bool
import GHC.TypeLits

-- | Check whether a type is a member of a list of types.
-- This is a type-level analogue of @'elem'@.
type family Elem x xs where
  Elem x '[] = 'False
  Elem x (x ': xs) = 'True
  Elem x (y ': xs) = Elem x xs

-- | Remove duplicates from a type-level list.
type family Nub xs where
  Nub '[] = '[]
  Nub (x ': xs) = If (Elem x xs) (Nub xs) (x ': Nub xs)

class KnownNats ns where
  natVals :: proxy ns -> [Integer]

instance KnownNats '[] where
  natVals _ = []

instance (KnownNat n, KnownNats ns) => KnownNats (n ': ns) where
  natVals _ = natVal (Proxy :: Proxy n) : natVals (Proxy :: Proxy ns)

type Example = '[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 1, 1, 1, 1, 1]

exampleVals :: [Integer]
exampleVals = natVals (Proxy :: Proxy (Nub Example))