-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Re-exports 'GHC.TypeLits', modifying it considering our practices.
module Util.TypeLits
  ( Symbol
  , KnownSymbol
  , AppendSymbol
  , symbolVal
  , symbolValT
  , symbolValT'

  , TypeError
  , ErrorMessage (..)

  , TypeErrorUnless
  , inTypeErrorUnless
  ) where

import Data.Constraint ((\\))
import GHC.TypeLits

import Util.Type

symbolValT :: forall s. KnownSymbol s => Proxy s -> Text
symbolValT :: Proxy s -> Text
symbolValT = String -> Text
forall a. ToText a => a -> Text
toText (String -> Text) -> (Proxy s -> String) -> Proxy s -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal

symbolValT' :: forall s. KnownSymbol s => Text
symbolValT' :: Text
symbolValT' = Proxy s -> Text
forall (s :: Symbol). KnownSymbol s => Proxy s -> Text
symbolValT (Proxy s
forall k (t :: k). Proxy t
Proxy @s)

-- | Conditional type error.
--
-- Note that @TypeErrorUnless cond err@ is the same as
-- @If cond () (TypeError err)@, but does not produce type-level error when
-- one of its arguments cannot be deduced.
type family TypeErrorUnless (cond :: Bool) (err :: ErrorMessage) :: Constraint where
  TypeErrorUnless 'True _ = ()
  TypeErrorUnless 'False err = TypeError err

-- | Reify the fact that condition under 'TypeErrorUnless' constraint can be
-- assumed to always hold.
inTypeErrorUnless
  :: forall cond err a.
      TypeErrorUnless cond err
  => (cond ~ 'True => a)
  -> a
inTypeErrorUnless :: ((cond ~ 'True) => a) -> a
inTypeErrorUnless a :: (cond ~ 'True) => a
a = (cond ~ 'True) => a
a ((cond ~ 'True) => a) -> Dict (cond ~ 'True) -> a
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ MockableConstraint (cond ~ 'True) => Dict (cond ~ 'True)
forall (c :: Constraint). MockableConstraint c => Dict c
provideConstraintUnsafe @(cond ~ 'True)