{-# OPTIONS_HADDOCK not-home #-}
module Morley.Michelson.Typed.Scope.Internal.ForbidT
( module Morley.Michelson.Typed.Scope.Internal.ForbidT
) where
import Data.Type.Bool (type (||))
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
import Type.Errors (WhenStuck)
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.Sing
import Morley.Util.Type (FailWhen)
data TPredicateSym
= PSOp
| PSContract
| PSTicket
| PSBigMap
| PSNestedBigMaps
| PSSaplingState
| PSNonComparable
genSingletonsType ''TPredicateSym
type TPredicateSymTypeName :: TPredicateSym -> Symbol
type family TPredicateSymTypeName p where
TPredicateSymTypeName 'PSOp = "`operation`"
TPredicateSymTypeName 'PSContract = "`contract`"
TPredicateSymTypeName 'PSTicket = "`ticket`"
TPredicateSymTypeName 'PSBigMap = "`big_map`"
TPredicateSymTypeName 'PSNestedBigMaps = "nested `big_map`s"
TPredicateSymTypeName 'PSSaplingState = "`sapling_state`"
TPredicateSymTypeName 'PSNonComparable = "non-comparable types"
type ContainsT :: TPredicateSym -> T -> Bool
type family ContainsT p t where
ContainsT 'PSOp 'TOperation = 'True
ContainsT 'PSContract ('TContract _) = 'True
ContainsT 'PSTicket ('TTicket _) = 'True
ContainsT 'PSBigMap ('TBigMap _ _) = 'True
ContainsT 'PSSaplingState ('TSaplingState _) = 'True
ContainsT 'PSNestedBigMaps ('TBigMap _ v) = ContainsT 'PSBigMap v
ContainsT 'PSNonComparable 'TBls12381Fr = 'True
ContainsT 'PSNonComparable 'TBls12381G1 = 'True
ContainsT 'PSNonComparable 'TBls12381G2 = 'True
ContainsT 'PSNonComparable ('TList _) = 'True
ContainsT 'PSNonComparable ('TSet _) = 'True
ContainsT 'PSNonComparable 'TOperation = 'True
ContainsT 'PSNonComparable ('TContract _) = 'True
ContainsT 'PSNonComparable ('TTicket _) = 'True
ContainsT 'PSNonComparable ('TLambda _ _) = 'True
ContainsT 'PSNonComparable ('TMap _ _) = 'True
ContainsT 'PSNonComparable ('TBigMap _ _) = 'True
ContainsT 'PSNonComparable 'TChest = 'True
ContainsT 'PSNonComparable 'TChestKey = 'True
ContainsT 'PSNonComparable ('TSaplingState _) = 'True
ContainsT 'PSNonComparable ('TSaplingTransaction _) = 'True
ContainsT p ('TOption t) = ContainsT p t
ContainsT p ('TList t) = ContainsT p t
ContainsT p ('TSet t) = ContainsT p t
ContainsT p ('TTicket t) = ContainsT p t
ContainsT p ('TPair a b) = ContainsT p a || ContainsT p b
ContainsT p ('TOr a b) = ContainsT p a || ContainsT p b
ContainsT p ('TBigMap k v) = ContainsT p k || ContainsT p v
ContainsT p ('TMap k v) = ContainsT p k || ContainsT p v
ContainsT _ _ = 'False
type ForbidTErrorMsg :: TPredicateSym -> T -> ErrorMessage
type family ForbidTErrorMsg p t where
ForbidTErrorMsg 'PSNestedBigMaps t =
'Text "Nested `big_map`s found in" ':$$: 'ShowType t ':$$: 'Text "are not allowed"
ForbidTErrorMsg 'PSNonComparable t =
'Text "Non-comparable type"
':$$: 'ShowType t
':$$: 'Text "is not allowed in this scope"
ForbidTErrorMsg p t =
'Text "Type " ':<>: 'Text (TPredicateSymTypeName p) ':<>: 'Text " found in"
':$$: 'ShowType t
':$$: 'Text "is not allowed in this scope"
type ForbidT :: TPredicateSym -> T -> Constraint
class ForbidManyT (ForbidT p t) '[p] t => ForbidT p t
instance ForbidManyT (ForbidT p t) '[p] t => ForbidT p t
type ForbidOp = ForbidT 'PSOp
type ForbidContract = ForbidT 'PSContract
type ForbidTicket = ForbidT 'PSTicket
type ForbidSaplingState = ForbidT 'PSSaplingState
type ForbidBigMap = ForbidT 'PSBigMap
type ForbidNestedBigMaps = ForbidT 'PSNestedBigMaps
type ForbidNonComparable = ForbidT 'PSNonComparable
type ForbidManyT' :: Constraint -> [TPredicateSym] -> [TPredicateSym] -> T -> Constraint
class ForbidManySuperC ps t => ForbidManyT' c ps' ps t where
type ForbidManySuperC ps t :: Constraint
instance ForbidManyT' c ps' '[] t where
type ForbidManySuperC '[] _ = ()
instance
( ForbidManyT' c ps' ps t
, DelayedContainsTCheck c ps' p t (ContainsT p t)
) => ForbidManyT' c ps' (p : ps) t where
type ForbidManySuperC (p : ps) t =
( ContainsT p t ~ 'False
, ForbidManySuperC ps t
)
class a ~ 'False => DelayedContainsTCheck c ps' p t a
instance DelayedContainsTCheck c ps' p t 'False
instance {-# incoherent #-}
( WhenStuck t (TypeError (ForbidManyTStuckErr c ps' t))
, FailWhen a (ForbidTErrorMsg p t)
) => DelayedContainsTCheck c ps' p t a
type ForbidManyT c ps = ForbidManyT' c ps ps
type TPredicateSymTypeNames :: [TPredicateSym] -> ErrorMessage
type family TPredicateSymTypeNames ps where
TPredicateSymTypeNames '[] = 'Text ""
TPredicateSymTypeNames '[p] = 'Text (TPredicateSymTypeName p)
TPredicateSymTypeNames '[p, q] =
'Text (TPredicateSymTypeName p) ':<>: 'Text " or " ':<>: 'Text (TPredicateSymTypeName q)
TPredicateSymTypeNames (p : ps) =
'Text (TPredicateSymTypeName p) ':<>: 'Text ", " ':<>: TPredicateSymTypeNames ps
type ForbidManyTStuckErr :: Constraint -> [TPredicateSym] -> T -> ErrorMessage
type ForbidManyTStuckErr c ps t =
'Text "Can't check if type" ':$$:
'ShowType t ':$$:
'Text "contains " ':<>: TPredicateSymTypeNames ps ':<>:
'Text ". Perhaps you need to add" ':$$:
'ShowType c ':$$:
'Text "constraint? You can also try adding a type annotation."