-- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA {-# LANGUAGE UndecidableSuperClasses #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-} {- | Module, containing restrictions imposed by instruction or value scope. Michelson have multiple restrictions on values, examples: * @operation@ type cannot appear in parameter. * @big_map@ type cannot appear in @PUSH@-able constants. * @contract@ type cannot appear in type we @UNPACK@ to. Thus we declare multiple "scopes" - constraints applied in corresponding situations, for instance * 'ParameterScope'; * 'StorageScope'; * 'ConstantScope'. Also we separate multiple "classes" of scope-related constraints. * 'ParameterScope' and similar ones are used within Michelson engine, they are understandable by GHC but produce not very clarifying errors. * 'ProperParameterBetterErrors' and similar ones are middle-layer constraints, they produce human-readable errors but GHC cannot make conclusions from them. They are supposed to be used only by eDSLs to define their own high-level constraints. * Lorentz and other eDSLs may declare their own constraints, in most cases you should use them. For example see @Lorentz.Constraints@ module. -} module Morley.Michelson.Typed.Scope ( -- * Scopes ConstantScope , DupableScope , StorageScope , PackedValScope , ParameterScope , UntypedValScope , UnpackedValScope , ViewableScope , ComparabilityScope , ProperParameterBetterErrors , ProperStorageBetterErrors , ProperConstantBetterErrors , ProperDupableBetterErrors , ProperPackedValBetterErrors , ProperUnpackedValBetterErrors , ProperUntypedValBetterErrors , ProperViewableBetterErrors , ProperNonComparableValBetterErrors , IsDupableScope , properParameterEvi , properStorageEvi , properConstantEvi , properDupableEvi , properPackedValEvi , properUnpackedValEvi , properViewableEvi , properUntypedValEvi , (:-)(..) , BadTypeForScope (..) , CheckScope (..) , WithDeMorganScope (..) , Comparable (..) , WellTyped (..) , NotWellTyped (..) -- * Implementation internals , HasNoBigMap , HasNoNestedBigMaps , HasNoOp , HasNoContract , HasNoTicket , ContainsBigMap , ContainsContract , ContainsNestedBigMaps , ContainsOp , ContainsTicket , IsComparable , ForbidOp , ForbidContract , ForbidTicket , ForbidBigMap , ForbidNestedBigMaps , ForbidNonComparable , FailOnBigMapFound , FailOnContractFound , FailOnNestedBigMapsFound , FailOnOperationFound , FailOnTicketFound , FailOnNonComparableFound , OpPresence (..) , ContractPresence (..) , TicketPresence (..) , BigMapPresence (..) , NestedBigMapsPresence (..) , checkOpPresence , checkContractTypePresence , checkTicketPresence , checkBigMapPresence , checkNestedBigMapsPresence , comparabilityPresence , opAbsense , contractTypeAbsense , bigMapAbsense , nestedBigMapsAbsense , forbiddenOp , forbiddenContractType , forbiddenBigMap , forbiddenNestedBigMaps , Comparability(..) , checkComparability , getComparableProofS , getWTP , getWTP' -- * Re-exports , withDict , SingI (..) ) where import Data.Bool.Singletons (SBool(..)) import Data.Constraint (Dict(..), withDict, (:-)(..), (\\)) import Data.Singletons (SLambda(..), Sing, SingI(..), fromSing, type (@@), type (~>), type Apply, withSingI, (@@)) import Data.Type.Bool (Not, type (&&), type (||)) import Fmt (Buildable(..)) import GHC.TypeLits (ErrorMessage(..), TypeError) import Data.Type.Equality ((:~:)(..)) import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc) import Morley.Michelson.Typed.Sing (SingT(..)) import Morley.Michelson.Typed.T (T(..)) import Unsafe.Coerce (unsafeCoerce) ---------------------------------------------------------------------------- -- Constraints ---------------------------------------------------------------------------- -- | Whether a value of this type _may_ contain an operation. -- -- In some scopes (constants, parameters, storage) appearing for operation type -- is prohibited. -- Operations in input/output of lambdas are allowed without limits though. type family ContainsOp (t :: T) :: Bool where ContainsOp 'TKey = 'False ContainsOp 'TUnit = 'False ContainsOp 'TSignature = 'False ContainsOp 'TChainId = 'False ContainsOp ('TOption t) = ContainsOp t ContainsOp ('TList t) = ContainsOp t ContainsOp ('TSet t) = ContainsOp t ContainsOp 'TOperation = 'True ContainsOp ('TContract _) = 'False ContainsOp ('TTicket t) = ContainsOp t ContainsOp ('TPair a b) = ContainsOp a || ContainsOp b ContainsOp ('TOr a b) = ContainsOp a || ContainsOp b ContainsOp ('TLambda _ _) = 'False ContainsOp ('TMap k v) = ContainsOp k || ContainsOp v ContainsOp ('TBigMap k v) = ContainsOp k || ContainsOp v ContainsOp _ = 'False -- | Whether a value of this type _may_ contain a @contract@ value. -- -- In some scopes (constants, storage) appearing for contract type -- is prohibited. -- Contracts in input/output of lambdas are allowed without limits though. type family ContainsContract (t :: T) :: Bool where ContainsContract 'TKey = 'False ContainsContract 'TUnit = 'False ContainsContract 'TSignature = 'False ContainsContract 'TChainId = 'False ContainsContract ('TOption t) = ContainsContract t ContainsContract ('TList t) = ContainsContract t ContainsContract ('TSet _) = 'False ContainsContract 'TOperation = 'False ContainsContract ('TContract _) = 'True ContainsContract ('TPair a b) = ContainsContract a || ContainsContract b ContainsContract ('TOr a b) = ContainsContract a || ContainsContract b ContainsContract ('TLambda _ _) = 'False ContainsContract ('TMap _ v) = ContainsContract v ContainsContract ('TBigMap _ v) = ContainsContract v ContainsContract _ = 'False -- | Whether a value of this type _may_ contain a @ticket@ value. type family ContainsTicket (t :: T) :: Bool where ContainsTicket ('TOption t) = ContainsTicket t ContainsTicket ('TList t) = ContainsTicket t ContainsTicket ('TSet _) = 'False ContainsTicket ('TTicket _) = 'True ContainsTicket ('TPair a b) = ContainsTicket a || ContainsTicket b ContainsTicket ('TOr a b) = ContainsTicket a || ContainsTicket b ContainsTicket ('TLambda _ _) = 'False ContainsTicket ('TMap _ v) = ContainsTicket v ContainsTicket ('TBigMap _ v) = ContainsTicket v ContainsTicket _ = 'False -- | Whether a value of this type _may_ contain a @big_map@ value. type family ContainsBigMap (t :: T) :: Bool where ContainsBigMap 'TKey = 'False ContainsBigMap 'TUnit = 'False ContainsBigMap 'TSignature = 'False ContainsBigMap 'TChainId = 'False ContainsBigMap ('TOption t) = ContainsBigMap t ContainsBigMap ('TList t) = ContainsBigMap t ContainsBigMap ('TSet _) = 'False ContainsBigMap 'TOperation = 'False ContainsBigMap ('TContract _) = 'False ContainsBigMap ('TPair a b) = ContainsBigMap a || ContainsBigMap b ContainsBigMap ('TOr a b) = ContainsBigMap a || ContainsBigMap b ContainsBigMap ('TLambda _ _) = 'False ContainsBigMap ('TMap _ v) = ContainsBigMap v ContainsBigMap ('TBigMap _ _) = 'True ContainsBigMap _ = 'False -- | Whether a value of this type _may_ contain nested @big_map@s. -- -- Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are -- prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more -- strict because they don't work with big_map at all. type family ContainsNestedBigMaps (t :: T) :: Bool where ContainsNestedBigMaps 'TKey = 'False ContainsNestedBigMaps 'TUnit = 'False ContainsNestedBigMaps 'TSignature = 'False ContainsNestedBigMaps 'TChainId = 'False ContainsNestedBigMaps ('TOption t) = ContainsNestedBigMaps t ContainsNestedBigMaps ('TList t) = ContainsNestedBigMaps t ContainsNestedBigMaps ('TSet _) = 'False ContainsNestedBigMaps 'TOperation = 'False ContainsNestedBigMaps ('TContract _) = 'False ContainsNestedBigMaps ('TPair a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b ContainsNestedBigMaps ('TOr a b) = ContainsNestedBigMaps a || ContainsNestedBigMaps b ContainsNestedBigMaps ('TLambda _ _) = 'False ContainsNestedBigMaps ('TMap _ v) = ContainsNestedBigMaps v ContainsNestedBigMaps ('TBigMap _ v) = ContainsBigMap v ContainsNestedBigMaps _ = 'False -- | Whether a value of this type _may_ contain a @samping_state@ value. type family ContainsSaplingState (t :: T) :: Bool where ContainsSaplingState ('TOption t) = ContainsSaplingState t ContainsSaplingState ('TList t) = ContainsSaplingState t ContainsSaplingState ('TPair a b) = ContainsSaplingState a || ContainsSaplingState b ContainsSaplingState ('TOr a b) = ContainsSaplingState a || ContainsSaplingState b ContainsSaplingState ('TMap _ v) = ContainsSaplingState v ContainsSaplingState ('TBigMap _ v) = ContainsSaplingState v ContainsSaplingState ('TSaplingState _) = 'True ContainsSaplingState _ = 'False -- | Constraint which ensures that type is comparable. type family IsComparable (t :: T) :: Bool where IsComparable ('TPair a b) = IsComparable a && IsComparable b IsComparable ('TOption t) = IsComparable t IsComparable 'TBls12381Fr = 'False IsComparable 'TBls12381G1 = 'False IsComparable 'TBls12381G2 = 'False IsComparable ('TList _) = 'False IsComparable ('TSet _) = 'False IsComparable 'TOperation = 'False IsComparable ('TContract _) = 'False IsComparable ('TTicket _) = 'False IsComparable ('TOr a b) = IsComparable a && IsComparable b IsComparable ('TLambda _ _) = 'False IsComparable ('TMap _ _) = 'False IsComparable ('TBigMap _ _) = 'False IsComparable 'TChest = 'False IsComparable 'TChestKey = 'False IsComparable ('TSaplingState _) = 'False IsComparable ('TSaplingTransaction _) = 'False IsComparable _ = 'True -- | Constraint which ensures that a value of type @t@ does not contain operations. -- -- Not just a type alias in order to be able to partially apply it -- (e.g. in 'Each'). class (ContainsOp t ~ 'False) => HasNoOp t instance (ContainsOp t ~ 'False) => HasNoOp t -- | Constraint which ensures that a value of type @t@ does not contain @contract@ values. class (ContainsContract t ~ 'False) => HasNoContract t instance (ContainsContract t ~ 'False) => HasNoContract t -- | Constraint which ensures that a value of type @t@ does not contain @ticket@ values. class (ContainsTicket t ~ 'False) => HasNoTicket t instance (ContainsTicket t ~ 'False) => HasNoTicket t -- | Constraint which ensures that a value of type @t@ does not contain @big_map@ values. class (ContainsBigMap t ~ 'False) => HasNoBigMap t instance (ContainsBigMap t ~ 'False) => HasNoBigMap t -- | Constraint which ensures that a value of type @t@ does not contain @sapling_state@ values. class (ContainsSaplingState t ~ 'False) => HasNoSaplingState t instance (ContainsSaplingState t ~ 'False) => HasNoSaplingState t -- | Constraint which ensures that there are no nested bigmaps. class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t -- | Report a human-readable error about 'TOperation' at a wrong place. type family FailOnOperationFound (enabled :: Bool) :: Constraint where FailOnOperationFound 'True = TypeError ('Text "Operations are not allowed in this scope") FailOnOperationFound 'False = () -- | Report a human-readable error about 'TContract' at a wrong place. type family FailOnContractFound (enabled :: Bool) :: Constraint where FailOnContractFound 'True = TypeError ('Text "Type `contract` is not allowed in this scope") FailOnContractFound 'False = () -- | Report a human-readable error about 'TTicket' at a wrong place. type family FailOnTicketFound (enabled :: Bool) :: Constraint where FailOnTicketFound 'True = TypeError ('Text "Type `ticket` is not allowed in this scope") FailOnTicketFound 'False = () -- | Report a human-readable error about 'TSaplingState' at a wrong place. type family FailOnSaplingStateFound (enabled :: Bool) :: Constraint where FailOnSaplingStateFound 'True = TypeError ('Text "Type `sapling_state` is not allowed in this scope") FailOnSaplingStateFound 'False = () -- | Report a human-readable error about 'TBigMap' at a wrong place. type family FailOnBigMapFound (enabled :: Bool) :: Constraint where FailOnBigMapFound 'True = TypeError ('Text "BigMaps are not allowed in this scope") FailOnBigMapFound 'False = () -- | Report a human-readable error that 'TBigMap' contains another 'TBigMap' type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where FailOnNestedBigMapsFound 'True = TypeError ('Text "Nested BigMaps are not allowed") FailOnNestedBigMapsFound 'False = () -- | Report a human-readable error that given value is not comparable type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where FailOnNonComparableFound 'True = () FailOnNonComparableFound 'False = TypeError ('Text "Only comparable types are allowed here") -- | This is like 'HasNoOp', it raises a more human-readable error -- when @t@ type is concrete, but GHC cannot make any conclusions -- from such constraint as it can for 'HasNoOp'. -- Though, hopefully, it will someday: -- . -- -- Use this constraint in our eDSL. type ForbidOp t = FailOnOperationFound (ContainsOp t) type ForbidContract t = FailOnContractFound (ContainsContract t) type ForbidTicket t = FailOnTicketFound (ContainsTicket t) type ForbidSaplingState t = FailOnSaplingStateFound (ContainsSaplingState t) type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t) type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t) -- | Constraint that rises human-readable error message, in case given value -- can't be compared type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t) -- | Evidence of that 'HasNoOp' is deducable from 'ForbidOp'. forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t forbiddenOpEvi = Sub $ -- It's not clear now to proof GHC that @HasNoOp t@ is implication of -- @ForbidOp t@, so we use @error@ below and also disable -- "-Wredundant-constraints" extension. case checkOpPresence (sing @t) of OpAbsent -> Dict OpPresent -> error "impossible" -- | Reify 'HasNoOp' contraint from 'ForbidOp'. -- -- Left for backward compatibility. forbiddenOp :: forall t a. (SingI t, ForbidOp t) => (HasNoOp t => a) -> a forbiddenOp = withDict $ forbiddenOpEvi @t forbiddenBigMapEvi :: forall t. (SingI t, ForbidBigMap t) :- HasNoBigMap t forbiddenBigMapEvi = Sub $ case checkBigMapPresence (sing @t) of BigMapAbsent -> Dict BigMapPresent -> error "impossible" forbiddenNestedBigMapsEvi :: forall t. (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t forbiddenNestedBigMapsEvi = Sub $ case checkNestedBigMapsPresence (sing @t) of NestedBigMapsAbsent -> Dict NestedBigMapsPresent -> error "impossible" forbiddenBigMap :: forall t a. (SingI t, ForbidBigMap t) => (HasNoBigMap t => a) -> a forbiddenBigMap = withDict $ forbiddenBigMapEvi @t forbiddenNestedBigMaps :: forall t a. (SingI t, ForbidNestedBigMaps t) => (HasNoNestedBigMaps t => a) -> a forbiddenNestedBigMaps = withDict $ forbiddenNestedBigMapsEvi @t -- | Reify 'HasNoContract' contraint from 'ForbidContract'. forbiddenContractTypeEvi :: forall t. (SingI t, ForbidContract t) :- HasNoContract t forbiddenContractTypeEvi = Sub $ case checkContractTypePresence (sing @t) of ContractAbsent -> Dict ContractPresent -> error "impossible" -- | Reify 'HasNoContract' contraint from 'ForbidContract'. forbiddenContractType :: forall t a. (SingI t, ForbidContract t) => (HasNoContract t => a) -> a forbiddenContractType = withDict $ forbiddenContractTypeEvi @t -- | Reify 'HasNoTicket' contraint from 'ForbidTicket'. forbiddenTicketTypeEvi :: forall t. (SingI t, ForbidTicket t) :- HasNoTicket t forbiddenTicketTypeEvi = Sub $ case checkTicketPresence (sing @t) of TicketAbsent -> Dict TicketPresent -> error "impossible" -- | Reify 'HasNoSaplingState' contraint from 'ForbidSaplingState'. forbiddenSaplingStateTypeEvi :: forall t. (SingI t, ForbidSaplingState t) :- HasNoSaplingState t forbiddenSaplingStateTypeEvi = Sub $ case checkSaplingStatePresence (sing @t) of SaplingStateAbsent -> Dict SaplingStatePresent -> error "impossible" -- | Whether a value of this type _may_ contain an operation. data OpPresence (t :: T) = ContainsOp t ~ 'True => OpPresent -- ^ A value of type @t@ may or may not contain an operation. | ContainsOp t ~ 'False => OpAbsent -- ^ A value of type @t@ cannot contain @big_map@ values. -- | Whether a value of this type _may_ contain a @contract@ value. data ContractPresence (t :: T) = ContainsContract t ~ 'True => ContractPresent -- ^ A value of type @t@ may or may not contain a @contract@ value. | ContainsContract t ~ 'False => ContractAbsent -- ^ A value of type @t@ cannot contain @contract@ values. -- | Whether a value of this type _may_ contain a @ticket@ value. data TicketPresence (t :: T) = ContainsTicket t ~ 'True => TicketPresent -- ^ A value of type @t@ may or may not contain a @ticket@ value. | ContainsTicket t ~ 'False => TicketAbsent -- ^ A value of type @t@ cannot contain @ticket@ values. -- | Whether a value of this type _may_ contain a @big_map@ value. data BigMapPresence (t :: T) = ContainsBigMap t ~ 'True => BigMapPresent -- ^ A value of type @t@ may or may not contain a @big_map@ value. | ContainsBigMap t ~ 'False => BigMapAbsent -- ^ A value of type @t@ cannot contain @big_map@ values. -- | Whether a value of this type _may_ contain nested @big_map@s. data NestedBigMapsPresence (t :: T) = ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent -- ^ A value of type @t@ may or may not contain nested @big_map@s. | ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent -- ^ A value of type @t@ cannot contain nested @big_map@s. -- | Whether a value of this type _may_ contain a @sapling_state@ value. data SaplingStatePresence (t :: T) = ContainsSaplingState t ~ 'True => SaplingStatePresent -- ^ A value of type @t@ may or may not contain a @sapling_state@ value. | ContainsSaplingState t ~ 'False => SaplingStateAbsent -- ^ A value of type @t@ cannot contain @sapling_state@ values. -- @rvem: IMO, generalization of OpPresence and BigMapPresence to -- TPresence is not worth it, due to the fact that -- it will require more boilerplate in checkTPresence implementation -- than it is already done in checkOpPresence and checkBigMapPresence -- | Check at runtime whether a value of the given type _may_ contain an operation. checkOpPresence :: Sing (ty :: T) -> OpPresence ty checkOpPresence = \case -- This is a sad amount of boilerplate, but at least -- there is no chance to make a mistake in it. -- We can't do in a simpler way while requiring only @Sing ty@ / @SingI ty@, -- and a more complex constraint would be too unpleasant and confusing to -- propagate everywhere. STKey -> OpAbsent STSignature -> OpAbsent STChainId -> OpAbsent STUnit -> OpAbsent STOption t -> case checkOpPresence t of OpPresent -> OpPresent OpAbsent -> OpAbsent STList t -> case checkOpPresence t of OpPresent -> OpPresent OpAbsent -> OpAbsent STSet a -> case checkOpPresence a of OpPresent -> OpPresent OpAbsent -> OpAbsent STOperation -> OpPresent STContract _ -> OpAbsent STTicket t -> case checkOpPresence t of OpPresent -> OpPresent OpAbsent -> OpAbsent STPair a b -> case (checkOpPresence a, checkOpPresence b) of (OpPresent, _) -> OpPresent (_, OpPresent) -> OpPresent (OpAbsent, OpAbsent) -> OpAbsent STOr a b -> case (checkOpPresence a, checkOpPresence b) of (OpPresent, _) -> OpPresent (_, OpPresent) -> OpPresent (OpAbsent, OpAbsent) -> OpAbsent STLambda _ _ -> OpAbsent STMap k v -> case (checkOpPresence k, checkOpPresence v) of (OpAbsent, OpAbsent) -> OpAbsent (OpPresent, _) -> OpPresent (_, OpPresent) -> OpPresent STBigMap k v -> case (checkOpPresence k, checkOpPresence v) of (OpAbsent, OpAbsent) -> OpAbsent (OpPresent, _) -> OpPresent (_, OpPresent) -> OpPresent STInt -> OpAbsent STNat -> OpAbsent STString -> OpAbsent STBytes -> OpAbsent STMutez -> OpAbsent STBool -> OpAbsent STKeyHash -> OpAbsent STBls12381Fr -> OpAbsent STBls12381G1 -> OpAbsent STBls12381G2 -> OpAbsent STTimestamp -> OpAbsent STAddress -> OpAbsent STChest -> OpAbsent STChestKey -> OpAbsent STTxRollupL2Address -> OpAbsent STNever -> OpAbsent STSaplingState _ -> OpAbsent STSaplingTransaction _ -> OpAbsent -- | Check at runtime whether a value of the given type _may_ contain a @contract@ value. checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty checkContractTypePresence = \case STKey -> ContractAbsent STSignature -> ContractAbsent STChainId -> ContractAbsent STUnit -> ContractAbsent STOption t -> case checkContractTypePresence t of ContractPresent -> ContractPresent ContractAbsent -> ContractAbsent STList t -> case checkContractTypePresence t of ContractPresent -> ContractPresent ContractAbsent -> ContractAbsent STSet _ -> ContractAbsent STOperation -> ContractAbsent STContract _ -> ContractPresent STTicket _ -> ContractAbsent -- contract type is not allowed in tickets at all STPair a b -> case (checkContractTypePresence a, checkContractTypePresence b) of (ContractPresent, _) -> ContractPresent (_, ContractPresent) -> ContractPresent (ContractAbsent, ContractAbsent) -> ContractAbsent STOr a b -> case (checkContractTypePresence a, checkContractTypePresence b) of (ContractPresent, _) -> ContractPresent (_, ContractPresent) -> ContractPresent (ContractAbsent, ContractAbsent) -> ContractAbsent STLambda _ _ -> ContractAbsent STMap _ v -> case checkContractTypePresence v of ContractPresent -> ContractPresent ContractAbsent -> ContractAbsent STBigMap _ v -> case checkContractTypePresence v of ContractPresent -> ContractPresent ContractAbsent -> ContractAbsent STInt -> ContractAbsent STNat -> ContractAbsent STString -> ContractAbsent STBytes -> ContractAbsent STMutez -> ContractAbsent STBool -> ContractAbsent STKeyHash -> ContractAbsent STBls12381Fr -> ContractAbsent STBls12381G1 -> ContractAbsent STBls12381G2 -> ContractAbsent STTimestamp -> ContractAbsent STAddress -> ContractAbsent STChest -> ContractAbsent STChestKey -> ContractAbsent STTxRollupL2Address -> ContractAbsent STNever -> ContractAbsent STSaplingState _ -> ContractAbsent STSaplingTransaction _ -> ContractAbsent -- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value. checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty checkTicketPresence = \case STKey -> TicketAbsent STSignature -> TicketAbsent STChainId -> TicketAbsent STUnit -> TicketAbsent STOption t -> case checkTicketPresence t of TicketPresent -> TicketPresent TicketAbsent -> TicketAbsent STList t -> case checkTicketPresence t of TicketPresent -> TicketPresent TicketAbsent -> TicketAbsent STSet _ -> TicketAbsent STOperation -> TicketAbsent STContract _ -> TicketAbsent STTicket _ -> TicketPresent STPair a b -> case (checkTicketPresence a, checkTicketPresence b) of (TicketPresent, _) -> TicketPresent (_, TicketPresent) -> TicketPresent (TicketAbsent, TicketAbsent) -> TicketAbsent STOr a b -> case (checkTicketPresence a, checkTicketPresence b) of (TicketPresent, _) -> TicketPresent (_, TicketPresent) -> TicketPresent (TicketAbsent, TicketAbsent) -> TicketAbsent STLambda _ _ -> TicketAbsent STMap _ v -> case checkTicketPresence v of TicketPresent -> TicketPresent TicketAbsent -> TicketAbsent STBigMap _ v -> case checkTicketPresence v of TicketPresent -> TicketPresent TicketAbsent -> TicketAbsent STInt -> TicketAbsent STNat -> TicketAbsent STString -> TicketAbsent STBytes -> TicketAbsent STMutez -> TicketAbsent STBool -> TicketAbsent STKeyHash -> TicketAbsent STBls12381Fr -> TicketAbsent STBls12381G1 -> TicketAbsent STBls12381G2 -> TicketAbsent STTimestamp -> TicketAbsent STAddress -> TicketAbsent STChest -> TicketAbsent STChestKey -> TicketAbsent STTxRollupL2Address -> TicketAbsent STNever -> TicketAbsent STSaplingState _ -> TicketAbsent STSaplingTransaction _ -> TicketAbsent -- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value. checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty checkBigMapPresence = \case -- More boilerplate to boilerplate god. STKey -> BigMapAbsent STSignature -> BigMapAbsent STChainId -> BigMapAbsent STUnit -> BigMapAbsent STOption t -> case checkBigMapPresence t of BigMapPresent -> BigMapPresent BigMapAbsent -> BigMapAbsent STList t -> case checkBigMapPresence t of BigMapPresent -> BigMapPresent BigMapAbsent -> BigMapAbsent STSet _ -> BigMapAbsent STOperation -> BigMapAbsent STContract _ -> BigMapAbsent STTicket _ -> BigMapAbsent -- big_maps are not allowed in tickets at all STPair a b -> case (checkBigMapPresence a, checkBigMapPresence b) of (BigMapPresent, _) -> BigMapPresent (_, BigMapPresent) -> BigMapPresent (BigMapAbsent, BigMapAbsent) -> BigMapAbsent STOr a b -> case (checkBigMapPresence a, checkBigMapPresence b) of (BigMapPresent, _) -> BigMapPresent (_, BigMapPresent) -> BigMapPresent (BigMapAbsent, BigMapAbsent) -> BigMapAbsent STLambda _ _ -> BigMapAbsent STMap _ v -> case checkBigMapPresence v of BigMapPresent -> BigMapPresent BigMapAbsent -> BigMapAbsent STBigMap _ _ -> BigMapPresent STInt -> BigMapAbsent STNat -> BigMapAbsent STString -> BigMapAbsent STBytes -> BigMapAbsent STMutez -> BigMapAbsent STBool -> BigMapAbsent STKeyHash -> BigMapAbsent STBls12381Fr -> BigMapAbsent STBls12381G1 -> BigMapAbsent STBls12381G2 -> BigMapAbsent STTimestamp -> BigMapAbsent STAddress -> BigMapAbsent STChest -> BigMapAbsent STChestKey -> BigMapAbsent STTxRollupL2Address -> BigMapAbsent STNever -> BigMapAbsent STSaplingState _ -> BigMapAbsent STSaplingTransaction _ -> BigMapAbsent -- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s. checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty checkNestedBigMapsPresence = \case -- More boilerplate to boilerplate god. STKey -> NestedBigMapsAbsent STSignature -> NestedBigMapsAbsent STChainId -> NestedBigMapsAbsent STUnit -> NestedBigMapsAbsent STOption t -> case checkNestedBigMapsPresence t of NestedBigMapsPresent -> NestedBigMapsPresent NestedBigMapsAbsent -> NestedBigMapsAbsent STList t -> case checkNestedBigMapsPresence t of NestedBigMapsPresent -> NestedBigMapsPresent NestedBigMapsAbsent -> NestedBigMapsAbsent STSet _ -> NestedBigMapsAbsent STOperation -> NestedBigMapsAbsent STContract _ -> NestedBigMapsAbsent STTicket _ -> NestedBigMapsAbsent STPair a b -> case (checkNestedBigMapsPresence a, checkNestedBigMapsPresence b) of (NestedBigMapsPresent, _) -> NestedBigMapsPresent (_, NestedBigMapsPresent) -> NestedBigMapsPresent (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsAbsent STOr a b -> case (checkNestedBigMapsPresence a, checkNestedBigMapsPresence b) of (NestedBigMapsPresent, _) -> NestedBigMapsPresent (_, NestedBigMapsPresent) -> NestedBigMapsPresent (NestedBigMapsAbsent, NestedBigMapsAbsent) -> NestedBigMapsAbsent STLambda _ _ -> NestedBigMapsAbsent STMap _ v -> case checkNestedBigMapsPresence v of NestedBigMapsPresent -> NestedBigMapsPresent NestedBigMapsAbsent -> NestedBigMapsAbsent STBigMap _ v -> case checkBigMapPresence v of BigMapPresent -> NestedBigMapsPresent BigMapAbsent -> NestedBigMapsAbsent STInt -> NestedBigMapsAbsent STNat -> NestedBigMapsAbsent STString -> NestedBigMapsAbsent STBytes -> NestedBigMapsAbsent STMutez -> NestedBigMapsAbsent STBool -> NestedBigMapsAbsent STKeyHash -> NestedBigMapsAbsent STBls12381Fr -> NestedBigMapsAbsent STBls12381G1 -> NestedBigMapsAbsent STBls12381G2 -> NestedBigMapsAbsent STTimestamp -> NestedBigMapsAbsent STAddress -> NestedBigMapsAbsent STChest -> NestedBigMapsAbsent STChestKey -> NestedBigMapsAbsent STTxRollupL2Address -> NestedBigMapsAbsent STNever -> NestedBigMapsAbsent STSaplingState _ -> NestedBigMapsAbsent STSaplingTransaction _ -> NestedBigMapsAbsent -- | Check at runtime whether a value of the given type _may_ contain a @sapling_state@ value. checkSaplingStatePresence :: Sing (ty :: T) -> SaplingStatePresence ty checkSaplingStatePresence = \case STKey -> SaplingStateAbsent STSignature -> SaplingStateAbsent STChainId -> SaplingStateAbsent STUnit -> SaplingStateAbsent STOption t -> case checkSaplingStatePresence t of SaplingStatePresent -> SaplingStatePresent SaplingStateAbsent -> SaplingStateAbsent STList t -> case checkSaplingStatePresence t of SaplingStatePresent -> SaplingStatePresent SaplingStateAbsent -> SaplingStateAbsent STSet _ -> SaplingStateAbsent STOperation -> SaplingStateAbsent STContract _ -> SaplingStateAbsent STTicket _ -> SaplingStateAbsent STPair a b -> case (checkSaplingStatePresence a, checkSaplingStatePresence b) of (SaplingStatePresent, _) -> SaplingStatePresent (_, SaplingStatePresent) -> SaplingStatePresent (SaplingStateAbsent, SaplingStateAbsent) -> SaplingStateAbsent STOr a b -> case (checkSaplingStatePresence a, checkSaplingStatePresence b) of (SaplingStatePresent, _) -> SaplingStatePresent (_, SaplingStatePresent) -> SaplingStatePresent (SaplingStateAbsent, SaplingStateAbsent) -> SaplingStateAbsent STLambda _ _ -> SaplingStateAbsent STMap _ v -> case checkSaplingStatePresence v of SaplingStatePresent -> SaplingStatePresent SaplingStateAbsent -> SaplingStateAbsent STBigMap _ v -> case checkSaplingStatePresence v of SaplingStatePresent -> SaplingStatePresent SaplingStateAbsent -> SaplingStateAbsent STInt -> SaplingStateAbsent STNat -> SaplingStateAbsent STString -> SaplingStateAbsent STBytes -> SaplingStateAbsent STMutez -> SaplingStateAbsent STBool -> SaplingStateAbsent STKeyHash -> SaplingStateAbsent STBls12381Fr -> SaplingStateAbsent STBls12381G1 -> SaplingStateAbsent STBls12381G2 -> SaplingStateAbsent STTimestamp -> SaplingStateAbsent STAddress -> SaplingStateAbsent STChest -> SaplingStateAbsent STChestKey -> SaplingStateAbsent STTxRollupL2Address -> SaplingStateAbsent STNever -> SaplingStateAbsent STSaplingState _ -> SaplingStatePresent STSaplingTransaction _ -> SaplingStateAbsent -- | Check at runtime that a value of the given type cannot contain operations. opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t) opAbsense s = case checkOpPresence s of OpPresent -> Nothing OpAbsent -> Just Dict -- | Check at runtime that a value of the given type cannot contain @contract@ values. contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t) contractTypeAbsense s = case checkContractTypePresence s of ContractPresent -> Nothing ContractAbsent -> Just Dict -- | Check at runtime that a value of the given type cannot contain @ticket@ values. ticketAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoTicket t) ticketAbsense s = case checkTicketPresence s of TicketPresent -> Nothing TicketAbsent -> Just Dict -- | Check at runtime that a value of the given type cannot containt @big_map@ values bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t) bigMapAbsense s = case checkBigMapPresence s of BigMapPresent -> Nothing BigMapAbsent -> Just Dict -- | Check at runtime that a value of the given type cannot containt @sapling_state@ values saplingStateAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoSaplingState t) saplingStateAbsense s = case checkSaplingStatePresence s of SaplingStatePresent -> Nothing SaplingStateAbsent -> Just Dict -- | Check at runtime that a value of the given type cannot contain nested @big_map@s. nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t) nestedBigMapsAbsense s = case checkNestedBigMapsPresence s of NestedBigMapsPresent -> Nothing NestedBigMapsAbsent -> Just Dict ---------------------------------------------------------------------------- -- Scopes ---------------------------------------------------------------------------- data BadTypeForScope = BtNotComparable | BtIsOperation | BtHasBigMap | BtHasNestedBigMap | BtHasContract | BtHasTicket | BtHasSaplingState deriving stock (Show, Eq, Generic) deriving anyclass (NFData) instance Buildable BadTypeForScope where build = buildRenderDoc instance RenderDoc BadTypeForScope where renderDoc _ = \case BtNotComparable -> "is not comparable" BtIsOperation -> "has 'operation' type" BtHasBigMap -> "has 'big_map'" BtHasNestedBigMap -> "has nested 'big_map'" BtHasContract -> "has 'contract' type" BtHasTicket -> "has 'ticket' type" BtHasSaplingState -> "has 'sapling_state' type" -- | Set of constraints that Michelson applies to parameters. -- -- Not just a type alias in order to be able to partially apply it class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t instance (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t -- | Set of constraints that Michelson applies to contract storage. -- -- Not just a type alias in order to be able to partially apply it class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t instance (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t -- | Set of constraints that Michelson applies to pushed constants. -- -- Not just a type alias in order to be able to partially apply it class (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t, HasNoSaplingState t) => ConstantScope t instance (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t, HasNoSaplingState t) => ConstantScope t -- | Alias for constraints which Michelson requires in @DUP@ instruction. class (SingI t, HasNoTicket t) => DupableScope t instance (SingI t, HasNoTicket t) => DupableScope t -- | Returns whether the type is dupable. type family IsDupableScope (t :: T) :: Bool where IsDupableScope t = Not (ContainsTicket t) -- | Set of constraints that Michelson applies to packed values. -- -- Not just a type alias in order to be able to partially apply it class (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoTicket t, HasNoSaplingState t) => PackedValScope t instance (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoTicket t, HasNoSaplingState t ) => PackedValScope t -- | Set of constraints that Michelson applies to unpacked values. -- -- It is different from 'PackedValScope', e.g. @contract@ type cannot appear -- in a value we unpack to. -- -- Not just a type alias in order to be able to partially apply it class (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t instance (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope 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 class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t -- | Alias for constraints which are required for untyped representation. type UntypedValScope t = (SingI t, HasNoOp t) ---------------------------------------------------------------------------- -- Conveniences ---------------------------------------------------------------------------- -- | Should be present for common scopes. class CheckScope (c :: Constraint) where -- | Check that constraint hold for a given type. checkScope :: Either BadTypeForScope (Dict c) instance SingI t => CheckScope (WellTyped t) where checkScope = first nwtCause $ getWTP @t instance SingI t => CheckScope (HasNoOp t) where checkScope = maybeToRight BtIsOperation $ opAbsense sing instance SingI t => CheckScope (HasNoBigMap t) where checkScope = maybeToRight BtHasBigMap $ bigMapAbsense sing instance SingI t => CheckScope (HasNoNestedBigMaps t) where checkScope = maybeToRight BtHasNestedBigMap $ nestedBigMapsAbsense sing instance SingI t => CheckScope (HasNoContract t) where checkScope = maybeToRight BtHasContract $ contractTypeAbsense sing instance SingI t => CheckScope (HasNoTicket t) where checkScope = maybeToRight BtHasTicket $ ticketAbsense sing instance SingI t => CheckScope (HasNoSaplingState t) where checkScope = maybeToRight BtHasSaplingState $ saplingStateAbsense sing instance SingI t => CheckScope (Comparable t) where checkScope = maybeToRight BtNotComparable $ comparabilityPresence sing -- | Alias for comparable types. type ComparabilityScope t = (SingI t, Comparable t) comparabilityPresence :: Sing t -> Maybe (Dict $ (Comparable t)) comparabilityPresence s = case checkComparability s of CanBeCompared -> Just Dict CannotBeCompared -> Nothing instance SingI t => CheckScope (ParameterScope t) where checkScope = (\Dict Dict Dict -> Dict) <$> checkScope @(WellTyped t) <*> checkScope @(HasNoOp t) <*> checkScope @(HasNoNestedBigMaps t) instance SingI t => CheckScope (StorageScope t) where checkScope = (\Dict Dict Dict Dict -> Dict) <$> checkScope @(WellTyped t) <*> checkScope @(HasNoOp t) <*> checkScope @(HasNoNestedBigMaps t) <*> checkScope @(HasNoContract t) instance SingI t => CheckScope (ConstantScope t) where checkScope = (\Dict Dict Dict Dict Dict Dict -> Dict) <$> checkScope @(WellTyped t) <*> checkScope @(HasNoOp t) <*> checkScope @(HasNoBigMap t) <*> checkScope @(HasNoContract t) <*> checkScope @(HasNoTicket t) <*> checkScope @(HasNoSaplingState t) instance SingI t => CheckScope (DupableScope t) where checkScope = (\Dict -> Dict) <$> checkScope @(HasNoTicket t) instance SingI t => CheckScope (PackedValScope t) where checkScope = (\Dict Dict Dict Dict Dict -> Dict) <$> checkScope @(WellTyped t) <*> checkScope @(HasNoOp t) <*> checkScope @(HasNoBigMap t) <*> checkScope @(HasNoTicket t) <*> checkScope @(HasNoSaplingState t) instance SingI t => CheckScope (UnpackedValScope t) where checkScope = (\Dict Dict Dict -> Dict) <$> checkScope @(WellTyped t) <*> checkScope @(PackedValScope t) <*> checkScope @(ConstantScope t) instance SingI t => CheckScope (ViewableScope t) where checkScope = (\Dict Dict Dict -> Dict) <$> checkScope @(HasNoOp t) <*> checkScope @(HasNoBigMap t) <*> checkScope @(HasNoTicket t) instance SingI t => CheckScope (ComparabilityScope t) where checkScope = (\Dict -> Dict) <$> checkScope @(Comparable t) -- | Allows using a scope that can be proven true with a De Morgan law. -- -- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a -- negative property we want to avoid as a 'Constraint'. -- The negative constraints are implemented with a type family that for some -- combination types resolves to itself applied to the type arguments in an @or@, -- e.g. A @pair l r@ has @x@ if @l@ or @r@ contain @x@. -- -- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@ -- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@. class WithDeMorganScope (c :: T -> Constraint) t a b where withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret -- | Produce evidence that the first argument of a disjunction -- is false if the whole disjunction is false. orL :: forall a b. (a || b) ~ 'False => Sing a -> a :~: 'False orL SFalse = Refl {-# NOINLINE [1] orL #-} -- This rule is *slightly* illegitimate, because the right hand side is lazier -- than the left hand side. In context, this is fine, and we really *want* to -- do it so we have at least some hope of avoiding building singletons that we -- don't end up using. We'd get a totally legitimate rule if we used a SingI -- constraint instead of a Sing argument, but then we'd need to use withSingI, -- which for some reason doesn't use the newfangled GHC machinery for such and -- therefore risks gumming up optimization. Of course, we could roll our own -- withSingI, but that's very hairy and GHC version dependent (the -- never-really-documented magicDict was recently replaced by withDict, which -- is documented in ... the type checker source code, apparently). {-# RULES "orL" forall s. orL s = unsafeCoerce Refl #-} -- | When a class looks like -- -- @ -- class (SomeTypeFamily t ~ 'False, ...) => TheClass t -- instance (SomeTypeFamily t ~ 'False, ...) => TheClass t -- @ -- -- and the additional constraints are satisfied by the instance constraints of -- the 'WithDeMorganScope' instance for @TheClass@, we can use -- `simpleWithDeMorgan` to define 'withDeMorganScope' for the instance. simpleWithDeMorgan :: forall sym a b ret. ((sym @@ a || sym @@ b) ~ 'False, SingI sym, SingI a) => (((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret -- Note: If the "orL" rule fires (which it should), we won't actually calculate -- the (likely recursive) `sing @sym @@ sing @a` at all. If we're lucky, GHC -- might not build the `SingI a` dictionary either. simpleWithDeMorgan f | Refl <- orL @(sym @@ a) @(sym @@ b) (sing @sym @@ sing @a) = f data ContainsOpSym :: T ~> Bool type instance Apply ContainsOpSym x = ContainsOp x instance SingI ContainsOpSym where sing = SLambda $ \t -> case checkOpPresence t of OpPresent -> STrue OpAbsent -> SFalse instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @a @b f instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @a @b f instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @k @v f instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @k @v f data ContainsContractSym :: T ~> Bool type instance Apply ContainsContractSym x = ContainsContract x instance SingI ContainsContractSym where sing = SLambda $ \t -> case checkContractTypePresence t of ContractPresent -> STrue ContractAbsent -> SFalse instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where withDeMorganScope f = simpleWithDeMorgan @ContainsContractSym @a @b f instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where withDeMorganScope f = simpleWithDeMorgan @ContainsContractSym @a @b f data ContainsTicketSym :: T ~> Bool type instance Apply ContainsTicketSym x = ContainsTicket x instance SingI ContainsTicketSym where sing = SLambda $ \t -> case checkTicketPresence t of TicketPresent -> STrue TicketAbsent -> SFalse instance SingI a => WithDeMorganScope HasNoTicket 'TPair a b where withDeMorganScope f = simpleWithDeMorgan @ContainsTicketSym @a @b f instance SingI a => WithDeMorganScope HasNoTicket 'TOr a b where withDeMorganScope f = simpleWithDeMorgan @ContainsTicketSym @a @b f data ContainsBigMapSym :: T ~> Bool type instance Apply ContainsBigMapSym x = ContainsBigMap x instance SingI ContainsBigMapSym where sing = SLambda $ \t -> case checkBigMapPresence t of BigMapPresent -> STrue BigMapAbsent -> SFalse instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where withDeMorganScope f = simpleWithDeMorgan @ContainsBigMapSym @a @b f instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where withDeMorganScope f = simpleWithDeMorgan @ContainsBigMapSym @a @b f data ContainsNestedBigMapsSym :: T ~> Bool type instance Apply ContainsNestedBigMapsSym x = ContainsNestedBigMaps x instance SingI ContainsNestedBigMapsSym where sing = SLambda $ \t -> case checkNestedBigMapsPresence t of NestedBigMapsPresent -> STrue NestedBigMapsAbsent -> SFalse instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where withDeMorganScope f = simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b f instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where withDeMorganScope f = simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b f instance ( WithDeMorganScope HasNoOp t a b , WithDeMorganScope HasNoNestedBigMaps t a b , WellTyped a, WellTyped b ) => WithDeMorganScope ParameterScope t a b where withDeMorganScope f = withDeMorganScope @HasNoOp @t @a @b $ withDeMorganScope @HasNoNestedBigMaps @t @a @b f instance ( WithDeMorganScope HasNoOp t a b , WithDeMorganScope HasNoNestedBigMaps t a b , WithDeMorganScope HasNoContract t a b , WellTyped a, WellTyped b ) => WithDeMorganScope StorageScope t a b where withDeMorganScope f = withDeMorganScope @HasNoOp @t @a @b $ withDeMorganScope @HasNoNestedBigMaps @t @a @b $ withDeMorganScope @HasNoContract @t @a @b f instance ( WithDeMorganScope HasNoOp t a b , WithDeMorganScope HasNoBigMap t a b , WithDeMorganScope HasNoContract t a b , WithDeMorganScope HasNoTicket t a b , WithDeMorganScope HasNoSaplingState t a b , WellTyped a, WellTyped b ) => WithDeMorganScope ConstantScope t a b where withDeMorganScope f = withDeMorganScope @HasNoOp @t @a @b $ withDeMorganScope @HasNoBigMap @t @a @b $ withDeMorganScope @HasNoContract @t @a @b $ withDeMorganScope @HasNoTicket @t @a @b $ withDeMorganScope @HasNoSaplingState @t @a @b f instance ( WithDeMorganScope HasNoOp t a b , WithDeMorganScope HasNoBigMap t a b , WithDeMorganScope HasNoTicket t a b , WithDeMorganScope HasNoSaplingState t a b , WellTyped a, WellTyped b ) => WithDeMorganScope PackedValScope t a b where withDeMorganScope f = withDeMorganScope @HasNoOp @t @a @b $ withDeMorganScope @HasNoBigMap @t @a @b $ withDeMorganScope @HasNoTicket @t @a @b $ withDeMorganScope @HasNoSaplingState @t @a @b f instance ( WithDeMorganScope PackedValScope t a b , WithDeMorganScope ConstantScope t a b , WellTyped a, WellTyped b ) => WithDeMorganScope UnpackedValScope t a b where withDeMorganScope f = withDeMorganScope @PackedValScope @t @a @b $ withDeMorganScope @ConstantScope @t @a @b f -- Versions for eDSL ---------------------------------------------------------------------------- {- These constraints are supposed to be used only in eDSL code and eDSL should define its own wrapers over it. -} type ProperParameterBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t) type ProperStorageBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t) type ProperConstantBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t) type ProperDupableBetterErrors t = (SingI t, ForbidTicket t) type ProperPackedValBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t) type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t) type ProperViewableBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t) type ProperUntypedValBetterErrors t = (SingI t, ForbidOp t) type ProperNonComparableValBetterErrors t = (SingI t, ForbidNonComparable t) properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t properParameterEvi = Sub $ Dict \\ forbiddenOpEvi @t \\ forbiddenNestedBigMapsEvi @t properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t properStorageEvi = Sub $ Dict \\ forbiddenOpEvi @t \\ forbiddenContractTypeEvi @t \\ forbiddenNestedBigMapsEvi @t \\ forbiddenContractTypeEvi @t properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t properConstantEvi = Sub $ Dict \\ forbiddenOpEvi @t \\ forbiddenBigMapEvi @t \\ forbiddenContractTypeEvi @t \\ forbiddenTicketTypeEvi @t \\ forbiddenSaplingStateTypeEvi @t properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t properDupableEvi = Sub $ Dict \\ forbiddenTicketTypeEvi @t properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t properPackedValEvi = Sub $ Dict \\ forbiddenOpEvi @t \\ forbiddenBigMapEvi @t \\ forbiddenTicketTypeEvi @t \\ forbiddenSaplingStateTypeEvi @t properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t properUnpackedValEvi = Sub $ Dict \\ properPackedValEvi @t \\ properConstantEvi @t properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t properViewableEvi = Sub $ Dict \\ forbiddenOpEvi @t \\ forbiddenBigMapEvi @t \\ forbiddenTicketTypeEvi @t properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t properUntypedValEvi = Sub $ Dict \\ forbiddenOpEvi @t class (IsComparable t ~ 'True, SingI t, ComparableSuperC t) => Comparable t where -- | Constraints required for instance of a given type. type ComparableSuperC t :: Constraint type ComparableSuperC _ = () instance ComparableSuperC ('TPair t1 t2) => Comparable ('TPair t1 t2) where type ComparableSuperC ('TPair t1 t2) = (Comparable t1, Comparable t2, FailOnNonComparableFound (IsComparable t1 && IsComparable t2)) instance ComparableSuperC ('TOr t1 t2) => Comparable ('TOr t1 t2) where type ComparableSuperC ('TOr t1 t2) = (Comparable t1, Comparable t2, FailOnNonComparableFound (IsComparable t1 && IsComparable t2)) instance ComparableSuperC ('TOption t) => Comparable ('TOption t) where type ComparableSuperC ('TOption t) = (Comparable t, ForbidNonComparable t) instance Comparable 'TUnit instance Comparable 'TInt instance Comparable 'TNat instance Comparable 'TString instance Comparable 'TBytes instance Comparable 'TMutez instance Comparable 'TBool instance Comparable 'TKeyHash instance Comparable 'TTimestamp instance Comparable 'TAddress instance Comparable 'TTxRollupL2Address instance Comparable 'TNever instance Comparable 'TChainId instance Comparable 'TSignature instance Comparable 'TKey -- | This class encodes Michelson rules w.r.t where it requires comparable -- types. Earlier we had a dedicated type for representing comparable types @CT@. -- But then we integreated those types into @T@. This meant that some of the -- types that could be formed with various combinations of @T@ would be -- illegal as per Michelson typing rule. Using this class, we inductively -- enforce that a type and all types it contains are well typed as per -- Michelson's rules. class (SingI t, WellTypedSuperC t) => WellTyped (t :: T) where -- | Constraints required for instance of a given type. type WellTypedSuperC t :: Constraint type WellTypedSuperC _ = () instance WellTyped 'TKey instance WellTyped 'TUnit instance WellTyped 'TNever instance WellTyped 'TSignature instance WellTyped 'TChainId instance WellTyped 'TChest instance WellTyped 'TChestKey instance WellTyped 'TTxRollupL2Address instance WellTypedSuperC ('TOption t) => WellTyped ('TOption t) where type WellTypedSuperC ('TOption t) = WellTyped t instance WellTypedSuperC ('TList t) => WellTyped ('TList t) where type WellTypedSuperC ('TList t) = WellTyped t instance WellTypedSuperC ('TSet t) => WellTyped ('TSet t) where type WellTypedSuperC ('TSet t) = (Comparable t, WellTyped t) instance WellTyped 'TOperation instance WellTypedSuperC ('TContract t) => WellTyped ('TContract t) where type WellTypedSuperC ('TContract t) = (WellTyped t, HasNoOp t) instance WellTypedSuperC ('TTicket t) => WellTyped ('TTicket t) where type WellTypedSuperC ('TTicket t) = (WellTyped t, Comparable t) instance WellTypedSuperC ('TPair t1 t2) => WellTyped ('TPair t1 t2) where type WellTypedSuperC ('TPair t1 t2) = (WellTyped t1, WellTyped t2) instance WellTypedSuperC ('TOr t1 t2) => WellTyped ('TOr t1 t2) where type WellTypedSuperC ('TOr t1 t2) = (WellTyped t1, WellTyped t2) instance WellTypedSuperC ('TLambda t1 t2) => WellTyped ('TLambda t1 t2) where type WellTypedSuperC ('TLambda t1 t2) = (WellTyped t1, WellTyped t2) instance WellTypedSuperC ('TMap k v) => WellTyped ('TMap k v) where type WellTypedSuperC ('TMap k v) = (Comparable k, WellTyped k, WellTyped v) instance WellTypedSuperC ('TBigMap k v) => WellTyped ('TBigMap k v) where type WellTypedSuperC ('TBigMap k v) = ( Comparable k, WellTyped k, WellTyped v , HasNoBigMap v, HasNoOp v) instance WellTyped 'TInt instance WellTyped 'TNat instance WellTyped 'TString instance WellTyped 'TBytes instance WellTyped 'TMutez instance WellTyped 'TBool instance WellTyped 'TKeyHash instance WellTyped 'TBls12381Fr instance WellTyped 'TBls12381G1 instance WellTyped 'TBls12381G2 instance WellTyped 'TTimestamp instance WellTyped 'TAddress instance (SingI n) => WellTyped ('TSaplingState n) where type WellTypedSuperC ('TSaplingState n) = (SingI n) instance (SingI n) => WellTyped ('TSaplingTransaction n) where type WellTypedSuperC ('TSaplingTransaction n) = (SingI n) -- | Error type for when a value is not well-typed. data NotWellTyped = NotWellTyped { nwtBadType :: T , nwtCause :: BadTypeForScope } instance Buildable NotWellTyped where build (NotWellTyped t c) = "Given type is not well typed because '" <> (build t) <> "' " <> (build c) data Comparability t where CanBeCompared :: (Comparable t) => Comparability t CannotBeCompared :: (IsComparable t ~ 'False) => Comparability t -- | Given a type, provide evidence that it is well typed w.r.t to the -- Michelson rules regarding where comparable types are required. getWTP :: forall t. (SingI t) => Either NotWellTyped (Dict (WellTyped t)) getWTP = getWTP' sing -- | Version of 'getWTP' that accepts 'Sing' at term-level. getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t)) getWTP' = \case STKey -> Right Dict STUnit -> Right Dict STSignature -> Right Dict STChainId -> Right Dict STOption s -> do Dict <- getWTP' s pure Dict STList s -> do Dict <- getWTP' s pure Dict STSet s -> do Dict <- getWTP' s Dict <- eitherWellTyped BtNotComparable getComparableProofS s pure Dict STOperation -> Right Dict STContract s -> do Dict <- getWTP' s Dict <- eitherWellTyped BtIsOperation opAbsense s pure Dict STTicket s -> do Dict <- getWTP' s Dict <- eitherWellTyped BtNotComparable getComparableProofS s pure Dict STPair s1 s2 -> do Dict <- getWTP' s1 Dict <- getWTP' s2 pure Dict STOr s1 s2 -> do Dict <- getWTP' s1 Dict <- getWTP' s2 pure Dict STLambda s1 s2 -> do Dict <- getWTP' s1 Dict <- getWTP' s2 pure Dict STMap s1 s2 -> do Dict <- getWTP' s1 Dict <- getWTP' s2 Dict <- eitherWellTyped BtNotComparable getComparableProofS s1 pure Dict STBigMap s1 s2 -> do Dict <- getWTP' s1 Dict <- getWTP' s2 Dict <- eitherWellTyped BtNotComparable getComparableProofS s1 Dict <- eitherWellTyped BtIsOperation opAbsense s2 Dict <- eitherWellTyped BtHasBigMap bigMapAbsense s2 pure Dict STInt -> Right Dict STNat -> Right Dict STString -> Right Dict STBytes -> Right Dict STMutez -> Right Dict STBool -> Right Dict STKeyHash -> Right Dict STBls12381Fr -> Right Dict STBls12381G1 -> Right Dict STBls12381G2 -> Right Dict STTimestamp -> Right Dict STAddress -> Right Dict STChest -> Right Dict STChestKey -> Right Dict STTxRollupL2Address -> Right Dict STNever -> Right Dict STSaplingState s -> withSingI s $ Right Dict STSaplingTransaction s -> withSingI s $ Right Dict where eitherWellTyped :: BadTypeForScope -> (Sing (ty :: T) -> Maybe a) -> Sing (ty :: T) -> Either NotWellTyped a eitherWellTyped bt sf sng = maybeToRight (NotWellTyped (fromSing sng) bt) $ sf sng getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a)) getComparableProofS s = case checkComparability s of CanBeCompared -> Just Dict CannotBeCompared -> Nothing checkComparability :: Sing t -> Comparability t checkComparability = \case STPair a b -> case (checkComparability a, checkComparability b) of (CanBeCompared, CanBeCompared) -> CanBeCompared (CannotBeCompared, _) -> CannotBeCompared (_, CannotBeCompared) -> CannotBeCompared STOr a b -> case (checkComparability a, checkComparability b) of (CanBeCompared, CanBeCompared) -> CanBeCompared (CannotBeCompared, _) -> CannotBeCompared (_, CannotBeCompared) -> CannotBeCompared STOption t -> case checkComparability t of CanBeCompared -> CanBeCompared CannotBeCompared -> CannotBeCompared STList _ -> CannotBeCompared STSet _ -> CannotBeCompared STOperation -> CannotBeCompared STContract _ -> CannotBeCompared STTicket _ -> CannotBeCompared STLambda _ _ -> CannotBeCompared STMap _ _ -> CannotBeCompared STBigMap _ _ -> CannotBeCompared STNever -> CanBeCompared STUnit -> CanBeCompared STInt -> CanBeCompared STNat -> CanBeCompared STString -> CanBeCompared STBytes -> CanBeCompared STMutez -> CanBeCompared STBool -> CanBeCompared STKeyHash -> CanBeCompared STBls12381Fr -> CannotBeCompared STBls12381G1 -> CannotBeCompared STBls12381G2 -> CannotBeCompared STTimestamp -> CanBeCompared STAddress -> CanBeCompared STKey -> CanBeCompared STSignature -> CanBeCompared STChainId -> CanBeCompared STChest -> CannotBeCompared STChestKey -> CannotBeCompared STTxRollupL2Address -> CanBeCompared STSaplingState _ -> CannotBeCompared STSaplingTransaction _ -> CannotBeCompared