diff --git a/definitions/package.yaml b/definitions/package.yaml
index 8fcc76bd84..1d3d02560d 100644
--- a/definitions/package.yaml
+++ b/definitions/package.yaml
@@ -19,45 +19,11 @@ ghc-options:
   - -Wincomplete-uni-patterns
 
 default-extensions:
-  - TemplateHaskell
-  - NoImplicitPrelude
-  # numbers, strings, lists
-  - NegativeLiterals
-  - NumericUnderscores
-  - OverloadedStrings
-  # function syntax
-  - BlockArguments
-  - EmptyCase
-  - LambdaCase
-  # Records
   - DuplicateRecordFields
   - NamedFieldPuns
+  - NoImplicitPrelude
+  - OverloadedStrings
   - RecordWildCards
-  # deriving
-  - DeriveAnyClass
-  - DeriveFunctor
-  - DeriveGeneric
-  - StandaloneDeriving
-  # type classes
-  - FunctionalDependencies
-  - FlexibleContexts
-  - FlexibleInstances
-  - InstanceSigs
-  - TypeSynonymInstances
-  - UndecidableInstances
-  # types
-  - DataKinds
-  - ConstraintKinds
-  - GADTs
-  - KindSignatures
-  - LiberalTypeSynonyms
-  - NoStarIsType
-  - PolyKinds
-  - RankNTypes
-  - ScopedTypeVariables
-  - TypeApplications
-  - TypeFamilies
-  - TypeOperators
   
 dependencies:
   - aeson
diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs
index 5b31fead81..1a9de076ed 100644
--- a/definitions/src/Simplex/Messaging/Protocol.hs
+++ b/definitions/src/Simplex/Messaging/Protocol.hs
@@ -1,4 +1,15 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Simplex.Messaging.Protocol where
 
@@ -30,11 +41,11 @@ data BrokerCS :: ConnectionState -> Type where
   BrkDrained  :: BrokerCS 'Drained
   BrkNone     :: BrokerCS 'None
 
-instance Auto (TyPred BrokerCS) 'New      where auto = BrkNew
-instance Auto (TyPred BrokerCS) 'Secured  where auto = BrkSecured
-instance Auto (TyPred BrokerCS) 'Disabled where auto = BrkDisabled
-instance Auto (TyPred BrokerCS) 'Drained  where auto = BrkDrained
-instance Auto (TyPred BrokerCS) 'None     where auto = BrkNone
+instance Auto (TyPred BrokerCS) 'New      where auto = autoTC
+instance Auto (TyPred BrokerCS) 'Secured  where auto = autoTC
+instance Auto (TyPred BrokerCS) 'Disabled where auto = autoTC
+instance Auto (TyPred BrokerCS) 'Drained  where auto = autoTC
+instance Auto (TyPred BrokerCS) 'None     where auto = autoTC
 
 -- sender connection states
 data SenderCS :: ConnectionState -> Type where
@@ -43,10 +54,10 @@ data SenderCS :: ConnectionState -> Type where
   SndSecured   :: SenderCS 'Secured
   SndNone      :: SenderCS 'None
 
-instance Auto (TyPred SenderCS) 'New       where auto = SndNew
-instance Auto (TyPred SenderCS) 'Confirmed where auto = SndConfirmed
-instance Auto (TyPred SenderCS) 'Secured   where auto = SndSecured
-instance Auto (TyPred SenderCS) 'None      where auto = SndNone
+instance Auto (TyPred SenderCS) 'New       where auto = autoTC
+instance Auto (TyPred SenderCS) 'Confirmed where auto = autoTC
+instance Auto (TyPred SenderCS) 'Secured   where auto = autoTC
+instance Auto (TyPred SenderCS) 'None      where auto = autoTC
 
 -- allowed participant connection states
 data HasState (p :: Participant) (s :: ConnectionState) :: Type where
@@ -54,7 +65,7 @@ data HasState (p :: Participant) (s :: ConnectionState) :: Type where
   BrkHasState :: Prf1 BrokerCS s => HasState 'Broker s
   SndHasState :: Prf1 SenderCS s => HasState 'Sender s
 
-class Prf p a s where auto' :: p a s
+class Prf t p s where auto' :: t p s
 instance                    Prf HasState 'Recipient s
   where auto' = RcpHasState
 instance Prf1 BrokerCS s => Prf HasState 'Broker s
diff --git a/definitions/src/Simplex/Messaging/ServerAPI.hs b/definitions/src/Simplex/Messaging/ServerAPI.hs
index 4efcd55ba3..8159db7294 100644
--- a/definitions/src/Simplex/Messaging/ServerAPI.hs
+++ b/definitions/src/Simplex/Messaging/ServerAPI.hs
@@ -1,4 +1,7 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Simplex.Messaging.ServerAPI
   ( ServerAPI
diff --git a/definitions/src/Simplex/Messaging/Test.hs b/definitions/src/Simplex/Messaging/Test.hs
new file mode 100644
index 0000000000..f9991febb7
--- /dev/null
+++ b/definitions/src/Simplex/Messaging/Test.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE DataKinds                      #-}
+{-# LANGUAGE EmptyCase                      #-}
+{-# LANGUAGE FlexibleContexts               #-}
+{-# LANGUAGE FlexibleInstances              #-}
+{-# LANGUAGE GADTs                          #-}
+{-# LANGUAGE InstanceSigs                   #-}
+{-# LANGUAGE LambdaCase                     #-}
+{-# LANGUAGE MultiParamTypeClasses          #-}
+{-# LANGUAGE PolyKinds                      #-}
+{-# LANGUAGE ScopedTypeVariables            #-}
+{-# LANGUAGE StandaloneDeriving             #-}
+{-# LANGUAGE TypeApplications               #-}
+{-# LANGUAGE TemplateHaskell                #-}
+{-# LANGUAGE TypeFamilies                   #-}
+{-# LANGUAGE TypeOperators                  #-}
+{-# LANGUAGE UndecidableInstances           #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+module Simplex.Messaging.Test where
+
+import ClassyPrelude
+
+import Data.Kind
+import Data.Singletons()
+import Data.Singletons.TH
+import Data.Type.Predicate
+import Data.Type.Predicate.Auto
+
+$(singletons [d|
+  data Participant = Recipient | Broker | Sender
+
+  data ConnectionState =  New       -- (participants: all) connection created (or received from sender)
+                        | Pending   -- (recipient) sent to sender out-of-band
+                        | Confirmed -- (recipient) confirmed by sender with the broker
+                        | Secured   -- (all) secured with the broker
+  |])
+
+-- broker connection states
+data BrokerCS :: ConnectionState -> Type where
+  BrkNew      :: BrokerCS 'New
+  BrkSecured  :: BrokerCS 'Secured
+
+instance Auto (TyPred BrokerCS) 'New where auto = autoTC
+instance Auto (TyPred BrokerCS) 'Secured where auto = autoTC
+
+data RBState (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
+  RBState :: Auto (TyPred BrokerCS) bs
+          => Sing rs -> Sing bs -> RBState rs bs
+
+data Box a = Num a => Box a
+
+goodBoxSample :: Box Int
+goodBoxSample = Box 1
+
+-- badBoxSample :: Box String
+-- badBox = Box "foo"
+
+goodSt :: RBState 'New 'New
+goodSt = RBState SNew SNew
+
+-- badSt :: RBState 'Pending 'Pending
+-- badSt = RBState SPending SPending
diff --git a/definitions/src/Simplex/Messaging/Types.hs b/definitions/src/Simplex/Messaging/Types.hs
index 114d9d85f0..cf99269b40 100644
--- a/definitions/src/Simplex/Messaging/Types.hs
+++ b/definitions/src/Simplex/Messaging/Types.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+
 module Simplex.Messaging.Types where
 
 import ClassyPrelude