{-# LANGUAGE
  KindSignatures #-}

-- |

-- = First-class instances

--

-- Type classes are data types.

--

-- For example, this type class:

--

-- @

-- class Eq a where

--   (==) :: a -> a -> Bool

-- @

--

-- compiles into a dictionary type that looks like this:

--

-- @

-- data DictEq a = Eq

--   { (|==) :: a -> a -> Bool }

-- @

--

-- This library makes that correspondence explicit.

--

-- == Overview

--

-- Every constraint @c@ is associated to a dictionary type @Dict c@.

--

-- Examples:

--

-- @

-- 'FCI.Dict' 'Eq' = 'FCI.Base.DictEq'

-- 'FCI.Dict' 'Functor' = 'FCI.Base.DictFunctor'

-- @

--

-- == Generate dictionary types

--

-- Dictionary types must first be explicitly defined for each class, using 'mkDict'.

--

-- @

-- 'mkDict' ''Eq

--

-- -- expands to --

--

-- data DictEq a = Eq

--   { (|==) :: a -> a -> Bool }

--

-- type instance 'Dict' (Eq a) = DictEq a

-- @

--

-- == Declare instances from dictionaries

--

-- An instance declaration @Eq T@ can be created from a dictionary @d :: Dict (Eq T)@

-- (@d@ can be any expression), using 'instanceDict'.

--

-- @

-- 'instanceDict' [| d :: 'Dict' (Eq T) |]

-- @

--

-- == Reflect a constraint as a dictionary

--

-- Any constraint can be turned into a dictionary, manipulating it as a value, using 'dict'.

--

-- @

-- 'dict' \@c :: c => 'Dict' c

-- @

--

-- The inverse, reifying a dictionary into a constraint, would break coherence.

-- This is extremely unsafe. For experimental purposes, an implementation can be found in "FCI.Unsafe".

module FCI (
    -- * API

    Dict

    -- ** Generate dictionary types

  , mkDict

    -- ** Declare instances from dictionaries

  , instanceDict
  , instanceDict_
  , instanceDictM
  , Overlap(Overlappable, Overlapping, Overlaps, Incoherent)

    -- ** Reflect constraints into dictionaries

  , dict
  ) where

import Data.Kind (Type, Constraint)
import FCI.Internal (dict)
import qualified FCI.Internal as Internal
import FCI.Internal.TH

-------------------------------------------------------------------------------

-- | Translation @Constraint -> Type@.

--

-- The underlying type family is hidden so that 'FCI.mkDict'

-- is the only way to extend it, maintaining invariants required by 'dict'.

--

-- For example:

--

-- @

-- class Bar a => Foo a where

--   baz :: a

--   qux :: a -> b -> [(a, b)]

--

-- 'FCI.mkDict' 'Foo

-- @

--

-- creates the following declarations:

--

-- @

-- type instance 'Dict' (Foo a) = DictFoo a

-- data DictFoo a = Foo {

--     _Bar :: 'Dict' (Bar a)

--   , baz  :: a

--   , qux  :: forall b. a -> b -> [(a, b)]

--   }

-- @

type Dict (c :: Constraint) = Internal.Dict c :: Type