-- 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
  ) where

import GHC.TypeLits

symbolValT :: forall s. KnownSymbol s => Proxy s -> Text
symbolValT = toText . symbolVal

symbolValT' :: forall s. KnownSymbol s => Text
symbolValT' = symbolValT (Proxy @s)

-- | Conditional type error.
--
-- There is a very subtle difference between 'TypeErrorUnless' and the following type family:
--
-- > type family TypeErrorUnlessAlternative (cond :: Bool) (err :: ErrorMessage) :: Constraint where
-- >   TypeErrorUnlessAlternative cond err =
-- >     ( If cond
-- >         (() :: Constraint)
-- >         (TypeError err)
-- >     , cond ~ 'True
-- >     )
--
-- If @cond@ cannot be fully reduced (e.g. it's a stuck type family), then:
--
-- * @TypeErrorUnless@ will state that the constraint cannot be deduced.
-- * @TypeErrorUnlessAlternative@ will fail with the given error message @err@.
--
-- For example:
--
-- > -- Partial function
-- > type family IsZero (n :: Peano) :: Bool where
-- >   IsZero ('S _) = 'False
-- >
-- > f1 :: TypeErrorUnless (IsZero n) ('Text "Expected zero") => ()
-- > f1 = ()
-- >
-- > f2 :: TypeErrorUnlessAlternative (IsZero n) ('Text "Expected zero") => ()
-- > f2 = ()
-- >
-- >
-- > f1res = f1 @'Z
-- > -- • Couldn't match type ‘IsZero 'Z’ with ‘'True’
-- >
-- > f2res = f2 @'Z
-- > -- • Expected zero
--
-- As you can see, the error message in @f2res@ is misleading (because the type argument
-- actually _is_ zero), so it's preferable to fail with the standard GHC error message.
type TypeErrorUnless (cond :: Bool) (err :: ErrorMessage) =
  ( TypeErrorUnlessHelper cond err
  -- Note: the '~' constraint below might seem redundant, but, without it,
  -- GHC would warn that the following pattern match is not exhaustive (even though it is):
  --
  -- > f :: TypeErrorUnless (n >= ToPeano 2) "some err msg" => Sing n -> ()
  -- > f = \case
  -- >   SS (SS SZ) -> ()
  -- >   SS (SS _) -> ()
  --
  -- GHC needs to "see" the type equality '~' in order to actually "learn" something from a
  -- type family's result.
  , cond ~ 'True
  )

type family TypeErrorUnlessHelper (cond :: Bool) (err :: ErrorMessage) :: Constraint where
  TypeErrorUnlessHelper 'True _ = ()
  TypeErrorUnlessHelper 'False err = TypeError err