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

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

{- | Module, containing restrictions imposed by instruction or value scope.

Michelson have multiple restrictions on values, examples:

* @operation@ type cannot appear in parameter.
* @big_map@ type cannot appear in @PUSH@-able constants.
* @contract@ type cannot appear in type we @UNPACK@ to.

Thus we declare multiple "scopes" - constraints applied in corresponding
situations, for instance

* 'ParameterScope';
* 'StorageScope';
* 'ConstantScope'.

Also we separate multiple "classes" of scope-related constraints.

* 'ParameterScope' and similar ones are used within Michelson engine,
they are understandable by GHC but produce not very clarifying errors.

* 'ProperParameterBetterErrors' and similar ones are middle-layer constraints,
they produce human-readable errors but GHC cannot make conclusions from them.
They are supposed to be used only by eDSLs to define their own high-level
constraints.

* Lorentz and other eDSLs may declare their own constraints, in most cases
you should use them. For example see @Lorentz.Constraints@ module.

-}

module Morley.Michelson.Typed.Scope
  ( -- * Scopes
    ConstantScope
  , DupableScope
  , StorageScope
  , PackedValScope
  , ParameterScope
  , UntypedValScope
  , UnpackedValScope
  , ViewableScope

  , ProperParameterBetterErrors
  , ProperStorageBetterErrors
  , ProperConstantBetterErrors
  , ProperDupableBetterErrors
  , ProperPackedValBetterErrors
  , ProperUnpackedValBetterErrors
  , ProperUntypedValBetterErrors
  , ProperViewableBetterErrors
  , ProperNonComparableValBetterErrors

  , properParameterEvi
  , properStorageEvi
  , properConstantEvi
  , properDupableEvi
  , properPackedValEvi
  , properUnpackedValEvi
  , properViewableEvi
  , properUntypedValEvi
  , (:-)(..)

  , BadTypeForScope (..)
  , CheckScope (..)
  , WithDeMorganScope (..)

    -- * Implementation internals
  , HasNoBigMap
  , HasNoNestedBigMaps
  , HasNoOp
  , HasNoContract
  , HasNoTicket
  , ContainsBigMap
  , ContainsContract
  , ContainsNestedBigMaps
  , ContainsOp
  , ContainsTicket
  , IsComparable

  , ForbidOp
  , ForbidContract
  , ForbidTicket
  , ForbidBigMap
  , ForbidNestedBigMaps
  , ForbidNonComparable
  , FailOnBigMapFound
  , FailOnContractFound
  , FailOnNestedBigMapsFound
  , FailOnOperationFound
  , FailOnTicketFound
  , FailOnNonComparableFound

  , OpPresence (..)
  , ContractPresence (..)
  , TicketPresence (..)
  , BigMapPresence (..)
  , NestedBigMapsPresence (..)
  , checkOpPresence
  , checkContractTypePresence
  , checkTicketPresence
  , checkBigMapPresence
  , checkNestedBigMapsPresence
  , opAbsense
  , contractTypeAbsense
  , bigMapAbsense
  , nestedBigMapsAbsense
  , forbiddenOp
  , forbiddenContractType
  , forbiddenBigMap
  , forbiddenNestedBigMaps

    -- * Re-exports
  , withDict
  , SingI (..)
  ) where

import Data.Constraint (Dict(..), withDict, (:-)(..), (\\))
import Data.Singletons (Sing, SingI(..))
import Data.Type.Bool (type (&&), type (||))
import Fmt (Buildable(..))
import GHC.TypeLits (ErrorMessage(..), TypeError)

import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc)
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))

----------------------------------------------------------------------------
-- Constraints
----------------------------------------------------------------------------
-- | Whether a value of this type _may_ contain an operation.
--
-- In some scopes (constants, parameters, storage) appearing for operation type
-- is prohibited.
-- Operations in input/output of lambdas are allowed without limits though.
type family ContainsOp (t :: T) :: Bool where
  ContainsOp 'TKey = 'False
  ContainsOp 'TUnit = 'False
  ContainsOp 'TSignature = 'False
  ContainsOp 'TChainId = 'False
  ContainsOp ('TOption t) = ContainsOp t
  ContainsOp ('TList t) = ContainsOp t
  ContainsOp ('TSet t) = ContainsOp t
  ContainsOp 'TOperation = 'True
  ContainsOp ('TContract _) = 'False
  ContainsOp ('TTicket t) = ContainsOp t
  ContainsOp ('TPair a b) = ContainsOp a || ContainsOp b
  ContainsOp ('TOr a b) = ContainsOp a || ContainsOp b
  ContainsOp ('TLambda _ _) = 'False
  ContainsOp ('TMap k v) = ContainsOp k || ContainsOp v
  ContainsOp ('TBigMap k v) = ContainsOp k || ContainsOp v
  ContainsOp _ = 'False

-- | Whether a value of this type _may_ contain a @contract@ value.
--
-- In some scopes (constants, storage) appearing for contract type
-- is prohibited.
-- Contracts in input/output of lambdas are allowed without limits though.
type family ContainsContract (t :: T) :: Bool where
  ContainsContract 'TKey = 'False
  ContainsContract 'TUnit = 'False
  ContainsContract 'TSignature = 'False
  ContainsContract 'TChainId = 'False
  ContainsContract ('TOption t) = ContainsContract t
  ContainsContract ('TList t) = ContainsContract t
  ContainsContract ('TSet _) = 'False
  ContainsContract 'TOperation = 'False
  ContainsContract ('TContract _) = 'True
  ContainsContract ('TPair a b) = ContainsContract a || ContainsContract b
  ContainsContract ('TOr a b) = ContainsContract a || ContainsContract b
  ContainsContract ('TLambda _ _) = 'False
  ContainsContract ('TMap _ v) = ContainsContract v
  ContainsContract ('TBigMap _ v) = ContainsContract v
  ContainsContract _ = 'False

-- | Whether a value of this type _may_ contain a @ticket@ value.
type family ContainsTicket (t :: T) :: Bool where
  ContainsTicket ('TOption t) = ContainsTicket t
  ContainsTicket ('TList t) = ContainsTicket t
  ContainsTicket ('TSet _) = 'False
  ContainsTicket ('TTicket _) = 'True
  ContainsTicket ('TPair a b) = ContainsTicket a || ContainsTicket b
  ContainsTicket ('TOr a b) = ContainsTicket a || ContainsTicket b
  ContainsTicket ('TLambda _ _) = 'False
  ContainsTicket ('TMap _ v) = ContainsTicket v
  ContainsTicket ('TBigMap _ v) = ContainsTicket v
  ContainsTicket _ = 'False

-- | Whether a value of this type _may_ contain a @big_map@ value.
type family ContainsBigMap (t :: T) :: Bool where
  ContainsBigMap 'TKey = 'False
  ContainsBigMap 'TUnit = 'False
  ContainsBigMap 'TSignature = 'False
  ContainsBigMap 'TChainId = 'False
  ContainsBigMap ('TOption t) = ContainsBigMap t
  ContainsBigMap ('TList t) = ContainsBigMap t
  ContainsBigMap ('TSet _) = 'False
  ContainsBigMap 'TOperation = 'False
  ContainsBigMap ('TContract _) = 'False
  ContainsBigMap ('TPair a b) = ContainsBigMap a || ContainsBigMap b
  ContainsBigMap ('TOr a b) = ContainsBigMap a || ContainsBigMap b
  ContainsBigMap ('TLambda _ _) = 'False
  ContainsBigMap ('TMap _ v) = ContainsBigMap v
  ContainsBigMap ('TBigMap _ _) = 'True
  ContainsBigMap _ = 'False

-- | Whether a value of this type _may_ contain nested @big_map@s.
--
-- Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are
-- prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more
-- strict because they don't work with big_map at all.
type family ContainsNestedBigMaps (t :: T) :: Bool where
  ContainsNestedBigMaps 'TKey = 'False
  ContainsNestedBigMaps 'TUnit = 'False
  ContainsNestedBigMaps 'TSignature = 'False
  ContainsNestedBigMaps 'TChainId = 'False
  ContainsNestedBigMaps ('TOption t) = ContainsNestedBigMaps t
  ContainsNestedBigMaps ('TList t) = ContainsNestedBigMaps t
  ContainsNestedBigMaps ('TSet _) = 'False
  ContainsNestedBigMaps 'TOperation = 'False
  ContainsNestedBigMaps ('TContract _) = 'False
  ContainsNestedBigMaps ('TPair a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b
  ContainsNestedBigMaps ('TOr a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b
  ContainsNestedBigMaps ('TLambda _ _) = 'False
  ContainsNestedBigMaps ('TMap _ v) = ContainsNestedBigMaps v
  ContainsNestedBigMaps ('TBigMap _ v) = ContainsBigMap v
  ContainsNestedBigMaps _ = 'False

-- | Constraint which ensures that type is comparable.
type family IsComparable (t :: T) :: Bool where
  IsComparable ('TPair a b) =  IsComparable a && IsComparable b
  IsComparable ('TOption t) = IsComparable t
  IsComparable 'TBls12381Fr = 'False
  IsComparable 'TBls12381G1 = 'False
  IsComparable 'TBls12381G2 = 'False
  IsComparable ('TList _) = 'False
  IsComparable ('TSet _) = 'False
  IsComparable 'TOperation = 'False
  IsComparable ('TContract _) = 'False
  IsComparable ('TTicket _) = 'False
  IsComparable ('TOr a b) = IsComparable a && IsComparable b
  IsComparable ('TLambda _ _) = 'False
  IsComparable ('TMap _ _) = 'False
  IsComparable ('TBigMap _ _) = 'False
  IsComparable 'TChest = 'False
  IsComparable 'TChestKey = 'False
  IsComparable _            = 'True

-- | Constraint which ensures that a value of type @t@ does not contain operations.
--
-- Not just a type alias in order to be able to partially apply it
-- (e.g. in 'Each').
class (ContainsOp t ~ 'False) => HasNoOp t
instance (ContainsOp t ~ 'False) => HasNoOp t

-- | Constraint which ensures that a value of type @t@ does not contain @contract@ values.
class (ContainsContract t ~ 'False) => HasNoContract t
instance (ContainsContract t ~ 'False) => HasNoContract t

-- | Constraint which ensures that a value of type @t@ does not contain @ticket@ values.
class (ContainsTicket t ~ 'False) => HasNoTicket t
instance (ContainsTicket t ~ 'False) => HasNoTicket t

-- | Constraint which ensures that a value of type @t@ does not contain @big_map@ values.
class (ContainsBigMap t ~ 'False) => HasNoBigMap t
instance (ContainsBigMap t ~ 'False) => HasNoBigMap t

-- | Constraint which ensures that there are no nested bigmaps.
class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t

-- | Report a human-readable error about 'TOperation' at a wrong place.
type family FailOnOperationFound (enabled :: Bool) :: Constraint where
  FailOnOperationFound 'True =
    TypeError ('Text "Operations are not allowed in this scope")
  FailOnOperationFound 'False = ()

-- | Report a human-readable error about 'TContract' at a wrong place.
type family FailOnContractFound (enabled :: Bool) :: Constraint where
  FailOnContractFound 'True =
    TypeError ('Text "Type `contract` is not allowed in this scope")
  FailOnContractFound 'False = ()

-- | Report a human-readable error about 'TTicket' at a wrong place.
type family FailOnTicketFound (enabled :: Bool) :: Constraint where
  FailOnTicketFound 'True =
    TypeError ('Text "Type `ticket` is not allowed in this scope")
  FailOnTicketFound 'False = ()

-- | Report a human-readable error about 'TBigMap' at a wrong place.
type family FailOnBigMapFound (enabled :: Bool) :: Constraint where
  FailOnBigMapFound 'True =
    TypeError ('Text "BigMaps are not allowed in this scope")
  FailOnBigMapFound 'False = ()

-- | Report a human-readable error that 'TBigMap' contains another 'TBigMap'
type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where
  FailOnNestedBigMapsFound 'True =
    TypeError ('Text "Nested BigMaps are not allowed")
  FailOnNestedBigMapsFound 'False = ()

-- | Report a human-readable error that given value is not comparable
type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where
  FailOnNonComparableFound 'True = ()
  FailOnNonComparableFound 'False =
    TypeError ('Text "Only comparable types are allowed here")

-- | This is like 'HasNoOp', it raises a more human-readable error
-- when @t@ type is concrete, but GHC cannot make any conclusions
-- from such constraint as it can for 'HasNoOp'.
-- Though, hopefully, it will someday:
-- <https://gitlab.haskell.org/ghc/ghc/issues/11503 #11503>.
--
-- Use this constraint in our eDSL.
type ForbidOp t = FailOnOperationFound (ContainsOp t)

type ForbidContract t = FailOnContractFound (ContainsContract t)

type ForbidTicket t = FailOnTicketFound (ContainsTicket t)

type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)

type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)

-- | Constraint that rises human-readable error message, in case given value
-- can't be compared
type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t)

-- | Evidence of that 'HasNoOp' is deducable from 'ForbidOp'.
forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi = Sub $
  -- It's not clear now to proof GHC that @HasNoOp t@ is implication of
  -- @ForbidOp t@, so we use @error@ below and also disable
  -- "-Wredundant-constraints" extension.
  case checkOpPresence (sing @t) of
    OpAbsent -> Dict
    OpPresent -> error "impossible"

-- | Reify 'HasNoOp' contraint from 'ForbidOp'.
--
-- Left for backward compatibility.
forbiddenOp
  :: forall t a.
     (SingI t, ForbidOp t)
  => (HasNoOp t => a)
  -> a
forbiddenOp = withDict $ forbiddenOpEvi @t

forbiddenBigMapEvi :: forall t. (SingI t, ForbidBigMap t) :- HasNoBigMap t
forbiddenBigMapEvi = Sub $
  case checkBigMapPresence (sing @t) of
    BigMapAbsent -> Dict
    BigMapPresent -> error "impossible"

forbiddenNestedBigMapsEvi :: forall t. (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
forbiddenNestedBigMapsEvi = Sub $
  case checkNestedBigMapsPresence (sing @t) of
    NestedBigMapsAbsent -> Dict
    NestedBigMapsPresent -> error "impossible"

forbiddenBigMap
  :: forall t a.
     (SingI t, ForbidBigMap t)
  => (HasNoBigMap t => a)
  -> a
forbiddenBigMap = withDict $ forbiddenBigMapEvi @t

forbiddenNestedBigMaps
  :: forall t a.
     (SingI t, ForbidNestedBigMaps t)
  => (HasNoNestedBigMaps t => a)
  -> a
forbiddenNestedBigMaps = withDict $ forbiddenNestedBigMapsEvi @t

-- | Reify 'HasNoContract' contraint from 'ForbidContract'.
forbiddenContractTypeEvi
  :: forall t. (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi = Sub $
  case checkContractTypePresence (sing @t) of
    ContractAbsent -> Dict
    ContractPresent -> error "impossible"

-- | Reify 'HasNoContract' contraint from 'ForbidContract'.
forbiddenContractType
  :: forall t a.
     (SingI t, ForbidContract t)
  => (HasNoContract t => a)
  -> a
forbiddenContractType = withDict $ forbiddenContractTypeEvi @t

-- | Reify 'HasNoTicket' contraint from 'ForbidTicket'.
forbiddenTicketTypeEvi
  :: forall t. (SingI t, ForbidTicket t) :- HasNoTicket t
forbiddenTicketTypeEvi = Sub $
  case checkTicketPresence (sing @t) of
    TicketAbsent -> Dict
    TicketPresent -> error "impossible"

-- | Whether a value of this type _may_ contain an operation.
data OpPresence (t :: T)
  = ContainsOp t ~ 'True => OpPresent
    -- ^ A value of type @t@ may or may not contain an operation.
  | ContainsOp t ~ 'False => OpAbsent
    -- ^ A value of type @t@ cannot contain @big_map@ values.

-- | Whether a value of this type _may_ contain a @contract@ value.
data ContractPresence (t :: T)
  = ContainsContract t ~ 'True => ContractPresent
    -- ^ A value of type @t@ may or may not contain a @contract@ value.
  | ContainsContract t ~ 'False => ContractAbsent
    -- ^ A value of type @t@ cannot contain @contract@ values.

-- | Whether a value of this type _may_ contain a @ticket@ value.
data TicketPresence (t :: T)
  = ContainsTicket t ~ 'True => TicketPresent
    -- ^ A value of type @t@ may or may not contain a @ticket@ value.
  | ContainsTicket t ~ 'False => TicketAbsent
    -- ^ A value of type @t@ cannot contain @ticket@ values.

-- | Whether a value of this type _may_ contain a @big_map@ value.
data BigMapPresence (t :: T)
  = ContainsBigMap t ~ 'True => BigMapPresent
    -- ^ A value of type @t@ may or may not contain a @big_map@ value.
  | ContainsBigMap t ~ 'False => BigMapAbsent
    -- ^ A value of type @t@ cannot contain @big_map@ values.

-- | Whether a value of this type _may_ contain nested @big_map@s.
data NestedBigMapsPresence (t :: T)
  = ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
    -- ^ A value of type @t@ may or may not contain nested @big_map@s.
  | ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent
    -- ^ A value of type @t@ cannot contain nested @big_map@s.

-- @rvem: IMO, generalization of OpPresence and BigMapPresence to
-- TPresence is not worth it, due to the fact that
-- it will require more boilerplate in checkTPresence implementation
-- than it is already done in checkOpPresence and checkBigMapPresence

-- | Check at runtime whether a value of the given type _may_ contain an operation.
checkOpPresence :: Sing (ty :: T) -> OpPresence ty
checkOpPresence = \case
  -- This is a sad amount of boilerplate, but at least
  -- there is no chance to make a mistake in it.
  -- We can't do in a simpler way while requiring only @Sing ty@ / @SingI ty@,
  -- and a more complex constraint would be too unpleasant and confusing to
  -- propagate everywhere.
  STKey -> OpAbsent
  STSignature -> OpAbsent
  STChainId -> OpAbsent
  STUnit -> OpAbsent
  STOption t -> case checkOpPresence t of
    OpPresent -> OpPresent
    OpAbsent -> OpAbsent
  STList t -> case checkOpPresence t of
    OpPresent -> OpPresent
    OpAbsent -> OpAbsent
  STSet a -> case checkOpPresence a of
    OpPresent -> OpPresent
    OpAbsent -> OpAbsent
  STOperation -> OpPresent
  STContract _ -> OpAbsent
  STTicket t -> case checkOpPresence t of
    OpPresent -> OpPresent
    OpAbsent -> OpAbsent
  STPair a b -> case (checkOpPresence a, checkOpPresence b) of
    (OpPresent, _) -> OpPresent
    (_, OpPresent) -> OpPresent
    (OpAbsent, OpAbsent) -> OpAbsent
  STOr a b -> case (checkOpPresence a, checkOpPresence b) of
    (OpPresent, _) -> OpPresent
    (_, OpPresent) -> OpPresent
    (OpAbsent, OpAbsent) -> OpAbsent
  STLambda _ _ -> OpAbsent
  STMap k v -> case (checkOpPresence k, checkOpPresence v) of
    (OpAbsent, OpAbsent) -> OpAbsent
    (OpPresent, _) -> OpPresent
    (_, OpPresent) -> OpPresent
  STBigMap k v -> case (checkOpPresence k, checkOpPresence v) of
    (OpAbsent, OpAbsent) -> OpAbsent
    (OpPresent, _) -> OpPresent
    (_, OpPresent) -> OpPresent
  STInt -> OpAbsent
  STNat -> OpAbsent
  STString -> OpAbsent
  STBytes -> OpAbsent
  STMutez -> OpAbsent
  STBool -> OpAbsent
  STKeyHash -> OpAbsent
  STBls12381Fr -> OpAbsent
  STBls12381G1 -> OpAbsent
  STBls12381G2 -> OpAbsent
  STTimestamp -> OpAbsent
  STAddress -> OpAbsent
  STChest -> OpAbsent
  STChestKey -> OpAbsent
  STNever -> OpAbsent

-- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
checkContractTypePresence = \case
  STKey -> ContractAbsent
  STSignature -> ContractAbsent
  STChainId -> ContractAbsent
  STUnit -> ContractAbsent
  STOption t -> case checkContractTypePresence t of
    ContractPresent -> ContractPresent
    ContractAbsent -> ContractAbsent
  STList t -> case checkContractTypePresence t of
    ContractPresent -> ContractPresent
    ContractAbsent -> ContractAbsent
  STSet _ -> ContractAbsent
  STOperation -> ContractAbsent
  STContract _ -> ContractPresent
  STTicket _ -> ContractAbsent  -- contract type is not allowed in tickets at all
  STPair a b -> case (checkContractTypePresence a, checkContractTypePresence b) of
    (ContractPresent, _) -> ContractPresent
    (_, ContractPresent) -> ContractPresent
    (ContractAbsent, ContractAbsent) -> ContractAbsent
  STOr a b -> case (checkContractTypePresence a, checkContractTypePresence b) of
    (ContractPresent, _) -> ContractPresent
    (_, ContractPresent) -> ContractPresent
    (ContractAbsent, ContractAbsent) -> ContractAbsent
  STLambda _ _ -> ContractAbsent
  STMap _ v -> case checkContractTypePresence v of
    ContractPresent -> ContractPresent
    ContractAbsent -> ContractAbsent
  STBigMap _ v -> case checkContractTypePresence v of
    ContractPresent -> ContractPresent
    ContractAbsent -> ContractAbsent
  STInt -> ContractAbsent
  STNat -> ContractAbsent
  STString -> ContractAbsent
  STBytes -> ContractAbsent
  STMutez -> ContractAbsent
  STBool -> ContractAbsent
  STKeyHash -> ContractAbsent
  STBls12381Fr -> ContractAbsent
  STBls12381G1 -> ContractAbsent
  STBls12381G2 -> ContractAbsent
  STTimestamp -> ContractAbsent
  STAddress -> ContractAbsent
  STChest -> ContractAbsent
  STChestKey -> ContractAbsent
  STNever -> ContractAbsent

-- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value.
checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty
checkTicketPresence = \case
  STKey -> TicketAbsent
  STSignature -> TicketAbsent
  STChainId -> TicketAbsent
  STUnit -> TicketAbsent
  STOption t -> case checkTicketPresence t of
    TicketPresent -> TicketPresent
    TicketAbsent -> TicketAbsent
  STList t -> case checkTicketPresence t of
    TicketPresent -> TicketPresent
    TicketAbsent -> TicketAbsent
  STSet _ -> TicketAbsent
  STOperation -> TicketAbsent
  STContract _ -> TicketAbsent
  STTicket _ -> TicketPresent
  STPair a b -> case (checkTicketPresence a, checkTicketPresence b) of
    (TicketPresent, _) -> TicketPresent
    (_, TicketPresent) -> TicketPresent
    (TicketAbsent, TicketAbsent) -> TicketAbsent
  STOr a b -> case (checkTicketPresence a, checkTicketPresence b) of
    (TicketPresent, _) -> TicketPresent
    (_, TicketPresent) -> TicketPresent
    (TicketAbsent, TicketAbsent) -> TicketAbsent
  STLambda _ _ -> TicketAbsent
  STMap _ v -> case checkTicketPresence v of
    TicketPresent -> TicketPresent
    TicketAbsent -> TicketAbsent
  STBigMap _ v -> case checkTicketPresence v of
    TicketPresent -> TicketPresent
    TicketAbsent -> TicketAbsent
  STInt -> TicketAbsent
  STNat -> TicketAbsent
  STString -> TicketAbsent
  STBytes -> TicketAbsent
  STMutez -> TicketAbsent
  STBool -> TicketAbsent
  STKeyHash -> TicketAbsent
  STBls12381Fr -> TicketAbsent
  STBls12381G1 -> TicketAbsent
  STBls12381G2 -> TicketAbsent
  STTimestamp -> TicketAbsent
  STAddress -> TicketAbsent
  STChest -> TicketAbsent
  STChestKey -> TicketAbsent
  STNever -> TicketAbsent

-- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence = \case
  -- More boilerplate to boilerplate god.
  STKey -> BigMapAbsent
  STSignature -> BigMapAbsent
  STChainId -> BigMapAbsent
  STUnit -> BigMapAbsent
  STOption t -> case checkBigMapPresence t of
    BigMapPresent -> BigMapPresent
    BigMapAbsent -> BigMapAbsent
  STList t -> case checkBigMapPresence t of
    BigMapPresent -> BigMapPresent
    BigMapAbsent -> BigMapAbsent
  STSet _ -> BigMapAbsent
  STOperation -> BigMapAbsent
  STContract _ -> BigMapAbsent
  STTicket _ -> BigMapAbsent  -- big_maps are not allowed in tickets at all
  STPair a b -> case (checkBigMapPresence a, checkBigMapPresence b) of
    (BigMapPresent, _) -> BigMapPresent
    (_, BigMapPresent) -> BigMapPresent
    (BigMapAbsent, BigMapAbsent) -> BigMapAbsent
  STOr a b -> case (checkBigMapPresence a, checkBigMapPresence b) of
    (BigMapPresent, _) -> BigMapPresent
    (_, BigMapPresent) -> BigMapPresent
    (BigMapAbsent, BigMapAbsent) -> BigMapAbsent
  STLambda _ _ -> BigMapAbsent
  STMap _ v -> case checkBigMapPresence v of
    BigMapPresent -> BigMapPresent
    BigMapAbsent -> BigMapAbsent
  STBigMap _ _ ->
    BigMapPresent
  STInt -> BigMapAbsent
  STNat -> BigMapAbsent
  STString -> BigMapAbsent
  STBytes -> BigMapAbsent
  STMutez -> BigMapAbsent
  STBool -> BigMapAbsent
  STKeyHash -> BigMapAbsent
  STBls12381Fr -> BigMapAbsent
  STBls12381G1 -> BigMapAbsent
  STBls12381G2 -> BigMapAbsent
  STTimestamp -> BigMapAbsent
  STAddress -> BigMapAbsent
  STChest -> BigMapAbsent
  STChestKey -> BigMapAbsent
  STNever -> BigMapAbsent

-- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
  -- More boilerplate to boilerplate god.
  STKey -> NestedBigMapsAbsent
  STSignature -> NestedBigMapsAbsent
  STChainId -> NestedBigMapsAbsent
  STUnit -> NestedBigMapsAbsent
  STOption t -> case checkNestedBigMapsPresence t of
    NestedBigMapsPresent -> NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsAbsent
  STList                   t -> case checkNestedBigMapsPresence t of
    NestedBigMapsPresent -> NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsAbsent
  STSet _ -> NestedBigMapsAbsent
  STOperation -> NestedBigMapsAbsent
  STContract _ -> NestedBigMapsAbsent
  STTicket _ -> NestedBigMapsAbsent
  STPair a b -> case (checkNestedBigMapsPresence a, checkNestedBigMapsPresence b) of
    (NestedBigMapsPresent, _) -> NestedBigMapsPresent
    (_, NestedBigMapsPresent) -> NestedBigMapsPresent
    (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsAbsent
  STOr a b -> case (checkNestedBigMapsPresence a, checkNestedBigMapsPresence b) of
    (NestedBigMapsPresent, _) -> NestedBigMapsPresent
    (_, NestedBigMapsPresent) -> NestedBigMapsPresent
    (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsAbsent
  STLambda _ _ -> NestedBigMapsAbsent
  STMap _ v -> case checkNestedBigMapsPresence v of
    NestedBigMapsPresent -> NestedBigMapsPresent
    NestedBigMapsAbsent -> NestedBigMapsAbsent
  STBigMap _ v -> case checkBigMapPresence v of
    BigMapPresent -> NestedBigMapsPresent
    BigMapAbsent -> NestedBigMapsAbsent
  STInt -> NestedBigMapsAbsent
  STNat -> NestedBigMapsAbsent
  STString -> NestedBigMapsAbsent
  STBytes -> NestedBigMapsAbsent
  STMutez -> NestedBigMapsAbsent
  STBool -> NestedBigMapsAbsent
  STKeyHash -> NestedBigMapsAbsent
  STBls12381Fr -> NestedBigMapsAbsent
  STBls12381G1 -> NestedBigMapsAbsent
  STBls12381G2 -> NestedBigMapsAbsent
  STTimestamp -> NestedBigMapsAbsent
  STAddress -> NestedBigMapsAbsent
  STChest -> NestedBigMapsAbsent
  STChestKey -> NestedBigMapsAbsent
  STNever -> NestedBigMapsAbsent

-- | Check at runtime that a value of the given type cannot contain operations.
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
opAbsense s = case checkOpPresence s of
  OpPresent -> Nothing
  OpAbsent -> Just Dict

-- | Check at runtime that a value of the given type cannot contain @contract@ values.
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense s = case checkContractTypePresence s of
  ContractPresent -> Nothing
  ContractAbsent -> Just Dict

-- | Check at runtime that a value of the given type cannot contain @ticket@ values.
ticketAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoTicket t)
ticketAbsense s = case checkTicketPresence s of
  TicketPresent -> Nothing
  TicketAbsent -> Just Dict

-- | Check at runtime that a value of the given type cannot containt @big_map@ values
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense s = case checkBigMapPresence s of
  BigMapPresent -> Nothing
  BigMapAbsent -> Just Dict

-- | Check at runtime that a value of the given type cannot contain nested @big_map@s.
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense s = case checkNestedBigMapsPresence s of
  NestedBigMapsPresent -> Nothing
  NestedBigMapsAbsent -> Just Dict

----------------------------------------------------------------------------
-- Scopes
----------------------------------------------------------------------------

data BadTypeForScope
  = BtNotComparable
  | BtIsOperation
  | BtHasBigMap
  | BtHasNestedBigMap
  | BtHasContract
  | BtHasTicket
  deriving stock (Show, Eq, Generic)
  deriving anyclass (NFData)

instance Buildable BadTypeForScope where
  build = buildRenderDoc

instance RenderDoc BadTypeForScope where
  renderDoc _ = \case
    BtNotComparable -> "is not comparable"
    BtIsOperation -> "has 'operation' type"
    BtHasBigMap -> "has 'big_map'"
    BtHasNestedBigMap -> "has nested 'big_map'"
    BtHasContract -> "has 'contract' type"
    BtHasTicket -> "has 'ticket' type"

-- | Set of constraints that Michelson applies to parameters.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t
instance (SingI t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t

-- | Set of constraints that Michelson applies to contract storage.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t
instance (SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t

-- | Set of constraints that Michelson applies to pushed constants.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t) => ConstantScope t
instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t) => ConstantScope t

-- | Alias for constraints which Michelson requires in @DUP@ instruction.
class (SingI t, HasNoTicket t) => DupableScope t
instance (SingI t, HasNoTicket t) => DupableScope t

-- | Set of constraints that Michelson applies to packed values.
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => PackedValScope t
instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => PackedValScope t

-- | Set of constraints that Michelson applies to unpacked values.
--
-- It is different from 'PackedValScope', e.g. @contract@ type cannot appear
-- in a value we unpack to.
--
-- Not just a type alias in order to be able to partially apply it
class (PackedValScope t, ConstantScope t) => UnpackedValScope t
instance (PackedValScope t, ConstantScope t) => UnpackedValScope t

-- | Set of constraints that Michelson applies to argument type and
-- return type of views.
-- All info related to views can be found in
-- [TZIP](https://gitlab.com/tezos/tzip/-/blob/master/drafts/current/draft_views.md).
--
-- Not just a type alias in order to be able to partially apply it
class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t
instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t

-- | Alias for constraints which are required for untyped representation.
type UntypedValScope t = (SingI t, HasNoOp t)

----------------------------------------------------------------------------
-- Conveniences
----------------------------------------------------------------------------

-- | Should be present for common scopes.
class CheckScope (c :: Constraint) where
  -- | Check that constraint hold for a given type.
  checkScope :: Either BadTypeForScope (Dict c)

instance SingI t => CheckScope (HasNoOp t) where
  checkScope = maybeToRight BtIsOperation $ opAbsense sing
instance SingI t => CheckScope (HasNoBigMap t) where
  checkScope = maybeToRight BtHasBigMap $ bigMapAbsense sing
instance SingI t => CheckScope (HasNoNestedBigMaps t) where
  checkScope = maybeToRight BtHasNestedBigMap $ nestedBigMapsAbsense sing
instance SingI t => CheckScope (HasNoContract t) where
  checkScope = maybeToRight BtHasContract $ contractTypeAbsense sing
instance SingI t => CheckScope (HasNoTicket t) where
  checkScope = maybeToRight BtHasTicket $ ticketAbsense sing

instance SingI t => CheckScope (ParameterScope t) where
  checkScope =
    (\Dict Dict -> Dict)
      <$> checkScope @(HasNoOp t)
      <*> checkScope @(HasNoNestedBigMaps t)

instance SingI t => CheckScope (StorageScope t) where
  checkScope =
    (\Dict Dict Dict -> Dict)
      <$> checkScope @(HasNoOp t)
      <*> checkScope @(HasNoNestedBigMaps t)
      <*> checkScope @(HasNoContract t)

instance SingI t => CheckScope (ConstantScope t) where
  checkScope =
    (\Dict Dict Dict Dict -> Dict)
      <$> checkScope @(HasNoOp t)
      <*> checkScope @(HasNoBigMap t)
      <*> checkScope @(HasNoContract t)
      <*> checkScope @(HasNoTicket t)

instance SingI t => CheckScope (DupableScope t) where
  checkScope =
    (\Dict -> Dict)
      <$> checkScope @(HasNoTicket t)

instance SingI t => CheckScope (PackedValScope t) where
  checkScope =
    (\Dict Dict Dict -> Dict)
      <$> checkScope @(HasNoOp t)
      <*> checkScope @(HasNoBigMap t)
      <*> checkScope @(HasNoTicket t)

instance SingI t => CheckScope (UnpackedValScope t) where
  checkScope =
    (\Dict Dict -> Dict)
      <$> checkScope @(PackedValScope t)
      <*> checkScope @(ConstantScope t)

instance SingI t => CheckScope (ViewableScope t) where
  checkScope =
    (\Dict Dict Dict -> Dict)
      <$> checkScope @(HasNoOp t)
      <*> checkScope @(HasNoBigMap t)
      <*> checkScope @(HasNoTicket t)

-- | Allows using a scope that can be proven true with a De Morgan law.
--
-- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a
-- negative property we want to avoid as a 'Constraint'.
-- The negative constraints are implemented with a type family that for some
-- combination types resolves to itself applied to the type arguments in an @or@,
-- e.g. A @pair l r@ has @x@ if @l@ or @r@ contain @x@.
--
-- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@
-- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@.
--
-- GHC is however not able to prove this, so we need to use another (impossible)
-- 'error' to forcefully "prove" one of the two scopes.
-- Funnily enough however GHC is able to prove that if one holds then the other
-- does too, so we don't actually have to prove both, see 'mkWithDeMorgan'.
class WithDeMorganScope (c :: T -> Constraint) t a b where
  withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret

-- | Helper to builds a 'WithDeMorganScope' by using a 'CheckScope' that we know
-- cannot fail.
--
-- This can be used to make instances that also prove the other side of a
-- negative @or-like@ scope constraint, see 'WithDeMorganScope'.
mkWithDeMorgan
  :: forall scope a ret. CheckScope (scope a)
  => (scope a => ret) -> ret
mkWithDeMorgan f = fromRight (error "impossible") $ do
  Dict <- checkScope @(scope a)
  pure f

instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where
  withDeMorganScope = mkWithDeMorgan @HasNoOp @a

instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where
  withDeMorganScope = mkWithDeMorgan @HasNoContract @a

instance SingI a => WithDeMorganScope HasNoTicket 'TPair a b where
  withDeMorganScope = mkWithDeMorgan @HasNoTicket @a

instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where
  withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a

instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where
  withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a

instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where
  withDeMorganScope = mkWithDeMorgan @HasNoOp @a

instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where
  withDeMorganScope = mkWithDeMorgan @HasNoContract @a

instance SingI a => WithDeMorganScope HasNoTicket 'TOr a b where
  withDeMorganScope = mkWithDeMorgan @HasNoTicket @a

instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where
  withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a

instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where
  withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a

instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where
  withDeMorganScope = mkWithDeMorgan @HasNoOp @k

instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where
  withDeMorganScope = mkWithDeMorgan @HasNoOp @k

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoNestedBigMaps t a b
  , SingI a, SingI b
  ) => WithDeMorganScope ParameterScope t a b where
  withDeMorganScope f =
    withDeMorganScope @HasNoOp @t @a @b $
    withDeMorganScope @HasNoNestedBigMaps @t @a @b f

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoNestedBigMaps t a b
  , WithDeMorganScope HasNoContract t a b
  , SingI a, SingI b
  ) => WithDeMorganScope StorageScope t a b where
  withDeMorganScope f =
    withDeMorganScope @HasNoOp @t @a @b $
    withDeMorganScope @HasNoNestedBigMaps @t @a @b $
    withDeMorganScope @HasNoContract @t @a @b f

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoBigMap t a b
  , WithDeMorganScope HasNoContract t a b
  , WithDeMorganScope HasNoTicket t a b
  , SingI a, SingI b
  ) => WithDeMorganScope ConstantScope t a b where
  withDeMorganScope f =
    withDeMorganScope @HasNoOp @t @a @b $
    withDeMorganScope @HasNoBigMap @t @a @b $
    withDeMorganScope @HasNoContract @t @a @b $
    withDeMorganScope @HasNoTicket @t @a @b f

instance
  ( WithDeMorganScope HasNoOp t a b
  , WithDeMorganScope HasNoBigMap t a b
  , WithDeMorganScope HasNoTicket t a b
  , SingI a, SingI b
  ) => WithDeMorganScope PackedValScope t a b where
  withDeMorganScope f =
    withDeMorganScope @HasNoOp @t @a @b $
    withDeMorganScope @HasNoBigMap @t @a @b $
    withDeMorganScope @HasNoTicket @t @a @b f

instance
  ( WithDeMorganScope PackedValScope t a b
  , WithDeMorganScope ConstantScope t a b
  , SingI a, SingI b
  ) => WithDeMorganScope UnpackedValScope t a b where
  withDeMorganScope f =
    withDeMorganScope @PackedValScope @t @a @b $
    withDeMorganScope @ConstantScope @t @a @b f

-- Versions for eDSL
----------------------------------------------------------------------------

{- These constraints are supposed to be used only in eDSL code and eDSL should
define its own wrapers over it.
-}

type ProperParameterBetterErrors t =
  (SingI t, ForbidOp t, ForbidNestedBigMaps t)

type ProperStorageBetterErrors t =
  (SingI t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)

type ProperConstantBetterErrors t =
  (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t)

type ProperDupableBetterErrors t =
  (SingI t, ForbidTicket t)

type ProperPackedValBetterErrors t =
  (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)

type ProperUnpackedValBetterErrors t =
  (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)

type ProperViewableBetterErrors t =
  (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)

type ProperUntypedValBetterErrors t =
  (SingI t, ForbidOp t)

type ProperNonComparableValBetterErrors t =
  (SingI t, ForbidNonComparable t)

properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi = Sub $
  Dict \\ forbiddenOpEvi @t \\ forbiddenNestedBigMapsEvi @t

properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t
properStorageEvi = Sub $
  Dict \\ forbiddenOpEvi @t
       \\ forbiddenContractTypeEvi @t
       \\ forbiddenNestedBigMapsEvi @t
       \\ forbiddenContractTypeEvi @t

properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi = Sub $
  Dict \\ forbiddenOpEvi @t
       \\ forbiddenBigMapEvi @t
       \\ forbiddenContractTypeEvi @t
       \\ forbiddenTicketTypeEvi @t

properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t
properDupableEvi = Sub $
  Dict \\ forbiddenTicketTypeEvi @t

properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi = Sub $
  Dict \\ forbiddenOpEvi @t
       \\ forbiddenBigMapEvi @t
       \\ forbiddenTicketTypeEvi @t

properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi = Sub $
  Dict \\ properPackedValEvi @t
       \\ properConstantEvi @t

properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t
properViewableEvi = Sub $
  Dict \\ forbiddenOpEvi @t
       \\ forbiddenBigMapEvi @t
       \\ forbiddenTicketTypeEvi @t

properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t
properUntypedValEvi = Sub $
  Dict \\ forbiddenOpEvi @t