[Git][ghc/ghc][wip/T18478] Add regression test for #18478
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Jul 20 13:37:11 UTC 2020
Sebastian Graf pushed to branch wip/T18478 at Glasgow Haskell Compiler / GHC
Commits:
39a5ed5e by Sebastian Graf at 2020-07-20T15:37:00+02:00
Add regression test for #18478
!3392 backported !2993 to GHC 8.10.2 which most probably is responsible
for fixing #18478, which triggered a pattern match checker performance
regression in GHC 8.10.1 as first observed in #17977.
- - - - -
2 changed files:
- + testsuite/tests/pmcheck/should_compile/T18478.hs
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
testsuite/tests/pmcheck/should_compile/T18478.hs
=====================================
@@ -0,0 +1,951 @@
+{-# 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 -fforce-recomp -Wincomplete-patterns #-}
+
+{- | 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 at -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 T18478
+ ( -- * 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 at . Rarely, the type and kind do not
+ -- match. For example, @Demote Nat@ is @Natural at .
+ 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 -> Type 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
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -120,6 +120,8 @@ test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18049', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18478', collect_compiler_stats('bytes allocated',10), compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/39a5ed5e2fb0cf042365814a03822491e61af463
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/39a5ed5e2fb0cf042365814a03822491e61af463
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200720/6225bbad/attachment-0001.html>
More information about the ghc-commits
mailing list