{-# LANGUAGE
  ConstraintKinds,
  GADTs,
  KindSignatures,
  RankNTypes,
  ScopedTypeVariables,
  TypeApplications,
  TypeFamilies,
  TypeFamilyDependencies,
  TypeOperators #-}

-- | Core types. This module is internal and provides no guarantees about

-- stability and safety of its interface. It is left visible only as an escape hatch.

module FCI.Internal
  ( Dict
  , dict
  , (==>)
  ) where

import Data.Kind (Type, Constraint)
import Unsafe.Coerce (unsafeCoerce)

-- $setup

-- >>> import Data.Coerce

-- >>> import FCI.Base


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

-- | Type family that maps a constraint to its first class representation -

-- should be generally used instead of its concrete result for consistency.

type family Dict (c :: Constraint) = (t :: Type) | t -> c
-- TODO: should be TC plugin? - tuples, QuantifiedConstraints etc.


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

infixr 0 ==>
infixr 1 :=>

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

-- | /Reflect/ a constraint as a dictionary value.

--

-- You can use @TypeApplications@ to make the constraint @c@ explicit.

-- 'Dict' is injective, so @c@ may be inferred sometimes.

dict :: forall c. c => Dict c
dict :: forall (c :: Constraint). c => Dict c
dict = case (Any -> Any) -> c :=> Dict c
forall a b. a -> b
unsafeCoerce Any -> Any
forall a. a -> a
id :: c :=> Dict c of Wants c => Dict c
d -> Dict c
c => Dict c
d

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

-- | /Reify/ a dictionary to resolve a constraint required by the second operand.

--

-- For example, this lets us use @+@ on a type that doesn't have a top-level

-- 'Num' instance.

--

-- >>> newtype Foo = Foo Int deriving Show

-- >>> (coerce (dict @(Num Int)) :: Dict (Num Foo)) ==> Foo 1 + Foo 2

-- Foo 3

--

-- This function is extremely __unsafe__.

-- It breaks the global property that there is at most one instance

-- for each constraint. For example, sets and maps in containers rely

-- on that property to maintain their invariants.

--

-- Use at your own risk.

(==>) :: forall c r. Dict c -> (c => r) -> r
Dict c
d ==> :: forall (c :: Constraint) r. Dict c -> (c => r) -> r
==> c => r
x = (c :=> r) -> Dict c -> r
forall a b. a -> b
unsafeCoerce (forall (c :: Constraint) r. (c => r) -> c :=> r
Wants @c @r r
c => r
x) Dict c
d

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

-- | Wrapper for value @r@ requiring constraint @c@. Used by 'dict' and ('==>')

-- to satisfy typechecker.

newtype c :=> r where
  Wants :: (c => r) -> c :=> r