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

{-# OPTIONS_HADDOCK not-home #-}

module Morley.Michelson.Typed.Scope.Internal.Scopes
  ( module Morley.Michelson.Typed.Scope.Internal.Scopes
  ) where

import Data.Singletons (SingI)
import Data.Type.Bool (Not)

import Morley.Michelson.Typed.Scope.Internal.Comparable
import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Scope.Internal.WellTyped
import Morley.Michelson.Typed.T (T(..))

{- $setup
>>> import Morley.Michelson.Typed.Scope
>>> import Morley.Michelson.Typed (T(..), SingT(..))
>>> import Morley.Util.Peano (pattern S, pattern Z)
>>> import Data.Type.Equality ((:~:)(..))
-}

{-
Note [WellTyped constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~

Try to put WellTyped constraint at the end of instance constraints. Because
WellTyped is a recursive type class, it loses context when it recurses, unlike
ForbidT constraints which do a type-family based check. The consequence is,
ForbidT constraints produce error messages with more context. The intention is
to show more informative errors first.

-- @lierdakil
-}

-- | Common constraints used for scopes defined below.
type CommonScopeC c ps t = (SingI t, ForbidManyT c ps t, WellTyped t)

{- | Set of constraints that Michelson applies to parameters.

Not just a type alias in order to be able to partially apply it

Produces human-readable error messages:

>>> () :: ParameterScope (TBigMap TUnit (TBigMap TUnit TOperation)) => ()
...
... Type `operation` found in
... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation)
... is not allowed in this scope
...
... Nested `big_map`s found in
... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation)
... are not allowed
...
>>> () :: ParameterScope (TBigMap TInt TNat) => ()
()

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ParameterScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation` or nested `big_map`s. Perhaps you need to add
... ParameterScope t0
... constraint? You can also try adding a type annotation.
...
-}
class ParameterScopeC (ParameterScope t) t => ParameterScope t
instance ParameterScopeC (ParameterScope t) t => ParameterScope t
type ParameterScopeC c t = CommonScopeC c ['PSOp, 'PSNestedBigMaps] t

{- | Set of constraints that Michelson applies to contract storage.

Not just a type alias in order to be able to partially apply it

Produces human-readable error messages:

>>> () :: StorageScope (TContract TOperation) => ()
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...
... Type `contract` found in
... 'TContract 'TOperation
... is not allowed in this scope
...
>>> () :: StorageScope TUnit => ()
()

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: StorageScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, nested `big_map`s or `contract`. Perhaps you need to add
... StorageScope t0
... constraint? You can also try adding a type annotation.
...
-}
class StorageScopeC (StorageScope t) t  => StorageScope t
instance StorageScopeC (StorageScope t) t => StorageScope t
type StorageScopeC c t = CommonScopeC c ['PSOp, 'PSNestedBigMaps, 'PSContract] t

{- | Set of constraints that Michelson applies to pushed constants.

Not just a type alias in order to be able to partially apply it

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ConstantScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
... ConstantScope t0
... constraint? You can also try adding a type annotation.
...
-}
class ConstantScopeC (ConstantScope t) t  => ConstantScope t
instance ConstantScopeC (ConstantScope t) t => ConstantScope t
type ConstantScopeC c t =
  CommonScopeC c ['PSOp, 'PSBigMap, 'PSContract, 'PSTicket, 'PSSaplingState] t

{- | Alias for constraints which Michelson requires in @DUP@ instruction.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: DupableScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `ticket`. Perhaps you need to add
... DupableScope t0
... constraint? You can also try adding a type annotation.
...
-}
class DupableScopeC (DupableScope t) t  => DupableScope t
instance DupableScopeC (DupableScope t) t => DupableScope t
type DupableScopeC c t = (SingI t, ForbidManyT c '[ 'PSTicket] t)

-- | Returns whether the type is dupable.
type family IsDupableScope (t :: T) :: Bool where
  IsDupableScope t = Not (ContainsT 'PSTicket t)

{- | Set of constraints that Michelson applies to packed values.

Not just a type alias in order to be able to partially apply it.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: PackedValScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map`, `ticket` or `sapling_state`. Perhaps you need to add
... PackedValScope t0
... constraint? You can also try adding a type annotation.
...
-}
class PackedValScopeC (PackedValScope t) t => PackedValScope t
instance PackedValScopeC (PackedValScope t) t => PackedValScope t
type PackedValScopeC c t =
  CommonScopeC c ['PSOp, 'PSBigMap, 'PSTicket, 'PSSaplingState] t

{- | Set of constraints that Michelson applies to unpacked values.
Same as 'ConstantScope'.

Not just a type alias in order to show better errors on ambiguity or missing
constraint.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: UnpackedValScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
... UnpackedValScope t0
... constraint? You can also try adding a type annotation.
...
-}
class UnpackedValScopeC (UnpackedValScope t) t => UnpackedValScope t
instance UnpackedValScopeC (UnpackedValScope t) t => UnpackedValScope t
type UnpackedValScopeC c t = ConstantScopeC c 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.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ViewableScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`, `big_map` or `ticket`. Perhaps you need to add
... ViewableScope t0
... constraint? You can also try adding a type annotation.
...
-}
class ViewableScopeC (ViewableScope t) t => ViewableScope t
instance ViewableScopeC (ViewableScope t) t => ViewableScope t
type ViewableScopeC c t = (SingI t, ForbidManyT c ['PSOp, 'PSBigMap, 'PSTicket] t)

{- | Alias for constraints which are required for untyped representation.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: UntypedValScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains `operation`. Perhaps you need to add
... UntypedValScope t0
... constraint? You can also try adding a type annotation.
...
-}
class UntypedValScopeC (UntypedValScope t) t => UntypedValScope t
instance UntypedValScopeC (UntypedValScope t) t => UntypedValScope t
type UntypedValScopeC c t = (SingI t, ForbidManyT c '[ 'PSOp] t)

{- | Alias for comparable types.

On ambiguous or polymorphic types, suggests adding the constraint:

>>> (const () :: ComparabilityScope t => f t -> ()) undefined
...
... Can't check if type
... t0
... contains non-comparable types. Perhaps you need to add
... ComparabilityScope t0
... constraint? You can also try adding a type annotation.
...
-}
class ComparabilityScopeC (ComparabilityScope t) t => ComparabilityScope t
instance ComparabilityScopeC (ComparabilityScope t) t => ComparabilityScope t
type ComparabilityScopeC c t = (SingI t, ForbidManyT c '[ 'PSNonComparable ] t, Comparable t)