{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Michelson.Typed.Scope
(
ComparabilityScope
, ParameterScope
, StorageScope
, ConstantScope
, PackedValScope
, UnpackedValScope
, PrintedValScope
, ProperParameterBetterErrors
, ProperStorageBetterErrors
, ProperConstantBetterErrors
, ProperPackedValBetterErrors
, ProperUnpackedValBetterErrors
, ProperPrintedValBetterErrors
, ProperComparabilityBetterErrors
, properParameterEvi
, properStorageEvi
, properConstantEvi
, properPackedValEvi
, properUnpackedValEvi
, properPrintedValEvi
, (:-)(..)
, BadTypeForScope (..)
, CheckScope (..)
, Comparable
, HasNoBigMap
, HasNoNestedBigMaps
, HasNoOp
, HasNoContract
, ContainsBigMap
, ContainsNestedBigMaps
, ForbidOp
, ForbidContract
, ForbidBigMap
, ForbidNestedBigMaps
, FailOnBigMapFound
, FailOnNestedBigMapsFound
, FailOnOperationFound
, ForbidNonComparable
, Comparability(..)
, OpPresence (..)
, ContractPresence (..)
, BigMapPresence (..)
, NestedBigMapsPresence (..)
, comparabilityPresence
, checkComparability
, checkOpPresence
, checkContractTypePresence
, checkBigMapPresence
, checkNestedBigMapsPresence
, opAbsense
, contractTypeAbsense
, bigMapAbsense
, nestedBigMapsAbsense
, forbiddenOp
, forbiddenContractType
, forbiddenBigMap
, forbiddenNestedBigMaps
, withDict
, SingI (..)
) where
import Data.Constraint ((:-)(..), Dict(..), withDict, (\\))
import qualified Data.Constraint as C
import Data.Singletons (SingI(..))
import Data.Type.Bool (type (&&), type (||))
import Fmt (Buildable(..))
import GHC.TypeLits (ErrorMessage(..), TypeError)
import Michelson.Typed.Sing (Sing(..))
import Michelson.Typed.T (T(..))
type family IsComparable (t :: T) :: Bool where
IsComparable ('Tc _) = 'True
IsComparable ('TPair a b) = IsComparable a && IsComparable b
IsComparable _ = 'False
type family ContainsOp (t :: T) :: Bool where
ContainsOp ('Tc _) = 'False
ContainsOp 'TKey = 'False
ContainsOp 'TUnit = 'False
ContainsOp 'TSignature = 'False
ContainsOp 'TChainId = 'False
ContainsOp ('TOption t) = ContainsOp t
ContainsOp ('TList t) = ContainsOp t
ContainsOp ('TSet _) = 'False
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 _ v) = ContainsOp v
ContainsOp ('TBigMap _ v) = ContainsOp v
type family ContainsContract (t :: T) :: Bool where
ContainsContract ('Tc _) = 'False
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
type family ContainsBigMap (t :: T) :: Bool where
ContainsBigMap ('Tc _) = 'False
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
type family ContainsNestedBigMaps (t :: T) :: Bool where
ContainsNestedBigMaps ('Tc _) = 'False
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
class (ContainsOp t ~ 'False) => HasNoOp t
instance (ContainsOp t ~ 'False) => HasNoOp t
class (ContainsContract t ~ 'False) => HasNoContract t
instance (ContainsContract t ~ 'False) => HasNoContract t
class (ContainsBigMap t ~ 'False) => HasNoBigMap t
instance (ContainsBigMap t ~ 'False) => HasNoBigMap t
class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
class (IsComparable t ~ 'True) => Comparable t
instance (IsComparable t ~ 'True) => Comparable t
type family FailOnOperationFound (enabled :: Bool) :: Constraint where
FailOnOperationFound 'True =
TypeError ('Text "Operations are not allowed in this scope")
FailOnOperationFound 'False = ()
type family FailOnContractFound (enabled :: Bool) :: Constraint where
FailOnContractFound 'True =
TypeError ('Text "Type `contract` is not allowed in this scope")
FailOnContractFound 'False = ()
type family FailOnBigMapFound (enabled :: Bool) :: Constraint where
FailOnBigMapFound 'True =
TypeError ('Text "BigMaps are not allowed in this scope")
FailOnBigMapFound 'False = ()
type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where
FailOnNestedBigMapsFound 'True =
TypeError ('Text "Nested BigMaps are not allowed")
FailOnNestedBigMapsFound 'False = ()
type family FailOnNonComparable (isComparable :: Bool) :: Constraint where
FailOnNonComparable 'False =
TypeError ('Text "The type is not comparable")
FailOnNonComparable 'True = ()
type ForbidOp t = FailOnOperationFound (ContainsOp t)
type ForbidContract t = FailOnContractFound (ContainsContract t)
type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)
type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
type ForbidNonComparable t = FailOnNonComparable (IsComparable t)
forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t
forbiddenOpEvi = Sub $
case checkOpPresence (sing @t) of
OpAbsent -> Dict
OpPresent -> error "impossible"
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
forbiddenContractTypeEvi
:: forall t. (SingI t, ForbidContract t) :- HasNoContract t
forbiddenContractTypeEvi = Sub $
case checkContractTypePresence (sing @t) of
ContractAbsent -> Dict
ContractPresent -> error "impossible"
forbiddenContractType
:: forall t a.
(SingI t, ForbidContract t)
=> (HasNoContract t => a)
-> a
forbiddenContractType = withDict $ forbiddenContractTypeEvi @t
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
data Comparability t where
CanBeCompared :: Comparable t => Comparability t
CannotBeCompared :: (IsComparable t ~ 'False) => Comparability t
checkComparability :: Sing t -> Comparability t
checkComparability = \case
STc _ -> CanBeCompared
STPair a b -> case (checkComparability a, checkComparability b) of
(CanBeCompared, CanBeCompared) -> CanBeCompared
(CannotBeCompared, _) -> CannotBeCompared
(_, CannotBeCompared) -> CannotBeCompared
STKey -> CannotBeCompared
STUnit -> CannotBeCompared
STSignature -> CannotBeCompared
STChainId -> CannotBeCompared
STOption _ -> CannotBeCompared
STList _ -> CannotBeCompared
STSet _ -> CannotBeCompared
STOperation -> CannotBeCompared
STContract _ -> CannotBeCompared
STOr _ _ -> CannotBeCompared
STLambda _ _ -> CannotBeCompared
STMap _ _ -> CannotBeCompared
STBigMap _ _ -> CannotBeCompared
checkOpPresence :: Sing (ty :: T) -> OpPresence ty
checkOpPresence = \case
STc _ -> OpAbsent
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 _ -> 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 _ v -> case checkOpPresence v of
OpPresent -> OpPresent
OpAbsent -> OpAbsent
STBigMap _ v -> case checkOpPresence v of
OpPresent -> OpPresent
OpAbsent -> OpAbsent
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
checkContractTypePresence = \case
STc _ -> ContractAbsent
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
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkBigMapPresence = \case
STc _ -> BigMapAbsent
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
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
checkNestedBigMapsPresence = \case
STc _ -> NestedBigMapsAbsent
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
comparabilityPresence :: Sing t -> Maybe (Dict $ Comparable t)
comparabilityPresence s = case checkComparability s of
CanBeCompared -> Just Dict
CannotBeCompared -> Nothing
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
opAbsense s = case checkOpPresence s of
OpPresent -> Nothing
OpAbsent -> Just Dict
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
contractTypeAbsense s = case checkContractTypePresence s of
ContractPresent -> Nothing
ContractAbsent -> Just Dict
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
bigMapAbsense s = case checkBigMapPresence s of
BigMapPresent -> Nothing
BigMapAbsent -> Just Dict
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
nestedBigMapsAbsense s = case checkNestedBigMapsPresence s of
NestedBigMapsPresent -> Nothing
NestedBigMapsAbsent -> Just Dict
data BadTypeForScope
= BtNotComparable
| BtIsOperation
| BtHasBigMap
| BtHasNestedBigMap
| BtHasContract
instance Buildable BadTypeForScope where
build = \case
BtNotComparable -> "not comparable"
BtIsOperation -> "has 'operation' type"
BtHasBigMap -> "has 'big_map'"
BtHasNestedBigMap -> "has nested 'big_map'"
BtHasContract -> "has 'contract' type"
type ComparabilityScope t =
(Typeable t, SingI t, Comparable t)
type ParameterScope t =
(Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t)
type StorageScope t =
(Typeable t, SingI t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t)
type ConstantScope t =
(SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t)
type PackedValScope t =
(SingI t, HasNoOp t, HasNoBigMap t)
type UnpackedValScope t =
(PackedValScope t, ConstantScope t)
type PrintedValScope t = (SingI t, HasNoOp t)
class CheckScope (c :: Constraint) where
checkScope :: Either BadTypeForScope (Dict c)
instance SingI t => CheckScope (Comparable t) where
checkScope = maybeToRight BtNotComparable $ comparabilityPresence sing
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 (ComparabilityScope t) where
checkScope =
(\Dict -> Dict) <$> checkScope @(Comparable t)
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)
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)
type ProperComparabilityBetterErrors t =
(SingI t, ForbidNonComparable t, Comparable 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 C.*** properConstantEvi @t
properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t
properPrintedValEvi = Sub $
Dict \\ forbiddenOpEvi @t