{-# 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 Data.Constraint (evidence, trans, weaken1)
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))
niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi =
forall (t :: T). ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi @(ToT a) ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)))
:- ParameterScope (ToT a))
-> (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a))),
KnownValue a)
:- (SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a))))
-> ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a))),
KnownValue a)
:- ParameterScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a))),
KnownValue a)
:- (SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1
niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi =
(((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
FailOnContractFound (ContainsContract (ToT a))),
KnownValue a) =>
Dict (StorageScope (ToT a)))
-> ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
FailOnContractFound (ContainsContract (ToT a))),
KnownValue a)
:- StorageScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
FailOnContractFound (ContainsContract (ToT a)))
:- StorageScope (ToT a))
-> Dict (StorageScope (ToT a))
forall (c :: Constraint) e. HasDict c e => e -> Dict c
evidence (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
FailOnContractFound (ContainsContract (ToT a)))
:- StorageScope (ToT a))
-> Dict (StorageScope (ToT a)))
-> ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
FailOnContractFound (ContainsContract (ToT a)))
:- StorageScope (ToT a))
-> Dict (StorageScope (ToT a))
forall a b. (a -> b) -> a -> b
$ forall (t :: T). ProperStorageBetterErrors t :- StorageScope t
properStorageEvi @(ToT a))
niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi =
forall (t :: T). ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi @(ToT a) ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))
:- ConstantScope (ToT a))
-> (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
KnownValue a)
:- (SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))))
-> ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
KnownValue a)
:- ConstantScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
KnownValue a)
:- (SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1
dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)
dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)
dupableEvi =
forall (t :: T). ProperDupableBetterErrors t :- DupableScope t
properDupableEvi @(ToT a) ((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a)))
:- DupableScope (ToT a))
-> (((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
KnownValue a)
:- (SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))))
-> ((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
KnownValue a)
:- DupableScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` ((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
KnownValue a)
:- (SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a)))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1
nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi =
forall (t :: T). ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi @(ToT a) ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))
:- PackedValScope (ToT a))
-> (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
KnownValue a)
:- (SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))))
-> ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
KnownValue a)
:- PackedValScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
KnownValue a)
:- (SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1
niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi =
forall (t :: T).
ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi @(ToT a) (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
(SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))))
:- UnpackedValScope (ToT a))
-> ((((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
(SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
KnownValue a)
:- ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
(SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))))
-> (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
(SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
KnownValue a)
:- UnpackedValScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` (((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
(SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a)))),
KnownValue a)
:- ((SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))),
(SingI (ToT a), WellTyped (ToT a),
FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnContractFound (ContainsContract (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)),
FailOnSaplingStateFound (ContainsSaplingState (ToT a))))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1
niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a)
niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a)
niceUntypedValueEvi =
forall (t :: T).
ProperUntypedValBetterErrors t :- UntypedValScope t
properUntypedValEvi @(ToT a) ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)))
:- UntypedValScope (ToT a))
-> (((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a))),
KnownValue a)
:- (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a))))
-> ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a))),
KnownValue a)
:- UntypedValScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a))),
KnownValue a)
:- (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1
niceViewableEvi :: forall a. NiceViewable a :- ViewableScope (ToT a)
niceViewableEvi :: forall a. NiceViewable a :- ViewableScope (ToT a)
niceViewableEvi =
forall (t :: T). ProperViewableBetterErrors t :- ViewableScope t
properViewableEvi @(ToT a) ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)))
:- ViewableScope (ToT a))
-> (((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a))),
KnownValue a)
:- (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a))))
-> ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a))),
KnownValue a)
:- ViewableScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a))),
KnownValue a)
:- (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
FailOnBigMapFound (ContainsBigMap (ToT a)),
FailOnTicketFound (ContainsTicket (ToT a)))
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1