{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies, AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilyDependencies, FlexibleContexts, MultiParamTypeClasses, Rank2Types #-}
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Internal.Data.Basic.TypeLevel
    ( AllSatisfy, MappableList(..), Elem, EqualOrError, CheckWithError
    , Not, ErrorText, type (++), Without, IsSubset, TypeSatisfies
    , OnMaybe, NotNull, ListToTuple
    , GHC.ErrorMessage(ShowType, (:<>:), (:$$:))
    , GHC.TypeError
    )  where

import Internal.Interlude

import GHC.TypeLits
import qualified GHC.TypeLits as GHC

type family AllSatisfy (c :: k -> Constraint) (l :: [k]) :: Constraint where
    AllSatisfy c '[] = ()
    AllSatisfy c (x ': xs) = (c x, AllSatisfy c xs)

class MappableList (l :: [k]) where
    mapTypeList :: AllSatisfy c l => proxy1 c -> (forall proxy2 x. c x => proxy2 x -> a) -> proxy3 l -> [a]

instance MappableList '[] where
    mapTypeList _ _ _ = []

instance MappableList ks => MappableList (k ': ks) where
    mapTypeList pc f _ = f (Proxy :: Proxy k) : mapTypeList pc f (Proxy :: Proxy ks)

type family Elem (x :: k) (xs :: [k]) :: Bool where
    Elem x '[] = 'False
    Elem x (x ': xs) = 'True
    Elem x (y ': xs) = Elem x xs

type family EqualOrError (a :: k) (b :: k) (err :: ErrorMessage) :: Constraint where
    EqualOrError a a err = ()
    EqualOrError a b err = GHC.TypeError err

type ErrorText = 'GHC.Text

type CheckWithError (b :: Bool) (err :: ErrorMessage) = EqualOrError b 'True err

type family Not (b :: Bool) where
    Not 'True = 'False
    Not 'False = 'True

type family IsSubset xs ys :: Constraint where
    IsSubset '[] ys = ()
    IsSubset (x ': xs) ys = (IsTrue (Elem x ys), IsSubset xs ys)

type IsTrue b = b ~ 'True

type family If (condition :: Bool) (t :: k) (e :: k) :: k where
    If 'True t e = t
    If 'False t e = e

type family Without (xs :: [k]) (ys :: [k]) :: [k] where
    Without xs '[] = xs
    Without '[] ys = '[]
    Without (x ': xs) ys = If (x `Elem` ys) (Without xs ys) (x ': Without xs ys)

type family NotMaybe (a :: *) :: Bool where
    NotMaybe (Maybe a) = 'False
    NotMaybe a = 'True

type FieldNullErr field =
    ErrorText "The field " ':<>: 'ShowType field ':<>: ErrorText " must not be optional (Maybe/Null)"
class CheckWithError (NotMaybe a) (FieldNullErr field) => NotNull (a :: *) (field :: Symbol)
instance CheckWithError (NotMaybe a) (FieldNullErr field) => NotNull a field

type family OnMaybe (a :: k) (f :: b -> k) (m :: Maybe b) :: k where
    OnMaybe a f ('Just b) = f b
    OnMaybe a f 'Nothing = a

type family FromJust (a :: Maybe x) :: x where
    FromJust ('Just x) = x

class c x => TypeSatisfies (c :: * -> Constraint) (x :: *) (field :: Symbol)
instance c x => TypeSatisfies c x field

type family ListToTuple (f :: k -> *) (l :: [k]) where
    ListToTuple f '[] = ()
    ListToTuple f '[a] = f a
    ListToTuple f '[a, b] = (f a, f b)
    ListToTuple f '[a, b, c] = (f a, f b, f c)
    ListToTuple f '[a, b, c, d] = (f a, f b, f c, f d)
    ListToTuple f '[a, b, c, d, e] = (f a, f b, f c, f d, f e)

type family xs ++ ys where
    '[] ++ ys = ys
    (x ': xs) ++ ys = x ': (xs ++ ys)