{-# LANGUAGE AllowAmbiguousTypes #-} -- for reifying

module TypeLevelShow.Doc where

import GHC.TypeLits qualified as TE -- TE = TypeError
import GHC.TypeLits ( Symbol, KnownSymbol, symbolVal' )
import GHC.Exts ( proxy# )

-- | Simple pretty document ADT.
--
-- Designed to work on both type level (as a limited 'TE.ErrorMessage') and term
-- level (as a boring ADT).
--
-- Note that 'TE.ShowType' is magical (see
-- @compiler/GHC/Core/Type.hs#L1309@), so we need to remove it for term level.
--
-- singletons-base defines a version of this, but retains the 'TE.ShowType'
-- constructor and is in the singletons ecosystem.
data Doc s
  = Text s
  -- ^ plain ol' text
  | Doc s :<>: Doc s
  -- ^ append docs next to each other
  | Doc s :$$: Doc s
  -- ^ stack docs on top of each other (newline)
    deriving stock Int -> Doc s -> ShowS
[Doc s] -> ShowS
Doc s -> String
(Int -> Doc s -> ShowS)
-> (Doc s -> String) -> ([Doc s] -> ShowS) -> Show (Doc s)
forall s. Show s => Int -> Doc s -> ShowS
forall s. Show s => [Doc s] -> ShowS
forall s. Show s => Doc s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall s. Show s => Int -> Doc s -> ShowS
showsPrec :: Int -> Doc s -> ShowS
$cshow :: forall s. Show s => Doc s -> String
show :: Doc s -> String
$cshowList :: forall s. Show s => [Doc s] -> ShowS
showList :: [Doc s] -> ShowS
Show

-- | Promoted 'Doc'.
type PDoc = Doc Symbol

-- | Render a 'PDoc' as an 'ErrorMessage', for type-level error messages.
--
-- 'PDoc' is a subset of 'ErrorMessage', so this is very boring.
type RenderDoc :: PDoc -> TE.ErrorMessage
type family RenderDoc doc where
    RenderDoc (Text s)   = TE.Text s
    RenderDoc (l :<>: r) = RenderDoc l TE.:<>: RenderDoc r
    RenderDoc (l :$$: r) = RenderDoc l TE.:$$: RenderDoc r

-- | Reify a promoted 'Doc' to the corresponding term-level one.
class ReifyDoc (doc :: PDoc) where
    -- TODO do we want to do IsString directly in here? will it guarantee better
    --      performance, rather than mapping afterwards? hard to say
    reifyDoc :: Doc String

instance KnownSymbol s => ReifyDoc (Text s) where
    reifyDoc :: Doc String
reifyDoc = String -> Doc String
forall s. s -> Doc s
Text (String -> Doc String) -> String -> Doc String
forall a b. (a -> b) -> a -> b
$ Proxy# s -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' (forall {k} (a :: k). Proxy# a
forall (a :: Symbol). Proxy# a
proxy# @s)

instance (ReifyDoc l, ReifyDoc r) => ReifyDoc (l :<>: r) where
    reifyDoc :: Doc String
reifyDoc = forall (doc :: PDoc). ReifyDoc doc => Doc String
reifyDoc @l Doc String -> Doc String -> Doc String
forall s. Doc s -> Doc s -> Doc s
:<>: forall (doc :: PDoc). ReifyDoc doc => Doc String
reifyDoc @r

instance (ReifyDoc l, ReifyDoc r) => ReifyDoc (l :$$: r) where
    reifyDoc :: Doc String
reifyDoc = forall (doc :: PDoc). ReifyDoc doc => Doc String
reifyDoc @l Doc String -> Doc String -> Doc String
forall s. Doc s -> Doc s -> Doc s
:$$: forall (doc :: PDoc). ReifyDoc doc => Doc String
reifyDoc @r