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

{-# OPTIONS_GHC -Wno-orphans #-}

-- | Support for uninhabited type.
--
-- Note: this module exists solely for historical reasons since the time when
-- 'Never' was not yet supported by the Michelson.
--
-- TODO [#549]: remove this module.
module Lorentz.Empty
  ( Empty
  , absurd_
  ) where

import Fmt (Buildable(..))

import Lorentz.Annotation (HasAnnotation)
import Lorentz.Base
import Lorentz.Doc
import Lorentz.Errors
import Lorentz.Value
import Michelson.Typed.Haskell.Doc

-- | Replacement for uninhabited type.
{-# DEPRECATED Empty "Use Never type instead" #-}
newtype Empty = Empty ()
  deriving stock (forall x. Empty -> Rep Empty x)
-> (forall x. Rep Empty x -> Empty) -> Generic Empty
forall x. Rep Empty x -> Empty
forall x. Empty -> Rep Empty x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Empty x -> Empty
$cfrom :: forall x. Empty -> Rep Empty x
Generic
  deriving anyclass (WellTypedToT Empty
WellTypedToT Empty
-> (Empty -> Value (ToT Empty))
-> (Value (ToT Empty) -> Empty)
-> IsoValue Empty
Value (ToT Empty) -> Empty
Empty -> Value (ToT Empty)
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT Empty) -> Empty
$cfromVal :: Value (ToT Empty) -> Empty
toVal :: Empty -> Value (ToT Empty)
$ctoVal :: Empty -> Value (ToT Empty)
$cp1IsoValue :: WellTypedToT Empty
IsoValue, AnnOptions
FollowEntrypointFlag -> Notes (ToT Empty)
(FollowEntrypointFlag -> Notes (ToT Empty))
-> AnnOptions -> HasAnnotation Empty
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> AnnOptions -> HasAnnotation a
annOptions :: AnnOptions
$cannOptions :: AnnOptions
getAnnotation :: FollowEntrypointFlag -> Notes (ToT Empty)
$cgetAnnotation :: FollowEntrypointFlag -> Notes (ToT Empty)
HasAnnotation)

instance TypeHasDoc Empty where
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    Markdown
"Type which should never be constructed.\n\n\
    \If appears as part of entrypoint argument, this means that the entrypoint \
    \should never be called."

-- | Someone constructed 'Empty' type.
type instance ErrorArg "emptySupplied" = UnitErrorArg

instance Buildable (CustomError "emptySupplied") where
  build :: CustomError "emptySupplied" -> Markdown
build (CustomError Label "emptySupplied"
_ (_, ())) =
    Markdown
"'Empty' value was passed to the contract."

instance CustomErrorHasDoc "emptySupplied" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Markdown
customErrDocMdCause =
    Markdown
"Value of type " Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Proxy Empty -> WithinParens -> Markdown
forall a. TypeHasDoc a => Proxy a -> WithinParens -> Markdown
typeDocMdReference (Proxy Empty
forall k (t :: k). Proxy t
Proxy @Empty) (Bool -> WithinParens
WithinParens Bool
False)
    Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Markdown
" has been supplied."

-- | Witness of that this code is unreachable.
absurd_ :: Empty : s :-> s'
absurd_ :: (Empty : s) :-> s'
absurd_ =
  Label "emptySupplied" -> (Empty : s) :-> s'
forall (tag :: Symbol) (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, ()), CustomErrorHasDoc tag) =>
Label tag -> s :-> any
failCustom_ IsLabel "emptySupplied" (Label "emptySupplied")
Label "emptySupplied"
#emptySupplied ((Empty : s) :-> s') -> (s' :-> s') -> (Empty : s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  DDescription -> s' :-> s'
forall di (s :: [*]). DocItem di => di -> s :-> s
doc (Markdown -> DDescription
DDescription Markdown
"Should never be called")