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

{-# LANGUAGE UndecidableSuperClasses #-}

-- | Scope-related constraints used in Lorentz.
--
-- This contains constraints from "Morley.Michelson.Typed.Scope" modified for use
-- in Lorentz.
module Lorentz.Constraints.Scopes
  ( -- * Grouped constraints
    NiceComparable
  , NiceConstant
  , Dupable
  , NiceFullPackedValue
  , NicePackedValue
  , NiceParameter
  , NiceUntypedValue
  , NiceStorage
  , NiceStorageFull
  , NiceUnpackedValue
  , NiceViewable
  , NiceNoBigMap

  , niceParameterEvi
  , niceStorageEvi
  , niceConstantEvi
  , dupableEvi
  , nicePackedValueEvi
  , niceUnpackedValueEvi
  , niceUntypedValueEvi
  , niceViewableEvi

    -- * Individual constraints (internals)
  , CanHaveBigMap
  , KnownValue
  , NoOperation
  , NoContractType
  , NoBigMap

  , -- * Re-exports
    withDict
  ) where

import Lorentz.Annotation (HasAnnotation)
import Morley.Michelson.Typed

-- We write these constraints as class + instance, rather than
-- type aliases, in order to allow their partial application.

-- | Gathers constraints, commonly required for values.
class (IsoValue a, Typeable a) => KnownValue a
instance (IsoValue a, Typeable a) => KnownValue a

-- | Ensure given type does not contain "operation".
class (ForbidOp (ToT a), IsoValue a) => NoOperation a
instance (ForbidOp (ToT a), IsoValue a) => NoOperation a

class (ForbidContract (ToT a), IsoValue a) => NoContractType a
instance (ForbidContract (ToT a), IsoValue a) => NoContractType a

class (ForbidBigMap (ToT a), IsoValue a) => NoBigMap a
instance (ForbidBigMap (ToT a), IsoValue a) => NoBigMap a

class (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a
instance (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a

-- | Constraint applied to any part of a parameter type.
--
-- Use t'Lorentz.Constraints.Derivative.NiceParameterFull' instead
-- when you need to know the contract's entrypoints at compile-time.
type NiceParameter a = (ProperParameterBetterErrors (ToT a), KnownValue a)

type NiceStorage a = (ProperStorageBetterErrors (ToT a), KnownValue a)

type NiceStorageFull a = (NiceStorage a, HasAnnotation a)

type NiceConstant a = (ProperConstantBetterErrors (ToT a), KnownValue a)

type Dupable a = (ProperDupableBetterErrors (ToT a), KnownValue a)

type NicePackedValue a = (ProperPackedValBetterErrors (ToT a), KnownValue a)

type NiceUnpackedValue a = (ProperUnpackedValBetterErrors (ToT a), KnownValue a)

type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a)

type NiceUntypedValue a = (ProperUntypedValBetterErrors (ToT a), KnownValue a)

type NiceViewable a = (ProperViewableBetterErrors (ToT a), KnownValue a)

-- | Constraint applied to any type, to check if Michelson representation (if exists) of this
-- type is Comparable. In case it is not prints human-readable error message
type NiceComparable n = (ProperNonComparableValBetterErrors (ToT n), KnownValue n, Comparable (ToT n))

type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n))

{-# DEPRECATED niceParameterEvi, niceStorageEvi, niceConstantEvi, dupableEvi
  , nicePackedValueEvi, niceUnpackedValueEvi, niceUntypedValueEvi
  , niceViewableEvi
  "This is no longer needed; the constraint implication is now trivial."
 #-}
niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi = (((SingI (ToT a), WellTyped (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsNestedBigMaps (ToT a)) 'False))
      ('Text "Nested BigMaps are not allowed")
      (() :: Constraint),
    ContainsNestedBigMaps (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (ParameterScope (ToT a)))
-> ((SingI (ToT a), WellTyped (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp (ToT a)) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsNestedBigMaps (ToT a)) 'False))
        ('Text "Nested BigMaps are not allowed")
        (() :: Constraint),
      ContainsNestedBigMaps (ToT a) ~ 'False)),
    KnownValue a)
   :- ParameterScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a), WellTyped (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp (ToT a)) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsNestedBigMaps (ToT a)) 'False))
     ('Text "Nested BigMaps are not allowed")
     (() :: Constraint),
   ContainsNestedBigMaps (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (ParameterScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi = (((SingI (ToT a), WellTyped (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsNestedBigMaps (ToT a)) 'False))
      ('Text "Nested BigMaps are not allowed")
      (() :: Constraint),
    ContainsNestedBigMaps (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsContract (ToT a)) 'False))
      ('Text "Type `contract` is not allowed in this scope")
      (() :: Constraint),
    ContainsContract (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (StorageScope (ToT a)))
-> ((SingI (ToT a), WellTyped (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp (ToT a)) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsNestedBigMaps (ToT a)) 'False))
        ('Text "Nested BigMaps are not allowed")
        (() :: Constraint),
      ContainsNestedBigMaps (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsContract (ToT a)) 'False))
        ('Text "Type `contract` is not allowed in this scope")
        (() :: Constraint),
      ContainsContract (ToT a) ~ 'False)),
    KnownValue a)
   :- StorageScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a), WellTyped (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp (ToT a)) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsNestedBigMaps (ToT a)) 'False))
     ('Text "Nested BigMaps are not allowed")
     (() :: Constraint),
   ContainsNestedBigMaps (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsContract (ToT a)) 'False))
     ('Text "Type `contract` is not allowed in this scope")
     (() :: Constraint),
   ContainsContract (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (StorageScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi = (((SingI (ToT a), WellTyped (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsContract (ToT a)) 'False))
      ('Text "Type `contract` is not allowed in this scope")
      (() :: Constraint),
    ContainsContract (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
      ('Text "Type `sapling_state` is not allowed in this scope")
      (() :: Constraint),
    ContainsSaplingState (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (ConstantScope (ToT a)))
-> ((SingI (ToT a), WellTyped (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp (ToT a)) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
        ('Text "BigMaps are not allowed in this scope")
        (() :: Constraint),
      ContainsBigMap (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsContract (ToT a)) 'False))
        ('Text "Type `contract` is not allowed in this scope")
        (() :: Constraint),
      ContainsContract (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
        ('Text "Type `ticket` is not allowed in this scope")
        (() :: Constraint),
      ContainsTicket (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
        ('Text "Type `sapling_state` is not allowed in this scope")
        (() :: Constraint),
      ContainsSaplingState (ToT a) ~ 'False)),
    KnownValue a)
   :- ConstantScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a), WellTyped (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp (ToT a)) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsContract (ToT a)) 'False))
     ('Text "Type `contract` is not allowed in this scope")
     (() :: Constraint),
   ContainsContract (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
     ('Text "Type `sapling_state` is not allowed in this scope")
     (() :: Constraint),
   ContainsSaplingState (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (ConstantScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)
dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)
dupableEvi = (((SingI (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (DupableScope (ToT a)))
-> ((SingI (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
        ('Text "Type `ticket` is not allowed in this scope")
        (() :: Constraint),
      ContainsTicket (ToT a) ~ 'False)),
    KnownValue a)
   :- DupableScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (DupableScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi = (((SingI (ToT a), WellTyped (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
      ('Text "Type `sapling_state` is not allowed in this scope")
      (() :: Constraint),
    ContainsSaplingState (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (PackedValScope (ToT a)))
-> ((SingI (ToT a), WellTyped (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp (ToT a)) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
        ('Text "BigMaps are not allowed in this scope")
        (() :: Constraint),
      ContainsBigMap (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
        ('Text "Type `ticket` is not allowed in this scope")
        (() :: Constraint),
      ContainsTicket (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
        ('Text "Type `sapling_state` is not allowed in this scope")
        (() :: Constraint),
      ContainsSaplingState (ToT a) ~ 'False)),
    KnownValue a)
   :- PackedValScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a), WellTyped (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp (ToT a)) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
     ('Text "Type `sapling_state` is not allowed in this scope")
     (() :: Constraint),
   ContainsSaplingState (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (PackedValScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi = ((((SingI (ToT a), WellTyped (ToT a),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp (ToT a)) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
       ('Text "BigMaps are not allowed in this scope")
       (() :: Constraint),
     ContainsBigMap (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
       ('Text "Type `sapling_state` is not allowed in this scope")
       (() :: Constraint),
     ContainsSaplingState (ToT a) ~ 'False)),
   (SingI (ToT a), WellTyped (ToT a),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsOp (ToT a)) 'False))
       ('Text "Operations are not allowed in this scope")
       (() :: Constraint),
     ContainsOp (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
       ('Text "BigMaps are not allowed in this scope")
       (() :: Constraint),
     ContainsBigMap (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsContract (ToT a)) 'False))
       ('Text "Type `contract` is not allowed in this scope")
       (() :: Constraint),
     ContainsContract (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
       ('Text "Type `ticket` is not allowed in this scope")
       (() :: Constraint),
     ContainsTicket (ToT a) ~ 'False),
    (FailWhenElsePoly
       (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
       ('Text "Type `sapling_state` is not allowed in this scope")
       (() :: Constraint),
     ContainsSaplingState (ToT a) ~ 'False))),
  KnownValue a) =>
 Dict (UnpackedValScope (ToT a)))
-> (((SingI (ToT a), WellTyped (ToT a),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsOp (ToT a)) 'False))
         ('Text "Operations are not allowed in this scope")
         (() :: Constraint),
       ContainsOp (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
         ('Text "BigMaps are not allowed in this scope")
         (() :: Constraint),
       ContainsBigMap (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
         ('Text "Type `ticket` is not allowed in this scope")
         (() :: Constraint),
       ContainsTicket (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
         ('Text "Type `sapling_state` is not allowed in this scope")
         (() :: Constraint),
       ContainsSaplingState (ToT a) ~ 'False)),
     (SingI (ToT a), WellTyped (ToT a),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsOp (ToT a)) 'False))
         ('Text "Operations are not allowed in this scope")
         (() :: Constraint),
       ContainsOp (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
         ('Text "BigMaps are not allowed in this scope")
         (() :: Constraint),
       ContainsBigMap (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsContract (ToT a)) 'False))
         ('Text "Type `contract` is not allowed in this scope")
         (() :: Constraint),
       ContainsContract (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
         ('Text "Type `ticket` is not allowed in this scope")
         (() :: Constraint),
       ContainsTicket (ToT a) ~ 'False),
      (FailWhenElsePoly
         (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
         ('Text "Type `sapling_state` is not allowed in this scope")
         (() :: Constraint),
       ContainsSaplingState (ToT a) ~ 'False))),
    KnownValue a)
   :- UnpackedValScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI (ToT a), WellTyped (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
      ('Text "Type `sapling_state` is not allowed in this scope")
      (() :: Constraint),
    ContainsSaplingState (ToT a) ~ 'False)),
  (SingI (ToT a), WellTyped (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsContract (ToT a)) 'False))
      ('Text "Type `contract` is not allowed in this scope")
      (() :: Constraint),
    ContainsContract (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsSaplingState (ToT a)) 'False))
      ('Text "Type `sapling_state` is not allowed in this scope")
      (() :: Constraint),
    ContainsSaplingState (ToT a) ~ 'False))),
 KnownValue a) =>
Dict (UnpackedValScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a)
niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a)
niceUntypedValueEvi = (((SingI (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (UntypedValScope (ToT a)))
-> ((SingI (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp (ToT a)) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp (ToT a) ~ 'False)),
    KnownValue a)
   :- UntypedValScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp (ToT a)) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (UntypedValScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict

niceViewableEvi :: forall a. NiceViewable a :- ViewableScope (ToT a)
niceViewableEvi :: forall a. NiceViewable a :- ViewableScope (ToT a)
niceViewableEvi = (((SingI (ToT a),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsOp (ToT a)) 'False))
      ('Text "Operations are not allowed in this scope")
      (() :: Constraint),
    ContainsOp (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
      ('Text "BigMaps are not allowed in this scope")
      (() :: Constraint),
    ContainsBigMap (ToT a) ~ 'False),
   (FailWhenElsePoly
      (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
      ('Text "Type `ticket` is not allowed in this scope")
      (() :: Constraint),
    ContainsTicket (ToT a) ~ 'False)),
  KnownValue a) =>
 Dict (ViewableScope (ToT a)))
-> ((SingI (ToT a),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsOp (ToT a)) 'False))
        ('Text "Operations are not allowed in this scope")
        (() :: Constraint),
      ContainsOp (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
        ('Text "BigMaps are not allowed in this scope")
        (() :: Constraint),
      ContainsBigMap (ToT a) ~ 'False),
     (FailWhenElsePoly
        (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
        ('Text "Type `ticket` is not allowed in this scope")
        (() :: Constraint),
      ContainsTicket (ToT a) ~ 'False)),
    KnownValue a)
   :- ViewableScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI (ToT a),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsOp (ToT a)) 'False))
     ('Text "Operations are not allowed in this scope")
     (() :: Constraint),
   ContainsOp (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsBigMap (ToT a)) 'False))
     ('Text "BigMaps are not allowed in this scope")
     (() :: Constraint),
   ContainsBigMap (ToT a) ~ 'False),
  (FailWhenElsePoly
     (Not (DefaultEq (ContainsTicket (ToT a)) 'False))
     ('Text "Type `ticket` is not allowed in this scope")
     (() :: Constraint),
   ContainsTicket (ToT a) ~ 'False)),
 KnownValue a) =>
Dict (ViewableScope (ToT a))
forall (a :: Constraint). a => Dict a
Dict