diff --git a/imsos-monad.cabal b/imsos-monad.cabal
--- a/imsos-monad.cabal
+++ b/imsos-monad.cabal
@@ -20,7 +20,7 @@
 -- PVP summary:     +-+------- breaking API changes
 --                  | | +----- non-breaking API additions
 --                  | | | +--- code changes with no API change
-version:            0.1.0.0
+version:            0.2.4.0
 
 -- A short (one-line) description of the package.
 synopsis:
@@ -64,17 +64,38 @@
     import:           warnings
 
     -- Modules exported by the library.
-    exposed-modules:  Control.Monad.IMSOS 
+    exposed-modules:  Control.Monad.IMSOS
+                     ,Control.Monad.IMSOS.Fixed
+                     ,Control.Monad.IMSOS.Layered
 
     -- Modules included in this library but not exported.
-    -- other-modules:
+    other-modules:   
+                     ,Control.Monad.IMSOS.Monad
+                     ,Control.Monad.IMSOS.Signatures
+                     ,Control.Monad.IMSOS.Rules.Relations
+                     ,Control.Monad.IMSOS.Algebras
+                     ,Control.Monad.IMSOS.LayeredAlgebras
+                     ,Control.Monad.IMSOS.Rules.Step
+                     ,Control.Monad.IMSOS.Rules.LayeredStep
+                     ,Control.Monad.IMSOS.LayeredTerms
 
+                     ,Data.Comp.SubsumeCommon
+                     ,Data.Comp.ProjectionExt
+                     ,Control.Monad.IMSOS.LayeredDeriving
+
+--                     ,Control.Monad.IMSOS.Cases.WhileFixed
+--                     ,Control.Monad.IMSOS.Cases.WhileLayered
+
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions:
 
     -- Other library packages from which modules are imported.
     build-depends:    base ^>=4.18.3.0
+                     ,containers ^>= 0.6
                      ,mtl ^>= 2.3.1
+                     ,random ^>= 1.3
+                     ,template-haskell ^>= 2.20
+                     ,compdata ^>= 0.13
 
     -- Directories containing source files.
     hs-source-dirs:   src
diff --git a/src/Control/Monad/IMSOS.hs b/src/Control/Monad/IMSOS.hs
--- a/src/Control/Monad/IMSOS.hs
+++ b/src/Control/Monad/IMSOS.hs
@@ -1,92 +1,4 @@
-{-# LANGUAGE UndecidableInstances
-  , FlexibleInstances
-  , FlexibleContexts
-  , MultiParamTypeClasses
-#-}
-
 module Control.Monad.IMSOS 
-  (MonadIMSOS(..), runIMSOS, yieldIMSOS
-  ,tell
-  ,local, reader
-  ,get, put, state
-  ,fail, throwError, catchError
-  ) where
-
-import Control.Applicative (Alternative(..))
-import Control.Monad.Error.Class
-import Control.Monad.Reader (MonadReader(..))
-import Control.Monad.State  (MonadState(..))
-import Control.Monad.Writer (MonadWriter(..))
-import Control.Monad (ap)
-
-newtype MonadIMSOS r s w me e a = MonadIMSOS (r -> s -> me e (a, s, w))
-
-instance Functor (me e) => Functor (MonadIMSOS r s w me e) where
-  fmap f (MonadIMSOS m) = MonadIMSOS m'
-    where m' r s = modify <$> m r s
-           where modify (a, s', w) = (f a, s', w)
-
-instance (MonadError e (me e), Monad (me e), Monoid w)
-    => Monad (MonadIMSOS r s w me e) where
-  (MonadIMSOS p) >>= m = MonadIMSOS $ \r1 s1  -> do
-     (a, s2, w2) <- p r1 s1
-     let MonadIMSOS q = m a
-     (b, s3, w3) <- q r1 s2
-     return (b, s3, w2 <> w3)
-
-instance (MonadError e (me e), Monad (me e), Monoid w)
-    => Applicative (MonadIMSOS r s w me e) where
-  pure a = MonadIMSOS m
-    where m _ s = pure (a, s, mempty)
-  (<*>) = ap
-
-instance (MonadError e (me e), Monad (me e), Alternative (me e), Monoid w)
-    => Alternative (MonadIMSOS r s w me e) where
-  empty = MonadIMSOS (\_ _ -> empty)
-  (MonadIMSOS p) <|> (MonadIMSOS q) = MonadIMSOS m
-    where m r s = p r s `catchError` \_ -> q r s
- 
---instance (MonadError e (me e), Monad (me e), Monoid w)
---    => MonadPlus (MonadIMSOS r s w me e)
-
-instance (MonadError String (me String), Monad (me String), Monoid w)
-    => MonadFail (MonadIMSOS r s w me String) where
-  fail = throwError
-
-instance (MonadError e (me e), Monad (me e), Monoid w)
-    => MonadReader r (MonadIMSOS r s w me e) where
-  ask = MonadIMSOS m 
-    where m r s = pure (r, s, mempty)
-  local f (MonadIMSOS p) = MonadIMSOS m
-    where m r s = p (f r) s
-
-instance (MonadError e (me e), Monad (me e), Monoid w)
-    => MonadState s (MonadIMSOS r s w me e) where
-  state act = MonadIMSOS m
-    where m _ s = pure (a, s', mempty)
-           where (a, s') = act s
-
-instance (MonadError e (me e), Monad (me e), Monoid w)
-    => MonadWriter w (MonadIMSOS r s w me e) where
-  tell w = MonadIMSOS m
-    where m _ s = pure ((), s, w)
-  listen (MonadIMSOS p) = MonadIMSOS m
-    where m r s = p r s >>= \(a, s', w) -> pure ((a,w), s', w)
-  pass (MonadIMSOS p) = MonadIMSOS m
-    where m r s = p r s >>= \((a,f), s', w) -> pure (a, s', f w)
-
-instance (MonadError e (me e), Monad (me e), Monoid w)
-    => MonadError e (MonadIMSOS r s w me e) where
-  throwError e = MonadIMSOS m
-    where m _ _ = throwError e
-  catchError (MonadIMSOS p) h = MonadIMSOS m
-    where m r s = p r s `catchError` \e -> 
-                  let MonadIMSOS q = h e
-                  in q r s -- continues with a state as if p not executed
-
-runIMSOS :: r -> s -> MonadIMSOS r s w me e a -> me e (a, s, w)
-runIMSOS r s (MonadIMSOS f) = f r s
+  (module Control.Monad.IMSOS.Layered) where
 
-yieldIMSOS :: Functor (me e) => 
-  r -> s -> ((a, s, w) -> y) -> MonadIMSOS r s w me e a -> me e y
-yieldIMSOS r s toyield m = toyield <$> runIMSOS r s m 
+import Control.Monad.IMSOS.Layered
diff --git a/src/Control/Monad/IMSOS/Algebras.hs b/src/Control/Monad/IMSOS/Algebras.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Algebras.hs
@@ -0,0 +1,41 @@
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+
+
+module Control.Monad.IMSOS.Algebras where
+
+import Data.Comp.Multi.Ops ( (:+:)(..))
+import Data.Comp.Multi ( Term, Alg, HFunctor (..), (:->) )
+import Data.Comp.Multi.Algebra (cata)
+import Data.Kind (Type)
+import Control.Monad.IMSOS.Signatures (Sort, HasSubSig (SubSig))
+
+class HasAlg f e where
+  sem :: Alg f (GetCarrier e)
+
+-- TODO can I get rid of this?
+newtype GetCarrier e i = GetCarrier { getCarrier :: CarrierOf e i i }
+
+class HasCarrier e s where
+  type CarrierOf e s :: Sort -> Type
+
+instance (HasAlg f e, HasAlg g e)
+  => HasAlg (f :+: g) e where
+    sem (Inl f) = sem @f f
+    sem (Inr g) = sem @g g
+
+eval :: forall eval sig sort.
+  (HFunctor sig, HasAlg sig eval)
+  => Term sig sort -> GetCarrier eval sort
+eval = cata (sem @sig @eval)
diff --git a/src/Control/Monad/IMSOS/Fixed.hs b/src/Control/Monad/IMSOS/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Fixed.hs
@@ -0,0 +1,49 @@
+module Control.Monad.IMSOS.Fixed
+  (
+  -- from IMSOS.Monad
+   MonadIMSOS(..), SemMonad, runIMSOS, yieldIMSOS
+  ,Control.Monad.IMSOS.Monad.tell, Control.Monad.IMSOS.Monad.listen, Control.Monad.IMSOS.Monad.censor
+  ,Control.Monad.IMSOS.Monad.local, Control.Monad.IMSOS.Monad.reader, Control.Monad.IMSOS.Monad.ask
+  ,Control.Monad.IMSOS.Monad.get, Control.Monad.IMSOS.Monad.put, Control.Monad.IMSOS.Monad.modify
+  ,fail, MonadError(..)
+  ,guard, Alternative(..)
+  -- from IMSOS.Rules.Relations
+  ,RelID(..), HasRulesErrors(..), SemEntities(..), HasDefaults(..), runSem, Rel
+  , GivesSemanticsTo, SharedSemEntities
+  -- from IMSOS.Signature 
+  ,Signature, HasSubSig(..)
+  --,IsSubSortWitness(..), Share, IsSubSort, HasSubSort, liftTerm, lowerTerm
+  -- from IMSOS.Rules.Step 
+  ,HasTaggedRel(..)
+  ,isValue, toValue, HasValOps(..), IsLangOp, IsValOp, ValOp, TermL, Language(..), Lang, Sort
+  ,StepDefined(..), StepRes(..), steps, stepsOrHalt, stepsOrHaltWhen, StepAvailable, StepsAvailable, StepsTo
+  -- to simplify writing rules
+  ,premise, premiseE, trans, notrans
+  -- from IMSOS.Rules.Trans
+  --,TransAvailable, TransDefined(..), (:~>:)(..), EvaluatesTo(..), EvalTag, Direct, Via
+  -- from ProjectionExt 
+  ,(:*:)(..), (:<~), (:<|), pr, uncons, recons
+  -- from Control.Monad.IMSOS.Algebras 
+  ,HasAlg(..), GetCarrier(..), HasCarrier(..), eval
+  ,Term, inject, project, unTerm
+  ,(:+:), (:<:), caseH
+  -- deriving hfunctors
+  ,HFunctor, makeHFunctor, smartConstructors, derive, K(..)
+  -- related to Show, Ord and Eq
+  ,ShowHF(), makeShowHF
+  ) where
+
+import Control.Monad.IMSOS.Signatures
+import Control.Monad.IMSOS.Monad
+import Control.Monad.IMSOS.Rules.Relations
+import Control.Monad.IMSOS.Algebras
+import Control.Monad.IMSOS.Rules.Step
+import Control.Monad.Error.Class (MonadError(..))
+import Control.Applicative (Alternative(..))
+import Data.Comp.ProjectionExt
+import Data.Comp.Multi.Ops  ((:+:), (:<:), caseH)
+import Data.Comp.Multi.Derive (makeHFunctor, HFunctor, smartConstructors, derive, makeShowHF, ShowHF)
+import Data.Comp.Multi.Sum (inject)
+import Data.Comp.Multi ( project, unTerm )
+import Data.Comp.Multi.Term ( Term )
+import Data.Comp.Multi.HFunctor (K(..))
diff --git a/src/Control/Monad/IMSOS/Layered.hs b/src/Control/Monad/IMSOS/Layered.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Layered.hs
@@ -0,0 +1,56 @@
+module Control.Monad.IMSOS.Layered
+  (
+  -- alternative definitions related to 'sort-polymorphic, layered terms'
+   Term(..), inject, project, unTerm, fixL
+  ,Alg, HasAlg(..), cata, eval
+  ,StepDefined(..), steps, stepsOrHalt, stepsOrHaltWhen, premise, premiseE, trans, notrans
+  ,isValue, toValue, HasValOps(..), StepsAvailable, StepsTo, SharedSemEntities, IsValOp, ValOp, IsLangOp
+  ,HasRulesErrors(..)
+  -- deriving 
+  ,smartConstructors
+
+  -- as in IMSOS.Fixed 
+
+  -- from IMSOS.Monad
+  ,MonadIMSOS(..), SemMonad, runIMSOS, yieldIMSOS
+  ,Control.Monad.IMSOS.Monad.tell, Control.Monad.IMSOS.Monad.listen, Control.Monad.IMSOS.Monad.censor
+  ,Control.Monad.IMSOS.Monad.local, Control.Monad.IMSOS.Monad.reader, Control.Monad.IMSOS.Monad.ask
+  ,Control.Monad.IMSOS.Monad.get, Control.Monad.IMSOS.Monad.put, Control.Monad.IMSOS.Monad.modify
+  ,fail, MonadError(..)
+  ,guard, Alternative(..)
+  -- from IMSOS.Rules.Relations
+  ,RelID(..), SemEntities(..), HasDefaults(..), runSem, Rel
+  , GivesSemanticsTo
+  -- from IMSOS.Signature 
+  ,Signature, HasSubSig(..)
+  --,IsSubSortWitness(..), Share, IsSubSort, HasSubSort, liftTerm, lowerTerm
+  -- from IMSOS.Rules.Step 
+  ,HasTaggedRel(..)
+  ,TermL, Language(..), Lang, Sort
+  -- to simplify writing rules
+  -- from IMSOS.Rules.Trans
+  --,TransAvailable, TransDefined(..), (:~>:)(..), EvaluatesTo(..), EvalTag, Direct, Via
+  -- from ProjectionExt 
+  ,(:*:)(..), (:<~), (:<|), pr, uncons, recons
+  -- from Control.Monad.IMSOS.Algebras 
+  ,(:+:), (:<:), caseH
+  -- deriving hfunctors
+  ,HFunctor, makeHFunctor, derive, K(..)
+  -- related to Show, Ord and Eq
+  ,ShowHF(), makeShowHF
+
+  ) where
+
+import Control.Monad.IMSOS.Monad
+import Control.Monad.IMSOS.LayeredAlgebras
+import Control.Monad.IMSOS.LayeredTerms
+import Control.Monad.IMSOS.LayeredDeriving (smartConstructors)
+import Control.Monad.IMSOS.Rules.LayeredStep
+import Control.Monad.IMSOS.Rules.Relations
+import Control.Monad.Except
+import Control.Applicative
+import Control.Monad.IMSOS.Signatures
+import Data.Comp.ProjectionExt
+import Data.Comp.Multi hiding (Alg, cata, unTerm, project, inject, Term)
+import Data.Comp.Multi.Derive hiding (smartConstructors)
+
diff --git a/src/Control/Monad/IMSOS/LayeredAlgebras.hs b/src/Control/Monad/IMSOS/LayeredAlgebras.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/LayeredAlgebras.hs
@@ -0,0 +1,49 @@
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+
+
+module Control.Monad.IMSOS.LayeredAlgebras where
+
+import Data.Comp.Multi ( HFunctor (..), (:->) )
+import Data.Kind (Type)
+import Control.Monad.IMSOS.Signatures (Sort, Sig)
+import Control.Monad.IMSOS.LayeredTerms (Term (..))
+import qualified Data.Comp.Multi as Multi
+import Data.Comp.Multi.Ops
+
+type Alg l c = Multi.Alg (Sig l) c
+
+class HasAlg f e where
+  sem :: Multi.Alg f (GetCarrier e)
+
+-- TODO can I get rid of this?
+newtype GetCarrier e i = GetCarrier { getCarrier :: CarrierOf e i i }
+
+class HasCarrier e s where
+  type CarrierOf e s :: Sort -> Type
+
+instance (HasAlg f e, HasAlg g e)
+  => HasAlg (f :+: g) e where
+    sem (Inl f) = sem @f f
+    sem (Inr g) = sem @g g
+
+cata :: forall l c. Alg l c -> Term l :-> c
+cata f = go 
+  where go :: forall j. Term l j -> c j
+        go (Term layer) = f (inj (hfmap go layer))
+
+eval :: forall eval l sort. 
+  (HasAlg (Sig l) eval)
+  => Term l sort -> GetCarrier eval sort 
+eval = cata (sem @(Sig l) @eval)
diff --git a/src/Control/Monad/IMSOS/LayeredDeriving.hs b/src/Control/Monad/IMSOS/LayeredDeriving.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/LayeredDeriving.hs
@@ -0,0 +1,212 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.IMSOS.Derive.SmartConstructors
+-- Description :  Derive smart constructors for the indexed LTerm representation.
+--
+-- This is adapted from Data.Comp.Multi.Derive.SmartConstructors in
+-- compdata-0.13.1.  Unlike compdata's version, the generated constructors
+-- build an LTerm layer:
+--
+--   LTerm (inj (Constructor ...))
+--
+-- rather than a compdata Cxt layer:
+--
+--   inject (Constructor ...)
+--
+-- Usage, assuming the corresponding names are in scope:
+--
+--   $(smartConstructorsLTerm ''LTerm ''HasSubSig ''SubSig ''Add)
+--
+-- For
+--
+--   data Add a i where
+--     Add :: a Expr -> a Expr -> Add a Expr
+--
+-- this generates, up to alpha-renaming:
+--
+--   iAdd
+--     :: ( HasSubSig l Expr
+--        , Add :<: SubSig l Expr
+--        )
+--     => LTerm l Expr -> LTerm l Expr -> LTerm l Expr
+--   iAdd x y = LTerm (inj (Add x y))
+--
+-- For non-nullary constructors the signature is deliberately inferred, as in
+-- compdata's original implementation.  This preserves the argument sorts of
+-- GADT constructors (for example, Expr -> Bool operators).
+--------------------------------------------------------------------------------
+module Control.Monad.IMSOS.LayeredDeriving
+  ( smartConstructorsLTerm
+  , smartConstructors
+  ) where
+
+import Control.Arrow ((&&&))
+import Control.Monad (liftM)
+import Data.Comp.Derive.Utils
+  ( DataInfo (..)
+  , abstractConType
+  , abstractNewtypeQ
+  , isEqualP
+  , newNames
+  , tyVarBndrName
+  )
+import Data.Comp.Multi.Ops ((:<:), inj)
+import Language.Haskell.TH hiding (Cxt)
+import Control.Monad.IMSOS.LayeredTerms (Term(..))
+import Control.Monad.IMSOS.Signatures (HasSubSig(..))
+
+smartConstructors = smartConstructorsLTerm ''Term 'Term ''HasSubSig ''SubSig 
+
+-- | Generate smart constructors for one signature functor, targeting a custom
+-- sort-dependent layered term type.
+--
+-- The first three arguments identify the custom API:
+--
+-- * the GADT constructor/type name @LTerm@;
+-- * the class name @HasSubSig@;
+-- * the associated type-family name @SubSig@.
+--
+-- The last argument is the signature functor to inspect, for example @''Add@.
+--
+-- Passing names rather than importing the IMSOS modules makes this derivation
+-- module independent of a particular LTerm implementation.
+
+-- | Generate smart constructors for one signature functor, targeting a custom
+-- sort-dependent LTerm.
+--
+-- Example:
+--
+--   $(smartConstructorsLTerm ''LTerm ''HasSubSig ''SubSig ''Add)
+smartConstructorsLTerm
+  :: Name  -- ^ LTerm type
+  -> Name  -- ^ LTerm constructor
+  -> Name  -- ^ HasSubSig class
+  -> Name  -- ^ SubSig associated type family
+  -> Name  -- ^ signature functor, for example Add
+  -> Q [Dec]
+smartConstructorsLTerm ltermName ltermCons hasSubSigName subSigName fname = do
+  -- `abstractNewtypeQ` already takes a `Q Info`; do not fmap it over
+  -- `reify fname`.
+  Just (DataInfo _cxt tname targs constrs _deriving) <-
+    abstractNewtypeQ (reify fname)
+
+  let iVar = tyVarBndrName (last targs)
+      cons = map (abstractConType &&& resultSort iVar) constrs
+
+  liftM concat $
+    mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
+  where
+    -- GHC reifies a GADT result such as
+    --
+    --   Done :: Done r Commands
+    --
+    -- as a `GadtC` result type.  Older reification styles can instead expose
+    -- the refinement as an equality predicate, so support both forms.
+    resultSort :: Name -> Con -> Maybe Type
+    resultSort iVar (ForallC _ cxt con) =
+      case [ y | Just (x, y) <- map isEqualP cxt, x == VarT iVar ] of
+        tp : _ -> Just tp
+        []     -> resultSort iVar con
+    resultSort _ (GadtC _ _ resultType) = finalArgument resultType
+    resultSort _ (RecGadtC _ _ resultType) = finalArgument resultType
+    resultSort _ _ = Nothing
+
+    finalArgument :: Type -> Maybe Type
+    finalArgument (AppT _ x) = Just x
+    finalArgument (SigT t _) = finalArgument t
+    finalArgument (ParensT t) = finalArgument t
+    finalArgument _ = Nothing
+
+    genSmartConstr
+      :: [Name]
+      -> Name
+      -> ((Name, Int), Maybe Type)
+      -> Q [Dec]
+    genSmartConstr targs' tname ((conName, arity), resultIndex) =
+      genSmartConstr'
+        targs'
+        tname
+        (mkName ('i' : nameBase conName))
+        conName
+        arity
+        resultIndex
+
+    genSmartConstr'
+      :: [Name]
+      -> Name
+      -> Name
+      -> Name
+      -> Int
+      -> Maybe Type
+      -> Q [Dec]
+    genSmartConstr' targs' tname smartName conName arity resultIndex = do
+      varNs <- newNames arity "x"
+
+      let pats = map varP varNs
+          vars = map varE varNs
+          layer = foldl appE (conE conName) vars
+          body =
+            appE (conE ltermCons)
+              (appE (varE 'inj) layer)
+          function =
+            [ funD smartName
+                [ clause pats (normalB body) []
+                ]
+            ]
+          sig
+            | arity == 0 =
+                genNullarySig targs' tname smartName resultIndex
+            | otherwise =
+                []
+
+      sequence (sig ++ function)
+
+    -- For constructors with fields, leave the signature inferred.  This
+    -- preserves their actual GADT argument sorts.  A nullary constructor
+    -- needs an explicit signature to avoid monomorphism-restriction issues.
+    genNullarySig
+      :: [Name]
+      -> Name
+      -> Name
+      -> Maybe Type
+      -> [Q Dec]
+    genNullarySig _ _ _ Nothing = []
+    genNullarySig targs' tname smartName (Just indexType) =
+      [ do
+          lVar <- newName "l"
+
+          let signatureParameters = init (init targs')
+
+              atomicSignature =
+                foldl appT (conT tname) (map varT signatureParameters)
+
+              targetSubSig =
+                conT subSigName
+                  `appT` varT lVar
+                  `appT` pure indexType
+
+              output =
+                conT ltermName
+                  `appT` varT lVar
+                  `appT` pure indexType
+
+              hasSubSigConstraint =
+                conT hasSubSigName
+                  `appT` varT lVar
+                  `appT` pure indexType
+
+              embedsInSubSig =
+                conT ''(:<:)
+                  `appT` atomicSignature
+                  `appT` targetSubSig
+
+              quantified =
+                PlainTV lVar SpecifiedSpec
+                  : map (`PlainTV` SpecifiedSpec) signatureParameters
+
+          sigD smartName $
+            forallT quantified
+              (sequence [hasSubSigConstraint, embedsInSubSig])
+              output
+      ]
diff --git a/src/Control/Monad/IMSOS/LayeredTerms.hs b/src/Control/Monad/IMSOS/LayeredTerms.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/LayeredTerms.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Module defining 'layered terms'.
+-- At each layer, an operator from `SubSig l i` is applied
+module Control.Monad.IMSOS.LayeredTerms where
+import Control.Monad.IMSOS.Signatures (HasSubSig(..), TermL, Sig)
+import Data.Comp.Multi ((:<:), inj, proj, HFunctor (hfmap), inject)
+import qualified Data.Comp.Multi as Multi
+
+data Term l i where 
+  Term ::
+   ( HasSubSig l i ) => 
+      SubSig l i (Term l) i -> Term l i
+
+unTerm :: Term l i -> SubSig l i (Term l) i
+unTerm (Term l) = l
+
+inject :: (f :<: SubSig l i, HasSubSig l i) 
+  => f (Term l) i -> Term l i
+inject = Term . inj
+
+project :: (f :<: SubSig l i) => Term l i -> Maybe (f (Term l) i)
+project = proj . unTerm
+
+fixL :: forall l i. Term l i -> TermL l i
+fixL = go
+  where
+    go :: forall j. Term l j -> TermL l j
+    go (Term layer) =
+      Data.Comp.Multi.inject (hfmap go layer)
+
+-- TODO: instances below might cause significant overhead due to fixing
+instance 
+  (Show (Multi.Term (Sig l) i)) 
+  => Show (Term l i) where 
+  show = show . fixL
+
+instance 
+  (Ord (Multi.Term (Sig l) i))
+  => Ord (Term l i) where 
+    compare l r = compare (fixL l) (fixL r)
+
+instance 
+  (Eq (Multi.Term (Sig l) i))
+  => Eq (Term l i) where 
+    l == r = fixL l == fixL r 
diff --git a/src/Control/Monad/IMSOS/Monad.hs b/src/Control/Monad/IMSOS/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Monad.hs
@@ -0,0 +1,163 @@
+{-# LANGUAGE UndecidableInstances
+  , FlexibleInstances
+  , FlexibleContexts
+  , MultiParamTypeClasses
+  , TypeOperators
+  , LambdaCase
+  , ScopedTypeVariables
+  , TypeApplications
+  , TupleSections
+  , AllowAmbiguousTypes
+#-}
+
+module Control.Monad.IMSOS.Monad
+  (MonadIMSOS(..), runIMSOS, yieldIMSOS
+  ,Control.Monad.IMSOS.Monad.tell, Control.Monad.IMSOS.Monad.listen, Control.Monad.IMSOS.Monad.censor
+  ,Control.Monad.IMSOS.Monad.local, Control.Monad.IMSOS.Monad.reader, Control.Monad.IMSOS.Monad.ask
+  ,Control.Monad.IMSOS.Monad.get, Control.Monad.IMSOS.Monad.put, Control.Monad.IMSOS.Monad.modify
+  ,fail, throwError, catchError
+  ,guard, (<|>)
+  ) where
+
+import Control.Applicative (Alternative(..))
+import Control.Monad.Error.Class
+import Control.Monad.Reader (MonadReader(..))
+import Control.Monad.State  (MonadState(..), modify)
+import Control.Monad.Writer (MonadWriter(..), censor)
+import Control.Monad (ap, join, guard)
+
+import Data.Foldable (toList)
+import Data.Comp.ProjectionExt ((:*:)(..), (:<~), (:<|), pr, uncons, recons, modify)
+
+newtype MonadIMSOS r s w me e fl a = MonadIMSOS {
+    unwrap :: r -> s -> me e (fl (a, s, w))
+  }
+
+instance (Functor (me e), Functor fl) => Functor (MonadIMSOS r s w me e fl) where
+  fmap f (MonadIMSOS m) = MonadIMSOS m'
+    where m' r s = fmap modify' <$> m r s
+           where modify' (a, s', w) = (f a, s', w)
+
+instance (Monad (me e), Monoid w, Traversable fl, Monad fl)
+    => Monad (MonadIMSOS r s w me e fl) where
+  (MonadIMSOS p) >>= m = MonadIMSOS $ \r1 s1  -> do
+     p_res <- p r1 s1
+     let modify' (a, s2, w2) = fmap (,w2) <$> q r1 s2
+          where MonadIMSOS q = m a
+     q_ress <- mapM modify' p_res
+     let mod2 :: ((b, s, w), w) -> (b, s, w)
+         mod2 ((b, s3, w3), w2) = (b, s3, w2 <> w3)
+     return (fmap mod2 (join q_ress))
+
+instance (Monad (me e), Monoid w, Monad fl, Traversable fl)
+    => Applicative (MonadIMSOS r s w me e fl) where
+  pure a = MonadIMSOS m
+    where m _ s = pure (pure (a, s, mempty))
+  (<*>) = ap
+
+instance (Monad (me e), MonadError e (me e), Monoid w
+         ,Alternative fl, Monad fl, Traversable fl)
+    => Alternative (MonadIMSOS r s w me e fl) where
+  empty = MonadIMSOS (\_ _ -> return empty)
+  (MonadIMSOS p) <|> (MonadIMSOS q) = MonadIMSOS m
+    where m r s = tryError (p r s) >>= \case
+                      Left _      -> q r s
+                      Right p_res -> tryError (q r s) >>= \case
+                          Left _ -> return empty
+                          Right q_res -> return (p_res <|> q_res)
+
+instance {-# INCOHERENT #-}
+  (MonadError String (me String), Monad (me String), Monoid w, Traversable fl, Monad fl)
+    => MonadFail (MonadIMSOS r s w me String fl) where
+  fail = throwError
+
+instance (MonadError e (me e), Monad (me e), Monoid w, Monad fl, Traversable fl)
+    => MonadReader r (MonadIMSOS r s w me e fl) where
+  ask = MonadIMSOS m
+    where m r s = pure $ pure (r, s, mempty)
+  local f (MonadIMSOS p) = MonadIMSOS m
+    where m r s = p (f r) s
+
+instance (MonadError e (me e), Monad (me e), Monoid w, Monad fl, Traversable fl)
+    => MonadState s (MonadIMSOS r s w me e fl) where
+  state act = MonadIMSOS m
+    where m _ s = pure $ pure (a, s', mempty)
+           where (a, s') = act s
+
+instance (MonadError e (me e), Monad (me e), Monoid w, Monad fl, Traversable fl)
+    => MonadWriter w (MonadIMSOS r s w me e fl) where
+  tell w = MonadIMSOS m
+    where m _ s = pure $ pure ((), s, w)
+  listen (MonadIMSOS p) = MonadIMSOS m
+    where m r s = p r s >>= \as -> pure (fmap modify' as)
+            where modify' (a, s', w) = ((a, w), s', w)
+  pass (MonadIMSOS p) = MonadIMSOS m
+    where m r s = p r s >>= \as -> pure (fmap modify' as)
+            where modify' ((a,f), s', w) = (a, s', f w)
+
+instance (MonadError e (me e), Monad (me e), Monoid w, Traversable fl, Monad fl)
+    => MonadError e (MonadIMSOS r s w me e fl) where
+  throwError e = MonadIMSOS m
+    where m _ _ = throwError e
+  catchError (MonadIMSOS p) h = MonadIMSOS m
+    where m r s = p r s `catchError` \e ->
+                  let MonadIMSOS q = h e
+                  in q r s -- continues with a state as if p not executed
+
+class Unifies a where
+    unify :: [a] -> a
+
+search :: (Unifies s, Unifies w, Monad (me e), Applicative fl, Foldable fl)
+  => MonadIMSOS r s w me e fl a -> MonadIMSOS r s w me e fl [a]
+search (MonadIMSOS p) = MonadIMSOS $ \r s -> do
+  (as, ss, ws) <- unzip3 . toList <$> p r s
+  return $ pure (as, unify ss, unify ws)
+
+runIMSOS :: (MonadError e (me e))
+  => r -> s -> MonadIMSOS r s w me e fl a -> me e (fl (a, s, w))
+runIMSOS r s (MonadIMSOS f) = f r s
+
+yieldIMSOS :: (Functor (me e), Functor fl, MonadFail (me e), MonadError e (me e)) =>
+  r -> s -> ((a, s, w) -> y) -> MonadIMSOS r s w me e fl a -> me e (fl y)
+yieldIMSOS r s toyield m = fmap toyield <$> runIMSOS r s m
+
+-- ------------------------------
+-- --- Auxiliary entities 
+-- ------------------------------
+
+instance (Semigroup f, Semigroup g)
+  => Semigroup (f :*: g) where
+  (l1 :*: r1) <> (l2 :*: r2) = (l1 <> l2) :*: (r1 <> r2)
+
+instance (Monoid f, Monoid g)
+  => Monoid (f :*: g) where
+    mempty = mempty :*: mempty
+
+tell :: forall f w m. (f :<| w, MonadWriter w m) => f -> m ()
+tell f = Control.Monad.Writer.tell (recons rem_ f)
+  where (_, rem_) = uncons @f (mempty @w)
+
+listen :: forall f w m a. (f :<~ w, MonadWriter w m) => m a -> m (a, f)
+listen m = fmap (pr @f) <$> Control.Monad.Writer.listen m
+
+censor :: forall f w m a. (f :<| w, MonadWriter w m) => (f -> f) -> m a ->  m a
+censor tr = Control.Monad.Writer.censor (Data.Comp.ProjectionExt.modify @f tr)
+
+get :: forall f s m. (f :<~ s, MonadState s m) => m f
+get = pr @f <$> Control.Monad.State.get
+
+put :: forall f s m. (f :<| s, MonadState s m) => f -> m ()
+put f = Control.Monad.IMSOS.Monad.modify (const f)
+
+modify :: forall f s m. (f :<| s, MonadState s m) => (f -> f) -> m ()
+modify tr = Control.Monad.State.modify (Data.Comp.ProjectionExt.modify @f tr)
+
+ask :: forall f r m. (f :<~ r, MonadReader r m) => m f
+ask = pr @f <$> Control.Monad.Reader.ask
+
+reader :: forall f r m a. (f :<| r, MonadReader r m) => (f -> a) -> m a
+reader tr = Control.Monad.Reader.reader tr'
+  where tr' r = tr (pr @f r)
+
+local :: forall f r m a. (f :<| r, MonadReader r m) => (f -> f) -> m a -> m a
+local tr = Control.Monad.Reader.local (Data.Comp.ProjectionExt.modify tr)
diff --git a/src/Control/Monad/IMSOS/Rules/LayeredStep.hs b/src/Control/Monad/IMSOS/Rules/LayeredStep.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Rules/LayeredStep.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Control.Monad.IMSOS.Rules.LayeredStep where
+
+import Data.Comp.Multi.Ops      ((:+:)(..), (:<:))
+
+import Control.Monad.IMSOS.Rules.Relations
+import Data.Comp.ProjectionExt ((:<~), pr)
+import Control.Monad.IMSOS.Monad (listen, get, MonadIMSOS)
+import Control.Monad.IMSOS.Signatures
+import Data.Kind (Type)
+import Control.Monad.Error.Class (MonadError(throwError))
+import Control.Monad.IMSOS.LayeredTerms (Term, unTerm, inject, project)
+import Data.Maybe (isJust)
+import Control.Applicative (Alternative(empty))
+
+-- ───────────────────────────────────────────────
+-- Rules
+-- ───────────────────────────────────────────────
+
+data StepRes (l :: Lang) (e :: Rel) (i :: Type) where
+  -- | the constraint on NoStep ensures only value operators are used
+  -- forcing the use of NoStep and ValOps mechanisms to be consistent
+  NoStep :: (IsValOp e l i f) => f (Term l) i  -> StepRes l e i
+  Step   :: (IsLangOp l i f)  => f (Term l) i  -> StepRes l e i
+
+-- |
+-- StepDefined is the main class to define by users to express I-MSOS rules
+-- instances are identified by `l` (language), `e` (relation) and `f` (operator)
+-- the sort `i` of the operator is implicit
+-- note that in StepDefined the order of the `e` and `l` is purposefully different
+-- compared to the helper functions defined below
+--
+class
+  StepDefined (l :: Lang) (e :: Rel) (f :: Signature) where
+  step :: forall i. f (Term l) i -> SemMonad l e (StepRes l e i)
+
+premiseE :: forall e l i.
+  ( e `GivesSemanticsTo` l
+  , HasRulesErrors (SemError l e)
+  , StepsAvailable e l i
+  )
+  => Term l i -> SemMonad l e (Term l i)
+premiseE t = step @l @e t' >>= \case
+  NoStep _  -> throwError (stepOnValueError (getRelID @e) t')
+  Step t''  -> return (inject t'')
+  where t' = unTerm t
+
+premise :: forall e l i.
+  ( e `GivesSemanticsTo` l
+  , StepsAvailable e l i
+  )
+  => Term l i -> SemMonad l e (Term l i)
+premise t = step @l @e t' >>= \case
+  NoStep _  -> empty 
+  Step t''  -> return (inject t'')
+  where t' = unTerm t
+
+notrans :: forall e l i f. (e `GivesSemanticsTo` l, IsValOp e l i f)
+  => f (Term l) i -> SemMonad l e (StepRes l e i)
+notrans = return . NoStep
+
+trans :: forall e l i f. (e `GivesSemanticsTo` l, IsLangOp l i f)
+  => f (Term l) i -> SemMonad l e (StepRes l e i)
+trans = return . Step
+
+steps :: forall e l f i.
+  ( e `GivesSemanticsTo` l
+  , StepsAvailable e l i
+  , IsValOp e l i f )
+    => Term l i -> SemMonad l e (f (Term l) i)
+steps t | Just v <- toValue @f @e @l t = return v
+        | otherwise                    = premise @e @l t >>= steps @e @l
+
+stepsOrHalt :: forall e h l f i.
+  ( e `GivesSemanticsTo` l
+  , StepsAvailable e l i
+  , IsValOp e l i f
+  , h :<~ SemWriter l e, Monoid h, Eq h
+  )
+    => Term l i -> SemMonad l e (Either (Term l i) (f (Term l) i))
+stepsOrHalt = stepsOrHaltWhen @e @l @f predicate
+  where predicate _ _ w = pr @h w /= mempty
+
+stepsOrHaltWhen :: forall e l f i.
+  ( e `GivesSemanticsTo` l
+  , StepsAvailable e l i
+  , IsValOp e l i f
+  )
+    => (Term l i -> SemState l e -> SemWriter l e -> Bool) -- predicate over an I-MSOS configuration
+          -> Term l i                                  -- consisting of term after step, state and writer values
+          -> SemMonad l e (Either (Term l i) (f (Term l) i))
+stepsOrHaltWhen predicate t
+  | Just v <- toValue @f @e @l t = return $ Right v
+  | otherwise = do
+            (t', w) <- listen @(SemWriter l e) (premise @e @l t)
+            s <- get @(SemState l e)
+            if predicate t' s w then return $ Left t'
+                                else stepsOrHaltWhen @e @l predicate t'
+
+instance
+  ( StepDefined l e f
+  , StepDefined l e g
+  )
+  => StepDefined l e (f :+: g) where
+  step (Inl f) = step @l @e f
+  step (Inr g) = step @l @e g
+
+
+-- | A transition relation identifies which subsignature of a language's
+-- signature identify the value operations of a particular sort 
+-- this will be used to determine termination of computations
+-- according to the relation
+class (ValOps l e i :<: SubSig l i, ValOps l e i :<: Sig l, HasSubSig l i) =>
+  HasValOps (l :: Lang) (e :: Rel) (i :: Sort) where
+    type ValOps l e i :: Signature
+
+-- | ValOp are those terms that are built only from value operators
+-- on the outermost level. 
+-- Useful to build semantic entities. 
+-- Only outermost operator is considered to support thunk-like values
+type ValOp l e i = ValOps l e i (Term l) i
+
+-- | Tests whether a term is a ValOp and converts if possible 
+toValue :: forall f e l i.
+  (HasValOps l e i, f :<: ValOps l e i, f :<: SubSig l i) =>
+    Term l i -> Maybe (f (Term l) i)
+toValue = project @f
+
+-- | Determine whether a term is constructed by a value constructor
+-- of the relevant sort `i` (for a given `e` and `l`)
+isValue :: forall e l i.
+  (HasValOps l e i)
+  => Term l i -> Bool
+isValue = isJust . toValue @(ValOps l e i) @e @l @i
+
+-- ───────────────────────────────────────────────
+-- Error handling
+-- ───────────────────────────────────────────────
+
+class HasRulesErrors e where
+  ruleAssertionError      :: String -> e
+  noApplicableRulesError  :: symb -> f (Term l) i -> e
+  stepOnValueError        :: symb -> f (Term l) i -> e
+
+instance (HasRulesErrors e, MonadError e (me e), Monoid w
+         ,Traversable fl, Monad fl) =>
+  MonadFail (MonadIMSOS r s w me e fl) where
+  fail = throwError . ruleAssertionError @e
+
+instance HasRulesErrors String where
+  ruleAssertionError          = id
+  noApplicableRulesError _ _  = "No rules applicable to term"
+  stepOnValueError _ _        = "attempting to step on value term"
+
+type StepAvailable e l i =
+    ( RelID e
+    , StepDefined l e (SubSig l i))
+
+type StepsAvailable e l i =
+    (StepAvailable e l i
+    ,HasSubSig l i
+    ,HasValOps l e i)
+
+type StepsTo e l i f =
+  (StepsAvailable e l i
+  ,IsValOp e l i f)
+
+type IsValOp e l i f =
+  (f :<: ValOps l e i
+  ,IsLangOp l i f)
+
+type IsLangOp l i f =
+  (f :<: Sig l
+  ,f :<: SubSig l i
+  ,HasSubSig l i)
+
+type SharedSemEntities l (e :: Rel) (e' :: Rel) =
+  ( SemEntities l e
+  , SemEntities l e
+  , SemAlternative l e ~ SemAlternative l e'
+  , SemMonadError l e  ~ SemMonadError l e'
+  , SemError l e       ~ SemError l e'
+  , SemState l e       ~ SemState l e'
+  , SemWriter l e      ~ SemWriter l e'
+  , SemReader l e      ~ SemReader l e'
+  )
diff --git a/src/Control/Monad/IMSOS/Rules/Relations.hs b/src/Control/Monad/IMSOS/Rules/Relations.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Rules/Relations.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Monad.IMSOS.Rules.Relations where
+
+--import Data.Comp.Multi.Term     (Term)
+
+import Control.Monad.IMSOS.Monad (MonadIMSOS, runIMSOS)
+import Control.Monad.IMSOS.Signatures
+import Control.Applicative       (Alternative(..))
+import Control.Monad.Error.Class (MonadError(..))
+import Data.Kind (Type)
+
+-- |
+-- Type class for introducing symbols used to identify transition _relations_
+--
+type Rel = Type
+class RelID e where
+  getRelID :: e
+
+-- | Tags are used to abstract over transition relations, independent of sort
+type Tag = Type
+
+-- | Type family that gives a specific Rel for a given Tag and Sort 
+class HasTaggedRel (tag :: Tag) (s :: Sort) (i :: Sort) where 
+  data TaggedRel tag s i :: Rel 
+
+-- | Transition relations have associated semantic entities
+-- and deal with non-determinism in a certain way (Alternative)
+class ( Alternative (SemAlternative l e)
+      , Monad (SemAlternative l e)
+      , Traversable (SemAlternative l e)
+      , MonadError (SemError l e) (SemMonadError l e (SemError l e))
+      , Monoid (SemWriter l e)
+      , HasDefaults l e
+      ) => SemEntities (l :: Lang) (e :: Rel) where
+  type SemReader       l e :: Type
+  type SemState        l e :: Type
+  type SemWriter       l e :: Type
+  type SemAlternative  l e :: Type -> Type
+  type SemError        l e :: Type
+  type SemMonadError   l e :: Type -> Type -> Type
+
+type SemMonad l e =
+      MonadIMSOS (SemReader l e) (SemState l e) (SemWriter l e)
+                 (SemMonadError l e) (SemError l e) (SemAlternative l e)
+
+type GivesSemanticsTo e l = (SemEntities l e, Language l, RelID e)
+
+class Monoid (SemWriter l e) => HasDefaults l e where
+  defaultReader :: SemReader l e
+  defaultState  :: SemState l e
+
+runSem :: forall e l a.
+  ( HasDefaults l e
+  , SemEntities l e
+  ) => SemMonad l e a -> SemMonadError l e (SemError l e) (SemAlternative l e (a, SemState l e, SemWriter l e))
+runSem = runIMSOS (defaultReader @l @e) (defaultState @l @e)
diff --git a/src/Control/Monad/IMSOS/Rules/Step.hs b/src/Control/Monad/IMSOS/Rules/Step.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Rules/Step.hs
@@ -0,0 +1,199 @@
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Control.Monad.IMSOS.Rules.Step where
+
+import Data.Comp.Multi.Ops      ((:+:)(..), (:<:))
+
+import Control.Monad.IMSOS.Rules.Relations
+import Data.Comp.ProjectionExt ((:<~), pr)
+import Control.Monad.IMSOS.Monad (listen, get, MonadIMSOS)
+import Control.Monad.IMSOS.Signatures
+import Data.Kind (Type)
+import Data.Comp.Multi.Term (Term)
+import Control.Monad.Error.Class (MonadError(throwError))
+import Data.Comp.Multi.Sum (inject)
+import Data.Comp.Multi ( unTerm, project )
+import Data.Maybe (isJust)
+import Control.Applicative (Alternative(empty))
+
+-- ───────────────────────────────────────────────
+-- Rules
+-- ───────────────────────────────────────────────
+
+data StepRes (l :: Lang) (e :: Sort -> Rel) (i :: Type) where
+  -- | the constraint on NoStep ensures only value operators are used
+  -- forcing the use of NoStep and ValOps mechanisms to be consistent
+  NoStep :: (IsValOp e l i f) => f (Term (Sig l)) i  -> StepRes l e i
+  Step   :: (IsLangOp l i f)  => f (Term (Sig l)) i  -> StepRes l e i
+
+-- |
+-- StepDefined is the main class to define by users to express I-MSOS rules
+-- instances are identified by `l` (language), `e` (relation) and `f` (operator)
+-- the sort `i` of the operator is implicit
+-- note that in StepDefined the order of the `e` and `l` is purposefully different
+-- compared to the helper functions defined below
+--
+class
+  StepDefined (l :: Lang) (t :: Type) (f :: Signature) where
+  step :: forall i. f (TermL l) i -> SemMonad l (TaggedRel t i i) (StepRes l (TaggedRel t i) i)
+
+premiseE :: forall t l i.
+  ( StepAvailable t l i
+  , HasRulesErrors (SemError l (TaggedRel t i i))
+  , TaggedRel t i i `GivesSemanticsTo` l
+  )
+  => TermL l i -> SemMonad l (TaggedRel t i i) (TermL l i)
+premiseE t = step @l @t t' >>= \case
+  NoStep _  -> throwError (stepOnValueError (getRelID @(TaggedRel t i i)) t')
+  Step t''  -> return (inject t'')
+  where t' = unTerm t
+
+premise :: forall t l i.
+  ( StepAvailable t l i
+  , TaggedRel t i i `GivesSemanticsTo` l
+  )
+  => TermL l i -> SemMonad l (TaggedRel t i i) (TermL l i)
+premise t = step @l @t t' >>= \case
+  NoStep _  -> empty
+  Step t''  -> return (inject t'')
+  where t' = unTerm t
+
+notrans :: forall e l i f. (e i `GivesSemanticsTo` l, IsValOp e l i f)
+  => f (TermL l) i -> SemMonad l (e i) (StepRes l e i)
+notrans = return . NoStep
+
+trans :: forall e l i f. (e i `GivesSemanticsTo` l, IsLangOp l i f)
+  => f (TermL l) i -> SemMonad l (e i) (StepRes l e i)
+trans = return . Step
+
+steps :: forall (t :: Tag) l f i.
+  ( TaggedRel t i i `GivesSemanticsTo` l
+  , StepsAvailable t l i
+  , IsValOp (TaggedRel t i) l i f )
+    => TermL l i -> SemMonad l (TaggedRel t i i) (f (TermL l) i)
+steps t | Just v <- toValue @f @t @l t = return v
+        | otherwise                    = premise @t @l t >>= steps @t @l
+
+stepsOrHalt :: forall (t :: Tag) h l f i.
+  ( TaggedRel t i i `GivesSemanticsTo` l
+  , StepsAvailable t l i
+  , IsValOp (TaggedRel t i) l i f
+  , h :<~ SemWriter l (TaggedRel t i i), Monoid h, Eq h
+  )
+    => TermL l i -> SemMonad l (TaggedRel t i i) (Either (TermL l i) (f (TermL l) i))
+stepsOrHalt = stepsOrHaltWhen @t @l @f predicate
+  where predicate _ _ w = pr @h w /= mempty
+
+stepsOrHaltWhen :: forall (t :: Tag) l f i.
+  ( TaggedRel t i i `GivesSemanticsTo` l
+  , StepsAvailable t l i
+  , IsValOp (TaggedRel t i) l i f
+  )
+    => (TermL l i -> SemState l (TaggedRel t i i) -> SemWriter l (TaggedRel t i i) -> Bool) -- predicate over an I-MSOS configuration
+          -> TermL l i                                  -- consisting of term after step, state and writer values
+          -> SemMonad l (TaggedRel t i i) (Either (TermL l i) (f (TermL l) i))
+stepsOrHaltWhen predicate t
+  | Just v <- toValue @f @t @l t = return $ Right v
+  | otherwise = do
+            (t', w) <- listen @(SemWriter l (TaggedRel t i i)) (premise @t @l t)
+            s <- get @(SemState l (TaggedRel t i i))
+            if predicate t' s w then return $ Left t'
+                                else stepsOrHaltWhen @t @l predicate t'
+
+instance
+  ( StepDefined l e f
+  , StepDefined l e g
+  )
+  => StepDefined l e (f :+: g) where
+  step (Inl f) = step @l @e f
+  step (Inr g) = step @l @e g
+
+
+-- | A transition relation identifies which subsignature of a language's
+-- signature identify the value operations of a particular sort 
+-- this will be used to determine termination of computations
+-- according to the relation
+class (ValOps l e i :<: Sig l) =>
+  HasValOps (l :: Lang) (e :: Sort -> Rel) (i :: Sort) where
+    type ValOps l e i :: Signature
+
+-- | ValOp are those terms that are built only from value operators
+-- on the outermost level. 
+-- Useful to build semantic entities. 
+-- Only outermost operator is considered to support thunk-like values
+type ValOp l e i = ValOps l e i (TermL l) i
+
+-- | Tests whether a term is a ValOp and converts if possible 
+toValue :: forall f t l i.
+  (HasValOps l (TaggedRel t i) i, f :<: ValOps l (TaggedRel t i) i, f :<: Sig l) =>
+    TermL l i -> Maybe (f (TermL l) i)
+toValue = project @f
+
+-- | Determine whether a term is constructed by a value constructor
+-- of the relevant sort `i` (for a given `e` and `l`)
+isValue :: forall t l i.
+  (HasValOps l (TaggedRel t i) i)
+  => TermL l i -> Bool
+isValue = isJust . toValue @(ValOps l (TaggedRel t i) i) @t @l @i
+
+-- ───────────────────────────────────────────────
+-- Error handling
+-- ───────────────────────────────────────────────
+
+class HasRulesErrors e where
+  ruleAssertionError      :: String -> e
+  noApplicableRulesError  :: symb -> f (Term g) i -> e
+  stepOnValueError        :: symb -> f (Term g) i -> e
+
+instance (HasRulesErrors e, MonadError e (me e), Monoid w
+         ,Traversable fl, Monad fl) =>
+  MonadFail (MonadIMSOS r s w me e fl) where
+  fail = throwError . ruleAssertionError @e
+
+instance HasRulesErrors String where
+  ruleAssertionError          = id
+  noApplicableRulesError _ _  = "No rules applicable to term"
+  stepOnValueError _ _        = "attempting to step on value term"
+
+type StepAvailable t l i =
+    ( RelID (TaggedRel t i i)
+    , StepDefined l t (Sig l))
+
+type StepsAvailable t l i =
+    (StepAvailable t l i
+    ,HasValOps l (TaggedRel t i) i)
+
+type StepsTo t l i f =
+  (StepsAvailable t l i
+  ,IsValOp (TaggedRel t i) l i f)
+
+type IsValOp e l i f =
+  (f :<: ValOps l e i
+  ,IsLangOp l i f)
+
+type IsLangOp l i f =
+  (f :<: Sig l)
+
+type SharedSemEntities l (t :: Tag) i j =
+  ( SemEntities l (TaggedRel t i i)
+  , SemEntities l (TaggedRel t j j)
+  , SemAlternative l (TaggedRel t i i) ~ SemAlternative l (TaggedRel t j j)
+  , SemMonadError l (TaggedRel t i i)  ~ SemMonadError l (TaggedRel t j j)
+  , SemError l (TaggedRel t i i)       ~ SemError l (TaggedRel t j j)
+  , SemState l (TaggedRel t i i)       ~ SemState l (TaggedRel t j j)
+  , SemWriter l (TaggedRel t i i)      ~ SemWriter l (TaggedRel t j j)
+  , SemReader l (TaggedRel t i i)      ~ SemReader l (TaggedRel t j j)
+  )
diff --git a/src/Control/Monad/IMSOS/Signatures.hs b/src/Control/Monad/IMSOS/Signatures.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/IMSOS/Signatures.hs
@@ -0,0 +1,65 @@
+
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Control.Monad.IMSOS.Signatures where
+
+import Data.Kind (Type)
+import Data.Comp.Multi.Term (Term)
+import Data.Comp.Multi ( (:<:), (:+:), HFunctor )
+import Data.Comp.Multi.Sum (project)
+
+-- | A 'language' l captures the abstract syntax of a language 
+-- by specifying a signature 
+
+type Lang = Type
+
+-- | A language consists of several sorts 
+type Sort = Type
+
+-- | The kind of signatures according to compdata (multi) library
+type Signature = (Sort -> Type) -> Sort -> Type
+
+class Language (l :: Lang) where
+    type Sorts l :: [Sort]
+
+-- | Subsignatures enable defining transition relations specific to 
+-- parts of the signature, as represented by a sort 
+class (Language l, HFunctor (SubSig l i), SubSig l i :<: Sig l) =>
+  HasSubSig (l :: Lang) (i :: Sort) where
+    type SubSig l i :: Signature
+
+-- | Fold a type-level list of signatures into a nested coproduct
+type family SumSigs (fs :: [Signature]) :: Signature where
+    SumSigs '[f]      = f
+    SumSigs (f ': fs) = f :+: SumSigs fs
+
+type family MapSubSig (l :: Lang) (sorts :: [Sort]) :: [Signature] where
+    MapSubSig l '[]       = '[]
+    MapSubSig l (i ': is) = SubSig l i ': MapSubSig l is
+
+-- | The signature of a language is automatically derived from the sorts
+type Sig l = SumSigs (MapSubSig l (Sorts l))
+
+-- | TermL is a convenience for referring to the type of terms of a language
+type TermL l = Term (Sig l)
+
+-- | Custom version of unTerm that ensures top-level operator is in relevant SubSig
+-- Its usage is unsafe only in the case when an operator is of sort `i`
+-- but is included in the signature for some other sort `j`
+-- and either there is no semantics associated with the language or
+-- there happens to be a semantics (instance of StepDefined) that yields
+-- a result of sort j
+-- unTerm :: forall l i. (SubSig l i :<: Sig l) => TermL l i -> SubSig l i (TermL l) i
+-- unTerm t | Just t' <- project @(SubSig l i) t = t'
+--          | otherwise = error "unTerm assertion failed: (Term (Sig l) i) not constructed by (SubSig l i)"
diff --git a/src/Data/Comp/ProjectionExt.hs b/src/Data/Comp/ProjectionExt.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/ProjectionExt.hs
@@ -0,0 +1,374 @@
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE KindSignatures         #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE TypeApplications       #-}
+
+-- ---------------------------------------------------------------------------
+-- Module      :  Data.Comp.ProjectionExt
+--
+-- Extends Data.Comp.Projection with:
+--
+--   1. Support for (:*:) products alongside tuples (,).
+--      Because Elem is a closed type family in the original module,
+--      we re-implement it here with the extra cases, and re-derive
+--      everything on top of it.  The original (:<) / pr are NOT
+--      re-exported; use (:<~) and pr~ from this module instead.
+--
+--   2. uncons — projects a component AND returns the remainder
+--      of the product with that component removed, as an abstract type.
+--
+--   3. recons — rebuilds the original product from a remainder
+--      and a (possibly modified) projected component.
+--
+-- Supported product constructors:
+--   (,)   — Haskell built-in pair
+--   (:*:) — GHC.Generics / Data.Functor.Product style functor product
+--           (used at kind Type by applying both sides to a common index)
+--
+-- Adding further product constructors (e.g. Data.Strict.Pair) requires
+-- one new equation in Elem, one in Remainder2, and two new instances
+-- each in Proj, ProjR, and Reconstruct.
+-- ---------------------------------------------------------------------------
+
+module Data.Comp.ProjectionExt
+  ( -- * Constraint and plain projection (replaces :< / pr)
+    (:<~), (:<|), (:*:)(..)
+  , pr
+    -- * Projection with remainder
+  , RemainderOf
+  , uncons
+  , recons
+  , modify
+    -- * Re-exported position machinery (for advanced use)
+  , Elem
+  ) where
+
+import Data.Comp.SubsumeCommon
+import Data.Kind    (Type)
+
+data a :*: b = a :*: b
+infixr 6 :*:
+
+-- ---------------------------------------------------------------------------
+-- 1.  Elem — closed type family recognising BOTH (,) and (:*:)
+--
+-- The structure exactly mirrors the original Elem, with every
+-- tuple case duplicated for (:*:).
+-- ---------------------------------------------------------------------------
+
+type family Elem (f :: Type) (g :: Type) :: Emb where
+
+  -- Base: exact match
+  Elem f f = 'Found 'Here
+
+  -- LHS is a tuple-pair: look for each component independently in g
+  Elem (f1, f2) g = Sum' (Elem f1 g) (Elem f2 g)
+
+  -- LHS is a (:*:)-pair: same idea
+  Elem (f1 :*: f2) g = Sum' (Elem f1 g) (Elem f2 g)
+
+  -- RHS is a tuple-pair: choose which side f lives in
+  Elem f (g1, g2) = Choose (Elem f g1) (Elem f g2)
+
+  -- RHS is a (:*:)-pair: same idea
+  Elem f (g1 :*: g2) = Choose (Elem f g1) (Elem f g2)
+
+  -- No match
+  Elem f g = 'NotFound
+
+-- ---------------------------------------------------------------------------
+-- 2.  Proj — plain projection, mirrors the original Proj class
+--     but dispatches on both (,) and (:*:) at the value level.
+-- ---------------------------------------------------------------------------
+
+class Proj (e :: Emb) (p :: Type) (q :: Type) where
+  proj' :: Proxy e -> q -> p
+
+-- Base: p is q
+instance Proj ('Found 'Here) f f where
+  proj' _ x = x
+
+-- p is in the left branch of a tuple
+instance Proj ('Found pos) f g
+    => Proj ('Found ('Le pos)) f (g, g') where
+  proj' _ (l, _) = proj' (P :: Proxy ('Found pos)) l
+
+-- p is in the right branch of a tuple
+instance Proj ('Found pos) f g
+    => Proj ('Found ('Ri pos)) f (g', g) where
+  proj' _ (_, r) = proj' (P :: Proxy ('Found pos)) r
+
+-- p is in the left branch of a (:*:)
+instance Proj ('Found pos) f g
+    => Proj ('Found ('Le pos)) f (g :*: g') where
+  proj' _ (l :*: _) = proj' (P :: Proxy ('Found pos)) l
+
+-- p is in the right branch of a (:*:)
+instance Proj ('Found pos) f g
+    => Proj ('Found ('Ri pos)) f (g' :*: g) where
+  proj' _ (_ :*: r) = proj' (P :: Proxy ('Found pos)) r
+
+-- p is a pair (f1, f2) scattered across q — tuple variant
+instance ( Proj ('Found p1) f1 g
+         , Proj ('Found p2) f2 g
+         )
+    => Proj ('Found ('Sum p1 p2)) (f1, f2) g where
+  proj' _ x =
+    ( proj' (P :: Proxy ('Found p1)) x
+    , proj' (P :: Proxy ('Found p2)) x
+    )
+
+-- p is a pair (f1 :*: f2) scattered across q — (:*:) variant
+instance ( Proj ('Found p1) f1 g
+         , Proj ('Found p2) f2 g
+         )
+    => Proj ('Found ('Sum p1 p2)) (f1 :*: f2) g where
+  proj' _ x =
+    proj' (P :: Proxy ('Found p1)) x
+    :*:
+    proj' (P :: Proxy ('Found p2)) x
+
+-- ---------------------------------------------------------------------------
+-- 3.  Public constraint and projection function (replaces :< / pr)
+-- ---------------------------------------------------------------------------
+
+-- | @p :\<~ q@ means @p@ is a uniquely-occurring component of @q@,
+-- where @q@ may be built from either @(,)@ or @(':*:')@ products.
+type p :<~ q = Proj (ComprEmb (Elem p q)) p q
+
+-- | Project component @p@ out of product @q@.
+--   Generalises 'Data.Comp.Projection.pr' to also handle @(':*:')@.
+pr :: forall p q. (p :<~ q) => q -> p
+pr = proj' (P :: Proxy (ComprEmb (Elem p q)))
+
+-- ---------------------------------------------------------------------------
+-- 4.  Remainder type family
+--
+-- Remainder e p q  is the type of q with the component at position e
+-- removed.  The result type depends on which product constructor was
+-- used at each node, so we need cases for both (,) and (:*:).
+-- ---------------------------------------------------------------------------
+
+type family Remainder (e :: Emb) (p :: Type) (q :: Type) :: Type where
+
+  -- Base: p was the whole product
+  Remainder ('Found 'Here) p p = ()
+
+  -- p was in the left branch of a tuple
+  Remainder ('Found ('Le pos)) p (g, g') =
+      (Remainder ('Found pos) p g, g')
+
+  -- p was in the right branch of a tuple
+  Remainder ('Found ('Ri pos)) p (g', g) =
+      (g', Remainder ('Found pos) p g)
+
+  -- p was in the left branch of a (:*:)
+  Remainder ('Found ('Le pos)) p (g :*: g') =
+      Remainder ('Found pos) p g :*: g'
+
+  -- p was in the right branch of a (:*:)
+  Remainder ('Found ('Ri pos)) p (g' :*: g) =
+      g' :*: Remainder ('Found pos) p g
+
+  -- p is a tuple-pair (f1, f2) scattered through q
+  Remainder ('Found ('Sum pos1 pos2)) (f1, f2) q =
+      Remainder ('Found pos2) f2 (Remainder ('Found pos1) f1 q)
+
+  -- p is a (:*:)-pair (f1 :*: f2) scattered through q
+  Remainder ('Found ('Sum pos1 pos2)) (f1 :*: f2) q =
+      Remainder ('Found pos2) f2 (Remainder ('Found pos1) f1 q)
+
+-- Convenience alias hiding the position evidence.
+type RemainderOf p q = Remainder (ComprEmb (Elem p q)) p q
+
+-- ---------------------------------------------------------------------------
+-- 5.  ProjR — projection that also returns the remainder
+-- ---------------------------------------------------------------------------
+
+class ProjR (e :: Emb) (p :: Type) (q :: Type) where
+  prR' :: Proxy e -> q -> (p, Remainder e p q)
+
+-- Base
+instance ProjR ('Found 'Here) f f where
+  prR' _ x = (x, ())
+
+-- Left branch of a tuple
+instance ProjR ('Found pos) f g
+    => ProjR ('Found ('Le pos)) f (g, g') where
+  prR' _ (l, r) =
+    let (p, remL) = prR' (P :: Proxy ('Found pos)) l
+    in  (p, (remL, r))
+
+-- Right branch of a tuple
+instance ProjR ('Found pos) f g
+    => ProjR ('Found ('Ri pos)) f (g', g) where
+  prR' _ (l, r) =
+    let (p, remR) = prR' (P :: Proxy ('Found pos)) r
+    in  (p, (l, remR))
+
+-- Left branch of a (:*:)
+instance ProjR ('Found pos) f g
+    => ProjR ('Found ('Le pos)) f (g :*: g') where
+  prR' _ (l :*: r) =
+    let (p, remL) = prR' (P :: Proxy ('Found pos)) l
+    in  (p, remL :*: r)
+
+-- Right branch of a (:*:)
+instance ProjR ('Found pos) f g
+    => ProjR ('Found ('Ri pos)) f (g' :*: g) where
+  prR' _ (l :*: r) =
+    let (p, remR) = prR' (P :: Proxy ('Found pos)) r
+    in  (p, l :*: remR)
+
+-- Scattered tuple-pair (f1, f2)
+instance ( ProjR ('Found pos1) f1 q
+         , ProjR ('Found pos2) f2 (Remainder ('Found pos1) f1 q)
+         )
+    => ProjR ('Found ('Sum pos1 pos2)) (f1, f2) q where
+  prR' _ x =
+    let (f1, rem1) = prR' (P :: Proxy ('Found pos1)) x
+        (f2, rem2) = prR' (P :: Proxy ('Found pos2)) rem1
+    in  ((f1, f2), rem2)
+
+-- Scattered (:*:)-pair (f1 :*: f2)
+instance ( ProjR ('Found pos1) f1 q
+         , ProjR ('Found pos2) f2 (Remainder ('Found pos1) f1 q)
+         )
+    => ProjR ('Found ('Sum pos1 pos2)) (f1 :*: f2) q where
+  prR' _ x =
+    let (f1, rem1) = prR' (P :: Proxy ('Found pos1)) x
+        (f2, rem2) = prR' (P :: Proxy ('Found pos2)) rem1
+    in  (f1 :*: f2, rem2)
+
+-- ---------------------------------------------------------------------------
+-- 6.  Reconstruct — inverse of ProjR
+-- ---------------------------------------------------------------------------
+
+class Reconstruct (e :: Emb) (p :: Type) (q :: Type) where
+  recons' :: Proxy e -> Remainder e p q -> p -> q
+
+-- Base
+instance Reconstruct ('Found 'Here) f f where
+  recons' _ () x = x
+
+-- Left branch of a tuple
+instance Reconstruct ('Found pos) f g
+    => Reconstruct ('Found ('Le pos)) f (g, g') where
+  recons' _ (remL, r) p =
+    (recons' (P :: Proxy ('Found pos)) remL p, r)
+
+-- Right branch of a tuple
+instance Reconstruct ('Found pos) f g
+    => Reconstruct ('Found ('Ri pos)) f (g', g) where
+  recons' _ (l, remR) p =
+    (l, recons' (P :: Proxy ('Found pos)) remR p)
+
+-- Left branch of a (:*:)
+instance Reconstruct ('Found pos) f g
+    => Reconstruct ('Found ('Le pos)) f (g :*: g') where
+  recons' _ (remL :*: r) p =
+    recons' (P :: Proxy ('Found pos)) remL p :*: r
+
+-- Right branch of a (:*:)
+instance Reconstruct ('Found pos) f g
+    => Reconstruct ('Found ('Ri pos)) f (g' :*: g) where
+  recons' _ (l :*: remR) p =
+    l :*: recons' (P :: Proxy ('Found pos)) remR p
+
+-- Scattered tuple-pair (f1, f2)
+instance ( Reconstruct ('Found pos2) f2 (Remainder ('Found pos1) f1 q)
+         , Reconstruct ('Found pos1) f1 q
+         )
+    => Reconstruct ('Found ('Sum pos1 pos2)) (f1, f2) q where
+  recons' _ rem2 (f1, f2) =
+    let rem1 = recons' (P :: Proxy ('Found pos2)) rem2 f2
+    in  recons' (P :: Proxy ('Found pos1)) rem1 f1
+
+-- Scattered (:*:)-pair (f1 :*: f2)
+instance ( Reconstruct ('Found pos2) f2 (Remainder ('Found pos1) f1 q)
+         , Reconstruct ('Found pos1) f1 q
+         )
+    => Reconstruct ('Found ('Sum pos1 pos2)) (f1 :*: f2) q where
+  recons' _ rem2 (f1 :*: f2) =
+    let rem1 = recons' (P :: Proxy ('Found pos2)) rem2 f2
+    in  recons' (P :: Proxy ('Found pos1)) rem1 f1
+
+-- ---------------------------------------------------------------------------
+-- 7.  Public API
+-- ---------------------------------------------------------------------------
+
+-- | Bundles all constraints needed for 'uncons' and 'recons'.
+type p :<| q =
+  ( ProjR       (ComprEmb (Elem p q)) p q
+  , Reconstruct (ComprEmb (Elem p q)) p q
+  , p :<~ q
+  )
+
+-- | Project component @p@ from product @q@, also returning the remainder.
+--
+-- The remainder type is abstract — it should only be passed to 'recons'.
+--
+-- Law:  @uncurry (flip recons) (uncons x) == x@
+--
+-- Examples:
+--   uncons @Int  (True, (42 :: Int, 'x'))  == (42,  (True, 'x'))
+--   uncons @Bool (True :*: (42 :: Int))     == (True, () :*: 42)
+uncons
+  :: forall p q. (p :<| q)
+  => q
+  -> (p, RemainderOf p q)
+uncons = prR' (P :: Proxy (ComprEmb (Elem p q)))
+
+-- | Reconstruct the original product from a remainder and a
+-- (possibly modified) projected component.
+--
+-- Examples:
+--   let (n, rem) = uncons @Int (True, (42 :: Int, 'x'))
+--   recons rem (n + 1)                    == (True, (43, 'x'))
+--
+--   let (b, rem) = uncons @Bool (True :*: (42 :: Int))
+--   recons rem (not b)                    == (False :*: 42)
+recons
+  :: forall p q. (p :<| q)
+  => RemainderOf p q
+  -> p
+  -> q
+recons = recons' (P :: Proxy (ComprEmb (Elem p q)))
+
+-- | Deconstruct and reconstruct a product, modifying a field
+-- determined by the type of the given transformation function.
+modify :: forall p q. (p :<| q)
+  => (p -> p) -> q -> q
+modify f q = recons rem (f p)
+  where (p, rem) = uncons @p q
+
+-- ---------------------------------------------------------------------------
+-- 8.  Sanity checks (unexported; remove before packaging)
+-- ---------------------------------------------------------------------------
+
+-- Tuple-only product
+_t1 :: (Bool, (Int, Char))
+_t1 = let (n, rem) = uncons @Int (True, (42 :: Int, 'x'))
+      in  recons rem (n + 1)           -- (True, (43, 'x'))
+
+-- (:*:)-only product
+_t2 :: Bool :*: Int
+_t2 = let (b, rem) = uncons @Bool (True :*: (42 :: Int))
+      in  recons rem (not b)           -- (False :*: 42)
+
+-- Mixed: tuple on the outside, (:*:) on the inside
+_t3 :: (Bool :*: Int, Char)
+_t3 = let (n, rem) = uncons @Int ((True :*: (42 :: Int)), 'x')
+      in  recons rem (n + 1)           -- ((True :*: 43), 'x')
+
+-- Mixed: (:*:) on the outside, tuple on the inside
+_t4 :: Bool :*: Int :*: Char
+_t4 = let (b, rem) = uncons @Bool (True :*: (42 :: Int) :*: 'x')
+      in  recons rem (not b)           -- ((False, 42) :*: 'x')
diff --git a/src/Data/Comp/SubsumeCommon.hs b/src/Data/Comp/SubsumeCommon.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/SubsumeCommon.hs
@@ -0,0 +1,168 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds            #-}
+
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.SubsumeCommon
+-- Copyright   :  (c) 2014 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Shared parts of the implementation of signature subsumption for
+-- both the base and the multi library.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.SubsumeCommon
+    ( ComprEmb
+    , Pos (..)
+    , Emb (..)
+    , Choose
+    , Sum'
+    , Proxy (..)
+    ) where
+
+-- | This type is used in its promoted form only. It represents
+-- pointers from the left-hand side of a subsumption to the right-hand
+-- side.
+data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos
+
+-- | This type is used in its promoted form only. It represents
+-- possible results for checking for subsumptions. 'Found' indicates a
+-- subsumption was found; 'NotFound' indicates no such subsumption was
+-- found. 'Ambiguous' indicates that there are duplicates on the left-
+-- or the right-hand side.
+data Emb = Found Pos | NotFound | Ambiguous
+
+data Proxy a = P
+
+
+type family Choose (e1 :: Emb) (r :: Emb) :: Emb where
+    Choose (Found x) (Found y) = Ambiguous
+    Choose Ambiguous y = Ambiguous
+    Choose x Ambiguous = Ambiguous
+    Choose (Found x) y = Found (Le x)
+    Choose x (Found y) = Found (Ri y)
+    Choose x y = NotFound
+
+
+type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
+    Sum' (Found x) (Found y) = Found (Sum x y)
+    Sum' Ambiguous y = Ambiguous
+    Sum' x Ambiguous = Ambiguous
+    Sum' NotFound y = NotFound
+    Sum' x NotFound = NotFound
+
+
+-- | This type family takes a position type and compresses it. That
+-- means it replaces each nested occurrence of
+--
+-- @
+--   Sum (prefix (Le Here)) (prefix (Ri Here))@
+-- @
+---
+-- with
+--
+-- @
+--   prefix Here@
+-- @
+--
+-- where @prefix@ is some composition of @Le@ and @Ri@. The rational
+-- behind this type family is that it provides a more compact proof
+-- term of a subsumption, and thus yields more efficient
+-- implementations of 'inj' and 'prj'.
+
+type family ComprPos (p :: Pos) :: Pos where
+    ComprPos Here = Here
+    ComprPos (Le p) = Le (ComprPos p)
+    ComprPos (Ri p) = Ri (ComprPos p)
+    ComprPos (Sum l r) = CombineRec (ComprPos l) (ComprPos r)
+
+
+-- | Helper type family for 'ComprPos'. Note that we could have
+-- defined this as a type synonym. But if we do that, performance
+-- becomes abysmal. I presume that the reason for this huge impact on
+-- performance lies in the fact that right-hand side of the defining
+-- equation duplicates the two arguments @l@ and @r@.
+type family CombineRec l r where
+    CombineRec l r = CombineMaybe (Sum l r) (Combine l r)
+
+-- | Helper type family for 'ComprPos'.
+type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where
+    CombineMaybe p (Just p') = p'
+    CombineMaybe p p'        = p
+
+
+-- | Helper type family for 'ComprPos'.
+type family Combine (l :: Pos) (r :: Pos) :: Maybe Pos where
+    Combine (Le l) (Le r) = Le' (Combine l r)
+    Combine (Ri l) (Ri r) = Ri' (Combine l r)
+    Combine (Le Here) (Ri Here) = Just Here
+    Combine l r = Nothing
+
+-- | 'Ri' lifted to 'Maybe'.
+type family Ri' (p :: Maybe Pos) :: Maybe Pos where
+    Ri' Nothing = Nothing
+    Ri' (Just p) = Just (Ri p)
+
+-- | 'Le' lifted to 'Maybe'.
+type family Le' (p :: Maybe Pos) :: Maybe Pos where
+    Le' Nothing = Nothing
+    Le' (Just p) = Just (Le p)
+
+
+-- | If the argument is not 'Found', this type family is the
+-- identity. Otherwise, the argument is of the form @Found p@, and
+-- this type family does two things: (1) it checks whether @p@ the
+-- contains duplicates; and (2) it compresses @p@ using 'ComprPos'. If
+-- (1) finds no duplicates, @Found (ComprPos p)@ is returned;
+-- otherwise @Ambiguous@ is returned.
+--
+-- For (1) it is assumed that @p@ does not contain 'Sum' nested
+-- underneath a 'Le' or 'Ri' (i.e. only at the root or underneath a
+-- 'Sum'). We will refer to such positions below as /atomic position/.
+-- Positions not containing 'Sum' are called /simple positions/.
+type family ComprEmb (e :: Emb) :: Emb where
+    ComprEmb (Found p) = Check (Dupl p) (ComprPos p)
+    ComprEmb e = e
+
+-- | Helper type family for 'ComprEmb'.
+type family Check (b :: Bool) (p :: Pos) where
+    Check False p = Found p
+    Check True  p = Ambiguous
+
+-- | This type family turns a list of /atomic position/ into a list of
+-- /simple positions/ by recursively splitting each position of the
+-- form @Sum p1 p2@ into @p1@ and @p2@.
+type family ToList (s :: [Pos]) :: [Pos] where
+    ToList (Sum p1 p2 ': s) = ToList (p1 ': p2 ': s)
+    ToList (p ': s) = p ': ToList s
+    ToList '[] = '[]
+
+-- | This type checks whether the argument (atomic) position has
+-- duplicates.
+type Dupl s = Dupl' (ToList '[s])
+
+-- | This type family checks whether the list of positions given as an
+-- argument contains any duplicates.
+type family Dupl' (s :: [Pos]) :: Bool where
+    Dupl' (p ': r) = OrDupl' (Find p r) r
+    Dupl' '[] = False
+
+-- | This type family checks whether its first argument is contained
+-- its second argument.
+type family Find (p :: Pos) (s :: [Pos]) :: Bool where
+    Find p (p ': r)  = True
+    Find p (p' ': r) = Find p r
+    Find p '[] = False
+
+-- | This type family returns @True@ if the first argument is true;
+-- otherwise it checks the second argument for duplicates.
+type family OrDupl' (a :: Bool) (b :: [Pos]) :: Bool where
+    OrDupl'  True  c  = True
+    OrDupl'  False c  = Dupl' c