Add regression test for #18478wip/T18478

!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 files changed, 953 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T18478.hs b/testsuite/tests/pmcheck/should_compile/T18478.hs
new file mode 100644
index 0000000000..372ac2d171
--- /dev/null
+++ b/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@-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@. 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 -> 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
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 2e4e3942ac..57527977ff 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/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,