-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

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

  , TypeError
  , ErrorMessage (..)

  , TypeErrorUnless
  , AssertTypesEqual
  ) where

import Data.Type.Equality (type (==))
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), KnownSymbol, Symbol, TypeError, symbolVal)

symbolValT :: forall s. KnownSymbol s => Proxy s -> Text
symbolValT :: forall (s :: Symbol). KnownSymbol s => 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' :: forall (s :: Symbol). KnownSymbol s => Text
symbolValT' = Proxy s -> Text
forall (s :: Symbol). KnownSymbol s => Proxy s -> Text
symbolValT (forall {k} (t :: k). Proxy t
forall {t :: Symbol}. Proxy t
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

-- | Condition Error helper to check if two types are equal
--
-- >>> :k! AssertTypesEqual Int Int ('Text "This should not result in a failure")
-- AssertTypesEqual Int Int ('Text "This should not result in a failure") :: Constraint
-- = (() :: Constraint, Int ~ Int)
--
-- >>> :k! AssertTypesEqual Bool Int ('Text "This should result in a failure")
-- AssertTypesEqual Bool Int ('Text "This should result in a failure") :: Constraint
-- = ((TypeError ...), Bool ~ Int)
type AssertTypesEqual a b (err :: ErrorMessage) =
  ( TypeErrorUnlessHelper (a == b) err
  -- The reasons for the constraint below are the same as those in @TypeErrorUnless@ constructor
  , a ~ b
  )