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

{-# OPTIONS_HADDOCK not-home #-}

module Polysemy.Internal.Sing where

import GHC.TypeLits (type (-), Nat)
import Polysemy.Internal.Kind (Effect)

data SList l where
  SEnd  :: SList '[]
  SCons :: SList xs -> SList (x ': xs)

class KnownList l where
  singList :: SList l

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

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

class ListOfLength (n :: Nat) (l :: [Effect]) where
  listOfLength :: SList l

instance {-# OVERLAPPING #-} (l ~ '[]) => ListOfLength 0 l where
  listOfLength :: SList l
listOfLength = SList l
forall a. 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 a (xs :: [a]) (x :: a). SList xs -> SList (x : xs)
SCons (forall (l :: [Effect]). ListOfLength (n - 1) l => SList l
forall (n :: Nat) (l :: [Effect]). ListOfLength n l => SList l
listOfLength @(n - 1))
  {-# INLINE listOfLength #-}