{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Description : Manage the implicit parameter namespace dynamically at compile time.
-- Copyright   : Copyright 2025 Shea Levy
-- License     : Apache-2.0
-- Maintainer  : shea@shealevy.com
--
-- Manage the implicit parameter namespace dynamically at compile time.
--
-- This is an implementation of [GHC proposal 737](https://github.com/ghc-proposals/ghc-proposals/pull/737).
-- Relative to that proposal, this suffers from the following (likely hypothetical) limitations:
--
--   * It may break if future GHC versions change the implementation of implicit parameters
--   * It doesn't mandate that 'bindImplicit' and 'implicitParameter' be fully applied,
--     nor guarantee that they don't impose additional runtime cost.
--   * It uses some auxiliary internal type-level machinery that can't be hidden.
--   * It is not inferred as safe Haskell (though it is safe).
module Data.Implicit where

import GHC.Base (IP, ip, withDict)
import GHC.TypeLits (Symbol)

-- | 'ImplicitParameter' @x@ @a@ is a t'Data.Kind.Constraint' that 'implicitParameter' @x@ is an implicit parameter of type @a@.
--
-- 'ImplicitParameter' constraints are propagated according to dynamic scoping rules.
-- In other words, GHC always takes the most nested parameter binding from the context
-- to find the value. @bindImplict x a (bindImplict x b (implicitParameter x))@
-- is equivalent to @b@ (including resulting in a type error if used where
-- a term whose type unifies with @a@'s but not @b@'s is expected).
--
-- To bind an implicit parameter, use 'bindImplicit'.
--
-- @ImplictParameter (MkIdent "foo") t@ is equivalent to @?foo :: t@.
type ImplicitParameter (x :: k) = IP (KeyName x)

-- | Bind implicit parameter @x@ to the provided @a@.
--
-- @bindImplicit (MkIdent "foo") x go@ is equivalent to @let ?foo = x in go@.
{-# INLINE bindImplicit #-}
bindImplicit :: forall x -> a -> ((ImplicitParameter x a) => b) -> b
bindImplicit _ = withDict

-- | Access implicit parameter bound to @x@.
--
-- @implicitParameter (MkIdent "foo")@ is equivalent to @?foo@.
{-# INLINE implicitParameter #-}
implicitParameter :: forall x -> (ImplicitParameter x a) => a
implicitParameter x = ip @(KeyName x)

-- | The kind of type-level representations of Haskell identifiers.
data Ident = MkIdent Symbol {- HLINT ignore "Use newtype instead of data" -}

-- | The identifier's name
type family IdentName (i :: Ident) :: Symbol where
  IdentName (MkIdent s) = s

-- *** Implementation details

-- | Helper data family to create a new 'Symbol' from a type-level value of any kind.
data family MkSymbol (t :: k) :: k'

-- | Turn the key of an 'ImplicitParameter' into a 'Symbol' for GHC's 'IP' type class.
--
-- 'Ident' ifiers are directly mapped to their underlying names.
--
-- Other type-level values are injected into 'Symbol' via 'MkSymbol'.
type KeyName :: forall k. k -> Symbol
type family KeyName t where
  KeyName i = IdentName i
  KeyName t = MkSymbol t