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