Created
July 18, 2020 12:01
-
-
Save Hithroc/ab1fbf776f1d24e023f8258c95ce0a2a to your computer and use it in GitHub Desktop.
GHC 8.10.1 compile time regression
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE UndecidableSuperClasses, FunctionalDependencies, RoleAnnotations, ExplicitNamespaces, TypeFamilies, RankNTypes, TypeApplications, LambdaCase, DerivingStrategies, ScopedTypeVariables, TypeOperators, DataKinds, PolyKinds, GADTs, TypeFamilyDependencies, ConstraintKinds, UndecidableInstances, TypeSynonymInstances, FlexibleInstances, DeriveGeneric, AllowAmbiguousTypes, StrictData #-} | |
{-# OPTIONS_GHC -Wno-redundant-constraints -Wno-overlapping-patterns -Wno-incomplete-patterns | |
-Weverything #-} | |
{- | 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 Michelson.Typed.Scope | |
( -- * Scopes | |
ConstantScope | |
, StorageScope | |
, PackedValScope | |
, ParameterScope | |
, PrintedValScope | |
, UnpackedValScope | |
, ProperParameterBetterErrors | |
, ProperStorageBetterErrors | |
, ProperConstantBetterErrors | |
, ProperPackedValBetterErrors | |
, ProperUnpackedValBetterErrors | |
, ProperPrintedValBetterErrors | |
, properParameterEvi | |
, properStorageEvi | |
, properConstantEvi | |
, properPackedValEvi | |
, properUnpackedValEvi | |
, properPrintedValEvi | |
, (:-)(..) | |
, BadTypeForScope (..) | |
, CheckScope (..) | |
-- * Implementation internals | |
, HasNoBigMap | |
, HasNoNestedBigMaps | |
, HasNoOp | |
, HasNoContract | |
, ContainsBigMap | |
, ContainsNestedBigMaps | |
, ForbidOp | |
, ForbidContract | |
, ForbidBigMap | |
, ForbidNestedBigMaps | |
, FailOnBigMapFound | |
, FailOnNestedBigMapsFound | |
, FailOnOperationFound | |
, OpPresence (..) | |
, ContractPresence (..) | |
, BigMapPresence (..) | |
, NestedBigMapsPresence (..) | |
, checkOpPresence | |
, checkContractTypePresence | |
, checkBigMapPresence | |
, checkNestedBigMapsPresence | |
, opAbsense | |
, contractTypeAbsense | |
, bigMapAbsense | |
, nestedBigMapsAbsense | |
, forbiddenOp | |
, forbiddenContractType | |
, forbiddenBigMap | |
, forbiddenNestedBigMaps | |
-- * Re-exports | |
, withDict | |
, SingI (..) | |
) where | |
import Data.Type.Bool (type (||)) | |
import Data.Type.Coercion | |
import GHC.TypeLits (ErrorMessage(..), TypeError) | |
import Data.Typeable | |
import GHC.Generics | |
import GHC.Exts | |
import Data.Kind | |
data T = | |
TKey | |
| TUnit | |
| TSignature | |
| TChainId | |
| TOption T | |
| TList T | |
| TSet T | |
| TOperation | |
| TContract T | |
| TPair T T | |
| TOr T T | |
| TLambda T T | |
| TMap T T | |
| TBigMap T T | |
| TInt | |
| TNat | |
| TString | |
| TBytes | |
| TMutez | |
| TBool | |
| TKeyHash | |
| TTimestamp | |
| TAddress | |
deriving stock (Eq, Show) | |
type family Sing :: k -> Type | |
class SingI a where | |
sing :: Sing a | |
class SingKind (k :: Type) where | |
-- | Get a base type from the promoted kind. For example, | |
-- @Demote Bool@ will be the type @Bool@. Rarely, the type and kind do not | |
-- match. For example, @Demote Nat@ is @Natural@. | |
type Demote k = (r :: Type) | r -> k | |
-- | Convert a singleton to its unrefined version. | |
fromSing :: Sing (a :: k) -> Demote k | |
-- | Convert an unrefined type to an existentially-quantified singleton type. | |
toSing :: Demote k -> SomeSing k | |
data SomeSing (k :: Type) :: Type where | |
SomeSing :: Sing (a :: k) -> SomeSing k | |
-- | Instance of data family 'Sing' for 'T'. | |
-- Custom instance is implemented in order to inject 'Typeable' | |
-- constraint for some of constructors. | |
data SingT :: T -> Type where | |
STKey :: SingT 'TKey | |
STUnit :: SingT 'TUnit | |
STSignature :: SingT 'TSignature | |
STChainId :: SingT 'TChainId | |
STOption :: (SingI a, Typeable a) => Sing a -> SingT ( 'TOption a) | |
STList :: (SingI a, Typeable a) => Sing a -> SingT ( 'TList a ) | |
STSet :: (SingI a, Typeable a) => Sing a -> SingT ( 'TSet a ) | |
STOperation :: SingT 'TOperation | |
STContract :: (SingI a, Typeable a) | |
=> Sing a -> SingT ( 'TContract a ) | |
STPair :: (SingI a, SingI b, Typeable a, Typeable b) | |
=> Sing a -> Sing b -> SingT ('TPair a b) | |
STOr :: (SingI a, SingI b, Typeable a, Typeable b) | |
=> Sing a -> Sing b -> SingT ('TOr a b) | |
STLambda :: (SingI a, SingI b, Typeable a, Typeable b) | |
=> Sing a -> Sing b -> SingT ('TLambda a b) | |
STMap :: (SingI a, SingI b, Typeable a, Typeable b) | |
=> Sing a -> Sing b -> SingT ('TMap a b) | |
STBigMap :: (SingI a, SingI b, Typeable a, Typeable b) | |
=> Sing a -> Sing b -> SingT ('TBigMap a b) | |
STInt :: SingT 'TInt | |
STNat :: SingT 'TNat | |
STString :: SingT 'TString | |
STBytes :: SingT 'TBytes | |
STMutez :: SingT 'TMutez | |
STBool :: SingT 'TBool | |
STKeyHash :: SingT 'TKeyHash | |
STTimestamp :: SingT 'TTimestamp | |
STAddress :: SingT 'TAddress | |
type instance Sing = SingT | |
--------------------------------------------- | |
-- Singleton-related helpers for T | |
-------------------------------------------- | |
-- | Version of 'SomeSing' with 'Typeable' constraint, | |
-- specialized for use with 'T' kind. | |
data SomeSingT where | |
SomeSingT :: forall (a :: T). (Typeable a, SingI a) | |
=> Sing a -> SomeSingT | |
-- | Version of 'withSomeSing' with 'Typeable' constraint | |
-- provided to processing function. | |
-- | |
-- Required for not to erase these useful constraints when doing | |
-- conversion from value of type 'T' to its singleton representation. | |
withSomeSingT | |
:: T | |
-> (forall (a :: T). (Typeable a, SingI a) => Sing a -> r) | |
-> r | |
withSomeSingT t f = (\(SomeSingT s) -> f s) (toSingT t) | |
-- | Version of 'fromSing' specialized for use with | |
-- @data instance Sing :: T -> Type@ which requires 'Typeable' | |
-- constraint for some of its constructors | |
fromSingT :: Sing (a :: T) -> T | |
fromSingT = \case | |
STKey -> TKey | |
STUnit -> TUnit | |
STSignature -> TSignature | |
STChainId -> TChainId | |
STOption t -> TOption (fromSingT t) | |
STList t -> TList (fromSingT t) | |
STSet t -> TSet (fromSingT t) | |
STOperation -> TOperation | |
STContract t -> TContract (fromSingT t) | |
STPair a b -> TPair (fromSingT a) (fromSingT b) | |
STOr a b -> TOr (fromSingT a) (fromSingT b) | |
STLambda a b -> TLambda (fromSingT a) (fromSingT b) | |
STMap a b -> TMap (fromSingT a) (fromSingT b) | |
STBigMap a b -> TBigMap (fromSingT a) (fromSingT b) | |
STInt -> TInt | |
STNat -> TNat | |
STString -> TString | |
STBytes -> TBytes | |
STMutez -> TMutez | |
STBool -> TBool | |
STKeyHash -> TKeyHash | |
STTimestamp -> TTimestamp | |
STAddress -> TAddress | |
-- | Version of 'toSing' which creates 'SomeSingT'. | |
toSingT :: T -> SomeSingT | |
toSingT = \case | |
TKey -> SomeSingT STKey | |
TUnit -> SomeSingT STUnit | |
TSignature -> SomeSingT STSignature | |
TChainId -> SomeSingT STChainId | |
TOption t -> withSomeSingT t $ \tSing -> SomeSingT $ STOption tSing | |
TList t -> withSomeSingT t $ \tSing -> SomeSingT $ STList tSing | |
TSet ct -> withSomeSingT ct $ \ctSing -> SomeSingT $ STSet ctSing | |
TOperation -> SomeSingT STOperation | |
TContract t -> withSomeSingT t $ \tSing -> SomeSingT $ STContract tSing | |
TPair l r -> | |
withSomeSingT l $ \lSing -> | |
withSomeSingT r $ \rSing -> | |
SomeSingT $ STPair lSing rSing | |
TOr l r -> | |
withSomeSingT l $ \lSing -> | |
withSomeSingT r $ \rSing -> | |
SomeSingT $ STOr lSing rSing | |
TLambda l r -> | |
withSomeSingT l $ \lSing -> | |
withSomeSingT r $ \rSing -> | |
SomeSingT $ STLambda lSing rSing | |
TMap l r -> | |
withSomeSingT l $ \lSing -> | |
withSomeSingT r $ \rSing -> | |
SomeSingT $ STMap lSing rSing | |
TBigMap l r -> | |
withSomeSingT l $ \lSing -> | |
withSomeSingT r $ \rSing -> | |
SomeSingT $ STBigMap lSing rSing | |
TInt -> SomeSingT STInt | |
TNat -> SomeSingT STNat | |
TString -> SomeSingT STString | |
TBytes -> SomeSingT STBytes | |
TMutez -> SomeSingT STMutez | |
TBool -> SomeSingT STBool | |
TKeyHash -> SomeSingT STKeyHash | |
TTimestamp -> SomeSingT STTimestamp | |
TAddress -> SomeSingT STAddress | |
instance SingKind T where | |
type Demote T = T | |
fromSing = fromSingT | |
toSing t = case toSingT t of SomeSingT s -> SomeSing s | |
instance SingI 'TKey where | |
sing = STKey | |
instance SingI 'TUnit where | |
sing = STUnit | |
instance SingI 'TSignature where | |
sing = STSignature | |
instance SingI 'TChainId where | |
sing = STChainId | |
instance (SingI a, Typeable a) => SingI ( 'TOption (a :: T)) where | |
sing = STOption sing | |
instance (SingI a, Typeable a) => SingI ( 'TList (a :: T)) where | |
sing = STList sing | |
instance (SingI a, Typeable a) => SingI ( 'TSet (a :: T)) where | |
sing = STSet sing | |
instance SingI 'TOperation where | |
sing = STOperation | |
instance (SingI a, Typeable a) => | |
SingI ( 'TContract (a :: T)) where | |
sing = STContract sing | |
instance (SingI a, Typeable a, Typeable b, SingI b) => | |
SingI ( 'TPair a b) where | |
sing = STPair sing sing | |
instance (SingI a, Typeable a, Typeable b, SingI b) => | |
SingI ( 'TOr a b) where | |
sing = STOr sing sing | |
instance (SingI a, Typeable a, Typeable b, SingI b) => | |
SingI ( 'TLambda a b) where | |
sing = STLambda sing sing | |
instance (SingI a, Typeable a, Typeable b, SingI b) => | |
SingI ( 'TMap a b) where | |
sing = STMap sing sing | |
instance (SingI a, Typeable a, Typeable b, SingI b) => | |
SingI ( 'TBigMap a b) where | |
sing = STBigMap sing sing | |
instance SingI 'TInt where | |
sing = STInt | |
instance SingI 'TNat where | |
sing = STNat | |
instance SingI 'TString where | |
sing = STString | |
instance SingI 'TBytes where | |
sing = STBytes | |
instance SingI 'TMutez where | |
sing = STMutez | |
instance SingI 'TBool where | |
sing = STBool | |
instance SingI 'TKeyHash where | |
sing = STKeyHash | |
instance SingI 'TTimestamp where | |
sing = STTimestamp | |
instance SingI 'TAddress where | |
sing = STAddress | |
data Dict :: Constraint -> * where | |
Dict :: a => Dict a | |
deriving Typeable | |
withDict :: HasDict c e => e -> (c => r) -> r | |
withDict d r = case evidence d of | |
Dict -> r | |
class HasDict c e | e -> c where | |
evidence :: e -> Dict c | |
instance HasDict a (Dict a) where | |
evidence = Prelude.id | |
instance a => HasDict b (a :- b) where | |
evidence (Sub x) = x | |
instance HasDict (Coercible a b) (Coercion a b) where | |
evidence Coercion = Dict | |
instance HasDict (a ~ b) (a :~: b) where | |
evidence Refl = Dict | |
infixl 1 \\ -- required comment | |
(\\) :: HasDict c e => (c => r) -> e -> r | |
r \\ d = withDict d r | |
infixr 9 :- | |
newtype a :- b = Sub (a => Dict b) | |
deriving Typeable | |
type role (:-) nominal nominal | |
(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d) | |
f *** g = Sub $ Dict \\ f \\ g | |
type f $ a = f a | |
infixr 2 $ | |
maybeToRight a Nothing = Left a | |
maybeToRight _ (Just a) = Right a | |
---------------------------------------------------------------------------- | |
-- Constraints | |
---------------------------------------------------------------------------- | |
-- | Whether this type contains 'TOperation' type. | |
-- | |
-- 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 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 this type contains 'TContract' type. | |
-- | |
-- 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 this type contains 'TBigMap' type. | |
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 t) = ContainsBigMap t | |
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 this type contains a type with nested 'TBigMap'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 doesn'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 t) = ContainsNestedBigMaps t | |
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 | |
-- | Constraint which ensures that operation type does not appear in a given type. | |
-- | |
-- 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 contract type does not appear in a given type. | |
class (ContainsContract t ~ 'False) => HasNoContract t | |
instance (ContainsContract t ~ 'False) => HasNoContract t | |
-- | Constraint which ensures that bigmap does not appear in a given type. | |
class (ContainsBigMap t ~ 'False) => HasNoBigMap t | |
instance (ContainsBigMap t ~ 'False) => HasNoBigMap 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 '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 = () | |
-- | 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: | |
-- <https://gitlab.haskell.org/ghc/ghc/issues/11503 #11503>. | |
-- | |
-- Use this constraint in our eDSL. | |
type ForbidOp t = FailOnOperationFound (ContainsOp t) | |
type ForbidContract t = FailOnContractFound (ContainsContract t) | |
type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t) | |
type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps 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 | |
-- | Whether the type contains 'TOperation', with proof. | |
data OpPresence (t :: T) | |
= ContainsOp t ~ 'True => OpPresent | |
| ContainsOp t ~ 'False => OpAbsent | |
data ContractPresence (t :: T) | |
= ContainsContract t ~ 'True => ContractPresent | |
| ContainsContract t ~ 'False => ContractAbsent | |
data BigMapPresence (t :: T) | |
= ContainsBigMap t ~ 'True => BigMapPresent | |
| ContainsBigMap t ~ 'False => BigMapAbsent | |
data NestedBigMapsPresence (t :: T) | |
= ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent | |
| ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent | |
-- @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 the given type contains 'TOperation'. | |
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 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 | |
STTimestamp -> OpAbsent | |
STAddress -> OpAbsent | |
-- | Check at runtime whether the given type contains 'TContract'. | |
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 | |
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 | |
STTimestamp -> ContractAbsent | |
STAddress -> ContractAbsent | |
-- | Check at runtime whether the given type contains 'TBigMap'. | |
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 t -> case checkBigMapPresence t of | |
BigMapPresent -> BigMapPresent | |
BigMapAbsent -> BigMapAbsent | |
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 | |
STTimestamp -> BigMapAbsent | |
STAddress -> BigMapAbsent | |
-- | Check at runtime whether the given type contains 'TBigMap'. | |
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 t -> case checkNestedBigMapsPresence t of | |
NestedBigMapsPresent -> NestedBigMapsPresent | |
NestedBigMapsAbsent -> 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 | |
STTimestamp -> NestedBigMapsAbsent | |
STAddress -> NestedBigMapsAbsent | |
-- | Check at runtime that the given type does not contain 'TOperation'. | |
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t) | |
opAbsense s = case checkOpPresence s of | |
OpPresent -> Nothing | |
OpAbsent -> Just Dict | |
-- | Check at runtime that the given type does not contain 'TContract'. | |
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t) | |
contractTypeAbsense s = case checkContractTypePresence s of | |
ContractPresent -> Nothing | |
ContractAbsent -> Just Dict | |
-- | Check at runtime that the given type does not containt 'TBigMap' | |
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t) | |
bigMapAbsense s = case checkBigMapPresence s of | |
BigMapPresent -> Nothing | |
BigMapAbsent -> Just Dict | |
-- | Check at runtime that the given type does not contain nested 'TBigMap' | |
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 | |
deriving stock (Show, Eq, Generic) | |
-- | Alias for constraints which Michelson applies to parameter. | |
type ParameterScope t = | |
(Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t) | |
-- | Alias for constraints which Michelson applies to contract storage. | |
type StorageScope t = | |
(Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) | |
-- | Alias for constraints which Michelson applies to pushed constants. | |
type ConstantScope t = | |
(SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t) | |
-- | Alias for constraints which Michelson applies to packed values. | |
type PackedValScope t = | |
(SingI t, HasNoOp t, HasNoBigMap t) | |
-- | Alias for constraints which Michelson applies to unpacked values. | |
-- | |
-- It is different from 'PackedValScope', e.g. @contract@ type cannot appear | |
-- in a value we unpack to. | |
type UnpackedValScope t = | |
(PackedValScope t, ConstantScope t) | |
-- | Alias for constraints which are required for printing. | |
type PrintedValScope 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 (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 (Typeable t, SingI t) => CheckScope (ParameterScope t) where | |
checkScope = | |
(\Dict Dict -> Dict) | |
<$> checkScope @(HasNoOp t) | |
<*> checkScope @(HasNoNestedBigMaps t) | |
instance (Typeable t, SingI t) => CheckScope (StorageScope t) where | |
checkScope = | |
(\Dict Dict Dict -> Dict) | |
<$> checkScope @(HasNoOp t) | |
<*> checkScope @(HasNoNestedBigMaps t) | |
<*> checkScope @(HasNoContract t) | |
instance (Typeable t, SingI t) => CheckScope (ConstantScope t) where | |
checkScope = | |
(\Dict Dict Dict -> Dict) | |
<$> checkScope @(HasNoOp t) | |
<*> checkScope @(HasNoBigMap t) | |
<*> checkScope @(HasNoContract t) | |
instance (Typeable t, SingI t) => CheckScope (PackedValScope t) where | |
checkScope = | |
(\Dict Dict -> Dict) | |
<$> checkScope @(HasNoOp t) | |
<*> checkScope @(HasNoBigMap t) | |
instance (Typeable t, SingI t) => CheckScope (UnpackedValScope t) where | |
checkScope = | |
(\Dict Dict -> Dict) | |
<$> checkScope @(PackedValScope t) | |
<*> checkScope @(ConstantScope t) | |
-- 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 = | |
(Typeable t, SingI t, ForbidOp t, ForbidNestedBigMaps t) | |
type ProperStorageBetterErrors t = | |
(Typeable t, SingI t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t) | |
type ProperConstantBetterErrors t = | |
(SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t) | |
type ProperPackedValBetterErrors t = | |
(SingI t, ForbidOp t, ForbidBigMap t) | |
type ProperUnpackedValBetterErrors t = | |
(ProperPackedValBetterErrors t, ProperConstantBetterErrors t) | |
type ProperPrintedValBetterErrors t = | |
(SingI t, ForbidOp 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 | |
properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t | |
properPackedValEvi = Sub $ | |
Dict \\ forbiddenOpEvi @t | |
\\ forbiddenBigMapEvi @t | |
properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t | |
properUnpackedValEvi = properPackedValEvi @t *** properConstantEvi @t | |
properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t | |
properPrintedValEvi = Sub $ | |
Dict \\ forbiddenOpEvi @t |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment