{-# LANGUAGE UndecidableSuperClasses #-}
module Lorentz.Constraints.Scopes
(
NiceComparable
, NiceConstant
, Dupable
, NiceFullPackedValue
, NicePackedValue
, NiceParameter
, NiceUntypedValue
, NiceStorage
, NiceStorageFull
, NiceUnpackedValue
, NiceViewable
, NiceNoBigMap
, niceParameterEvi
, niceStorageEvi
, niceConstantEvi
, dupableEvi
, nicePackedValueEvi
, niceUnpackedValueEvi
, niceUntypedValueEvi
, niceViewableEvi
, CanHaveBigMap
, KnownValue
, NoOperation
, NoContractType
, NoBigMap
,
withDict
) where
import Lorentz.Annotation (HasAnnotation)
import Morley.Michelson.Typed
class (IsoValue a, Typeable a) => KnownValue a
instance (IsoValue a, Typeable a) => KnownValue a
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
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)
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