{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK not-home #-}

-- | This module is intended for internal use only, and may change without
-- warning in subsequent releases.
module Optics.Internal.Optic.TypeLevel where

import Data.Kind
import GHC.TypeLits

-- | A list of index types, used for indexed optics.
--
-- @since 0.2
type IxList = [Type]

-- | An alias for an empty index-list
type NoIx = ('[] :: IxList)

-- | Singleton index list
type WithIx i = ('[i] :: IxList)

----------------------------------------
-- Elimination forms in error messages

type family ShowSymbolWithOrigin symbol origin :: ErrorMessage where
  ShowSymbolWithOrigin symbol origin = 'Text "  "
                                 ':<>: QuoteSymbol symbol
                                 ':<>: 'Text " (from "
                                 ':<>: 'Text origin
                                 ':<>: 'Text ")"

type family ShowSymbolsWithOrigin (fs :: [(Symbol, Symbol)]) :: ErrorMessage where
  ShowSymbolsWithOrigin '[ '(symbol, origin) ] =
    ShowSymbolWithOrigin symbol origin
  ShowSymbolsWithOrigin ('(symbol, origin) ': rest) =
    ShowSymbolWithOrigin symbol origin ':$$: ShowSymbolsWithOrigin rest

type family ShowOperators (ops :: [Symbol]) :: ErrorMessage where
  ShowOperators '[op] =
    QuoteSymbol op ':<>: 'Text " (from Optics.Operators)"
  ShowOperators (op ': rest) =
    QuoteSymbol op ':<>: 'Text " " ':<>: ShowOperators rest

type family AppendEliminations a b where
  AppendEliminations '(fs1, ops1) '(fs2, ops2) =
    '(Append fs1 fs2, Append ops1 ops2)

type family ShowEliminations forms :: ErrorMessage where
  ShowEliminations '(fs, ops) =
    ShowSymbolsWithOrigin fs ':$$: 'Text "  " ':<>: ShowOperators ops

----------------------------------------
-- Lists

-- | Reverse a type-level list.
type family Reverse (xs :: [k]) (acc :: [k]) :: [k] where
  Reverse '[]      acc = acc
  Reverse (x : xs) acc = Reverse xs (x : acc)

-- | Curry a type-level list.
--
-- In pseudo (dependent-)Haskell:
--
-- @
-- 'Curry' xs y = 'foldr' (->) y xs
-- @
type family Curry (xs :: IxList) (y :: Type) :: Type where
  Curry '[]       y = y
  Curry (x ': xs) y = x -> Curry xs y

-- | Append two type-level lists together.
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
  Append '[]       ys  = ys -- needed for (<%>) and (%>)
  Append xs        '[] = xs -- needed for (<%)
  Append (x ': xs) ys  = x ': Append xs ys

-- | Class that is inhabited by all type-level lists @xs@, providing the ability
-- to compose a function under @'Curry' xs@.
class CurryCompose xs where
  -- | Compose a function under @'Curry' xs@.  This generalises @('.')@ (aka
  -- 'fmap' for @(->)@) to work for curried functions with one argument for each
  -- type in the list.
  composeN :: (i -> j) -> Curry xs i -> Curry xs j

instance CurryCompose '[] where
  composeN :: forall i j. (i -> j) -> Curry '[] i -> Curry '[] j
composeN = forall a. a -> a
id

instance CurryCompose xs => CurryCompose (x ': xs) where
  composeN :: forall i j. (i -> j) -> Curry (x : xs) i -> Curry (x : xs) j
composeN i -> j
ij Curry (x : xs) i
f = forall (xs :: IxList) i j.
CurryCompose xs =>
(i -> j) -> Curry xs i -> Curry xs j
composeN @xs i -> j
ij forall b c a. (b -> c) -> (a -> b) -> a -> c
. Curry (x : xs) i
f

----------------------------------------
-- Indices

-- | Tagged version of 'Data.Type.Equality.(:~:)' for carrying evidence that two
-- index lists in a curried form are equal.
data IxEq i is js where
  IxEq :: IxEq i is is

-- | In pseudo (dependent-)Haskell, provide a witness
--
-- @
-- foldr f (foldr f init xs) ys = foldr f init (ys ++ xs)
--    where f = (->)
-- @
--
-- @since 0.4
--
class AppendIndices xs ys ks | xs ys -> ks where
  appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i)

-- | If the second list is empty, we can pick the first list
-- even if nothing is known about it.
instance {-# INCOHERENT #-} xs ~ zs => AppendIndices xs '[] zs where
  appendIndices :: forall i. IxEq i (Curry xs (Curry '[] i)) (Curry zs i)
appendIndices = forall {k} {k} (i :: k) (is :: k). IxEq i is is
IxEq

instance ys ~ zs => AppendIndices '[] ys zs where
  appendIndices :: forall i. IxEq i (Curry '[] (Curry ys i)) (Curry zs i)
appendIndices = forall {k} {k} (i :: k) (is :: k). IxEq i is is
IxEq

instance AppendIndices xs ys ks => AppendIndices (x ': xs) ys (x ': ks) where
  appendIndices :: forall i. IxEq i (Curry (x ': xs) (Curry ys i)) (Curry (x ': ks) i)
  appendIndices :: forall i. IxEq i (Curry (x : xs) (Curry ys i)) (Curry (x : ks) i)
appendIndices | IxEq i (Curry xs (Curry ys i)) (Curry ks i)
IxEq <- forall (xs :: IxList) (ys :: IxList) (ks :: IxList) i.
AppendIndices xs ys ks =>
IxEq i (Curry xs (Curry ys i)) (Curry ks i)
appendIndices @xs @ys @ks @i = forall {k} {k} (i :: k) (is :: k). IxEq i is is
IxEq

----------------------------------------
-- Either

-- | If lhs is 'Right', return it. Otherwise check rhs.
type family FirstRight (m1 :: Either e a) (m2 :: Either e a) :: Either e a where
  FirstRight ('Right a) _ = 'Right a
  FirstRight          _ b = b

type family FromRight (def :: b) (e :: Either a b) :: b where
  FromRight _   ('Right b) = b
  FromRight def ('Left  _) = def

type family IsLeft (e :: Either a b) :: Bool where
  IsLeft ('Left _)  = 'True
  IsLeft ('Right _) = 'False

----------------------------------------
-- Errors

-- | Show a custom type error if @p@ is true.
type family When (p :: Bool) (err :: Constraint) :: Constraint where
  When 'True  err = err
  When 'False _   = ()

-- | Show a custom type error if @p@ is false (or stuck).
type family Unless (p :: Bool) (err :: Constraint) :: Constraint where
  Unless 'True  _   = ()
  Unless 'False err = err

-- | Use with 'Unless' to detect stuck (undefined) type families.
type family Defined (f :: k) :: Bool where
  Defined (f _) = Defined f
  Defined _     = 'True

-- | Show a type surrounded by quote marks.
type family QuoteType (x :: t) :: ErrorMessage where
  QuoteType x = 'Text "‘" ':<>: 'ShowType x ':<>: 'Text "’"

-- | Show a symbol surrounded by quote marks.
type family QuoteSymbol (x :: Symbol) :: ErrorMessage where
  QuoteSymbol x = 'Text "‘" ':<>: 'Text x ':<>: 'Text "’"

type family ToOrdinal (n :: Nat) :: ErrorMessage where
  ToOrdinal 1 = 'Text "1st"
  ToOrdinal 2 = 'Text "2nd"
  ToOrdinal 3 = 'Text "3rd"
  ToOrdinal n = 'ShowType n ':<>: 'Text "th"

----------------------------------------
-- Misc

-- | Derive the shape of @a@ from the shape of @b@.
class HasShapeOf (a :: k) (b :: k)
instance {-# OVERLAPPING #-} (fa ~ f a, HasShapeOf f g) => HasShapeOf fa (g b)
instance (a ~ b) => HasShapeOf a b