diff --git a/Readme.md b/Readme.md
--- a/Readme.md
+++ b/Readme.md
@@ -63,7 +63,7 @@
     let ?bounds = fsm in
     -- show the data
     unlines $
-      [ "The FSM has " ++ show (elements ((#) :: T State)) ++ " states."
+      [ "The FSM has " ++ show (elements (type State)) ++ " states."
       ] ++
       [ "Labels:"
       ] ++
diff --git a/finite.cabal b/finite.cabal
--- a/finite.cabal
+++ b/finite.cabal
@@ -1,5 +1,5 @@
 name:                finite
-version:             1.4.1.4
+version:             1.5.0.0
 synopsis:            Finite ranges via types
 description:         A framework for capturing finite ranges with
                      types, where the sizes of the ranges are not
@@ -20,6 +20,7 @@
 build-type:          Simple
 extra-source-files:  Readme.md
 cabal-version:       >=1.10
+tested-with:         GHC == 9.10.1, GHC == 9.12.1
 
 source-repository head
   type:     git
@@ -34,11 +35,11 @@
     -fignore-asserts
 
   build-depends:
-      base >=4.7 && <4.22
+      base >=4.20 && <4.22
     , array >=0.5 && <0.6
-    , containers >=0.5 && <0.8
-    , hashable >=1.2 && <1.6
-    , template-haskell >=2.11 && <2.24
+    , containers >=0.7 && <0.8
+    , hashable >=1.5 && <1.6
+    , template-haskell >=2.22 && <2.24
     , QuickCheck >=2.10 && <=2.16
 
   exposed-modules:
@@ -49,7 +50,6 @@
     Finite.Class
     Finite.PowerSet
     Finite.Collection
-    Finite.Type
 
   hs-source-dirs:
     src/lib
@@ -75,9 +75,9 @@
     src/test
 
   build-depends:
-      base >=4.7 && <4.22
-    , hashable >=1.2 && <1.6
-    , Cabal >=2.4 && < 3.15
+      base >=4.20 && <4.22
+    , hashable >=1.5 && <1.6
+    , Cabal >=3.12 && < 3.15
     , QuickCheck >=2.10 && <=2.16
     , finite
 
diff --git a/src/lib/Finite.hs b/src/lib/Finite.hs
--- a/src/lib/Finite.hs
+++ b/src/lib/Finite.hs
@@ -13,16 +13,13 @@
 -- The framework supports:
 --
 -- * Easy access to the object's elements via types.
--- * Efficient bidirectional mappings between indices and the
---   elements.
+-- * Efficient bidirectional mappings between indices and the elements.
 -- * Implicit total orderings on the elements.
 -- * Powerset Support.
--- * Extension of a single context to a range of contexts via
---   collections.
+-- * Extension of a single context to a range of contexts via collections.
 -- * Easy passing of the context via implict parameters.
--- * Generics Support: Finite range types can be easily constructed
---   out of other finite range types using Haskell's `data`
---   constructor.
+-- * Generics Support: Finite range types can be easily constructed out
+--   of other finite range types using Haskell's `data` constructor.
 -- * Template Haskell: Easy creation of basic finite instances using
 --   short Haskell templates, as well as the extension of existing
 --   types to more feature rich parameter spaces (requires the
@@ -32,39 +29,23 @@
 
 module Finite
   ( -- * The Finite Class
-    Finite(..)
+    FiniteBounds
+  , Finite(..)
   , GFinite(..)
-  , FiniteBounds
+  , withBounds
   , -- * Powersets
     PowerSet
   , -- * Collections
     Collection(..)
-  , -- * Polymorphic Type Access
-    T
-  , (#)
-  , (\#)
-  , (<<#)
-  , (#<<)
-  , v2t
-  , t2v
   ) where
 
 -----------------------------------------------------------------------------
 
-import Finite.Type
-  ( T
-  , FiniteBounds
-  , (#)
-  , (\#)
-  , (<<#)
-  , (#<<)
-  , t2v
-  , v2t
-  )
-
 import Finite.Class
-  ( Finite(..)
+  ( FiniteBounds
+  , Finite(..)
   , GFinite(..)
+  , withBounds
   )
 
 import Finite.PowerSet
diff --git a/src/lib/Finite/Class.hs b/src/lib/Finite/Class.hs
--- a/src/lib/Finite/Class.hs
+++ b/src/lib/Finite/Class.hs
@@ -9,21 +9,28 @@
 
 {-# LANGUAGE
 
-    MultiWayIf
-  , TypeOperators
+    ConstraintKinds
   , DefaultSignatures
-  , MultiParamTypeClasses
   , FlexibleContexts
   , FlexibleInstances
+  , ImplicitParams
+  , LambdaCase
+  , MultiParamTypeClasses
+  , TypeOperators
+  , ScopedTypeVariables
+  , RankNTypes
+  , RequiredTypeArguments
+  , ViewPatterns
 
   #-}
 
 -----------------------------------------------------------------------------
 
 module Finite.Class
-  ( T
+  ( FiniteBounds
   , Finite(..)
   , GFinite(..)
+  , withBounds
   ) where
 
 -----------------------------------------------------------------------------
@@ -32,16 +39,6 @@
   ( assert
   )
 
-import Finite.Type
-  ( T
-  , FiniteBounds
-  , (#<<)
-  , (<<#)
-  , v2t
-  , (\#)
-  , (#)
-  )
-
 import GHC.Generics
   ( Generic
   , Rep
@@ -63,309 +60,183 @@
 
 -----------------------------------------------------------------------------
 
--- | The 'Finite' class.
+-- | A better looking constraint specifier.
+type FiniteBounds b = (?bounds :: b)
 
-class Finite b a where
+-----------------------------------------------------------------------------
 
+-- | A more ergonomic way to set the implicit parameter.
+withBounds :: b -> (FiniteBounds b => c) -> c
+withBounds b x = let ?bounds = b in x
+
+-----------------------------------------------------------------------------
+
+-- | The 'Finite' class.
+class Finite b a where
   -- | Returns the number of elements associated with the given type.
-  elements
-    :: FiniteBounds b
-    => T a -> Int
+  elements :: forall c -> (a ~ c, FiniteBounds b) => Int
 
   default elements
-    :: (Generic a, GFinite b (Rep a), FiniteBounds b)
-    => T a -> Int
-
-  elements t = gelements #<< from <<# t
+    :: (Generic a, GFinite b (Rep a)) =>
+    forall c -> (a ~ c, FiniteBounds b) => Int
+  elements _ = gelements (Rep a)
 
   -- | Turns the value in the associated range into an Int uniquely
   -- identifiying the value.
-  index
-    :: FiniteBounds b
-    => a -> Int
-
-  default index
-    :: (Generic a, GFinite b (Rep a), FiniteBounds b)
-    => a -> Int
+  index :: FiniteBounds b => a -> Int
 
-  index v = (+ (offset $ v2t v)) $ gindex $ from v
+  default index ::
+    (Generic a, GFinite b (Rep a), FiniteBounds b) =>
+    a -> Int
+  index v = (+ (offset a)) $ gindex $ from v
 
   -- | Turns an Int back to the value that is associated with it.
-  value
-    :: FiniteBounds b => Int -> a
+  value :: FiniteBounds b => Int -> a
 
-  default value
-    :: (Generic a, GFinite b (Rep a), FiniteBounds b)
-    => Int -> a
+  default value ::
+    (Generic a, GFinite b (Rep a), FiniteBounds b) => Int -> a
 
-  value v =
-    let
-      o = offset $ v2t r
-      e = elements $ v2t r
-      r = to $ gvalue (v - o)
-    in
-      assert (v >= o && v < o + e) r
+  value v = assert (v >= o && v < o + e) $ to $ gvalue (v - o)
+   where
+    o = offset a
+    e = elements a
 
   -- | Allows to put an offset to the integer mapping. Per default the
   -- offset is zero.
-  offset
-    :: FiniteBounds b
-    => T a -> Int
-
+  offset :: forall c -> (a ~ c, FiniteBounds b) => Int
   offset _ = 0
 
   -- | Returns a finite list of all elements of that type.
-  values
-    :: FiniteBounds b
-    => [a]
-
-  values =
-    let
-      rs = map value xs
-      o = offset $ f rs
-      n = elements $ f rs
-      xs = [o, o + 1 .. o + n - 1]
-    in
-      rs
-
-    where
-      f :: [a] -> T a
-      f _ = (#)
+  values :: FiniteBounds b => [a]
+  values = value <$> [o, o + 1 .. o + n - 1]
+   where
+    n = elements a
+    o = offset a
 
   -- | Complements a given list of elements of that type
-  complement
-    :: FiniteBounds b
-    => [a] -> [a]
-
-  complement xs =
-    let
-      o = offset $ f rs
-      n = elements $ f rs
-      s = S.fromList $ map index xs
-      a = S.fromAscList [o, o + 1 .. o + n - 1]
-      rs = map value $ S.toList $ S.difference a s
-    in
-      rs
-
-    where
-      f :: [a] -> T a
-      f _ = (#)
+  complement :: FiniteBounds b => [a] -> [a]
+  complement xs = value <$> ys
+   where
+    o  = offset a
+    n  = elements a
+    s  = S.fromList $ map index xs
+    as = S.fromAscList [o, o + 1 .. o + n - 1]
+    ys = S.toList $ S.difference as s
 
   -- | Less than operator according to the implicit total index order.
-  (|<|)
-    :: FiniteBounds b
-    => a -> a -> Bool
-
-  (|<|) x y =
-    index x < index y
-
+  (|<|) :: FiniteBounds b => a -> a -> Bool
+  x |<| y = index x < index y
   infixr |<|
 
   -- | Less or equal than operator according to the implicit total
   -- index order.
-  (|<=|)
-    :: FiniteBounds b
-    => a -> a -> Bool
-
-  (|<=|) x y =
-    index x <= index y
-
+  (|<=|) :: FiniteBounds b => a -> a -> Bool
+  x |<=| y = index x <= index y
   infixr |<=|
 
   -- | Greater or equal than operator according to the implicit total
   -- index order.
-  (|>=|)
-    :: FiniteBounds b
-    => a -> a -> Bool
-
-  (|>=|) x y =
-    index x >= index y
-
+  (|>=|) :: FiniteBounds b => a -> a -> Bool
+  x |>=| y = index x >= index y
   infixr |>=|
 
-  -- | Greater than operator according to the implicit total index
-  -- order.
-  (|>|)
-    :: FiniteBounds b
-    => a -> a -> Bool
-
-  (|>|) x y =
-    index x > index y
-
+  -- | Greater than operator according to the implicit total index order.
+  (|>|) :: FiniteBounds b  => a -> a -> Bool
+  x |>| y = index x > index y
   infixr |>|
 
   -- | Equal operator according to the implicit total index order.
-  (|==|)
-    :: FiniteBounds b
-    => a -> a -> Bool
-
-  (|==|) x y =
-    index x == index y
-
+  (|==|) :: FiniteBounds b => a -> a -> Bool
+  x |==| y = index x == index y
   infixr |==|
 
   -- | Unequal operator according to the implicit total index order.
-  (|/=|)
-    :: FiniteBounds b
-    => a -> a -> Bool
-
-  (|/=|) x y =
-    index x /= index y
-
+  (|/=|) :: FiniteBounds b  => a -> a -> Bool
+  x |/=| y = index x /= index y
   infixr |/=|
 
-
   -- | First element according to the total index order.
-  initial
-    :: FiniteBounds b
-    => T a -> a
-
-  initial t =
-    value $ offset t
+  initial :: forall c -> (a ~ c, FiniteBounds b) => a
+  initial x = value $ offset x
 
   -- | Last element according to the total index order.
-  final
-    :: FiniteBounds b
-    => T a -> a
-
-  final t =
-    value $ offset t + elements t - 1
+  final :: forall c -> (a ~ c, FiniteBounds b) => a
+  final x = value $ offset x + elements x - 1
 
   -- | Next element according to the total index order (undefined for
   -- the last element).
-  next
-    :: FiniteBounds b
-    => a -> a
-
-  next x =
-    let i = index x
-    in assert (i < offset (v2t x) + elements (v2t x) - 1)
-       $ value (i + 1)
+  next :: FiniteBounds b => a -> a
+  next (index -> i) = assert (i < offset a + elements a - 1) $ value (i + 1)
 
   -- | Previous element according to the total index order (undefined
   -- for the first element).
-  previous
-    :: FiniteBounds b
-    => a -> a
-
-  previous x =
-    let i = index x
-    in assert (i > offset (v2t x))
-       $ value (i - 1)
+  previous :: FiniteBounds b => a -> a
+  previous (index -> i) = assert (i > offset a) $ value (i - 1)
 
   -- | The upper and lower bounds of the instance.
-  bounds
-    :: FiniteBounds b
-    => T a -> (a, a)
-
-  bounds t =
-    (initial t, final t)
+  bounds :: forall c -> (c ~ a, FiniteBounds b) => (a, a)
+  bounds x = (initial x, final x)
 
 -----------------------------------------------------------------------------
 
 -- | Generics implementation for the 'Finite' class. The
 -- realization is closely related to the one presented at
 -- https://wiki.haskell.org/GHC.Generics.
-
 class GFinite b f where
-  gelements :: FiniteBounds b => T (f a) -> Int
+  gelements :: forall c -> (c ~ f, FiniteBounds b) => Int
   gindex :: FiniteBounds b => f a -> Int
   gvalue :: FiniteBounds b => Int -> f a
 
 -----------------------------------------------------------------------------
 
 -- | :*: instance.
-
-instance
-  (GFinite b f, GFinite b g)
-    => GFinite b (f :*: g) where
-
-  gelements x =
-    gelements (((\#) :: T ((f :*: g) a) -> T (f a)) x) *
-    gelements (((\#) :: T ((f :*: g) a) -> T (g a)) x)
-
-  gindex (f :*: g) =
-    (gindex f * (gelements #<< g)) + gindex g
-
-  gvalue n =
-    let
-      m = gelements #<< g
-      f = gvalue (n `div` m)
-      g = gvalue (n `mod` m)
-    in
-     (f :*: g)
+instance (GFinite b f, GFinite b g) => GFinite b (f :*: g) where
+  gelements _ = gelements f * gelements g
+  gindex (f :*: g) = gindex f * gelements (type g) + gindex g
+  gvalue n = f :*: g
+   where
+    m = gelements (type g)
+    f = gvalue (n `div` m)
+    g = gvalue (n `mod` m)
 
 -----------------------------------------------------------------------------
 
 -- | :+: instance.
-
-instance
-  (GFinite b f, GFinite b g)
-    => GFinite b (f :+: g) where
-
-  gelements x =
-    gelements (((\#) :: T ((f :+: g) a) -> T (f a)) x) +
-    gelements (((\#) :: T ((f :+: g) a) -> T (g a)) x)
-
-  gindex x = case x of
-    R1 y -> gindex y
-    L1 y -> gindex y + gelements (((\#) :: (f :+: g) a -> T (g a)) x)
-
-  gvalue n =
-    let
-      m = gelements #<< g
-      g = gvalue (n `mod` m)
-      f = gvalue (n - m)
-    in if
-      | n < m     -> R1 g
-      | otherwise -> L1 f
+instance (GFinite b f, GFinite b g) => GFinite b (f :+: g) where
+  gelements _ = gelements f + gelements g
+  gindex = \case
+    R1 x -> gindex x
+    L1 x -> gindex x + gelements g
+  gvalue n
+    | n < m     = R1 g
+    | otherwise = L1 f
+   where
+    m = gelements (type g)
+    g = gvalue (n `mod` m)
+    f = gvalue (n - m)
 
 -----------------------------------------------------------------------------
 
 -- | U1 instance.
-
-instance
-  GFinite c U1 where
-
+instance GFinite c U1 where
   gelements _ = 1
-
   gindex U1 = 0
-
   gvalue _ = U1
 
 -----------------------------------------------------------------------------
 
 -- | M1 instance.
-
-instance
-  (GFinite c f)
-    => GFinite c (M1 i v f) where
-
-  gelements =
-    gelements . ((\#) :: T ((M1 i v f) p) -> T (f p))
-
+instance GFinite c f => GFinite c (M1 i v f) where
+  gelements _ = gelements f
   gindex (M1 x) = gindex x
-
   gvalue = M1 . gvalue
 
 -----------------------------------------------------------------------------
 
 -- | K1 instance.
-
-instance
-  (Finite b a)
-    => GFinite b (K1 i a) where
-
-  gelements =
-    elements . ((\#) :: T ((K1 i a) c) -> T a)
-
-  gindex (K1 x) = index x - (offset #<< x)
-
-  gvalue n =
-    let
-      m = offset #<< x
-      x = value (n + m)
-    in
-      K1 x
+instance Finite b a => GFinite b (K1 i a) where
+  gelements _ = elements a
+  gindex (K1 x) = index x - offset a
+  gvalue n = K1 $ value (n + offset a)
 
 -----------------------------------------------------------------------------
diff --git a/src/lib/Finite/Collection.hs b/src/lib/Finite/Collection.hs
--- a/src/lib/Finite/Collection.hs
+++ b/src/lib/Finite/Collection.hs
@@ -10,9 +10,10 @@
 
 {-# LANGUAGE
 
-    MultiParamTypeClasses
+    ImplicitParams
   , LambdaCase
-  , ImplicitParams
+  , MultiParamTypeClasses
+  , ScopedTypeVariables
 
   #-}
 
@@ -22,19 +23,13 @@
 
 -----------------------------------------------------------------------------
 
-import Finite.Type
-  ( T
-  , v2t
-  , (#<<)
-  , FiniteBounds
-  )
-
 import Finite.Class
   ( Finite
   , elements
   , offset
   , value
   , index
+  , withBounds
   )
 
 import Data.Array.IArray
@@ -55,9 +50,7 @@
 
 -- | The 'Collection' type provides a set of items, each assigning an
 -- index of type @i@ to a value of type @a@.
-
-data Collection i a =
-  Item i a
+data Collection i a = Item i a
   deriving
     ( -- | Equality can be checked for collections, if the index type
       -- and the elements can be checked for equality.
@@ -77,77 +70,32 @@
 -- the bounds. Since the 'FiniteBounds' parameter always gives a
 -- finite sized array of bounding parameters, it is guaranteed that
 -- the connected collection has a finite bound as well.
-
 instance (Ix i, Finite b a) => Finite (Array i b) (Collection i a) where
-
-  elements t =
-    sum $ map (elms t) $ assocs ?bounds
-
-    where
-      conv
-        :: T (Collection i a) -> T a
-
-      conv = undefined
-
-
-      elms
-        :: Finite b a => T (Collection i a) -> (i, b) -> Int
-
-      elms t (_,b) =
-        let ?bounds = b
-        in elements $ conv t
-
-  index (Item j v) =
-    let
-      -- array bounds
-      (l,u) = bounds ?bounds
-      -- list of indicies that appear before j
-      ys = assert (inRange (l,u) j) $ init $ range (l,j)
-      -- offset induces by these indices
-      o = sum $ map ((elms v .) (?bounds !)) ys
-      -- index of v with the bounds at position j
-      idx = let ?bounds = ?bounds ! j
-            in index v - offset #<< v
-    in
-      o + idx
-
-    where
-      elms
-        :: Finite b a => a -> b -> Int
+  elements _ = sum $ (`withBounds` elements a) . snd <$> assocs ?bounds
 
-      elms v b =
-        let ?bounds = b
-        in elements $ v2t v
+  index (Item j v) = o + idx
+   where
+    -- array bounds
+    (l, u) = bounds ?bounds
+    -- list of indicies that appear before j
+    ys = assert (inRange (l, u) j) $ init $ range (l, j)
+    -- offset induces by these indices
+    o = sum $ map ((`withBounds` elements a) . (?bounds !)) ys
+    -- index of v with the bounds at position j
+    idx = withBounds (?bounds ! j) $ index v - offset a
 
   value n =
-    let
-      -- elements of the whole collection
-      e = elements $ v2t r
-      -- array bounds
-      b = bounds ?bounds
-      -- target array index and reminder used as sub-index
-      (j,m) = position (conv r) n (range b)
-      -- result
-      r = let ?bounds = ?bounds ! j
-          in Item j $ value (m + offset (conv r))
-    in
-      assert (n >= 0 && n < e) r
-
-    where
-      conv
-        :: Collection i a -> T a
-
-      conv = undefined
-
-
-      position
-        :: (Ix i, Finite b a, FiniteBounds (Array i b))
-        => T a -> Int -> [i] -> (i,Int)
+    assert (n >= 0 && n < elements (Collection i a))
+      $ withBounds (?bounds ! j) $ Item j $ value (m + offset a)
+   where
+    -- target array index and reminder used as sub-index
+    (j, m) = position n $ range $ bounds ?bounds
 
-      position t n = \case
-        []   -> assert False undefined
-        x:xr ->
-          let m = let ?bounds = ?bounds ! x in elements t
-          in if m <= n then position t (n - m) xr else (x,n)
+    position n = \case
+      []                 -> assert False undefined
+      x : xr | m <= n    -> position (n - m) xr
+             | otherwise -> (x, n)
+       where
+        m = withBounds (?bounds ! x) $ elements a
 
 -----------------------------------------------------------------------------
diff --git a/src/lib/Finite/PowerSet.hs b/src/lib/Finite/PowerSet.hs
--- a/src/lib/Finite/PowerSet.hs
+++ b/src/lib/Finite/PowerSet.hs
@@ -9,12 +9,10 @@
 
 {-# LANGUAGE
 
-    MultiParamTypeClasses
+    BangPatterns
   , FlexibleInstances
-  , FlexibleContexts
-  , LambdaCase
-  , MultiWayIf
-  , BangPatterns
+  , MultiParamTypeClasses
+  , ScopedTypeVariables
 
   #-}
 
@@ -26,14 +24,6 @@
 
 -----------------------------------------------------------------------------
 
-import Finite.Type
-  ( T
-  , (#)
-  , (\#)
-  , (#<<)
-  , v2t
-  )
-
 import Finite.Class
   ( Finite(..)
   )
@@ -47,51 +37,41 @@
 -- | Powersets are just lists of the correpsonding elements. The type
 -- has only been added for clearification. Consider the corresponding
 -- instance of 'Finite' for possible applications.
-
 type PowerSet a = [a]
 
 -----------------------------------------------------------------------------
 
 -- | If the number of elements associated with a type is finite, then
 -- it also has finite number of powersets.
-
 instance Finite b a => Finite b (PowerSet a) where
-
-  elements =
-    pow2 2 . elements . ((\#) :: T (PowerSet a) -> T a)
-
-    where
-      pow2 !a !n = case n of
-        0 -> 1
-        1 -> a
-        _ -> pow2 (2*a) (n-1)
-
-  index = \case
-    []     -> 0
-    (y:yr) -> powsum (0,2,idx y,yr)
-
-    where
-      idx x = index x - offset #<< x
+  elements _ = pow2 2 $ elements a
+   where
+    pow2 !a !n = case n of
+      0 -> 1
+      1 -> a
+      _ -> pow2 (2 * a) (n - 1)
 
-      powsum !p = case p of
-        (a,_,0,[])   ->
-          a + (1 - (a `mod` 2))
-        (a,p,1,[])   ->
-          a + ((1 - ((a `mod` (2*p)) `div` p)) * p)
-        (a,_,0,x:xr) ->
-          powsum (a + (1 - (a `mod` 2)),2,idx x,xr)
-        (a,p,1,x:xr) ->
-          powsum (a + ((1 - ((a `mod` (2*p)) `div` p)) * p), 2, idx x, xr)
-        (a,p,n,xs)   ->
-          powsum (a,2*p,n-1,xs)
+  index [] = 0
+  index (y : yr) = powsum (0, 2, idx y, yr)
+   where
+    idx x = index x - offset a
+    powsum !p = case p of
+      (a, _, 0, []) ->
+        a + (1 - (a `mod` 2))
+      (a, p, 1, []) ->
+        a + ((1 - ((a `mod` (2 * p)) `div` p)) * p)
+      (a, _, 0, x : xr) ->
+        powsum (a + (1 - (a `mod` 2)), 2, idx x, xr)
+      (a, p, 1, x : xr) ->
+        powsum (a + ((1 - ((a `mod` (2 * p)) `div` p)) * p), 2, idx x, xr)
+      (a, p, n, xs) ->
+        powsum (a, 2 * p, n - 1, xs)
 
   value n =
-    let ty :: T [a] -> T a
-        ty _ = (#)
-        bs = map (value . (+ (offset $ ty $ v2t bs))) $ bin n
-    in assert (n >= 0 && n < (elements #<< bs)) bs
+    assert (n >= 0 && n < elements (PowerSet a))
+      $ value . (+ offset a) <$> bin n
 
-  offset = offset . ((\#) :: T (PowerSet a) -> T a)
+  offset _ = offset a
 
   values = powerset values
 
@@ -99,30 +79,22 @@
 
 -- | Converts an Int value to a list of Int values of logarithmic size
 -- encoding the original value.
-
-bin
-  :: Int -> [Int]
-
-bin x =
-  let
-    bin (a,!s,!n)
-      | n <= 0         = reverse a
-      | n `mod` 2 == 1 = bin (s:a, s+1, n `div` 2)
-      | otherwise     = bin (a, s+1, n `div` 2)
-  in
-    bin ([],0,x)
+bin :: Int -> [Int]
+bin x = f ([], 0, x)
+ where
+  f (a, !s, !n)
+    | n <= 0         = reverse a
+    | n `mod` 2 == 1 = f (s : a, s + 1, n `div` 2)
+    | otherwise      = f (    a, s + 1, n `div` 2)
 
 -----------------------------------------------------------------------------
 
 -- | Creates the powerset of a set, for sets represented as lists. If
 -- the given list is sorted, the created powerset will be sorted
 -- lexographically and the elements themselve will be sorted as well.
-
-powerset
-  :: [a] -> [[a]]
-
-powerset =
-  let f x a = [x] : foldr ((:) . (x:)) a a
-  in  ([]:) . foldr f []
+powerset :: [a] -> [[a]]
+powerset = ([] :) . foldr f []
+ where
+  f x a = [x] : foldr ((:) . (x :)) a a
 
 -----------------------------------------------------------------------------
diff --git a/src/lib/Finite/TH.hs b/src/lib/Finite/TH.hs
--- a/src/lib/Finite/TH.hs
+++ b/src/lib/Finite/TH.hs
@@ -9,10 +9,14 @@
 
 {-# LANGUAGE
 
-    LambdaCase
+    CPP
   , ImplicitParams
+  , ImpredicativeTypes
+  , LambdaCase
+  , RequiredTypeArguments
   , TemplateHaskell
-  , CPP
+  , TypeOperators
+  , ViewPatterns
 
   #-}
 
@@ -46,13 +50,10 @@
   , hashWithSalt
   )
 
-import Finite.Type
-  ( T
-  , FiniteBounds
-  )
-
 import Finite.Class
-  ( Finite(..)
+  ( FiniteBounds
+  , Finite(..)
+  , withBounds
   )
 
 import Data.Char
@@ -135,10 +136,7 @@
 --   negate = Example . negage . example
 --   signum = Example . signum . example
 --   fromInteger = Example . fromInteger
-
-newInstance
-  :: String -> Q [Dec]
-
+newInstance :: String -> Q [Dec]
 newInstance = \case
   [] -> assert False undefined
   (x:xr) -> assert (isUpper x) $ do
@@ -415,10 +413,7 @@
 --   elements _ = getBound ?bounds
 --   value = Example
 --   index = example
-
-baseInstance
-  :: Q Type -> Q Exp -> String -> Q [Dec]
-
+baseInstance :: Q Type -> Q Exp -> String -> Q [Dec]
 baseInstance bounds f = \case
   []     -> assert False undefined
   (x:xr) -> assert (isUpper x) $ do
@@ -479,10 +474,7 @@
 -----------------------------------------------------------------------------
 
 -- | Combined 'newInstance' with 'baseInstance'.
-
-newBaseInstance
-  :: Q Type -> Q Exp -> String -> Q [Dec]
-
+newBaseInstance :: Q Type -> Q Exp -> String -> Q [Dec]
 newBaseInstance bounds f name = do
   xs <- newInstance name
   ys <- baseInstance bounds f name
@@ -511,10 +503,7 @@
 --   offset = let ?bounds = translate ?bounds in offset
 --   value = let ?bounds = translate ?bounds in value
 --   index = let ?bounds = translate ?bounds in index
-
-extendInstance
-  :: Q Type -> Q Type -> Q Exp -> Q [Dec]
-
+extendInstance :: Q Type -> Q Type -> Q Exp -> Q [Dec]
 extendInstance rtype bounds access = do
   let tmpV = mkName "x"
   d_finite_instance <-
@@ -588,69 +577,43 @@
 -- >>> polyType [t|Maybe|] "a"
 -- <BLANKLINE>
 -- Maybe a
-
-polyType
-  :: Q Type -> String -> Q Type
-
-polyType con str = do
+polyType :: Q Type -> String -> Q Type
+polyType con (mkName -> name) = do
   t <- con
-  return $ t `AppT` (VarT $ mkName str)
+  return $ t `AppT` VarT name
 
 -----------------------------------------------------------------------------
 
-appBounds
-  :: FiniteBounds b
-  => (b -> a) -> a
-
-appBounds x =
-  x ?bounds
+appBounds :: FiniteBounds b=> (b -> a) -> a
+appBounds x = x ?bounds
 
 -----------------------------------------------------------------------------
 
-elementsSwitch
-  :: (Finite b' a, FiniteBounds b)
-  => (b -> b') -> T a -> Int
-
-elementsSwitch f =
-  let ?bounds = f ?bounds
-  in elements
+elementsSwitch ::
+  (Finite b' a, FiniteBounds b) => (b -> b') ->
+  Finite b a => forall c -> (c ~ a, FiniteBounds b) => Int
+elementsSwitch f x = withBounds (f ?bounds) $ elements x
 
 -----------------------------------------------------------------------------
 
-offsetSwitch
-  :: (Finite b' a, FiniteBounds b)
-  => (b -> b') -> T a -> Int
-
-offsetSwitch f =
-  let ?bounds = f ?bounds
-  in offset
+offsetSwitch ::
+  (Finite b' a, FiniteBounds b) => (b -> b') ->
+  Finite b a => forall c -> (c ~ a, FiniteBounds b) => Int
+offsetSwitch f x = withBounds (f ?bounds) $ offset x
 
 -----------------------------------------------------------------------------
 
-indexSwitch
-  :: (Finite b' a, FiniteBounds b)
-  => (b -> b') -> a -> Int
-
-indexSwitch f =
-  let ?bounds = f ?bounds
-  in index
+indexSwitch :: (Finite b' a, FiniteBounds b) => (b -> b') -> a -> Int
+indexSwitch f = withBounds (f ?bounds) index
 
 -----------------------------------------------------------------------------
 
-valueSwitch
-  :: (Finite b' a, FiniteBounds b)
-  => (b -> b') -> Int -> a
-
-valueSwitch f =
-  let ?bounds = f ?bounds
-  in value
+valueSwitch :: (Finite b' a, FiniteBounds b) => (b -> b') -> Int -> a
+valueSwitch f = withBounds (f ?bounds) value
 
 -----------------------------------------------------------------------------
 
-inRange
-  :: Int -> Int -> Bool
-
-inRange x y =
-  x >= 0 && x < y
+inRange :: Int -> Int -> Bool
+inRange x y = x >= 0 && x < y
 
 -----------------------------------------------------------------------------
diff --git a/src/lib/Finite/Type.hs b/src/lib/Finite/Type.hs
deleted file mode 100644
--- a/src/lib/Finite/Type.hs
+++ /dev/null
@@ -1,93 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Finite.Type
--- Maintainer  :  Felix Klein
---
--- Type association to pass types via functions.
---
------------------------------------------------------------------------------
-
-{-# LANGUAGE
-
-    ImplicitParams
-  , ConstraintKinds
-
-  #-}
-
------------------------------------------------------------------------------
-
-module Finite.Type
-  ( T
-  , FiniteBounds
-  , (#)
-  , (\#)
-  , (<<#)
-  , (#<<)
-  , t2v
-  , v2t
-  ) where
-
------------------------------------------------------------------------------
-
--- | A better looking constraint specifier.
-
-type FiniteBounds b = (?bounds :: b)
-
------------------------------------------------------------------------------
-
--- | A type dummy.
-
-newtype T a = T ()
-
------------------------------------------------------------------------------
-
--- | The type dummy instance.
-
-(#) :: T a
-(#) = T ()
-
------------------------------------------------------------------------------
-
--- | A type dummy returning function. Intended to use the type engine
--- for accessing the type of the argument. Note that "@(\\#) :: a -> T
--- a@" is just a special instance.
-
-(\#) :: b -> T a
-(\#) _ = (#)
-
------------------------------------------------------------------------------
-
--- | Get some undefined value of the given type. Intended to be used
--- for extracting type information of polymorph types only.
-
-t2v :: T a -> a
-t2v _ = undefined
-
------------------------------------------------------------------------------
-
--- | Replace a function's argument by its type dummy. Intended to be used
--- for extracting type information of polymorph types only.
-
-infixr <<#
-
-(<<#) :: (a -> b) -> T a -> b
-(<<#) f _ = f undefined
-
------------------------------------------------------------------------------
-
--- | Get the type of a given value.
-
-v2t :: a -> T a
-v2t = (\#)
-
------------------------------------------------------------------------------
-
--- | Replace a function's dummy type argument with its value taking
--- equivalent.
-
-infixr #<<
-
-(#<<) :: (T a -> b) -> a -> b
-(#<<) f _ = f $ T ()
-
------------------------------------------------------------------------------
diff --git a/src/test/Test.hs b/src/test/Test.hs
--- a/src/test/Test.hs
+++ b/src/test/Test.hs
@@ -9,12 +9,14 @@
 
 {-# LANGUAGE
 
-    LambdaCase
+    DeriveGeneric
+  , ExplicitNamespaces
   , ImplicitParams
+  , LambdaCase
+  , MultiParamTypeClasses
+  , RankNTypes
   , RecordWildCards
-  , DeriveGeneric
   , TemplateHaskell
-  , MultiParamTypeClasses
 
   #-}
 
@@ -140,36 +142,33 @@
       { run =
          (Finished . allPass) <$> sequence
            (map quickCheckResult
-              [ \x -> let ?bounds = Bounds $ abs x + 1 in
-                      elements ((#) :: T AInst) == abs x + 1
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      offset ((#) :: T AInst) == 0
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map index (values :: [AInst]) == [0,1..abs x]
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map value [0,1..abs x] == (values :: [AInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      all (\x -> x == value (index x)) (values :: [AInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      complement (filter (odd . index) (values :: [AInst]))
-                      == filter (even . index) (values :: [AInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      initial ((#) :: T AInst) |<=| final ((#) :: T AInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else next (initial ((#) :: T AInst))
-                             |>=| initial ((#) :: T AInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else previous (final ((#) :: T AInst))
-                             |/=| final ((#) :: T AInst)
+              [ \x -> sb x $ elements (type AInst) == abs x + 1
+              , \x -> sb x $ offset (type AInst) == 0
+              , \x -> sb x $ map index vs == [0,1..abs x]
+              , \x -> sb x $ map value [0,1..abs x] == vs
+              , \x -> sb x $ all (\x -> x == value (index x)) vs
+              , \x -> sb x $ complement (filter (odd . index) vs)
+                               == filter (even . index) vs
+              , \x -> sb x $ initial (type AInst) |<=| final (type AInst)
+              , \x -> sb x $ abs x < 1 ||
+                               next (initial (type AInst))
+                                 |>=| initial (type AInst)
+              , \x -> sb x $ abs x < 1 ||
+                               previous (final (type AInst))
+                                 |/=| final (type AInst)
               ])
       , name = "TH: baseInstance"
       , tags = []
       , options = []
       , setOption = \_ _ -> Right t02
       }
+     where
+      vs :: FiniteBounds Bounds => [AInst]
+      vs = values
 
+      sb :: Int -> (FiniteBounds Bounds => c) -> c
+      sb x = withBounds $ Bounds $ abs x + 1
+
     t03 = TestInstance
       { run =
          (Finished . allPass) <$> sequence
@@ -182,29 +181,20 @@
               , \x -> hash (BInst x) == hash (BInst x)
               , \x -> not $ null $ range (BInst 0, BInst $ abs x)
               , \x -> (BInst x) + (BInst 1) == (BInst 1) + (BInst x)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      elements ((#) :: T BInst) == abs x + 1
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      offset ((#) :: T BInst) == 0
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map index (values :: [BInst]) == [0,1..abs x]
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map value [0,1..abs x] == (values :: [BInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      all (\x -> x == value (index x)) (values :: [BInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      complement (filter (odd . index) (values :: [BInst]))
-                      == filter (even . index) (values :: [BInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      initial ((#) :: T BInst) |<=| final ((#) :: T BInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else next (initial ((#) :: T BInst))
-                             |>=| initial ((#) :: T BInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else previous (final ((#) :: T BInst))
-                             |/=| final ((#) :: T BInst)
+              , \x -> sb x $ elements (type BInst) == abs x + 1
+              , \x -> sb x $ offset (type BInst) == 0
+              , \x -> sb x $ map index vs == [0,1..abs x]
+              , \x -> sb x $ map value [0,1..abs x] == vs
+              , \x -> sb x $ all (\x -> x == value (index x)) vs
+              , \x -> sb x $ complement (filter (odd . index) vs)
+                               == filter (even . index) vs
+              , \x -> sb x $ initial (type BInst) |<=| final (type BInst)
+              , \x -> sb x $ abs x < 1 ||
+                               next (initial (type BInst))
+                                 |>=| initial (type BInst)
+              , \x -> sb x $ abs x < 1 ||
+                               previous (final (type BInst))
+                                 |/=| final (type BInst)
               ] ++
               [ quickCheckResult $ \x -> bInst x == bInst x
               ])
@@ -213,137 +203,124 @@
       , options = []
       , setOption = \_ _ -> Right t03
       }
+     where
+      vs :: FiniteBounds Bounds => [BInst]
+      vs = values
 
+      sb :: Int -> (FiniteBounds Bounds => c) -> c
+      sb x = withBounds $ Bounds $ abs x + 1
+
     t04 = TestInstance
       { run =
          (Finished . allPass) <$> sequence
            (map quickCheckResult
-              [ \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      elements ((#) :: T AInst) == abs x + 1
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      offset ((#) :: T AInst) == 0
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      map index (values :: [AInst]) == [0,1..abs x]
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      map value [0,1..abs x] == (values :: [AInst])
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      all (\x -> x == value (index x)) (values :: [AInst])
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      complement (filter (odd . index) (values :: [AInst]))
-                      == filter (even . index) (values :: [AInst])
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      initial ((#) :: T AInst) |<=| final ((#) :: T AInst)
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else next (initial ((#) :: T AInst))
-                             |>=| initial ((#) :: T AInst)
-              , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else previous (final ((#) :: T AInst))
-                             |/=| final ((#) :: T AInst)
+              [ \x -> sb x $ elements (type AInst) == abs x + 1
+              , \x -> sb x $ offset (type AInst) == 0
+              , \x -> sb x $ map index vs == [0,1..abs x]
+              , \x -> sb x $ map value [0,1..abs x] == vs
+              , \x -> sb x $ all (\x -> x == value (index x)) vs
+              , \x -> sb x $ complement (filter (odd . index) vs)
+                               == filter (even . index) vs
+              , \x -> sb x $ initial (type AInst) |<=| final (type AInst)
+              , \x -> sb x $ abs x < 1 ||
+                             next (initial (type AInst))
+                               |>=| initial (type AInst)
+              , \x -> sb x $ abs x < 1 ||
+                             previous (final (type AInst))
+                               |/=| final (type AInst)
               ])
       , name = "TH: extendInstance"
       , tags = []
       , options = []
       , setOption = \_ _ -> Right t04
       }
+     where
+      vs :: FiniteBounds BBounds => [AInst]
+      vs = values
 
+      sb :: Int -> (FiniteBounds BBounds => c) -> c
+      sb x = withBounds $ BBounds $ Bounds $ abs x + 1
+
     t05 = TestInstance
       { run =
          (Finished . allPass) <$> sequence
            (map quickCheckResult
-              [ \x -> let ?bounds = Bounds $ abs x + 1 in
-                      elements ((#) :: T GInst)
-                        == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      offset ((#) :: T GInst) == 0
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map index (values :: [GInst])
-                        == [0,1..elements ((#) :: T GInst) - 1]
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map value [0,1..elements ((#) :: T GInst) - 1]
-                        == (values :: [GInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      all (\x -> x == value (index x)) (values :: [GInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      complement (filter (odd . index) (values :: [GInst]))
-                      == filter (even . index) (values :: [GInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      initial ((#) :: T GInst) |<=| final ((#) :: T GInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else next (initial ((#) :: T GInst))
-                             |>=| initial ((#) :: T GInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else previous (final ((#) :: T GInst))
-                             |/=| final ((#) :: T GInst)
+              [ \x -> sb x $ elements (type GInst)
+                               == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)
+              , \x -> sb x $ offset (type GInst) == 0
+              , \x -> sb x $ map index vs == [0,1..elements (type GInst) - 1]
+              , \x -> sb x $ map value [0,1..elements (type GInst) - 1] == vs
+              , \x -> sb x $ all (\x -> x == value (index x)) vs
+              , \x -> sb x $ complement (filter (odd . index) vs)
+                               == filter (even . index) vs
+              , \x -> sb x $ initial (type GInst) |<=| final (type GInst)
+              , \x -> sb x $ abs x < 1 ||
+                             next (initial (type GInst))
+                               |>=| initial (type GInst)
+              , \x -> sb x $ abs x < 1 ||
+                             previous (final (type GInst))
+                               |/=| final (type GInst)
               ])
       , name = "Generics"
       , tags = []
       , options = []
       , setOption = \_ _ -> Right t05
       }
+     where
+      vs :: FiniteBounds Bounds => [GInst]
+      vs = values
 
+      sb :: Int -> (FiniteBounds Bounds => c) -> c
+      sb x = withBounds $ Bounds $ abs x + 1
+
     t06 = TestInstance
       { run =
          (Finished . allPass) <$> sequence
            (map quickCheckResult
-              [ \x -> let ?bounds = Bounds $ abs x + 1 in
-                      elements ((#) :: T OInst) == abs x + 1
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      offset ((#) :: T OInst) == 3
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map index (values :: [OInst]) == [3,4..abs x + 3]
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map value [3,4..abs x + 3] == (values :: [OInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      all (\x -> x == value (index x)) (values :: [OInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      complement (filter (odd . index) (values :: [OInst]))
-                      == filter (even . index) (values :: [OInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      initial ((#) :: T OInst) |<=| final ((#) :: T OInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else next (initial ((#) :: T OInst))
-                             |>=| initial ((#) :: T OInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else previous (final ((#) :: T OInst))
-                             |/=| final ((#) :: T OInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      elements ((#) :: T TInst)
-                        == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      offset ((#) :: T TInst) == 0
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map index (values :: [TInst])
-                        == [0,1..elements ((#) :: T TInst) - 1]
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      map value [0,1..elements ((#) :: T TInst) - 1]
-                        == (values :: [TInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      all (\x -> x == value (index x)) (values :: [TInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      complement (filter (odd . index) (values :: [TInst]))
-                      == filter (even . index) (values :: [TInst])
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      initial ((#) :: T TInst) |<=| final ((#) :: T TInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else next (initial ((#) :: T TInst))
-                             |>=| initial ((#) :: T TInst)
-              , \x -> let ?bounds = Bounds $ abs x + 1 in
-                      if abs x < 1 then True
-                      else previous (final ((#) :: T TInst))
-                             |/=| final ((#) :: T TInst)
+              [ \x -> sb x $ elements (type OInst) == abs x + 1
+              , \x -> sb x $ offset (type OInst) == 3
+              , \x -> sb x $ map index ovs == [3,4..abs x + 3]
+              , \x -> sb x $ map value [3,4..abs x + 3] == ovs
+              , \x -> sb x $ all (\x -> x == value (index x)) ovs
+              , \x -> sb x $ complement (filter (odd . index) ovs)
+                        == filter (even . index) ovs
+              , \x -> sb x $ initial (type OInst) |<=| final (type OInst)
+              , \x -> sb x $ abs x < 1 ||
+                             next (initial (type OInst))
+                               |>=| initial (type OInst)
+              , \x -> sb x $ abs x < 1 ||
+                             previous (final (type OInst))
+                               |/=| final (type OInst)
+              , \x -> sb x $ elements (type TInst)
+                               == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)
+              , \x -> sb x $ offset (type TInst) == 0
+              , \x -> sb x $ map index tvs == [0,1..elements (type TInst) - 1]
+              , \x -> sb x $ map value [0,1..elements (type TInst) - 1] == tvs
+              , \x -> sb x $ all (\x -> x == value (index x)) tvs
+              , \x -> sb x $ complement (filter (odd . index) tvs)
+                               == filter (even . index) tvs
+              , \x -> sb x $ initial (type TInst) |<=| final (type TInst)
+              , \x -> sb x $ abs x < 1 ||
+                             next (initial (type TInst))
+                               |>=| initial (type TInst)
+              , \x -> sb x $ abs x < 1 ||
+                             previous (final (type TInst))
+                               |/=| final (type TInst)
               ])
       , name = "Offset"
       , tags = []
       , options = []
       , setOption = \_ _ -> Right t06
       }
+     where
+      ovs :: FiniteBounds Bounds => [OInst]
+      ovs = values
+
+      tvs :: FiniteBounds Bounds => [TInst]
+      tvs = values
+
+      sb :: Int -> (FiniteBounds Bounds => c) -> c
+      sb x = withBounds $ Bounds $ abs x + 1
 
     allPass xs = case dropWhile (isSuccess) xs of
       []  -> Pass