diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,16 @@
 # Version history for ral
 
+## 0.2
+
+- `fin-0.2` support
+- Add `indexed-traversable` instances
+- Explicitly mark all modules as Safe or Trustworthy.
+
+## 0.1.1
+
+- Add `reverse` and `itraverse_` to `Data.RAVec.Tree`
+- Add `Data.RAVec.Tree.DF`
+
 ## 0.1
 
 - First version. Released on an unsuspecting world.
diff --git a/ral.cabal b/ral.cabal
--- a/ral.cabal
+++ b/ral.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               ral
-version:            0.1
+version:            0.2
 synopsis:           Random access lists
 category:           Data, Dependent Types, Singletons
 description:
@@ -25,7 +25,7 @@
 license-file:       LICENSE
 author:             Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:          (c) 2019 Oleg Grenrus
+copyright:          (c) 2019-2021 Oleg Grenrus
 build-type:         Simple
 extra-source-files: ChangeLog.md
 tested-with:
@@ -35,7 +35,9 @@
    || ==8.2.2
    || ==8.4.4
    || ==8.6.5
-   || ==8.8.1
+   || ==8.8.4
+   || ==8.10.4
+   || ==9.0.1
 
 source-repository head
   type:     git
@@ -72,29 +74,32 @@
     Data.RAVec
     Data.RAVec.NonEmpty
     Data.RAVec.Tree
+    Data.RAVec.Tree.DF
 
   other-modules:
     Data.RAList.Internal
     Data.RAList.NonEmpty.Internal
     Data.RAList.Tree.Internal
+    TrustworthyCompat
 
   -- GHC boot libs
   build-depends:
-    , base     >=4.7     && <4.14
+    , base     >=4.7     && <4.16
     , deepseq  >=1.3.0.1 && <1.5
 
   if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.4 && <0.20
+    build-depends: semigroups >=0.18.5 && <0.20
 
   -- siblings
   build-depends:
     , bin  ^>=0.1
-    , fin  ^>=0.1.1
+    , fin  ^>=0.2
 
   -- other dependencies
   build-depends:
-    , hashable    >=1.2.7.0 && <1.4
-    , QuickCheck  ^>=2.13.2
+    , hashable             >=1.2.7.0 && <1.4
+    , indexed-traversable  ^>=0.1.1
+    , QuickCheck           ^>=2.14.2
 
   if flag(distributive)
     build-depends: distributive >=0.5.3 && <0.7
@@ -103,7 +108,12 @@
       build-depends: adjunctions ^>=4.4
 
   if flag(semigroupoids)
-    build-depends: semigroupoids >=5.2.2 && <5.4
+    build-depends: semigroupoids ^>=5.3.5
+
+  if impl(ghc >=9.0)
+    -- these flags may abort compilation with GHC-8.10
+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
 
 -- dump-core
 -- if impl(ghc >= 8.0)
diff --git a/src/Data/RAList.hs b/src/Data/RAList.hs
--- a/src/Data/RAList.hs
+++ b/src/Data/RAList.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Safe #-}
 -- | Random access list.
 --
 -- This module is designed to imported qualifed.
@@ -29,8 +30,8 @@
     itraverse,
     ) where
 
-import Prelude (Maybe (..))
 import Data.RAList.Internal
+import Prelude              (Maybe (..))
 
 import qualified Data.RAList.NonEmpty as NE
 
diff --git a/src/Data/RAList/Internal.hs b/src/Data/RAList/Internal.hs
--- a/src/Data/RAList/Internal.hs
+++ b/src/Data/RAList/Internal.hs
@@ -1,11 +1,13 @@
-{-# LANGUAGE CPP                 #-}
-{-# LANGUAGE DeriveFoldable      #-}
-{-# LANGUAGE DeriveFunctor       #-}
-{-# LANGUAGE DeriveTraversable   #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE InstanceSigs        #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE DeriveFoldable        #-}
+{-# LANGUAGE DeriveFunctor         #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Safe                  #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
 module Data.RAList.Internal (
     RAList (..),
     -- * Showing
@@ -48,6 +50,10 @@
 import qualified Data.Traversable as I (Traversable (..))
 import qualified Test.QuickCheck  as QC
 
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
 import qualified Data.RAList.NonEmpty.Internal as NE
 
 -- $setup
@@ -109,6 +115,19 @@
 #ifdef MIN_VERSION_semigroupoids
 -- Apply, Bind
 #endif
+
+-- | @since 0.2
+instance WI.FunctorWithIndex Int RAList where
+    imap = imap
+
+-- | @since 0.2
+instance WI.FoldableWithIndex Int RAList where
+    ifoldMap = ifoldMap
+    -- ifoldr   = ifoldr -- TODO, PR welcome!
+
+-- | @since 0.2
+instance WI.TraversableWithIndex Int RAList where
+    itraverse = itraverse
 
 -------------------------------------------------------------------------------
 -- Showing
diff --git a/src/Data/RAList/NonEmpty.hs b/src/Data/RAList/NonEmpty.hs
--- a/src/Data/RAList/NonEmpty.hs
+++ b/src/Data/RAList/NonEmpty.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP  #-}
+{-# LANGUAGE Safe #-}
 -- | Non-empty random access list.
 --
 -- This module is designed to imported qualifed.
@@ -40,11 +41,11 @@
 #endif
     ) where
 
-import Prelude (snd)
 import Data.RAList.NonEmpty.Internal
+import Prelude                       (snd)
 
-import Data.RAList.Tree (Leaf (..), Node (..))
 import Data.RAList.Internal (RAList (..))
+import Data.RAList.Tree     (Leaf (..), Node (..))
 
 -- $setup
 -- >>> import Prelude (($))
@@ -62,17 +63,17 @@
 tail :: NERAList a -> RAList a
 tail r = snd (uncons r)
 
--- | 
+-- |
 -- >>> uncons $ fromNonEmpty $ 'a' :| "bcdef"
 -- ('a',fromList "bcdef")
 uncons :: NERAList a -> (a, RAList a)
 uncons (NE (Last  (Lf x)))   = (x, Empty)
 uncons (NE (Cons1 (Lf x) r)) = (x, NonEmpty (NE (Cons0 r)))
-uncons (NE (Cons0        r)) = 
+uncons (NE (Cons0        r)) =
     let (Lf x, r') = unconsTree r in (x, NonEmpty (NE r'))
 
 unconsTree :: NERAList' (Node t) a -> (t a, NERAList' t a)
 unconsTree (Last  (Nd x y))   = (x, Last y)
 unconsTree (Cons1 (Nd x y) r) = (x, Cons1 y (Cons0 r))
-unconsTree (Cons0          r) = 
+unconsTree (Cons0          r) =
     let (Nd x y, r') = unconsTree r in (x, Cons1 y r')
diff --git a/src/Data/RAList/NonEmpty/Internal.hs b/src/Data/RAList/NonEmpty/Internal.hs
--- a/src/Data/RAList/NonEmpty/Internal.hs
+++ b/src/Data/RAList/NonEmpty/Internal.hs
@@ -1,12 +1,14 @@
-{-# LANGUAGE BangPatterns        #-}
-{-# LANGUAGE CPP                 #-}
-{-# LANGUAGE DeriveFoldable      #-}
-{-# LANGUAGE DeriveFunctor       #-}
-{-# LANGUAGE DeriveTraversable   #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE InstanceSigs        #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE BangPatterns          #-}
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE DeriveFoldable        #-}
+{-# LANGUAGE DeriveFunctor         #-}
+{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Safe                  #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
 module Data.RAList.NonEmpty.Internal (
     NERAList (..),
     NERAList' (..),
@@ -61,6 +63,10 @@
 import qualified Data.Traversable   as I (Traversable (..))
 import qualified Test.QuickCheck    as QC
 
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
 #ifdef MIN_VERSION_semigroupoids
 import Data.Functor.Apply (Apply (..))
 
@@ -165,6 +171,19 @@
 #ifdef MIN_VERSION_semigroupoids
 -- Apply, Bind
 #endif
+
+-- | @since 0.2
+instance WI.FunctorWithIndex Int NERAList where
+    imap = imap
+
+-- | @since 0.2
+instance WI.FoldableWithIndex Int NERAList where
+    ifoldMap = ifoldMap
+    -- ifoldr   = ifoldr -- TODO, PR welcome!
+
+-- | @since 0.2
+instance WI.TraversableWithIndex Int NERAList where
+    itraverse = itraverse
 
 -------------------------------------------------------------------------------
 -- Showing
diff --git a/src/Data/RAList/Tree.hs b/src/Data/RAList/Tree.hs
--- a/src/Data/RAList/Tree.hs
+++ b/src/Data/RAList/Tree.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Safe #-}
 module Data.RAList.Tree (
     Leaf (..),
     Node (..),
diff --git a/src/Data/RAList/Tree/Internal.hs b/src/Data/RAList/Tree/Internal.hs
--- a/src/Data/RAList/Tree/Internal.hs
+++ b/src/Data/RAList/Tree/Internal.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE DeriveFunctor     #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE Safe              #-}
 {-# LANGUAGE TypeFamilies      #-}
 module Data.RAList.Tree.Internal (
     Leaf (..),
diff --git a/src/Data/RAVec.hs b/src/Data/RAVec.hs
--- a/src/Data/RAVec.hs
+++ b/src/Data/RAVec.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE TypeFamilies          #-}
@@ -30,6 +31,7 @@
     toList,
     toNonEmpty,
     fromList,
+    reifyList,
     reifyNonEmpty,
 
     -- * Indexing
@@ -44,6 +46,9 @@
     foldr,
     ifoldr,
 
+    -- * Special folds
+    null,
+
     -- * Mapping
     map,
     imap,
@@ -68,7 +73,8 @@
     )  where
 
 import Prelude
-       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Ord (..), Show, ($), (.))
+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Ord (..), Show, ($),
+       (.))
 
 import Control.Applicative (Applicative (..), (<$>))
 import Control.DeepSeq     (NFData (..))
@@ -79,7 +85,6 @@
 import Data.Monoid         (Monoid (..))
 import Data.Semigroup      (Semigroup (..))
 import Data.Type.Bin       (SBin (..), SBinI (..), SBinPI (..))
-import Data.Type.Equality  ((:~:) (..))
 import Data.Typeable       (Typeable)
 
 import qualified Data.RAVec.NonEmpty as NE
@@ -89,6 +94,10 @@
 import qualified Data.Traversable as I (Traversable (..))
 import qualified Test.QuickCheck  as QC
 
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
 #ifdef MIN_VERSION_distributive
 import qualified Data.Distributive as I (Distributive (..))
 
@@ -105,15 +114,18 @@
 #endif
 
 import Data.RAVec.NonEmpty (NERAVec (..))
+import TrustworthyCompat
 
 -- $setup
 -- >>> :set -XScopedTypeVariables -XDataKinds
--- >>> import Prelude (print, Char, Bounded (..))
+-- >>> import Prelude (print, Char, Bounded (..), Maybe (..), (.), ($), Eq (..))
 -- >>> import Data.List (sort)
 -- >>> import Data.Wrd (Wrd (..))
--- >>> import Data.Bin.Pos (top, pop)
+-- >>> import Data.Bin.Pos (Pos (..), top, pop)
 -- >>> import Data.BinP.PosP (PosP (..), PosP' (..))
+-- >>> import Data.List.NonEmpty (NonEmpty (..))
 -- >>> import qualified Data.Bin.Pos as P
+-- >>> import qualified Data.Type.Bin as B
 
 -------------------------------------------------------------------------------
 -- Random access vec
@@ -149,6 +161,19 @@
 instance I.Traversable (RAVec b) where
     traverse = traverse
 
+-- | @since 0.2
+instance WI.FunctorWithIndex (Pos n) (RAVec n) where
+    imap = imap
+
+-- | @since 0.2
+instance WI.FoldableWithIndex (Pos n) (RAVec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+-- | @since 0.2
+instance WI.TraversableWithIndex (Pos n) (RAVec n) where
+    itraverse = itraverse
+
 #ifdef MIN_VERSION_semigroupoids
 instance b ~ 'BP n => I.Foldable1 (RAVec b) where
     foldMap1   = foldMap1
@@ -457,5 +482,5 @@
 
 instance (B.SBinI b, QC.Function a) => QC.Function (RAVec b a) where
     function = case B.sbin :: B.SBin b of
-        SBZ -> QC.functionMap (\Empty -> ())       (\() -> Empty) 
+        SBZ -> QC.functionMap (\Empty -> ())       (\() -> Empty)
         SBP -> QC.functionMap (\(NonEmpty r) -> r) NonEmpty
diff --git a/src/Data/RAVec/NonEmpty.hs b/src/Data/RAVec/NonEmpty.hs
--- a/src/Data/RAVec/NonEmpty.hs
+++ b/src/Data/RAVec/NonEmpty.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE Safe                  #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE TypeFamilies          #-}
@@ -67,13 +68,14 @@
     liftShrink, liftShrink',
     ) where
 
-import Prelude (Bool (..), uncurry, Int, Eq (..), Functor (..), Ord (..), Show, seq, ($), (.))
+import Prelude
+       (Bool (..), Eq (..), Functor (..), Int, Ord (..), Show, seq, uncurry,
+       ($), (.))
 
 import Control.Applicative (Applicative (..), (<$>))
 import Control.DeepSeq     (NFData (..))
 import Data.Bin            (BinP (..))
 import Data.BinP.PosP      (PosP (..), PosP' (..))
-import Data.Coerce         (coerce)
 import Data.Hashable       (Hashable (..))
 import Data.List.NonEmpty  (NonEmpty (..))
 import Data.Monoid         (Monoid (..))
@@ -91,6 +93,10 @@
 import qualified Data.Traversable as I (Traversable (..))
 import qualified Test.QuickCheck  as QC
 
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
 #ifdef MIN_VERSION_distributive
 import qualified Data.Distributive as I (Distributive (..))
 
@@ -106,7 +112,8 @@
 import qualified Data.Semigroup.Traversable as I (Traversable1 (..))
 #endif
 
-import Data.RAVec.Tree (Tree (..))
+import Data.RAVec.Tree   (Tree (..))
+import TrustworthyCompat
 
 -- $setup
 -- >>> :set -XScopedTypeVariables -XDataKinds
@@ -168,6 +175,32 @@
 
 instance I.Traversable (NERAVec' n b) where
     traverse = traverse'
+
+-- | @since 0.2
+instance WI.FunctorWithIndex (PosP n) (NERAVec n) where
+    imap = imap
+
+-- | @since 0.2
+instance WI.FoldableWithIndex (PosP n) (NERAVec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+-- | @since 0.2
+instance WI.TraversableWithIndex (PosP n) (NERAVec n) where
+    itraverse = itraverse
+
+-- | @since 0.2
+instance WI.FunctorWithIndex (PosP' n m) (NERAVec' n m) where
+    imap = imap'
+
+-- | @since 0.2
+instance WI.FoldableWithIndex (PosP' n m) (NERAVec' n m) where
+    ifoldMap = ifoldMap'
+    ifoldr   = ifoldr'
+
+-- | @since 0.2
+instance WI.TraversableWithIndex (PosP' n m) (NERAVec' n m) where
+    itraverse = itraverse'
 
 #ifdef MIN_VERSION_semigroupoids
 instance I.Foldable1 (NERAVec b) where
diff --git a/src/Data/RAVec/Tree.hs b/src/Data/RAVec/Tree.hs
--- a/src/Data/RAVec/Tree.hs
+++ b/src/Data/RAVec/Tree.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs                  #-}
 {-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE Safe                   #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE StandaloneDeriving     #-}
 {-# LANGUAGE TypeFamilies           #-}
@@ -18,6 +19,7 @@
 
     -- * Conversions
     toList,
+    reverse,
 
     -- * Indexing
     (!),
@@ -36,7 +38,12 @@
     ifoldr1Map,
     foldl,
     ifoldl,
+
+    -- * Special folds
     length,
+    null,
+    sum,
+    product,
 
     -- * Mapping
     map,
@@ -47,7 +54,7 @@
     traverse1,
     itraverse1,
 #endif
-    -- TODO: itraverse_,
+    itraverse_,
 
     -- * Zipping
     zipWith,
@@ -60,15 +67,15 @@
     -- * QuickCheck
     liftArbitrary,
     liftShrink,
-
     ) where
 
 import Prelude
-       (Bool (..), Eq (..), Functor (..), Int, Ord (..), Show, id, seq,
-       uncurry, ($), (*), (.))
+       (Bool (..), Eq (..), Functor (..), Int, Num, Ord (..), Show, id, seq,
+       uncurry, ($), (*), (+), (.))
 
 import Control.Applicative (Applicative (..), (<$>))
 import Control.DeepSeq     (NFData (..))
+import Control.Monad       (void)
 import Data.Hashable       (Hashable (..))
 import Data.Monoid         (Monoid (..))
 import Data.Nat            (Nat (..))
@@ -83,6 +90,10 @@
 import qualified Data.Traversable as I (Traversable (..))
 import qualified Test.QuickCheck  as QC
 
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
 #ifdef MIN_VERSION_distributive
 import qualified Data.Distributive as I (Distributive (..))
 
@@ -101,7 +112,9 @@
 -- $setup
 -- >>> :set -XScopedTypeVariables
 -- >>> import Data.Proxy (Proxy (..))
--- >>> import Prelude (Char, not, uncurry, flip)
+-- >>> import Prelude (Char, not, uncurry, flip, ($), Bool (..))
+-- >>> import Data.Wrd (Wrd (..))
+-- >>> import qualified Data.Type.Nat as N
 
 -------------------------------------------------------------------------------
 -- Data
@@ -139,7 +152,7 @@
     foldr   = foldr
     foldl   = foldl
 #if MIN_VERSION_base(4,8,0)
-    null _ = False
+    null   = null
     toList = toList
     length = length
 #endif
@@ -147,6 +160,19 @@
 instance I.Traversable (Tree n) where
     traverse = traverse
 
+-- | @since 0.2
+instance WI.FunctorWithIndex (Wrd n) (Tree n) where
+    imap = imap
+
+-- | @since 0.2
+instance WI.FoldableWithIndex (Wrd n) (Tree n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+-- | @since 0.2
+instance WI.TraversableWithIndex (Wrd n) (Tree n) where
+    itraverse = itraverse
+
 #ifdef MIN_VERSION_semigroupoids
 instance I.Foldable1 (Tree n) where
     foldMap1 = foldMap1
@@ -175,6 +201,8 @@
     liftA2 = zipWith
 #endif
 
+-- TODO: Monad
+
 #ifdef MIN_VERSION_distributive
 instance N.SNatI n => I.Distributive (Tree n) where
     distribute f = tabulate (\k -> fmap (! k) f)
@@ -249,6 +277,21 @@
 rightmost (Node _ y) = rightmost y
 
 -------------------------------------------------------------------------------
+-- Reverse
+-------------------------------------------------------------------------------
+
+-- | Reverse 'Tree'.
+--
+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
+-- >>> reverse t
+-- Node (Node (Leaf 'd') (Leaf 'c')) (Node (Leaf 'b') (Leaf 'a'))
+--
+-- @since 0.1.1
+reverse :: Tree n a -> Tree n a
+reverse t@(Leaf _) = t
+reverse (Node x y) = Node (reverse y) (reverse x)
+
+-------------------------------------------------------------------------------
 -- Folds
 -------------------------------------------------------------------------------
 
@@ -296,8 +339,14 @@
 ifoldl f z (Leaf x)   = f WE z x
 ifoldl f z (Node x y) = ifoldl (goLeft f) (ifoldl (goRight f) z x) y
 
--- TODO: foldl
+-------------------------------------------------------------------------------
+-- Special folds
+-------------------------------------------------------------------------------
 
+-- | @since 0.1.1
+null :: Tree n a -> Bool
+null _ = False
+
 -- | >>> length (universe :: Tree N.Nat3 (Wrd N.Nat3))
 -- 8
 --
@@ -307,6 +356,20 @@
     go !acc (Leaf _)   = acc
     go  acc (Node x _) = go (2 * acc) x
 
+-- | Non-strict 'sum'.
+--
+-- @since 0.1.1
+sum :: Num a => Tree n a -> a
+sum (Leaf a)   = a
+sum (Node x y) = sum x + sum y
+
+-- | Non-strict 'product'.
+--
+-- @since 0.1.1
+product :: Num a => Tree n a -> a
+product (Leaf a)   = a
+product (Node x y) = product x * product y
+
 -------------------------------------------------------------------------------
 -- Mapping
 -------------------------------------------------------------------------------
@@ -340,6 +403,12 @@
 itraverse1 f (Leaf x)   = Leaf <$> f WE x
 itraverse1 f (Node x y) = Node <$> itraverse1 (goLeft f) x <.> itraverse1 (goRight f) y
 #endif
+
+-- |
+-- @since 0.1.1
+itraverse_ :: forall n f a b. Applicative f => (Wrd n -> a -> f b) -> Tree n a -> f ()
+itraverse_ f (Leaf x)   = void (f WE x)
+itraverse_ f (Node x y) = itraverse_ (f . W0) x *> itraverse_ (f . W1) y
 
 -------------------------------------------------------------------------------
 -- Zipping
diff --git a/src/Data/RAVec/Tree/DF.hs b/src/Data/RAVec/Tree/DF.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/RAVec/Tree/DF.hs
@@ -0,0 +1,726 @@
+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE DeriveDataTypeable     #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE Safe                   #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+-- | Depth indexed perfect tree as data family.
+module Data.RAVec.Tree.DF (
+    Tree (..),
+
+    -- * Construction
+    singleton,
+
+    -- * Conversions
+    toList,
+    reverse,
+
+    -- * Indexing
+    (!),
+    tabulate,
+    leftmost,
+    rightmost,
+
+    -- * Folds
+    foldMap,
+    foldMap1,
+    ifoldMap,
+    ifoldMap1,
+    foldr,
+    ifoldr,
+    foldr1Map,
+    ifoldr1Map,
+    foldl,
+    ifoldl,
+
+    -- * Special folds
+    length,
+    null,
+    sum,
+    product,
+
+    -- * Mapping
+    map,
+    imap,
+    traverse,
+    itraverse,
+#ifdef MIN_VERSION_semigroupoids
+    traverse1,
+    itraverse1,
+#endif
+    itraverse_,
+
+    -- * Zipping
+    zipWith,
+    izipWith,
+    repeat,
+
+    -- * Universe
+    universe,
+
+    -- * QuickCheck
+    liftArbitrary,
+    liftShrink,
+
+    -- * Ensure spine
+    ensureSpine,
+) where
+
+import Prelude
+       (Bool (..), Eq (..), Functor (..), Int, Num, Ord (..), Ordering (..),
+       Show (..), ShowS, flip, id, seq, showChar, showParen, showString,
+       uncurry, ($), (&&), (*), (+), (.))
+
+import Control.Applicative (Applicative (..), liftA2, (<$>))
+import Control.DeepSeq     (NFData (..))
+import Control.Monad       (void)
+import Data.Hashable       (Hashable (..))
+import Data.Monoid         (Monoid (..))
+import Data.Nat            (Nat (..))
+import Data.Semigroup      (Semigroup (..))
+import Data.Wrd            (Wrd (..))
+
+import qualified Data.Type.Nat as N
+
+-- instances
+import qualified Data.Foldable    as I (Foldable (..))
+import qualified Data.Traversable as I (Traversable (..))
+import qualified Test.QuickCheck  as QC
+
+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))
+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))
+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))
+
+#ifdef MIN_VERSION_distributive
+import qualified Data.Distributive as I (Distributive (..))
+
+#ifdef MIN_VERSION_adjunctions
+import qualified Data.Functor.Rep as I (Representable (..))
+#endif
+#endif
+
+#ifdef MIN_VERSION_semigroupoids
+import Data.Functor.Apply (Apply (..))
+
+import qualified Data.Semigroup.Foldable    as I (Foldable1 (..))
+import qualified Data.Semigroup.Traversable as I (Traversable1 (..))
+#endif
+
+-- $setup
+-- >>> :set -XScopedTypeVariables
+-- >>> import Data.Proxy (Proxy (..))
+-- >>> import Prelude (Char, not, uncurry, flip, error, ($), Bool (..), id)
+-- >>> import Data.Wrd (Wrd (..))
+-- >>> import qualified Data.Type.Nat as N
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+data family Tree (n :: Nat) a
+
+newtype instance Tree 'Z     a = Leaf a
+data instance    Tree ('S n) a = Node (Tree n a) (Tree n a)
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance (Eq a, N.SNatI n) => Eq (Tree n a) where
+    (==) = getEqual (N.induction1 start step) where
+        start :: Equal 'Z a
+        start = Equal $ \(Leaf x) (Leaf y) -> x == y
+
+        step :: Equal m a -> Equal ('S m) a
+        step (Equal go) = Equal $ \(Node x1 y1) (Node x2 y2) ->
+            go x1 x2 && go y1 y2
+
+newtype Equal n a = Equal { getEqual :: Tree n a -> Tree n a -> Bool }
+
+instance (Ord a, N.SNatI n) => Ord (Tree n a) where
+    compare = getCompare (N.induction1 start step) where
+        start :: Compare 'Z a
+        start = Compare $ \(Leaf x) (Leaf y) -> compare x y
+
+        step :: Compare m a -> Compare ('S m) a
+        step (Compare go) = Compare $ \(Node x1 y1) (Node x2 y2) ->
+            go x1 x2 <> go y1 y2
+
+newtype Compare n a = Compare { getCompare :: Tree n a -> Tree n a -> Ordering }
+
+instance (Show a, N.SNatI n) => Show (Tree n a) where
+    showsPrec = getShowsPrec (N.induction1 start step) where
+        start :: ShowsPrec 'Z a
+        start = ShowsPrec $ \d (Leaf x) -> showParen (d > 10)
+            $ showString "Leaf "
+            . showsPrec 11 x
+
+        step :: ShowsPrec m a -> ShowsPrec ('S m) a
+        step (ShowsPrec go) = ShowsPrec $ \d (Node x y) -> showParen (d > 10)
+            $ showString "Node "
+            . go 11 x
+            . showChar ' '
+            . go 11 y
+
+newtype ShowsPrec n a = ShowsPrec { getShowsPrec :: Int -> Tree n a -> ShowS }
+
+instance N.SNatI n => Functor (Tree n) where
+    fmap = map
+
+instance N.SNatI n => I.Foldable (Tree n) where
+    foldMap = foldMap
+
+    foldr  = foldr
+    -- foldl' = foldl'
+
+#if MIN_VERSION_base(4,8,0)
+    null    = null
+    length  = length
+    sum     = sum
+    product = product
+#endif
+
+#ifdef MIN_VERSION_semigroupoids
+instance (N.SNatI n) => I.Foldable1 (Tree n) where
+    foldMap1 = foldMap1
+
+instance (N.SNatI n) => I.Traversable1 (Tree n) where
+    traverse1 = traverse1
+#endif
+
+instance N.SNatI n => I.Traversable (Tree n) where
+    traverse = traverse
+
+-- | @since 0.2
+instance N.SNatI n => WI.FunctorWithIndex (Wrd n) (Tree n) where
+    imap = imap
+
+-- | @since 0.2
+instance N.SNatI n => WI.FoldableWithIndex (Wrd n) (Tree n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+-- | @since 0.2
+instance N.SNatI n => WI.TraversableWithIndex (Wrd n) (Tree n) where
+    itraverse = itraverse
+
+instance (NFData a, N.SNatI n) => NFData (Tree n a) where
+    rnf = getRnf (N.induction1 z s) where
+        z           = Rnf $ \(Leaf x)   -> rnf x
+        s (Rnf rec) = Rnf $ \(Node x y) -> rec x `seq` rec y
+
+newtype Rnf n a = Rnf { getRnf :: Tree n a -> () }
+
+instance (Hashable a, N.SNatI n) => Hashable (Tree n a) where
+    hashWithSalt = getHashWithSalt (N.induction1 z s) where
+        z = HashWithSalt $ \salt (Leaf x) -> salt `hashWithSalt` x
+        s (HashWithSalt rec) = HashWithSalt $ \salt (Node x y) -> rec (rec salt x) y
+
+newtype HashWithSalt n a = HashWithSalt { getHashWithSalt :: Int -> Tree n a -> Int }
+
+instance N.SNatI n => Applicative (Tree n) where
+    pure = repeat
+    (<*>)  = zipWith ($)
+    _ *> x = x
+    x <* _ = x
+#if MIN_VERSION_base(4,10,0)
+    liftA2 = zipWith
+#endif
+
+-- TODO: Monad
+
+#ifdef MIN_VERSION_distributive
+instance N.SNatI n => I.Distributive (Tree n) where
+    distribute f = tabulate (\k -> fmap (! k) f)
+
+#ifdef MIN_VERSION_adjunctions
+instance N.SNatI n => I.Representable (Tree n) where
+    type Rep (Tree n) = Wrd n
+    tabulate = tabulate
+    index    = (!)
+#endif
+#endif
+
+instance (Semigroup a, N.SNatI n) => Semigroup (Tree n a) where
+    (<>) = zipWith (<>)
+
+instance (Monoid a, N.SNatI n) => Monoid (Tree n a) where
+    mempty = pure mempty
+    mappend = zipWith mappend
+
+#ifdef MIN_VERSION_semigroupoids
+instance N.SNatI n => Apply (Tree n) where
+    (<.>) = zipWith ($)
+    _ .> x = x
+    x <. _ = x
+    liftF2 = zipWith
+
+-- TODO: Bind
+#endif
+
+-------------------------------------------------------------------------------
+-- Construction
+-------------------------------------------------------------------------------
+
+-- | 'Tree' with exactly one element.
+--
+-- >>> singleton True
+-- Leaf True
+--
+singleton :: a -> Tree 'Z a
+singleton = Leaf
+
+-------------------------------------------------------------------------------
+-- Conversions
+-------------------------------------------------------------------------------
+
+-- | Convert 'Tree' to list.
+--
+-- >>> toList $ Node (Node (Leaf 'f') (Leaf 'o')) (Node (Leaf 'o') (Leaf 'd'))
+-- "food"
+toList :: forall n a. N.SNatI n => Tree n a -> [a]
+toList xs = getToList (N.induction1 start step) xs [] where
+    start :: ToList 'Z a
+    start = ToList (\(Leaf x) -> (x :))
+
+    step :: ToList m a -> ToList ('S m) a
+    step (ToList f) = ToList $ \(Node x y) -> f x . f y
+
+newtype ToList n a = ToList { getToList :: Tree n a -> [a] -> [a] }
+
+-------------------------------------------------------------------------------
+-- Indexing
+-------------------------------------------------------------------------------
+
+flipIndex :: N.SNatI n => Wrd n -> Tree n a -> a
+flipIndex = getIndex (N.induction1 start step) where
+    start :: Index 'Z a
+    start = Index $ \_ (Leaf x) -> x
+
+    step :: Index m a-> Index ('N.S m) a
+    step (Index go) = Index $ \i (Node x y) -> case i of
+        W0 j -> go j x
+        W1 j -> go j y
+
+newtype Index n a = Index { getIndex :: Wrd n -> Tree n a -> a }
+
+-- | Indexing.
+--
+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
+-- >>> t ! W1 (W0 WE)
+-- 'c'
+--
+(!) :: N.SNatI n => Tree n a -> Wrd n -> a
+(!) = flip flipIndex
+
+-- | Tabulating, inverse of '!'.
+--
+-- >>> tabulate id :: Tree N.Nat2 (Wrd N.Nat2)
+-- Node (Node (Leaf 0b00) (Leaf 0b01)) (Node (Leaf 0b10) (Leaf 0b11))
+tabulate :: N.SNatI n => (Wrd n -> a) -> Tree n a
+tabulate = getTabulate (N.induction1 start step) where
+    start :: Tabulate 'Z a
+    start = Tabulate $ \f -> Leaf (f WE)
+
+    step :: Tabulate m a -> Tabulate ('S m) a
+    step (Tabulate go) = Tabulate $ \f -> Node (go (f . W0)) (go (f . W1))
+
+newtype Tabulate n a = Tabulate { getTabulate :: (Wrd n -> a) -> Tree n a }
+
+leftmost :: N.SNatI n => Tree n a -> a
+leftmost = getTheMost (N.induction1 start step) where
+    start :: TheMost 'Z a
+    start = TheMost $ \(Leaf x) -> x
+
+    step :: TheMost m a -> TheMost ('S m) a
+    step (TheMost go) = TheMost $ \(Node x _) -> go x
+
+rightmost :: N.SNatI n => Tree n a -> a
+rightmost = getTheMost (N.induction1 start step) where
+    start :: TheMost 'Z a
+    start = TheMost $ \(Leaf x) -> x
+
+    step :: TheMost m a -> TheMost ('S m) a
+    step (TheMost go) = TheMost $ \(Node _ y) -> go y
+
+newtype TheMost n a = TheMost { getTheMost :: Tree n a -> a }
+
+-------------------------------------------------------------------------------
+-- Reverse
+-------------------------------------------------------------------------------
+
+-- | Reverse 'Tree'.
+--
+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
+-- >>> reverse t
+-- Node (Node (Leaf 'd') (Leaf 'c')) (Node (Leaf 'b') (Leaf 'a'))
+--
+reverse :: forall n a. N.SNatI n => Tree n a -> Tree n a
+reverse = getReverse (N.induction1 start step) where
+    start :: Reverse 'Z a
+    start = Reverse id
+
+    step :: N.SNatI m => Reverse m a -> Reverse ('S m) a
+    step (Reverse go) = Reverse $ \(Node x y) -> Node (go y) (go x)
+
+newtype Reverse n a = Reverse { getReverse :: Tree n a -> Tree n a }
+
+-------------------------------------------------------------------------------
+-- Mapping
+-------------------------------------------------------------------------------
+
+-- | >>> map not $ Node (Leaf True) (Leaf False)
+-- Node (Leaf False) (Leaf True)
+--
+map :: forall a b n. N.SNatI n => (a -> b) -> Tree n a -> Tree n b
+map f = getMap $ N.induction1 start step where
+    start :: Map a 'Z b
+    start = Map $ \(Leaf x) -> Leaf (f x)
+
+    step :: Map a m b -> Map a ('S m) b
+    step (Map go) = Map $ \(Node x y) -> Node (go x) (go y)
+
+newtype Map a n b = Map { getMap :: Tree n a -> Tree n b }
+
+-- |
+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))
+-- >>> imap (,) t
+-- Node (Node (Leaf (0b00,'a')) (Leaf (0b01,'b'))) (Node (Leaf (0b10,'c')) (Leaf (0b11,'d')))
+--
+imap :: N.SNatI n => (Wrd n -> a -> b) -> Tree n a -> Tree n b
+imap = getIMap $ N.induction1 start step where
+    start :: IMap a 'Z b
+    start = IMap $ \f (Leaf x) -> Leaf (f WE x)
+
+    step :: IMap a m b -> IMap a ('S m) b
+    step (IMap go) = IMap $ \f (Node x y) ->
+        Node (go (f . W0) x) (go (f . W1) y)
+
+newtype IMap a n b = IMap { getIMap :: (Wrd n -> a -> b) -> Tree n a -> Tree n b }
+
+-- | Apply an action to every element of a 'Tree', yielding a 'Tree' of results.
+traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Tree n a -> f (Tree n b)
+traverse f =  getTraverse $ N.induction1 start step where
+    start :: Traverse f a 'Z b
+    start = Traverse $ \(Leaf x) -> Leaf <$> f x
+
+    step :: Traverse f a m b -> Traverse f a ('S m) b
+    step (Traverse go) = Traverse $ \(Node x y) -> liftA2 Node (go x) (go y)
+{-# INLINE traverse #-}
+
+newtype Traverse f a n b = Traverse { getTraverse :: Tree n a -> f (Tree n b) }
+
+-- | Apply an action to every element of a 'Tree' and its index, yielding a 'Tree' of results.
+itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
+itraverse = getITraverse $ N.induction1 start step where
+    start :: ITraverse f a 'Z b
+    start = ITraverse $ \f (Leaf x) -> Leaf <$> f WE x
+
+    step :: ITraverse f a m b -> ITraverse f a ('S m) b
+    step (ITraverse go) = ITraverse $ \f (Node x y) -> liftA2 Node (go (f . W0) x) (go (f . W1) y)
+{-# INLINE itraverse #-}
+
+newtype ITraverse f a n b = ITraverse { getITraverse :: (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b) }
+
+#ifdef MIN_VERSION_semigroupoids
+-- | Apply an action to non-empty 'Tree', yielding a 'Tree' of results.
+traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Tree n a -> f (Tree n b)
+traverse1 f = getTraverse $ N.induction1 start step where
+    start :: Traverse f a 'Z b
+    start = Traverse $ \(Leaf x) -> Leaf <$> f x
+
+    step :: Traverse f a m b -> Traverse f a ('S m) b
+    step (Traverse go) = Traverse $ \(Node x y) -> liftF2 Node (go x) (go y)
+{-# INLINE traverse1 #-}
+
+itraverse1 :: forall n f a b. (Apply f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)
+itraverse1 = getITraverse $ N.induction1 start step where
+    start :: ITraverse f a 'Z b
+    start = ITraverse $ \f (Leaf x) -> Leaf <$> f WE x
+
+    step :: ITraverse f a m b -> ITraverse f a ('S m) b
+    step (ITraverse go) = ITraverse $ \f (Node x y) -> liftF2 Node (go (f . W0) x) (go (f . W1) y)
+{-# INLINE itraverse1 #-}
+#endif
+
+-- | Apply an action to every element of a 'Tree' and its index, ignoring the results.
+itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f ()
+itraverse_ = getITraverse_ $ N.induction1 start step where
+    start :: ITraverse_ f a 'Z b
+    start = ITraverse_ $ \f (Leaf x) -> void (f WE x)
+
+    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b
+    step (ITraverse_ go) = ITraverse_ $ \f (Node x y) -> go (f . W0) x *> go (f . W1) y
+
+newtype ITraverse_ f a n b = ITraverse_ { getITraverse_ :: (Wrd n -> a -> f b) -> Tree n a -> f () }
+
+-------------------------------------------------------------------------------
+-- Folding
+-------------------------------------------------------------------------------
+
+-- | See 'I.Foldable'.
+foldMap :: forall a n m. (Monoid m, N.SNatI n) => (a -> m) -> Tree n a -> m
+foldMap f = getFold (N.induction1 start step) where
+    start :: Fold a 'Z m
+    start = Fold $ \(Leaf x) -> f x
+
+    step :: Fold a p m -> Fold a ('S p) m
+    step (Fold g) = Fold $ \(Node x y) -> g x `mappend` g y
+
+newtype Fold a n b = Fold  { getFold  :: Tree n a -> b }
+
+-- | See 'I.Foldable1'.
+foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Tree n a -> s
+foldMap1 f = getFold $ N.induction1 start step where
+    start :: Fold a 'Z s
+    start = Fold $ \(Leaf x) -> f x
+
+    step :: Fold a m s -> Fold a ('S m) s
+    step (Fold g) = Fold $ \(Node x y) -> g x <> g y
+
+-- | See 'I.FoldableWithIndex'.
+ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Wrd n -> a -> m) -> Tree n a -> m
+ifoldMap = getIFoldMap $ N.induction1 start step where
+    start :: IFoldMap a 'Z m
+    start = IFoldMap $ \f (Leaf x) -> f WE x
+
+    step :: IFoldMap a p m -> IFoldMap a ('S p) m
+    step (IFoldMap go) = IFoldMap $ \f (Node x y) -> go (f . W0) x `mappend` go (f . W1) y
+
+newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Wrd n -> a -> m) -> Tree n a -> m }
+
+-- | There is no type-class for this :(
+ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Wrd ('S n) -> a -> s) -> Tree ('S n) a -> s
+ifoldMap1 = getIFoldMap $ N.induction1 start step where
+    start :: IFoldMap a 'Z m
+    start = IFoldMap $ \f (Leaf x) -> f WE x
+
+    step :: IFoldMap a p s -> IFoldMap a ('S p) s
+    step (IFoldMap go) = IFoldMap $ \f (Node x y) -> go (f . W0) x <> go (f . W1) y
+
+
+
+
+-- | Right fold.
+foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Tree n a -> b
+foldr f = getFoldr (N.induction1 start step) where
+    start :: Foldr a 'Z b
+    start = Foldr $ \z (Leaf x) -> f x z
+
+    step :: Foldr a m b -> Foldr a ('S m) b
+    step (Foldr go) = Foldr $ \z (Node x y) -> go (go z y) x
+
+newtype Foldr a n b = Foldr { getFoldr :: b -> Tree n a -> b }
+
+-- | Right fold with an index.
+ifoldr :: forall a b n. N.SNatI n => (Wrd n -> a -> b -> b) -> b -> Tree n a -> b
+ifoldr = getIFoldr $ N.induction1 start step where
+    start :: IFoldr a 'Z b
+    start = IFoldr $ \f z (Leaf x) -> f WE x z
+
+    step :: IFoldr a m b -> IFoldr a ('S m) b
+    step (IFoldr go) = IFoldr $ \f z (Node x y) -> go (f . W0) (go (f . W1) z y) x
+
+newtype IFoldr a n b = IFoldr { getIFoldr :: (Wrd n -> a -> b -> b) -> b -> Tree n a -> b }
+
+foldr1Map :: forall a b n. N.SNatI n => (a -> b -> b) -> (a -> b) -> Tree n a -> b
+foldr1Map f = getFoldr1 (N.induction1 start step) where
+    start :: Foldr1 a 'Z b
+    start = Foldr1 $ \z (Leaf x) -> z x
+
+    step :: Foldr1 a m b -> Foldr1 a ('S m) b
+    step (Foldr1 go) = Foldr1 $ \z (Node x y) -> go (\z0 -> f z0 (go z y)) x
+
+newtype Foldr1 a n b = Foldr1 { getFoldr1 :: (a -> b) -> Tree n a -> b }
+
+ifoldr1Map :: (Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b
+ifoldr1Map = ifoldr1Map
+
+-- | Left fold.
+foldl :: forall a b n. N.SNatI n => (b -> a -> b) -> b -> Tree n a -> b
+foldl f = getFoldl (N.induction1 start step) where
+    start :: Foldl a 'Z b
+    start = Foldl $ \z (Leaf x) -> f z x
+
+    step :: Foldl a m b -> Foldl a ('S m) b
+    step (Foldl go) = Foldl $ \z (Node x y) -> go (go z x) y
+
+newtype Foldl a n b = Foldl { getFoldl :: b -> Tree n a -> b }
+
+-- | Left fold with an index.
+ifoldl :: forall a b n. N.SNatI n => (Wrd n -> b -> a -> b) -> b -> Tree n a -> b
+ifoldl = getIFoldl $ N.induction1 start step where
+    start :: IFoldl a 'Z b
+    start = IFoldl $ \f z (Leaf x) -> f WE z x
+
+    step :: IFoldl a m b -> IFoldl a ('S m) b
+    step (IFoldl go) = IFoldl $ \f z (Node x y) -> go (f . W0) (go (f . W1) z x) y
+
+newtype IFoldl a n b = IFoldl { getIFoldl :: (Wrd n -> b -> a -> b) -> b -> Tree n a -> b }
+
+-- | Yield the length of a 'Tree'. /O(n)/
+length :: forall n a. N.SNatI n => Tree n a -> Int
+length _ = getLength l where
+    l :: Length n
+    l = N.induction (Length 1) $ \(Length n) -> Length (2 * n)
+
+newtype Length (n :: Nat) = Length { getLength :: Int }
+
+-- | Test whether a 'Tree' is empty. It never is. /O(1)/
+null :: Tree n a -> Bool
+null _ = False
+
+-------------------------------------------------------------------------------
+-- Special folds
+-------------------------------------------------------------------------------
+
+-- | Non-strict 'sum'.
+sum :: (Num a, N.SNatI n) => Tree n a -> a
+sum = getFold $ N.induction1 start step where
+    start :: Num a => Fold a 'Z a
+    start = Fold $ \(Leaf x) -> x
+
+    step :: Num a => Fold a m a -> Fold a ('S m) a
+    step (Fold f) = Fold $ \(Node x y) -> f x + f y
+
+-- | Non-strict 'product'.
+product :: (Num a, N.SNatI n) => Tree n a -> a
+product = getFold $ N.induction1 start step where
+    start :: Num a => Fold a 'Z a
+    start = Fold $ \(Leaf x) -> x
+
+    step :: Num a => Fold a m a -> Fold a ('S m) a
+    step (Fold f) = Fold $ \(Node x y) -> f x * f y
+
+-------------------------------------------------------------------------------
+-- Zipping
+-------------------------------------------------------------------------------
+
+-- | Zip two 'Tree's with a function.
+zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
+zipWith f = getZipWith $ N.induction start step where
+    start :: ZipWith a b c 'Z
+    start = ZipWith $ \(Leaf x) (Leaf y) -> Leaf (f x y)
+
+    step :: ZipWith a b c m -> ZipWith a b c ('S m)
+    step (ZipWith go) = ZipWith $ \(Node x y) (Node u v) -> Node (go x u) (go y v)
+
+newtype ZipWith a b c n = ZipWith { getZipWith :: Tree n a -> Tree n b -> Tree n c }
+
+-- | Zip two 'Tree's. with a function that also takes the elements' indices.
+izipWith :: N.SNatI n => (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c
+izipWith = getIZipWith $ N.induction start step where
+    start :: IZipWith a b c 'Z
+    start = IZipWith $ \f (Leaf x) (Leaf y) -> Leaf (f WE x y)
+
+    step :: IZipWith a b c m -> IZipWith a b c ('S m)
+    step (IZipWith go) = IZipWith $ \f (Node x y) (Node u v) -> Node (go (f . W0) x u) (go (f . W1) y v)
+
+newtype IZipWith a b c n = IZipWith { getIZipWith :: (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c }
+
+-- | Repeat value
+--
+-- >>> repeat 'x' :: Tree N.Nat2 Char
+-- Node (Node (Leaf 'x') (Leaf 'x')) (Node (Leaf 'x') (Leaf 'x'))
+--
+repeat :: N.SNatI n => x -> Tree n x
+repeat x = N.induction1 (Leaf x) $ \t -> Node t t
+
+-------------------------------------------------------------------------------
+-- Monadic
+-------------------------------------------------------------------------------
+
+-- TODO
+
+-------------------------------------------------------------------------------
+-- universe
+-------------------------------------------------------------------------------
+
+-- | Get all @'Wrd' n@ in a @'Tree' n@.
+--
+-- >>> universe :: Tree N.Nat2 (Wrd N.Nat2)
+-- Node (Node (Leaf 0b00) (Leaf 0b01)) (Node (Leaf 0b10) (Leaf 0b11))
+universe :: N.SNatI n => Tree n (Wrd n)
+universe = tabulate id
+
+-------------------------------------------------------------------------------
+-- EnsureSpine
+-------------------------------------------------------------------------------
+
+-- | Ensure spine.
+--
+-- If we have an undefined 'Tree',
+--
+-- >>> let v = error "err" :: Tree N.Nat2 Char
+--
+-- And insert data into it later:
+--
+-- >>> let setHead :: a -> Tree N.Nat2 a -> Tree N.Nat2 a; setHead x (Node (Node _ u) v) = Node (Node (Leaf x) u) v
+--
+-- Then without a spine, it will fail:
+--
+-- >>> leftmost $ setHead 'x' v
+-- *** Exception: err
+-- ...
+--
+-- But with the spine, it won't:
+--
+-- >>> leftmost $ setHead 'x' $ ensureSpine v
+-- 'x'
+--
+ensureSpine :: N.SNatI n => Tree n a -> Tree n a
+ensureSpine = getEnsureSpine (N.induction1 first step) where
+    first :: EnsureSpine 'Z a
+    first = EnsureSpine $ \ ~(Leaf x) -> Leaf x
+
+    step :: EnsureSpine m a -> EnsureSpine ('S m) a
+    step (EnsureSpine go) = EnsureSpine $ \ ~(Node x y) -> Node (go x) (go y)
+
+newtype EnsureSpine n a = EnsureSpine { getEnsureSpine :: Tree n a -> Tree n a }
+
+-------------------------------------------------------------------------------
+-- QuickCheck
+-------------------------------------------------------------------------------
+
+instance N.SNatI n => QC.Arbitrary1 (Tree n) where
+    liftArbitrary = liftArbitrary
+    liftShrink    = liftShrink
+
+liftArbitrary :: forall n a. N.SNatI n => QC.Gen a -> QC.Gen (Tree n a)
+liftArbitrary arb = getArb $ N.induction1 start step where
+    start :: Arb 'Z a
+    start = Arb $ Leaf <$> arb
+
+    step :: Arb m a -> Arb ('S m) a
+    step (Arb rec) = Arb $ liftA2 Node rec rec
+
+newtype Arb n a = Arb { getArb :: QC.Gen (Tree n a) }
+
+liftShrink :: forall n a. N.SNatI n => (a -> [a]) -> Tree n a -> [Tree n a]
+liftShrink shr = getShr $ N.induction1 start step where
+    start :: Shr 'Z a
+    start = Shr $ \(Leaf x) ->Leaf <$> shr x
+
+    step :: Shr m a -> Shr ('S m) a
+    step (Shr rec) = Shr $ \(Node x y) ->
+        uncurry Node <$> QC.liftShrink2 rec rec (x, y)
+
+newtype Shr n a = Shr { getShr :: Tree n a -> [Tree n a] }
+
+instance (N.SNatI n, QC.Arbitrary a) => QC.Arbitrary (Tree n a) where
+    arbitrary = QC.arbitrary1
+    shrink    = QC.shrink1
+
+instance (N.SNatI n, QC.CoArbitrary a) => QC.CoArbitrary (Tree n a) where
+    coarbitrary v = case N.snat :: N.SNat n of
+        N.SZ -> QC.variant (0 :: Int) . (case v of (Leaf x) -> QC.coarbitrary x)
+        N.SS -> QC.variant (1 :: Int) . (case v of (Node x y) -> QC.coarbitrary (x, y))
+
+instance (N.SNatI n, QC.Function a) => QC.Function (Tree n a) where
+    function = case N.snat :: N.SNat n of
+        N.SZ -> QC.functionMap (\(Leaf x) -> x) Leaf
+        N.SS -> QC.functionMap (\(Node x y) -> (x, y)) (\(x,y) -> Node x y)
diff --git a/src/TrustworthyCompat.hs b/src/TrustworthyCompat.hs
new file mode 100644
--- /dev/null
+++ b/src/TrustworthyCompat.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE Trustworthy #-}
+module TrustworthyCompat (
+    (:~:) (..),
+    TestEquality (..),
+    coerce,
+) where
+
+import Data.Coerce        (coerce)
+import Data.Type.Equality (TestEquality (..), (:~:) (..))