Safe Haskell	Safe-Inferred
Language	GHC2021

TypeLevelShow.Doc

Contents

Term level
Type level
Singleton

Synopsis

data Doc s
- = Text s
- | (Doc s) :<>: (Doc s)
- | (Doc s) :$$: (Doc s)
renderDoc :: Doc String -> String
type PDoc = Doc Symbol
type family RenderPDoc doc where ...
type family ErrorPDoc doc where ...
data SDoc (doc :: PDoc) where
- SText :: SSymbol s -> SDoc (Text s)
- (:$<>:) :: SDoc docl -> SDoc docr -> SDoc (docl :<>: docr)
- (:$$$:) :: SDoc docl -> SDoc docr -> SDoc (docl :$$: docr)
class SingDoc (doc :: PDoc) where
- singDoc :: SDoc doc
demoteDoc :: SDoc doc -> Doc String
reifyDoc :: forall (doc :: PDoc). SingDoc doc => Doc String
errorPDoc :: forall (doc :: PDoc) a. SingDoc doc => a

Term level

data Doc s Source #

Simple pretty document ADT.

Designed to work on both type level (as a limited ErrorMessage) and term level (as a boring ADT).

Note that ShowType is magical (see compilerGHCCore/Type.hs#L1309), so we need to remove it for term level.

singletons-base defines a version of this, but retains the ShowType constructor and is in the singletons ecosystem.

Constructors

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)

Instances

Instances details

Demotable SDoc Source #
Instance details Defined in TypeLevelShow.Doc Associated Types type Demote SDoc # Methods demote :: forall (k1 :: k). SDoc k1 -> Demote SDoc #
SingDoc doc => SingI (doc :: PDoc) Source #
Instance details Defined in TypeLevelShow.Doc Associated Types type Sing :: k -> Type # Methods sing' :: Sing doc #
Show s => Show (Doc s) Source #
Instance details Defined in TypeLevelShow.Doc Methods showsPrec :: Int -> Doc s -> ShowS # show :: Doc s -> String # showList :: [Doc s] -> ShowS #
type Sing Source #
Instance details Defined in TypeLevelShow.Doc type Sing = SDoc
type Demote SDoc Source #
Instance details Defined in TypeLevelShow.Doc type Demote SDoc = Doc String

renderDoc :: Doc String -> String Source #

Render a Doc as a String, formatted how ErrorMessages get displayed.

Type level

type PDoc = Doc Symbol Source #

Promoted Doc.

type family RenderPDoc doc where ... Source #

Render a PDoc as an ErrorMessage, for type-level error messages.

PDoc is a subset of ErrorMessage, so this is very boring.

Equations

RenderPDoc (Text s) = Text s
RenderPDoc (l :<>: r) = RenderPDoc l :<>: RenderPDoc r
RenderPDoc (l :$$: r) = RenderPDoc l :$$: RenderPDoc r

type family ErrorPDoc doc where ... Source #

Render a PDoc as an ErrorMessage, and wrap it in a TypeError.

Note that this must be a type family, or the PDoc won't actually get rendered.

Equations

ErrorPDoc doc = TypeError (RenderPDoc doc)

Singleton

data SDoc (doc :: PDoc) where Source #

Singleton Doc.

Constructors

SText :: SSymbol s -> SDoc (Text s)
(:$<>:) :: SDoc docl -> SDoc docr -> SDoc (docl :<>: docr)
(:$$$:) :: SDoc docl -> SDoc docr -> SDoc (docl :$$: docr)

Instances

Instances details

Demotable SDoc Source #
Instance details Defined in TypeLevelShow.Doc Associated Types type Demote SDoc # Methods demote :: forall (k1 :: k). SDoc k1 -> Demote SDoc #
type Demote SDoc Source #
Instance details Defined in TypeLevelShow.Doc type Demote SDoc = Doc String

class SingDoc (doc :: PDoc) where Source #

Produce the singleton for the given promoted Doc.

Methods

singDoc :: SDoc doc Source #

Instances

Instances details

KnownSymbol s => SingDoc ('Text s) Source #
Instance details Defined in TypeLevelShow.Doc Methods singDoc :: SDoc ('Text s) Source #
(SingDoc l, SingDoc r) => SingDoc (l ':$$: r) Source #
Instance details Defined in TypeLevelShow.Doc Methods singDoc :: SDoc (l ':$$: r) Source #
(SingDoc l, SingDoc r) => SingDoc (l ':<>: r) Source #
Instance details Defined in TypeLevelShow.Doc Methods singDoc :: SDoc (l ':<>: r) Source #

demoteDoc :: SDoc doc -> Doc String Source #

Demote an SDoc singleton to the corresponding base Doc.

reifyDoc :: forall (doc :: PDoc). SingDoc doc => Doc String Source #

Reify a promoted Doc to the corresponding term-level one.

errorPDoc :: forall (doc :: PDoc) a. SingDoc doc => a Source #

Render a PDoc as a String, and call error on it.

This enables using the same code for type- and term- "runtime" errors. This can't be typechecked, naturally, but it's still nice.