{-# LANGUAGE UndecidableInstances #-} -- for recursive SingI constraints

-- Orphan instances when we define them elsewhere, so here they shall stay.

module Singleraeh.SingI where

import Data.Kind ( Type )
import GHC.TypeLits

import Singleraeh.Bool
import Singleraeh.Tuple
import Singleraeh.Either
import Singleraeh.Maybe

class SingI (a :: k) where
    type Sing :: k -> Type
    sing' :: Sing a

sing :: forall {k} (a :: k). SingI a => Sing a
sing :: forall {k} (a :: k). SingI a => Sing a
sing = forall {k} (a :: k). SingI a => Sing a
sing' @_ @a

instance KnownNat n => SingI n where
    type Sing = SNat
    sing' :: Sing n
sing' = SNat n
Sing n
forall (n :: Nat). KnownNat n => SNat n
SNat

instance KnownSymbol str => SingI str where
    type Sing = SSymbol
    sing' :: Sing str
sing' = SSymbol str
Sing str
forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol

instance KnownChar ch => SingI ch where
    type Sing = SChar
    sing' :: Sing ch
sing' = SChar ch
Sing ch
forall (c :: Char). KnownChar c => SChar c
SChar

instance SingBool b => SingI b where
    type Sing = SBool
    sing' :: Sing b
sing' = SBool b
Sing b
forall (b :: Bool). SingBool b => SBool b
singBool

instance SingTuple2 SingI SingI Sing Sing lr => SingI lr where
    type Sing = STuple2 Sing Sing
    sing' :: Sing lr
sing' = forall {a} {b} (cl :: a -> Constraint) (cr :: b -> Constraint)
       (sl :: a -> Type) (sr :: b -> Type) (lr :: (a, b)).
SingTuple2 cl cr sl sr lr =>
(forall (l :: a). cl l => sl l)
-> (forall (r :: b). cr r => sr r) -> STuple2 sl sr lr
forall (cl :: lk -> Constraint) (cr :: rk -> Constraint)
       (sl :: lk -> Type) (sr :: rk -> Type) (lr :: (lk, rk)).
SingTuple2 cl cr sl sr lr =>
(forall (l :: lk). cl l => sl l)
-> (forall (r :: rk). cr r => sr r) -> STuple2 sl sr lr
singTuple2 @SingI @SingI Sing l
forall (l :: lk). SingI l => Sing l
forall {k} (a :: k). SingI a => Sing a
sing Sing r
forall (r :: rk). SingI r => Sing r
forall {k} (a :: k). SingI a => Sing a
sing

instance SingEither SingI SingI Sing Sing elr => SingI elr where
    type Sing = SEither Sing Sing
    sing' :: Sing elr
sing' = forall {l} {r} (cl :: l -> Constraint) (cr :: r -> Constraint)
       (sl :: l -> Type) (sr :: r -> Type) (elr :: Either l r).
SingEither cl cr sl sr elr =>
(forall (l1 :: l). cl l1 => sl l1)
-> (forall (r1 :: r). cr r1 => sr r1) -> SEither sl sr elr
forall (cl :: lk -> Constraint) (cr :: rk -> Constraint)
       (sl :: lk -> Type) (sr :: rk -> Type) (elr :: Either lk rk).
SingEither cl cr sl sr elr =>
(forall (l1 :: lk). cl l1 => sl l1)
-> (forall (r1 :: rk). cr r1 => sr r1) -> SEither sl sr elr
singEither @SingI @SingI Sing l1
forall (l1 :: lk). SingI l1 => Sing l1
forall {k} (a :: k). SingI a => Sing a
sing Sing r1
forall (r1 :: rk). SingI r1 => Sing r1
forall {k} (a :: k). SingI a => Sing a
sing

instance SingMaybe SingI Sing ma => SingI ma where
    type Sing = SMaybe Sing
    sing' :: Sing ma
sing' = forall {a} (ca :: a -> Constraint) (sa :: a -> Type)
       (ma :: Maybe a).
SingMaybe ca sa ma =>
(forall (a1 :: a). ca a1 => sa a1) -> SMaybe sa ma
forall (ca :: ak -> Constraint) (sa :: ak -> Type)
       (ma :: Maybe ak).
SingMaybe ca sa ma =>
(forall (a1 :: ak). ca a1 => sa a1) -> SMaybe sa ma
singMaybe @SingI Sing a1
forall (a1 :: ak). SingI a1 => Sing a1
forall {k} (a :: k). SingI a => Sing a
sing