diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Change Log
 
+## 0.4
+
+* Allow a wide range of dynamically sorted values (not just expressions)
+* Utility for extracting array accesses
+
 ## 0.3.1
 
 * Utility for extracting constants from expressions
diff --git a/expressions.cabal b/expressions.cabal
--- a/expressions.cabal
+++ b/expressions.cabal
@@ -1,5 +1,5 @@
 name:                expressions
-version:             0.3.1
+version:             0.4
 synopsis:            Expressions and Formulae a la carte
 description:
   This package is aimed at providing means of fixing a first-order language and
@@ -53,8 +53,9 @@
                        Data.Expression.Utils.Indexed.Foldable,
                        Data.Expression.Utils.Indexed.Functor,
                        Data.Expression.Utils.Indexed.Show,
-                       Data.Expression.Utils.Indexed.Sum
-                       Data.Expression.Utils.Indexed.Traversable
+                       Data.Expression.Utils.Indexed.Sum,
+                       Data.Expression.Utils.Indexed.Traversable,
+                       Data.Expression.Utils.Indexed.Tuple
   other-extensions:    DataKinds,
                        FlexibleContexts,
                        FlexibleInstances,
diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs
--- a/src/Data/Expression.hs
+++ b/src/Data/Expression.hs
@@ -283,7 +283,7 @@
 
             var''' n s
 
-        var''' :: VariableName -> DynamicSort -> Parser (DynamicallySorted f)
+        var''' :: VariableName -> DynamicSort -> Parser (DynamicallySortedFix f)
         var''' n (DynamicSort (s :: Sing s)) = return $ dynvar n s
 
 -- | A smart constructor for variables of any sort in any language
@@ -295,12 +295,12 @@
 var :: forall f s. ( VarF :<: f, SingI s ) => VariableName -> IFix f s
 var n = inject (Var n (sing :: Sing s))
 
--- | Like @var@ except it hides the sort inside @DynamicallySorted@
-dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySorted f
+-- | Like @var@ except it hides the sort inside @DynamicallySortedFix@
+dynvar :: forall f (s :: Sort). VarF :<: f => VariableName -> Sing s -> DynamicallySortedFix f
 dynvar n s = DynamicallySorted s $ withSort s $ var n
 
 -- | Collects a list of all variables occurring in an expression (bound or free).
-vars :: ( VarF :<: f, IFoldable f, IFunctor f ) => IFix f s -> [DynamicallySorted VarF]
+vars :: ( VarF :<: f, IFoldable f, IFunctor f ) => IFix f s -> [DynamicallySorted Var]
 vars = nub . F.getConst . icata vars' where
     vars' a = case prj a of
         Just (Var n s) -> F.Const [dynvar n s]
@@ -564,7 +564,7 @@
 
 instance ( UniversalF v :<: f, SingI v ) => Parseable (UniversalF v) f where
     parser _ r = forall' <?> "Universal" where
-        var' :: Parser (DynamicallySorted VarF)
+        var' :: Parser (DynamicallySorted Var)
         var' = parser (Proxy :: Proxy VarF) var'
 
         forall' = do
@@ -588,7 +588,7 @@
 
 instance ( ExistentialF v :<: f, SingI v ) => Parseable (ExistentialF v) f where
     parser _ r = exists' <?> "Existential" where
-        var' :: Parser (DynamicallySorted VarF)
+        var' :: Parser (DynamicallySorted Var)
         var' = parser (Proxy :: Proxy VarF) var'
 
         exists' = do
@@ -612,11 +612,11 @@
 
 class MaybeQuantified f where
     isQuantified' :: MaybeQuantified g => f (IFix g) s -> F.Const Any s
-    freevars' :: f (F.Const [DynamicallySorted VarF]) s -> F.Const [DynamicallySorted VarF] s
+    freevars' :: f (F.Const [DynamicallySorted Var]) s -> F.Const [DynamicallySorted Var] s
 
 instance MaybeQuantified VarF where
     isQuantified' _ = coerce False
-    freevars' (Var n s) = coerce [dynvar n s]
+    freevars' (Var n s) = coerce [dynvar n s :: DynamicallySorted Var]
 
 instance MaybeQuantified (UniversalF v) where
     isQuantified' _ = coerce True
@@ -645,7 +645,7 @@
 isQuantifierFree = P.not . isQuantified
 
 -- | Collects a list of all free variables occurring in an expression.
-freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted VarF]
+freevars :: ( IFunctor f, MaybeQuantified f ) => IFix f s -> [DynamicallySorted Var]
 freevars = nub . coerce . icata freevars'
 
 -- | A smart constructor for universally quantified formulae
@@ -753,7 +753,7 @@
 prenex f = let (a, (_, q)) = runState (imapM (pushQuantifier . unIFix) (nnf f)) (freenames f, id) in q a
 
 class Bind f g where
-    bind :: Proxy f -> IFix g s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
+    bind :: Proxy f -> IFix g s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted Var], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
 
 instance forall g v. ( VarF :<: g, EqualityF :<: g, NegationF :<: g, DisjunctionF :<: g, UniversalF v :<: g, MaybeQuantified g, SingI v ) => Bind (UniversalF v) g where
     bind _ a = case index (unIFix a) %~ (sing :: Sing v) of
@@ -799,7 +799,7 @@
     bind _ _ = Nothing
 
 class Bind' f g where
-    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
+    bind' :: Bind g g => f (IFix g) s -> Maybe (Bool, State (VariableNamePool, [([DynamicallySorted Var], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s))
 
 instance VarF :<: g => Bind' VarF g where
     bind' v = Just (True, return . inject $ v)
@@ -823,11 +823,11 @@
 instance {-# OVERLAPPABLE #-} f :<: g => Bind' f g where
     bind' a = bind (Proxy :: Proxy g) (inject a)
 
-bind'' :: forall f (s :: Sort). ( Bind f f, Bind' f f ) => IFix f s -> State (VariableNamePool, [([DynamicallySorted VarF], IFix f 'BooleanSort -> IFix f 'BooleanSort)]) (IFix f s)
+bind'' :: forall f (s :: Sort). ( Bind f f, Bind' f f ) => IFix f s -> State (VariableNamePool, [([DynamicallySorted Var], IFix f 'BooleanSort -> IFix f 'BooleanSort)]) (IFix f s)
 bind'' a = fromMaybe (return a) . fmap snd . bind' . unIFix $ a
 
 class MaybeQuantified'' f g where
-    flatten' :: ( Bind g g, Bind' g g ) => f (IFix g) s -> State (VariableNamePool, [([DynamicallySorted VarF], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)
+    flatten' :: ( Bind g g, Bind' g g ) => f (IFix g) s -> State (VariableNamePool, [([DynamicallySorted Var], IFix g 'BooleanSort -> IFix g 'BooleanSort)]) (IFix g s)
 
 instance ArrayF :<: g => MaybeQuantified'' ArrayF g where
     flatten' (Select is es a i) = do
diff --git a/src/Data/Expression/Array.hs b/src/Data/Expression/Array.hs
--- a/src/Data/Expression/Array.hs
+++ b/src/Data/Expression/Array.hs
@@ -19,8 +19,10 @@
 
 module Data.Expression.Array ( ArrayF(..)
                              , select
-                             , store ) where
+                             , store
+                             , accesses ) where
 
+import Control.Monad.Trans.Writer
 import Data.Coerce
 import Data.Functor.Const
 import Data.Singletons
@@ -34,6 +36,7 @@
 import Data.Expression.Utils.Indexed.Show
 import Data.Expression.Utils.Indexed.Sum
 import Data.Expression.Utils.Indexed.Traversable
+import Data.Expression.Utils.Indexed.Tuple
 
 -- | A functor representing array-theoretic terms (`select` and `store` also known as "read" and "write")
 data ArrayF a (s :: Sort) where
@@ -85,14 +88,14 @@
             _ <- char ')'
             store'' a i v
 
-        select'' :: DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)
+        select'' :: DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)
         select'' (DynamicallySorted (SArraySort is1 es) a)
                  (DynamicallySorted is2                 i) = case is1 %~ is2 of
             Proved Refl -> return . DynamicallySorted es $ inject (Select is1 es a i)
             Disproved _ -> fail "ill-sorted select"
         select'' _ _ = fail "selecting from non-array"
 
-        store'' :: DynamicallySorted f -> DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)
+        store'' :: DynamicallySortedFix f -> DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)
         store''  (DynamicallySorted as@(SArraySort _ _) a)
                  (DynamicallySorted is                  i)
                  (DynamicallySorted es                  v) = case as %~ SArraySort is es of
@@ -107,3 +110,25 @@
 -- | A smart constructor for store
 store :: ( ArrayF :<: f, SingI i, SingI e ) => IFix f ('ArraySort i e) -> IFix f i -> IFix f e -> IFix f ('ArraySort i e)
 store a i v = inject (Store sing sing a i v)
+
+newtype Array1 f (i :: Sort) (e :: Sort) = Array1 (IFix f ('ArraySort i e))
+newtype Array2 f (i :: Sort)             = Array2 (DynamicallySorted (Array1 f i))
+
+type ArrayAccess f = DynamicallySorted (IT2 (Array2 f) (IFix f))
+
+instance ( IFunctor f, IShow f ) => Show (Array1 f i e) where
+  show (Array1 f) = show f
+
+instance ( IFunctor f, IShow f ) => Show (Array2 f i) where
+  show (Array2 f) = show f
+
+-- | Collects pairs of arrays and indices that appear together in some @select@ and/or @store@ within an expression
+accesses :: forall f (s :: Sort). ( ArrayF :<: f, ITraversable f ) => IFix f s -> [ArrayAccess f]
+accesses = execWriter . imapM accesses' where
+  accesses' :: forall (s' :: Sort). IFix f s' -> Writer [ArrayAccess f] (IFix f s')
+  accesses' e = do
+    case match e of
+      Just (Select is es a i)   -> tell [ DynamicallySorted is (IT2 (Array2 (DynamicallySorted es (Array1 a)), i)) ]
+      Just (Store  is es a i _) -> tell [ DynamicallySorted is (IT2 (Array2 (DynamicallySorted es (Array1 a)), i)) ]
+      _                         -> return ()
+    return e
diff --git a/src/Data/Expression/Equality.hs b/src/Data/Expression/Equality.hs
--- a/src/Data/Expression/Equality.hs
+++ b/src/Data/Expression/Equality.hs
@@ -65,7 +65,7 @@
         _ <- char ')'
         equals a b <?> "Equality" where
 
-        equals :: DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)
+        equals :: DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)
         equals (DynamicallySorted s1 a)
                (DynamicallySorted s2 b) = case s1 %~ s2 of
             Proved Refl -> return . toDynamicallySorted . inject $ Equals s1 a b
diff --git a/src/Data/Expression/IfThenElse.hs b/src/Data/Expression/IfThenElse.hs
--- a/src/Data/Expression/IfThenElse.hs
+++ b/src/Data/Expression/IfThenElse.hs
@@ -69,7 +69,7 @@
         _ <- char ')'
         ifThenElse i t e <?> "IfThenElse" where
 
-        ifThenElse :: DynamicallySorted f -> DynamicallySorted f -> DynamicallySorted f -> Parser (DynamicallySorted f)
+        ifThenElse :: DynamicallySortedFix f -> DynamicallySortedFix f -> DynamicallySortedFix f -> Parser (DynamicallySortedFix f)
         ifThenElse (DynamicallySorted s1 i)
                    (DynamicallySorted s2 t)
                    (DynamicallySorted s3 e) = case s1 %~ SBooleanSort of
diff --git a/src/Data/Expression/Parser.hs b/src/Data/Expression/Parser.hs
--- a/src/Data/Expression/Parser.hs
+++ b/src/Data/Expression/Parser.hs
@@ -63,7 +63,7 @@
 
 -- | Expressions that can be parsed
 class Parseable f g where
-    parser :: Proxy f -> Parser (DynamicallySorted g) -> Parser (DynamicallySorted g)
+    parser :: Proxy f -> Parser (DynamicallySortedFix g) -> Parser (DynamicallySortedFix g)
 
 -- | Tries to parse the entire input text and produce an expression in desired language and with desired sort.
 parse :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Text -> Maybe (IFix f s)
diff --git a/src/Data/Expression/Sort.hs b/src/Data/Expression/Sort.hs
--- a/src/Data/Expression/Sort.hs
+++ b/src/Data/Expression/Sort.hs
@@ -6,6 +6,7 @@
            , GADTs
            , KindSignatures
            , OverloadedStrings
+           , QuantifiedConstraints
            , RankNTypes
            , ScopedTypeVariables
            , TemplateHaskell
@@ -29,6 +30,7 @@
                             , withSort
                             , DynamicSort(..)
                             , DynamicallySorted(..)
+                            , DynamicallySortedFix
                             , parseSort
                             , toDynamicallySorted
                             , toStaticSort
@@ -40,9 +42,7 @@
 import Data.Singletons.Decide
 import Data.Singletons.TH
 
-import Data.Expression.Utils.Indexed.Eq
 import Data.Expression.Utils.Indexed.Functor
-import Data.Expression.Utils.Indexed.Show
 
 -- | A universe of recognized sorts
 data Sort = BooleanSort                                  -- ^ booleans (true, false)
@@ -86,16 +86,19 @@
         Proved Refl -> True
         Disproved _ -> False
 
+-- | A value of some sort
+data DynamicallySorted (d :: Sort -> *) where
+  DynamicallySorted :: forall (s :: Sort) d. Sing s -> d s -> DynamicallySorted d
+
 -- | An expression of some sort (obtained for example during parsing)
-data DynamicallySorted (f :: (Sort -> *) -> (Sort -> *)) where
-  DynamicallySorted :: forall (s :: Sort) f. Sing s -> IFix f s -> DynamicallySorted f
+type DynamicallySortedFix f = DynamicallySorted (IFix f)
 
-instance IEq1 f => Eq (DynamicallySorted f) where
+instance (forall (s :: Sort). Eq (d s)) => Eq (DynamicallySorted d) where
     DynamicallySorted sa a == DynamicallySorted sb b = case sa %~ sb of
         Proved Refl -> a == b
         Disproved _ -> False
 
-instance (IFunctor f, IShow f) => Show (DynamicallySorted f) where
+instance (forall (s :: Sort). Show (d s)) => Show (DynamicallySorted d) where
     show (DynamicallySorted _ a) = show a
 
 -- | Tries to convert some sort (`DynamicSort`) to a requested sort.
@@ -106,12 +109,12 @@
         Disproved _ -> Nothing
 
 -- | Converts a statically sorted expression to a dynamically sorted one.
-toDynamicallySorted :: forall f (s :: Sort). SingI s => IFix f s -> DynamicallySorted f
+toDynamicallySorted :: forall d (s :: Sort). SingI s => d s -> DynamicallySorted d
 toDynamicallySorted = DynamicallySorted (sing :: Sing s)
 
 -- | Tries to convert an expression (`DynamicallySorted`) of some sort to an expression of requested sort.
 -- Performs no conversions.
-toStaticallySorted :: forall f (s :: Sort). SingI s => DynamicallySorted f -> Maybe (IFix f s)
+toStaticallySorted :: forall d (s :: Sort). SingI s => DynamicallySorted d -> Maybe (d s)
 toStaticallySorted dx = case dx of
     DynamicallySorted s x -> case s %~ (sing :: Sing s) of
         Proved Refl -> Just x
diff --git a/src/Data/Expression/Utils/Indexed/Tuple.hs b/src/Data/Expression/Utils/Indexed/Tuple.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Expression/Utils/Indexed/Tuple.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE TypeInType #-}
+
+--------------------------------------------------------------------------------
+-- |
+-- Module     :  Data.Expression.Array
+-- Copyright  :  (C) 2017-18 Jakub Daniel
+-- License    :  BSD-style (see the file LICENSE)
+-- Maintainer :  Jakub Daniel <jakub.daniel@protonmail.com>
+-- Stability  :  experimental
+--------------------------------------------------------------------------------
+
+module Data.Expression.Utils.Indexed.Tuple where
+
+newtype IT2 (a :: k -> *)
+            (b :: k -> *)
+            (i :: k) = IT2 { getIT2 :: (a i, b i) }
+
+newtype IT3 (a :: k -> *)
+            (b :: k -> *)
+            (c :: k -> *)
+            (i :: k) = IT3 { getIT3 :: (a i, b i, c i) }
+
+newtype IT4 (a :: k -> *)
+            (b :: k -> *)
+            (c :: k -> *)
+            (d :: k -> *)
+            (i :: k) = IT4 { getIT4 :: (a i, b i, c i, d i) }
+
+newtype IT5 (a :: k -> *)
+            (b :: k -> *)
+            (c :: k -> *)
+            (d :: k -> *)
+            (e :: k -> *)
+            (i :: k) = IT5 { getIT5 :: (a i, b i, c i, d i, e i) }
+
+newtype IT6 (a :: k -> *)
+            (b :: k -> *)
+            (c :: k -> *)
+            (d :: k -> *)
+            (e :: k -> *)
+            (f :: k -> *)
+            (i :: k) = IT6 { getIT6 :: (a i, b i, c i, d i, e i, f i) }
+
+newtype IT7 (a :: k -> *)
+            (b :: k -> *)
+            (c :: k -> *)
+            (d :: k -> *)
+            (e :: k -> *)
+            (f :: k -> *)
+            (g :: k -> *)
+            (i :: k) = IT7 { getIT7 :: (a i, b i, c i, d i, e i, f i, g i) }
+
+newtype IT8 (a :: k -> *)
+            (b :: k -> *)
+            (c :: k -> *)
+            (d :: k -> *)
+            (e :: k -> *)
+            (f :: k -> *)
+            (g :: k -> *)
+            (h :: k -> *)
+            (i :: k) = IT8 { getIT8 :: (a i, b i, c i, d i, e i, f i, g i, h i) }
+
+instance ( Show (a i), Show (b i) ) => Show (IT2 a b i) where
+  show (IT2 (a, b)) = "(" ++ show a ++ ", " ++ show b ++ ")"