{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

{-# OPTIONS_HADDOCK not-home #-}

-- | Description: Singleton list
module Polysemy.Internal.Sing where

import GHC.TypeLits (Nat, type (-))

import Polysemy.Internal.Kind (Effect)

------------------------------------------------------------------------------
-- | A singleton type used as a witness for type-level lists.
data SList l where
  SEnd  :: SList '[]
  SCons :: SList xs -> SList (x ': xs)

------------------------------------------------------------------------------
-- | A singleton list constructor class.
class KnownList l where
  singList :: SList l

instance KnownList '[] where
  singList :: SList '[]
singList = SList '[]
forall k. SList '[]
SEnd
  {-# INLINE singList #-}

instance KnownList xs => KnownList (x ': xs) where
  singList :: SList (x : xs)
singList = SList xs -> SList (x : xs)
forall {k} (xs :: [k]) (x :: k). SList xs -> SList (x : xs)
SCons SList xs
forall {k} (l :: [k]). KnownList l => SList l
singList
  {-# INLINE singList #-}

------------------------------------------------------------------------------
-- | A utility class for constructing a type-level list of a given length.
class ListOfLength (n :: Nat) (l :: [Effect]) where
  listOfLength :: SList l

instance {-# OVERLAPPING #-} (l ~ '[]) => ListOfLength 0 l where
  listOfLength :: SList l
listOfLength = SList l
SList '[]
forall k. SList '[]
SEnd
  {-# INLINE listOfLength #-}

instance (ListOfLength (n - 1) xs, l ~ (x ': xs)) => ListOfLength n l where
  listOfLength :: SList l
listOfLength = SList xs -> SList (x : xs)
forall {k} (xs :: [k]) (x :: k). SList xs -> SList (x : xs)
SCons (forall (n :: Nat) (l :: [Effect]). ListOfLength n l => SList l
listOfLength @(n - 1))
  {-# INLINE listOfLength #-}