diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,79 +1,84 @@
-# 0.8.1.0
-
-- Add `(Fcf.Combinators.>>=)`
-- Resolve warnings about deprecated `TypeInType`
-
-# 0.8.0.1
-
-- Bump upper bounds for GHC 9.0
-- Update doctests for cabal-docspec
-
-# 0.8.0.0
-
-- Add modules
-    + `Fcf.Data.Symbol` (currently just reexports `Symbol`) (thanks to gspia)
-    + `Fcf.Data.Function`
-    + "Overloaded type families" ("type-level type classes")
-        * `Fcf.Class.Ord`
-        * `Fcf.Class.Monoid`
-        * `Fcf.Class.Monoid.Types` (which exports just an `Endo a` to wrap `a -> Exp a`)
-        * `Fcf.Class.Functor`
-        * `Fcf.Class.Bifunctor`
-        * `Fcf.Class.Foldable`
-
-- Add functions in `Fcf.Data.List`:
-  `Intersperse`, `Intercalate`, `Span`, `Break`, `Tails`, `IsPrefixOf`,
-  `IsSuffixOf`, `IsInfixOf`, `Partition`.
-- Generalize `Foldr`, `Concat` and `ConcatMap` to foldable types.
-
-- Remove deprecated `Guarded`, `Guard((:=))`, `Otherwise`.
-- Deprecate `Fcf.Classes`
-
-# 0.7.0.0
-
-- Add `Unfoldr`, `Concat`, `ConcatMap`, `Replicate`, `Take`, `Drop`,
-  `TakeWhile`, `DropWhile`, `Reverse` to `Data.List`. (thanks to gspia)
-- Change `Elem`, `Lookup`, `Zip` to be `data` instead of `type` synonyms.
-- Fix performance of `Filter` and `Find`.
-
-# 0.6.0.0
-
-- Add `Fcf.Utils.Case` (thanks to TheMatten)
-- Deprecate `Fcf.Bool.Guarded`
-- GHC 8.8 compatibility
-
-# 0.5.0.0
-
-- Modularized library
-
-- `Fcf.Utils`:
-
-    + Add `TError`
-    + Rename `Collapse` to `Constraints`
-
-- `Fcf.Data.List`: Added `Cons`, `Last`, `Init`, `Elem`
-
-# 0.4.0.0
-
-- New functions (thanks to blmage)
-
-    + `LiftM`, `LiftM2`, `LiftM3`
-    + `(<=)`, `(>=)`, `(<)`, `(>)`
-    + `Guarded`, `Guard((:=))`, `Otherwise`
-
-# 0.3.0.1
-
-- GHC 8.6 compatibility
-
-# 0.3.0.0
-
-- More new functions, (thanks to isovector)
-
-# 0.2.0.0
-
-- A whole bunch of basic functions (thanks to isovector)
-- Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`)
-
-# 0.1.0.0
-
-Initial version
+# 0.8.2.0 - 2025-10-12
+
+- Add `Fcf.Utils.Assert` and `Fcf.Utils.AssertNot`.
+- Export everything in `Fcf`
+
+# 0.8.1.0
+
+- Add `(Fcf.Combinators.>>=)`
+- Resolve warnings about deprecated `TypeInType`
+
+# 0.8.0.1
+
+- Bump upper bounds for GHC 9.0
+- Update doctests for cabal-docspec
+
+# 0.8.0.0
+
+- Add modules
+    + `Fcf.Data.Symbol` (currently just reexports `Symbol`) (thanks to gspia)
+    + `Fcf.Data.Function`
+    + "Overloaded type families" ("type-level type classes")
+        * `Fcf.Class.Ord`
+        * `Fcf.Class.Monoid`
+        * `Fcf.Class.Monoid.Types` (which exports just an `Endo a` to wrap `a -> Exp a`)
+        * `Fcf.Class.Functor`
+        * `Fcf.Class.Bifunctor`
+        * `Fcf.Class.Foldable`
+
+- Add functions in `Fcf.Data.List`:
+  `Intersperse`, `Intercalate`, `Span`, `Break`, `Tails`, `IsPrefixOf`,
+  `IsSuffixOf`, `IsInfixOf`, `Partition`.
+- Generalize `Foldr`, `Concat` and `ConcatMap` to foldable types.
+
+- Remove deprecated `Guarded`, `Guard((:=))`, `Otherwise`.
+- Deprecate `Fcf.Classes`
+
+# 0.7.0.0
+
+- Add `Unfoldr`, `Concat`, `ConcatMap`, `Replicate`, `Take`, `Drop`,
+  `TakeWhile`, `DropWhile`, `Reverse` to `Data.List`. (thanks to gspia)
+- Change `Elem`, `Lookup`, `Zip` to be `data` instead of `type` synonyms.
+- Fix performance of `Filter` and `Find`.
+
+# 0.6.0.0
+
+- Add `Fcf.Utils.Case` (thanks to TheMatten)
+- Deprecate `Fcf.Bool.Guarded`
+- GHC 8.8 compatibility
+
+# 0.5.0.0
+
+- Modularized library
+
+- `Fcf.Utils`:
+
+    + Add `TError`
+    + Rename `Collapse` to `Constraints`
+
+- `Fcf.Data.List`: Added `Cons`, `Last`, `Init`, `Elem`
+
+# 0.4.0.0
+
+- New functions (thanks to blmage)
+
+    + `LiftM`, `LiftM2`, `LiftM3`
+    + `(<=)`, `(>=)`, `(<)`, `(>)`
+    + `Guarded`, `Guard((:=))`, `Otherwise`
+
+# 0.3.0.1
+
+- GHC 8.6 compatibility
+
+# 0.3.0.0
+
+- More new functions, (thanks to isovector)
+
+# 0.2.0.0
+
+- A whole bunch of basic functions (thanks to isovector)
+- Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`)
+
+# 0.1.0.0
+
+Initial version
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright Li-yao Xia (c) 2018-2024
+Copyright Li-yao Xia (c) 2018-2025
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of
 this software and associated documentation files (the “Software”), to deal in
diff --git a/first-class-families.cabal b/first-class-families.cabal
--- a/first-class-families.cabal
+++ b/first-class-families.cabal
@@ -1,63 +1,63 @@
-name:                first-class-families
-version:             0.8.1.0
-synopsis:
-  First-class type families
-description:
-  A library for type-level programming.
-  .
-  See README.
-homepage:            https://github.com/Lysxia/first-class-families#readme
-license:             MIT
-license-file:        LICENSE
-author:              Li-yao Xia
-maintainer:          lysxia@gmail.com
-copyright:           2018-2024 Li-yao Xia
-category:            Other
-build-type:          Simple
-extra-source-files:  README.md, CHANGELOG.md
-cabal-version:       >=1.10
-tested-with:
-  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,
-  GHC == 8.8.1, GHC == 8.10.1, GHC == 9.0.1, GHC == 9.2.1,
-  GHC == 9.2.8, GHC == 9.4.8, GHC == 9.6.4, GHC == 9.8.2,
-  GHC == 9.10.1
-
-library
-  hs-source-dirs:      src
-  exposed-modules:
-    Fcf
-    Fcf.Core
-    Fcf.Combinators
-    Fcf.Data.Bool
-    Fcf.Data.Common
-    Fcf.Data.Function
-    Fcf.Data.List
-    Fcf.Data.Nat
-    Fcf.Data.Symbol
-    Fcf.Classes
-    Fcf.Class.Bifunctor
-    Fcf.Class.Foldable
-    Fcf.Class.Functor
-    Fcf.Class.Monoid
-    Fcf.Class.Monoid.Types
-    Fcf.Class.Ord
-    Fcf.Utils
-  build-depends:
-    base >= 4.9 && < 5
-  ghc-options:         -Wall
-  default-language:    Haskell2010
-  if impl(ghc < 8.6)
-    default-extensions: TypeInType
-
-test-suite fcf-test
-  type:                exitcode-stdio-1.0
-  hs-source-dirs:      test
-  main-is:             test.hs
-  default-language:    Haskell2010
-  build-depends:
-    base,
-    first-class-families
-
-source-repository head
-  type:     git
-  location: https://github.com/Lysxia/first-class-families
+name:                first-class-families
+version:             0.8.2.0
+synopsis:
+  First-class type families
+description:
+  A library for type-level programming.
+  .
+  See README.
+homepage:            https://github.com/Lysxia/first-class-families#readme
+license:             MIT
+license-file:        LICENSE
+author:              Li-yao Xia
+maintainer:          lysxia@gmail.com
+copyright:           2018-2025 Li-yao Xia
+category:            Other
+build-type:          Simple
+extra-source-files:  README.md, CHANGELOG.md
+cabal-version:       >=1.10
+tested-with:
+  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,
+  GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.1,
+  GHC == 9.2.8, GHC == 9.4.8, GHC == 9.6.7, GHC == 9.8.4,
+  GHC == 9.10.1, GHC == 9.12.2
+
+library
+  hs-source-dirs:      src
+  exposed-modules:
+    Fcf
+    Fcf.Core
+    Fcf.Combinators
+    Fcf.Data.Bool
+    Fcf.Data.Common
+    Fcf.Data.Function
+    Fcf.Data.List
+    Fcf.Data.Nat
+    Fcf.Data.Symbol
+    Fcf.Classes
+    Fcf.Class.Bifunctor
+    Fcf.Class.Foldable
+    Fcf.Class.Functor
+    Fcf.Class.Monoid
+    Fcf.Class.Monoid.Types
+    Fcf.Class.Ord
+    Fcf.Utils
+  build-depends:
+    base >= 4.9 && < 5
+  ghc-options:         -Wall
+  default-language:    Haskell2010
+  if impl(ghc < 8.6)
+    default-extensions: TypeInType
+
+test-suite fcf-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             test.hs
+  default-language:    Haskell2010
+  build-depends:
+    base,
+    first-class-families
+
+source-repository head
+  type:     git
+  location: https://github.com/Lysxia/first-class-families
diff --git a/src/Fcf.hs b/src/Fcf.hs
--- a/src/Fcf.hs
+++ b/src/Fcf.hs
@@ -1,150 +1,186 @@
-{-# LANGUAGE TypeOperators #-}
-
--- | First-class type families
---
--- For example, here is a regular type family:
---
--- @
--- type family   FromMaybe (a :: k) (m :: Maybe k) :: k
--- type instance FromMaybe a 'Nothing  = a
--- type instance FromMaybe a ('Just b) = b
--- @
---
--- With @Fcf@, it translates to a @data@ declaration:
---
--- @
--- data FromMaybe :: k -> Maybe k -> 'Exp' k
--- type instance 'Eval' (FromMaybe a 'Nothing)  = a
--- type instance 'Eval' (FromMaybe a ('Just b)) = b
--- @
---
--- - Fcfs can be higher-order.
--- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.
---
--- Essential language extensions for "Fcf":
---
--- > {-# LANGUAGE
--- >     DataKinds,
--- >     PolyKinds,
--- >     TypeFamilies,
--- >     TypeOperators,
--- >     UndecidableInstances #-}
-
-module Fcf
-  ( -- * First-class type families
-
-    Exp
-  , Eval
-  , type (@@)
-
-    -- ** Functional combinators
-
-  , Pure
-  , Pure1
-  , Pure2
-  , Pure3
-  , type (=<<)
-  , type (<=<)
-  , LiftM
-  , LiftM2
-  , LiftM3
-  , Join
-  , type (<$>)
-  , type (<*>)
-  , Flip
-  , ConstFn
-  , type ($)
-
-    -- * Operations on common types
-
-    -- ** Pairs
-
-  , Uncurry
-  , Fst
-  , Snd
-  , type (***)
-
-    -- ** Either
-
-  , UnEither
-  , IsLeft
-  , IsRight
-
-    -- ** Maybe
-
-  , UnMaybe
-  , FromMaybe
-  , IsNothing
-  , IsJust
-
-    -- ** Lists
-
-  , Foldr
-  , UnList
-  , type (++)
-  , Filter
-  , Head
-  , Tail
-  , Null
-  , Length
-  , Find
-  , FindIndex
-  , Lookup
-  , SetIndex
-  , ZipWith
-  , Zip
-  , Unzip
-  , Cons2
-
-    -- ** Bool
-
-  , UnBool
-  , type (||)
-  , type (&&)
-  , Not
-
-    -- ** Case splitting
-
-  , Case
-  , Match()
-  , type (-->)
-  , Is
-  , Any
-  , Else
-
-    -- ** Nat
-
-  , type (+)
-  , type (-)
-  , type (Fcf.Data.Nat.*)
-  , type (^)
-  , type (<=)
-  , type (>=)
-  , type (<)
-  , type (>)
-
-    -- * Overloaded operations
-
-  , Map
-  , Bimap
-
-    -- * Miscellaneous
-
-  , Error
-  , Constraints
-  , TyEq
-  , Stuck
-  , IsBool(_If)
-  , If
-
-  ) where
-
-import Fcf.Core
-import Fcf.Combinators
-import Fcf.Data.Bool
-import Fcf.Data.Common
-import Fcf.Data.List
-import Fcf.Data.Nat
-import Fcf.Class.Functor
-import Fcf.Class.Bifunctor
-import Fcf.Utils
+{-# LANGUAGE TypeOperators #-}
+
+-- | First-class type families
+--
+-- For example, here is a regular type family:
+--
+-- @
+-- type family   FromMaybe (a :: k) (m :: Maybe k) :: k
+-- type instance FromMaybe a 'Nothing  = a
+-- type instance FromMaybe a ('Just b) = b
+-- @
+--
+-- With @Fcf@, it translates to a @data@ declaration:
+--
+-- @
+-- data FromMaybe :: k -> Maybe k -> 'Exp' k
+-- type instance 'Eval' (FromMaybe a 'Nothing)  = a
+-- type instance 'Eval' (FromMaybe a ('Just b)) = b
+-- @
+--
+-- - Fcfs can be higher-order.
+-- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.
+--
+-- Essential language extensions for "Fcf":
+--
+-- > {-# LANGUAGE
+-- >     DataKinds,
+-- >     PolyKinds,
+-- >     TypeFamilies,
+-- >     TypeOperators,
+-- >     UndecidableInstances #-}
+
+module Fcf
+  ( -- * First-class type families
+
+    Exp
+  , Eval
+  , type (@@)
+
+    -- ** Functional combinators
+
+  , Pure
+  , Pure1
+  , Pure2
+  , Pure3
+  , Pure4
+  , Pure5
+  , Pure6
+  , Pure7
+  , Pure8
+  , Pure9
+  , type (=<<)
+  , type (>>=)
+  , type (<=<)
+  , LiftM
+  , LiftM2
+  , LiftM3
+  , Join
+  , type (<$>)
+  , type (<*>)
+  , Flip
+  , ConstFn
+  , type ($)
+
+    -- * Operations on common types
+
+    -- ** Pairs
+
+  , Uncurry
+  , Fst
+  , Snd
+  , type (***)
+
+    -- ** Either
+
+  , UnEither
+  , IsLeft
+  , IsRight
+
+    -- ** Maybe
+
+  , UnMaybe
+  , FromMaybe
+  , IsNothing
+  , IsJust
+
+    -- ** Lists
+
+  , type (++)
+  , Head
+  , Last
+  , Tail
+  , Cons
+  , Snoc
+  , Cons2
+  , Init
+  , Uncons
+  , Unsnoc
+  , Singleton
+  , Null
+  , Length
+  , Reverse
+  , Intersperse
+  , Intercalate
+  , Foldr
+  , UnList
+  , Concat
+  , ConcatMap
+  , Unfoldr
+  , Replicate
+  , Take
+  , Drop
+  , SplitAt
+  , TakeWhile
+  , DropWhile
+  , Span
+  , Break
+  , Tails
+  , IsPrefixOf
+  , IsSuffixOf
+  , IsInfixOf
+  , Elem
+  , Lookup
+  , Find
+  , Filter
+  , Partition
+  , FindIndex
+  , SetIndex
+  , ZipWith
+  , Zip
+  , Unzip
+
+    -- ** Bool
+
+  , UnBool
+  , type (||)
+  , type (&&)
+  , Not
+
+    -- ** Case splitting
+
+  , Case
+  , Match()
+  , type (-->)
+  , Is
+  , Any
+  , Else
+
+    -- ** Nat
+
+  , type (+)
+  , type (-)
+  , type (Fcf.Data.Nat.*)
+  , type (^)
+  , type (<=)
+  , type (>=)
+  , type (<)
+  , type (>)
+
+    -- * Overloaded operations
+
+  , Map
+  , Bimap
+
+    -- * Miscellaneous
+
+  , Error
+  , Constraints
+  , TyEq
+  , Stuck
+  , IsBool(_If)
+  , If
+  , Assert
+  , AssertNot
+
+  ) where
+
+import Fcf.Core
+import Fcf.Combinators
+import Fcf.Data.Bool
+import Fcf.Data.Common
+import Fcf.Data.List
+import Fcf.Data.Nat
+import Fcf.Class.Functor
+import Fcf.Class.Bifunctor
+import Fcf.Utils
diff --git a/src/Fcf/Combinators.hs b/src/Fcf/Combinators.hs
--- a/src/Fcf/Combinators.hs
+++ b/src/Fcf/Combinators.hs
@@ -13,6 +13,12 @@
   , Pure1
   , Pure2
   , Pure3
+  , Pure4
+  , Pure5
+  , Pure6
+  , Pure7
+  , Pure8
+  , Pure9
   , type (=<<)
   , type (>>=)
   , type (<=<)
@@ -46,6 +52,24 @@
 
 data Pure3 :: (a -> b -> c -> d) -> a -> b -> c -> Exp d
 type instance Eval (Pure3 f x y z) = f x y z
+
+data Pure4 :: (a -> b -> c -> d -> e) -> a -> b -> c -> d -> Exp e
+type instance Eval (Pure4 f w x y z) = f w x y z
+
+data Pure5 :: (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> Exp f
+type instance Eval (Pure5 f v w x y z) = f v w x y z
+
+data Pure6 :: (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> Exp g
+type instance Eval (Pure6 f u v w x y z) = f u v w x y z
+
+data Pure7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> a -> b -> c -> d -> e -> f -> g -> Exp h
+type instance Eval (Pure7 f t u v w x y z) = f t u v w x y z
+
+data Pure8 :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> a -> b -> c -> d -> e -> f -> g -> h -> Exp i
+type instance Eval (Pure8 f s t u v w x y z) = f s t u v w x y z
+
+data Pure9 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> a -> b -> c -> d -> e -> f -> g -> h -> i -> Exp j
+type instance Eval (Pure9 f r s t u v w x y z) = f r s t u v w x y z
 
 data (=<<) :: (a -> Exp b) -> Exp a -> Exp b
 type instance Eval (k =<< e) = Eval (k (Eval e))
diff --git a/src/Fcf/Data/List.hs b/src/Fcf/Data/List.hs
--- a/src/Fcf/Data/List.hs
+++ b/src/Fcf/Data/List.hs
@@ -1,575 +1,621 @@
-{-# LANGUAGE
-    DataKinds,
-    PolyKinds,
-    TypeFamilies,
-    TypeOperators,
-    UndecidableInstances #-}
-
--- | Lists.
---
--- See also "Fcf.Class.Foldable" for additional functions.
-module Fcf.Data.List
-  ( -- * Basic functions
-    type (++)
-  , Head
-  , Last
-  , Tail
-  , Cons
-  , Snoc
-  , Cons2
-  , Init
-  , Null
-  , Length
-
-  -- * List transformations
-  , Reverse
-  , Intersperse
-  , Intercalate
-
-  -- * Reducing lists
-  -- | See also "Fcf.Class.Foldable".
-  , Foldr
-  , UnList
-  , Concat
-  , ConcatMap
-
-  -- * Unfolding and building
-  , Unfoldr
-  , Replicate
-
-  -- * Sublists
-  , Take
-  , Drop
-  , TakeWhile
-  , DropWhile
-  , Span
-  , Break
-  , Tails
-
-  -- ** Predicates
-  , IsPrefixOf
-  , IsSuffixOf
-  , IsInfixOf
-
-  -- * Searching
-  , Elem
-  , Lookup
-  , Find
-  , Filter
-  , Partition
-
-  -- * Indexing lists
-  , FindIndex
-  , SetIndex
-
-  -- * Zipping and unzipping
-  , ZipWith
-  , Zip
-  , Unzip
-  ) where
-
-import qualified GHC.TypeLits as TL
-
-import Fcf.Core
-import Fcf.Combinators
-import Fcf.Class.Functor (Map)
-import Fcf.Class.Monoid (type (<>))
-import Fcf.Class.Foldable
-import Fcf.Data.Bool
-import Fcf.Data.Common
-import Fcf.Data.Nat
-import Fcf.Utils (If, TyEq)
-
--- $setup
--- >>> :set -XGADTs -XUndecidableInstances
--- >>> import Fcf.Core (Exp, Eval)
--- >>> import Fcf.Combinators
--- >>> import Fcf.Class.Foldable (Concat)
--- >>> import Fcf.Class.Monoid ()
--- >>> import Fcf.Data.Nat
--- >>> import Fcf.Utils (If, TyEq)
--- >>> import Data.Type.Ord ()
--- >>> import qualified GHC.TypeLits as TL
--- >>> import GHC.TypeLits (Nat)
--- >>> import Numeric.Natural (Natural)
-
--- | List catenation.
---
--- === __Example__
---
--- >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--- >>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
--- Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
--- = Ex [1, 2, 3, 4]
---
-data (++) :: [a] -> [a] -> Exp [a]
-type instance Eval ((++) xs ys) = xs <> ys
-
-
-data Head :: [a] -> Exp (Maybe a)
-type instance Eval (Head '[]) = 'Nothing
-type instance Eval (Head (a ': _as)) = 'Just a
-
-data Last :: [a] -> Exp (Maybe a)
-type instance Eval (Last '[]) = 'Nothing
-type instance Eval (Last (a ': '[])) = 'Just a
-type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))
-
-data Init :: [a] -> Exp (Maybe [a])
-type instance Eval (Init '[]) = 'Nothing
-type instance Eval (Init (a ': '[])) = 'Just '[]
-type instance Eval (Init (a ': b ': as)) =
-  Eval (Map (Cons a) =<< (Init (b ': as)))
-
-data Tail :: [a] -> Exp (Maybe [a])
-type instance Eval (Tail '[]) = 'Nothing
-type instance Eval (Tail (_a ': as)) = 'Just as
-
-data Null :: [a] -> Exp Bool
-type instance Eval (Null '[]) = 'True
-type instance Eval (Null (a ': as)) = 'False
-
-data Length :: [a] -> Exp Nat
-type instance Eval (Length '[]) = 0
-type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
-
-
--- | Append an element to a list.
---
--- === __Example__
---
--- >>> :kind! Eval (Cons 1 [2, 3])
--- Eval (Cons 1 [2, 3]) :: [Natural]
--- = [1, 2, 3]
--- >>> :kind! Eval (Cons Int [Char, Maybe Double])
--- Eval (Cons Int [Char, Maybe Double]) :: [*]
--- = [Int, Char, Maybe Double]
---
-data Cons :: a -> [a] -> Exp [a]
-type instance Eval (Cons a as) = a ': as
-
--- | Append elements to two lists. Used in the definition of 'Unzip'.
-data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
-type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
-
--- | Append an element to the end of a list.
---
--- === __Example__
---
--- >>> :kind! Eval (Snoc [1,2,3] 4)
--- Eval (Snoc [1,2,3] 4) :: [Natural]
--- = [1, 2, 3, 4]
-data Snoc :: [a] -> a -> Exp [a]
-type instance Eval (Snoc lst a) = Eval (lst ++ '[a])
-
-
--- Helper for Reverse. This corresponds to rev in the data list lib.
-data Rev :: [a] -> [a] -> Exp [a]
-type instance Eval (Rev '[]       ys) = ys
-type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys))
-
-
--- | Reverse a list.
---
--- === __Example__
---
--- >>> :kind! Eval (Reverse [1,2,3,4,5])
--- Eval (Reverse [1,2,3,4,5]) :: [Natural]
--- = [5, 4, 3, 2, 1]
-data Reverse :: [a] -> Exp [a]
-type instance Eval (Reverse l) = Eval (Rev l '[])
-
--- | Intersperse a separator between elements of a list.
---
--- === __Example__
---
--- >>> :kind! Eval (Intersperse 0 [1,2,3,4])
--- Eval (Intersperse 0 [1,2,3,4]) :: [Natural]
--- = [1, 0, 2, 0, 3, 0, 4]
-data Intersperse :: a -> [a] -> Exp [a]
-type instance Eval (Intersperse _   '[]      ) = '[]
-type instance Eval (Intersperse sep (x ': xs)) = x ': Eval (PrependToAll sep xs)
-
--- | Helper for Intersperse
-data PrependToAll :: a -> [a] -> Exp [a]
-type instance Eval (PrependToAll _   '[]      ) = '[]
-type instance Eval (PrependToAll sep (x ': xs)) = sep ': x ': Eval (PrependToAll sep xs)
-
--- | Join a list of words separated by some word.
---
--- === __Example__
---
--- >>> :kind! Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ])
--- Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
--- = ["Lorem", ", ", "ipsum", ", ", "dolor"]
-data Intercalate :: [a] -> [[a]] -> Exp [a]
-type instance Eval (Intercalate xs xss) = Eval (Concat =<< Intersperse xs xss)
-
-
--- | This is 'Foldr' with its argument flipped.
-data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
-type instance Eval (UnList y f xs) = Eval (Foldr f y xs)
-
-
--- Helper for the Unfoldr.
-data UnfoldrCase :: (b -> Exp (Maybe (a, b))) -> Maybe (a, b) -> Exp [a]
-type instance Eval (UnfoldrCase f ('Just ab)) =
-  Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))
-type instance Eval (UnfoldrCase _ 'Nothing) = '[]
-
--- | Unfold a generator into a list.
---
--- === __Example__
---
--- >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
--- >>> :{
--- type instance Eval (ToThree b) =
---   If (4 TL.<=? b)
---     Nothing
---     (Just '(b, b TL.+ 1))
--- :}
---
--- >>> :kind! Eval (Unfoldr ToThree 0)
--- Eval (Unfoldr ToThree 0) :: [Natural]
--- = [0, 1, 2, 3]
---
--- See also the definition of `Replicate`.
-data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]
-type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c))
-
-
--- Helper for the Replicate.
-data NumIter :: a -> Nat -> Exp (Maybe (a, Nat))
-type instance Eval (NumIter a s) =
-  If (Eval (s > 0))
-    ('Just '(a, s TL.- 1))
-    'Nothing
-
--- | Repeat the same element in a list.
---
--- === __Example__
---
--- >>> :kind! Eval (Replicate 4 '("ok", 2))
--- Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Natural)]
--- = ['("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
-data Replicate :: Nat -> a -> Exp [a]
-type instance Eval (Replicate n a) = Eval (Unfoldr (NumIter a) n)
-
-
--- | Take a prefix of fixed length.
---
--- === __Example__
---
--- >>> :kind! Eval (Take 2 [1,2,3,4,5])
--- Eval (Take 2 [1,2,3,4,5]) :: [Natural]
--- = [1, 2]
-data Take :: Nat -> [a] -> Exp [a]
-type instance Eval (Take n as) = Take_ n as
-
-type family Take_ (n :: Nat) (xs :: [a]) :: [a] where
-  Take_ 0 _         = '[]
-  Take_ _ '[]       = '[]
-  Take_ n (x ': xs) = x ': Take_ (n TL.- 1) xs
-
--- | Drop a prefix of fixed length, evaluate to the remaining suffix.
---
--- === __Example__
---
--- >>> :kind! Eval (Drop 2 [1,2,3,4,5])
--- Eval (Drop 2 [1,2,3,4,5]) :: [Natural]
--- = [3, 4, 5]
-data Drop :: Nat -> [a] -> Exp [a]
-type instance Eval (Drop n as) = Drop_ n as
-
-type family Drop_ (n :: Nat) (xs :: [a]) :: [a] where
-  Drop_ 0 xs        = xs
-  Drop_ _ '[]       = '[]
-  Drop_ n (x ': xs) = Drop_ (n TL.- 1) xs
-
--- | Take the longest prefix of elements satisfying a predicate.
---
--- === __Example__
---
--- >>> :kind! Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5])
--- Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
--- = [1, 2, 3]
-data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
-type instance Eval (TakeWhile p '[]) = '[]
-type instance Eval (TakeWhile p (x ': xs)) =
-  Eval (If (Eval (p x))
-      ('(:) x <$> TakeWhile p xs)
-      (Pure '[]))
-
--- | Drop the longest prefix of elements satisfying a predicate,
--- evaluate to the remaining suffix.
---
--- === __Example__
---
--- :kind! Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5])
--- Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
--- = [4, 5]
-data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
-type instance Eval (DropWhile p '[]) = '[]
-type instance Eval (DropWhile p (x ': xs)) =
-  Eval (If (Eval (p x))
-      (DropWhile p xs)
-      (Pure (x ': xs)))
-
-
--- | 'Span', applied to a predicate @p@ and a list @xs@, returns a tuple:
--- the first component is the longest prefix (possibly empty) of @xs@ whose elements
--- satisfy @p@;
--- the second component is the remainder of the list.
---
--- See also 'TakeWhile', 'DropWhile', and 'Break'.
---
--- === __Example__
---
--- >>> :kind! Eval (Span (Flip (<) 3) [1,2,3,4,1,2])
--- Eval (Span (Flip (<) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
--- = '([1, 2], [3, 4, 1, 2])
---
--- >>> :kind! Eval (Span (Flip (<) 9) [1,2,3])
--- Eval (Span (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
--- = '([1, 2, 3], '[])
---
--- >>> :kind! Eval (Span (Flip (<) 0) [1,2,3])
--- Eval (Span (Flip (<) 0) [1,2,3]) :: ([Natural], [Natural])
--- = '( '[], [1, 2, 3])
-data Span :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
-type instance Eval (Span p lst) = '( Eval (TakeWhile p lst), Eval (DropWhile p lst))
-
-
--- | 'Break', applied to a predicate @p@ and a list @xs@, returns a tuple:
--- the first component is the longest prefix (possibly empty) of @xs@ whose elements
--- /do not satisfy/ @p@; the second component is the remainder of the list.
---
--- === __Example__
---
--- >>> :kind! Eval (Break (Flip (>) 3) [1,2,3,4,1,2])
--- Eval (Break (Flip (>) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
--- = '([1, 2, 3], [4, 1, 2])
---
--- >>> :kind! Eval (Break (Flip (<) 9) [1,2,3])
--- Eval (Break (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
--- = '( '[], [1, 2, 3])
---
--- >>> :kind! Eval (Break (Flip (>) 9) [1,2,3])
--- Eval (Break (Flip (>) 9) [1,2,3]) :: ([Natural], [Natural])
--- = '([1, 2, 3], '[])
-data Break :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
-type instance Eval (Break p lst) = Eval (Span (Not <=< p) lst)
-
-
--- | List of suffixes of a list.
---
--- === __Example__
---
--- >>> :kind! Eval (Tails [0,1,2,3])
--- Eval (Tails [0,1,2,3]) :: [[Natural]]
--- = [[0, 1, 2, 3], [1, 2, 3], [2, 3], '[3]]
-data Tails :: [a] -> Exp [[a]]
-type instance Eval (Tails '[]) = '[]
-type instance Eval (Tails (a ': as)) = (a ': as) ': Eval (Tails as)
-
-
--- | Return @True@ when the first list is a prefix of the second.
---
--- === __Example__
---
--- >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5])
--- Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5]) :: Bool
--- = True
---
--- >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5])
--- Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--- = False
---
--- >>> :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
--- Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--- = True
---
--- >>> :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
--- Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
--- = False
-data IsPrefixOf :: [a] -> [a] -> Exp Bool
-type instance Eval (IsPrefixOf xs ys) = IsPrefixOf_ xs ys
-
--- helper for IsPrefixOf
-type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where
-  IsPrefixOf_ '[] _ = 'True
-  IsPrefixOf_ _ '[] = 'False
-  IsPrefixOf_ (x ': xs) (y ': ys) =
-     Eval ((Eval (TyEq x y)) && IsPrefixOf_ xs ys)
-
-
--- | Return @True@ when the first list is a suffix of the second.
---
--- === __Example__
---
--- >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5])
--- Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5]) :: Bool
--- = True
---
--- >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5])
--- Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5]) :: Bool
--- = False
---
--- >>> :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
--- Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
--- = True
---
--- >>> :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
--- Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
--- = False
-data IsSuffixOf :: [a] -> [a] -> Exp Bool
-type instance Eval (IsSuffixOf xs ys) =
-  Eval (IsPrefixOf (Reverse @@ xs) (Reverse @@ ys))
-
-
--- | Return @True@ when the first list is contained within the second.
---
--- === __Example__
---
--- >>> :kind! Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6])
--- Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6]) :: Bool
--- = True
---
--- >>> :kind! Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6])
--- Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6]) :: Bool
--- = False
-data IsInfixOf :: [a] -> [a] -> Exp Bool
-type instance Eval (IsInfixOf xs ys) = Eval (Any (IsPrefixOf xs) =<< Tails ys)
-
-
--- | Return @True@ if an element is in a list.
---
--- See also 'FindIndex'.
---
--- === __Example__
---
--- >>> :kind! Eval (Elem 1 [1,2,3])
--- Eval (Elem 1 [1,2,3]) :: Bool
--- = True
--- >>> :kind! Eval (Elem 1 [2,3])
--- Eval (Elem 1 [2,3]) :: Bool
--- = False
---
-data Elem :: a -> [a] -> Exp Bool
-type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)
-
--- | Find an element associated with a key in an association list.
-data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
-type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =
-  Eval (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
-
-
--- | Find @Just@ the first element satisfying a predicate, or evaluate to
--- @Nothing@ if no element satisfies the predicate.
---
--- === __Example__
---
--- >>> :kind! Eval (Find (TyEq 0) [1,2,3])
--- Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
--- = Nothing
---
--- >>> :kind! Eval (Find (TyEq 0) [1,2,3,0])
--- Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
--- = Just 0
-data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
-type instance Eval (Find _p '[]) = 'Nothing
-type instance Eval (Find p (a ': as)) =
-  Eval (If (Eval (p a))
-    (Pure ('Just a))
-    (Find p as))
-
-
--- | Keep all elements that satisfy a predicate, remove all that don't.
---
--- === __Example__
---
--- >>> :kind! Eval (Filter ((>) 3) [1,2,3,0])
--- Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural]
--- = [1, 2, 0]
-data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
-type instance Eval (Filter _p '[]) = '[]
-type instance Eval (Filter p (a ': as)) =
-  Eval (If (Eval (p a))
-    ('(:) a <$> Filter p as)
-    (Filter p as))
-
-
--- | Split a list into one where all elements satisfy a predicate,
--- and a second where no elements satisfy it.
---
--- === __Example__
---
--- >>> :kind! Eval (Partition ((>=) 35) [20, 30, 40, 50])
--- Eval (Partition ((>=) 35) [20, 30, 40, 50]) :: ([Natural],
---                                                 [Natural])
--- = '([20, 30], [40, 50])
-data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
-type instance Eval (Partition p lst) = Eval (Foldr (PartHelp p) '( '[], '[]) lst)
-
--- | Helper for 'Partition'.
-data PartHelp :: (a -> Exp Bool) -> a -> ([a],[a]) -> Exp ([a],[a])
-type instance Eval (PartHelp p a '(xs,ys)) =
-  If (Eval (p a))
-    '(a ': xs, ys)
-    '(xs, a ': ys)
-
-
--- | Find the index of an element satisfying the predicate.
---
--- === __Example__
---
--- >>> :kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
--- Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural
--- = Just 2
---
--- >>> :kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
--- Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural
--- = Nothing
-data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
-type instance Eval (FindIndex _p '[]) = 'Nothing
-type instance Eval (FindIndex p (a ': as)) =
-  Eval (If (Eval (p a))
-    (Pure ('Just 0))
-    (Map ((+) 1) =<< FindIndex p as))
-
-
--- | Modify an element at a given index.
---
--- The list is unchanged if the index is out of bounds.
---
--- === __Example__
---
--- >>> :kind! Eval (SetIndex 2 7 [1,2,3])
--- Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
--- = [1, 2, 7]
-data SetIndex :: Nat -> a -> [a] -> Exp [a]
-type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
-
-type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
-  SetIndexImpl _n _a' '[] = '[]
-  SetIndexImpl 0 a' (_a ': as) = a' ': as
-  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as
-
--- | Combine elements of two lists pairwise.
---
--- === __Example__
---
--- >>> :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
--- Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
--- = [2, 3, 4]
-data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
-type instance Eval (ZipWith _f '[] _bs) = '[]
-type instance Eval (ZipWith _f _as '[]) = '[]
-type instance Eval (ZipWith f (a ': as) (b ': bs)) =
-  Eval (f a b) ': Eval (ZipWith f as bs)
-
-data Zip :: [a] -> [b] -> Exp [(a, b)]
-type instance Eval (Zip as bs) = Eval (ZipWith (Pure2 '(,)) as bs)
-
-data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
-type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Lists.
+--
+-- See also "Fcf.Class.Foldable" for additional functions.
+module Fcf.Data.List
+  ( -- * Basic functions
+    type (++)
+  , Head
+  , Last
+  , Tail
+  , Cons
+  , Snoc
+  , Cons2
+  , Init
+  , Uncons
+  , Unsnoc
+  , Singleton
+  , Null
+  , Length
+
+  -- * List transformations
+  , Reverse
+  , Intersperse
+  , Intercalate
+
+  -- * Reducing lists
+  -- | See also "Fcf.Class.Foldable".
+  , Foldr
+  , UnList
+  , Concat
+  , ConcatMap
+
+  -- * Unfolding and building
+  , Unfoldr
+  , Replicate
+
+  -- * Sublists
+  , Take
+  , Drop
+  , SplitAt
+  , TakeWhile
+  , DropWhile
+  , Span
+  , Break
+  , Tails
+
+  -- ** Predicates
+  , IsPrefixOf
+  , IsSuffixOf
+  , IsInfixOf
+
+  -- * Searching
+  , Elem
+  , Lookup
+  , Find
+  , Filter
+  , Partition
+
+  -- * Indexing lists
+  , FindIndex
+  , SetIndex
+
+  -- * Zipping and unzipping
+  , ZipWith
+  , Zip
+  , Unzip
+  ) where
+
+import qualified GHC.TypeLits as TL
+
+import Fcf.Core
+import Fcf.Combinators
+import Fcf.Class.Functor (Map)
+import Fcf.Class.Monoid (type (<>))
+import Fcf.Class.Foldable
+import Fcf.Data.Bool
+import Fcf.Data.Common
+import Fcf.Data.Nat
+import Fcf.Utils (If, TyEq)
+
+-- $setup
+-- >>> :set -XGADTs -XUndecidableInstances -XDataKinds
+-- >>> import Fcf.Core (Exp, Eval)
+-- >>> import Fcf.Combinators
+-- >>> import Fcf.Class.Foldable (Concat)
+-- >>> import Fcf.Class.Functor ()
+-- >>> import Fcf.Class.Monoid ()
+-- >>> import Fcf.Data.Nat
+-- >>> import Fcf.Utils (If, TyEq)
+-- >>> import Data.Type.Ord ()
+-- >>> import qualified GHC.TypeLits as TL
+-- >>> import GHC.TypeLits (Nat)
+-- >>> import Numeric.Natural (Natural)
+
+-- | List catenation.
+--
+-- === __Example__
+--
+-- >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
+-- >>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
+-- Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
+-- = Ex [1, 2, 3, 4]
+--
+data (++) :: [a] -> [a] -> Exp [a]
+type instance Eval ((++) xs ys) = xs <> ys
+
+
+data Head :: [a] -> Exp (Maybe a)
+type instance Eval (Head '[]) = 'Nothing
+type instance Eval (Head (a ': _as)) = 'Just a
+
+data Last :: [a] -> Exp (Maybe a)
+type instance Eval (Last '[]) = 'Nothing
+type instance Eval (Last (a ': '[])) = 'Just a
+type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))
+
+data Init :: [a] -> Exp (Maybe [a])
+type instance Eval (Init '[]) = 'Nothing
+type instance Eval (Init (a ': '[])) = 'Just '[]
+type instance Eval (Init (a ': b ': as)) =
+  Eval (Map (Cons a) =<< (Init (b ': as)))
+
+data Uncons :: [a] -> Exp (Maybe (a, [a]))
+type instance Eval (Uncons '[]) = 'Nothing
+type instance Eval (Uncons (a ': xs)) = 'Just '(a, xs)
+
+-- | Decompose a list into 'init' and 'last'
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Unsnoc '[])
+-- Eval (Unsnoc '[]) :: Maybe ([a], a)
+-- = Nothing
+--
+-- >>> :kind! Eval (Unsnoc '[1])
+-- Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural)
+-- = Just '( '[], 1)
+--
+-- >>> :kind! Eval (Unsnoc '[1,2,3])
+-- Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural)
+-- = Just '([1, 2], 3)
+data Unsnoc :: [a] -> Exp (Maybe ([a], a))
+type instance Eval (Unsnoc '[]) = 'Nothing
+type instance Eval (Unsnoc (x ': '[])) = 'Just '( '[], x)
+type instance Eval (Unsnoc (x ': y ': ys)) = Eval (Map (PrependF x) =<< Unsnoc (y ': ys))
+
+data PrependF :: a -> ([a], a) -> Exp ([a], a)
+type instance Eval (PrependF x '(xs, y)) = '(x ': xs, y)
+
+data Singleton :: a -> Exp [a]
+type instance Eval (Singleton x) = '[x]
+
+data Tail :: [a] -> Exp (Maybe [a])
+type instance Eval (Tail '[]) = 'Nothing
+type instance Eval (Tail (_a ': as)) = 'Just as
+
+data Null :: [a] -> Exp Bool
+type instance Eval (Null '[]) = 'True
+type instance Eval (Null (a ': as)) = 'False
+
+data Length :: [a] -> Exp Nat
+type instance Eval (Length '[]) = 0
+type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
+
+
+-- | Append an element to a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Cons 1 [2, 3])
+-- Eval (Cons 1 [2, 3]) :: [Natural]
+-- = [1, 2, 3]
+-- >>> :kind! Eval (Cons Int [Char, Maybe Double])
+-- Eval (Cons Int [Char, Maybe Double]) :: [*]
+-- = [Int, Char, Maybe Double]
+--
+data Cons :: a -> [a] -> Exp [a]
+type instance Eval (Cons a as) = a ': as
+
+-- | Append elements to two lists. Used in the definition of 'Unzip'.
+data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
+type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
+
+-- | Append an element to the end of a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Snoc [1,2,3] 4)
+-- Eval (Snoc [1,2,3] 4) :: [Natural]
+-- = [1, 2, 3, 4]
+data Snoc :: [a] -> a -> Exp [a]
+type instance Eval (Snoc lst a) = Eval (lst ++ '[a])
+
+
+-- Helper for Reverse. This corresponds to rev in the data list lib.
+data Rev :: [a] -> [a] -> Exp [a]
+type instance Eval (Rev '[]       ys) = ys
+type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys))
+
+
+-- | Reverse a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Reverse [1,2,3,4,5])
+-- Eval (Reverse [1,2,3,4,5]) :: [Natural]
+-- = [5, 4, 3, 2, 1]
+data Reverse :: [a] -> Exp [a]
+type instance Eval (Reverse l) = Eval (Rev l '[])
+
+-- | Intersperse a separator between elements of a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Intersperse 0 [1,2,3,4])
+-- Eval (Intersperse 0 [1,2,3,4]) :: [Natural]
+-- = [1, 0, 2, 0, 3, 0, 4]
+data Intersperse :: a -> [a] -> Exp [a]
+type instance Eval (Intersperse _   '[]      ) = '[]
+type instance Eval (Intersperse sep (x ': xs)) = x ': Eval (PrependToAll sep xs)
+
+-- | Helper for Intersperse
+data PrependToAll :: a -> [a] -> Exp [a]
+type instance Eval (PrependToAll _   '[]      ) = '[]
+type instance Eval (PrependToAll sep (x ': xs)) = sep ': x ': Eval (PrependToAll sep xs)
+
+-- | Join a list of words separated by some word.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ])
+-- Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
+-- = ["Lorem", ", ", "ipsum", ", ", "dolor"]
+data Intercalate :: [a] -> [[a]] -> Exp [a]
+type instance Eval (Intercalate xs xss) = Eval (Concat =<< Intersperse xs xss)
+
+
+-- | This is 'Foldr' with its argument flipped.
+data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
+type instance Eval (UnList y f xs) = Eval (Foldr f y xs)
+
+
+-- Helper for the Unfoldr.
+data UnfoldrCase :: (b -> Exp (Maybe (a, b))) -> Maybe (a, b) -> Exp [a]
+type instance Eval (UnfoldrCase f ('Just ab)) =
+  Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))
+type instance Eval (UnfoldrCase _ 'Nothing) = '[]
+
+-- | Unfold a generator into a list.
+--
+-- === __Example__
+--
+-- >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
+-- >>> :{
+-- type instance Eval (ToThree b) =
+--   If (4 TL.<=? b)
+--     Nothing
+--     (Just '(b, b TL.+ 1))
+-- :}
+--
+-- >>> :kind! Eval (Unfoldr ToThree 0)
+-- Eval (Unfoldr ToThree 0) :: [Natural]
+-- = [0, 1, 2, 3]
+--
+-- See also the definition of `Replicate`.
+data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]
+type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c))
+
+
+-- Helper for the Replicate.
+data NumIter :: a -> Nat -> Exp (Maybe (a, Nat))
+type instance Eval (NumIter a s) =
+  If (Eval (s > 0))
+    ('Just '(a, s TL.- 1))
+    'Nothing
+
+-- | Repeat the same element in a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Replicate 4 '("ok", 2))
+-- Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Natural)]
+-- = ['("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
+data Replicate :: Nat -> a -> Exp [a]
+type instance Eval (Replicate n a) = Eval (Unfoldr (NumIter a) n)
+
+
+-- | Take a prefix of fixed length.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Take 2 [1,2,3,4,5])
+-- Eval (Take 2 [1,2,3,4,5]) :: [Natural]
+-- = [1, 2]
+data Take :: Nat -> [a] -> Exp [a]
+type instance Eval (Take n as) = Take_ n as
+
+type family Take_ (n :: Nat) (xs :: [a]) :: [a] where
+  Take_ 0 _         = '[]
+  Take_ _ '[]       = '[]
+  Take_ n (x ': xs) = x ': Take_ (n TL.- 1) xs
+
+-- | Drop a prefix of fixed length, evaluate to the remaining suffix.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Drop 2 [1,2,3,4,5])
+-- Eval (Drop 2 [1,2,3,4,5]) :: [Natural]
+-- = [3, 4, 5]
+data Drop :: Nat -> [a] -> Exp [a]
+type instance Eval (Drop n as) = Drop_ n as
+
+type family Drop_ (n :: Nat) (xs :: [a]) :: [a] where
+  Drop_ 0 xs        = xs
+  Drop_ _ '[]       = '[]
+  Drop_ n (x ': xs) = Drop_ (n TL.- 1) xs
+
+-- | Return a tuple where first element is @xs@ prefix of length @n@
+-- and second element is the remainder of the list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (SplitAt 3 '[1,2,3,4,5])
+-- Eval (SplitAt 3 '[1,2,3,4,5]) :: ([Natural], [Natural])
+-- = '([1, 2, 3], [4, 5])
+data SplitAt :: Nat -> [a] -> Exp ([a], [a])
+type instance Eval (SplitAt n xs) = '(Eval (Take n xs), Eval (Drop n xs))
+
+-- | Take the longest prefix of elements satisfying a predicate.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5])
+-- Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
+-- = [1, 2, 3]
+data TakeWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
+type instance Eval (TakeWhile p '[]) = '[]
+type instance Eval (TakeWhile p (x ': xs)) =
+  Eval (If (Eval (p x))
+      ('(:) x <$> TakeWhile p xs)
+      (Pure '[]))
+
+-- | Drop the longest prefix of elements satisfying a predicate,
+-- evaluate to the remaining suffix.
+--
+-- === __Example__
+--
+-- :kind! Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5])
+-- Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
+-- = [4, 5]
+data DropWhile :: (a -> Exp Bool) -> [a] -> Exp [a]
+type instance Eval (DropWhile p '[]) = '[]
+type instance Eval (DropWhile p (x ': xs)) =
+  Eval (If (Eval (p x))
+      (DropWhile p xs)
+      (Pure (x ': xs)))
+
+
+-- | 'Span', applied to a predicate @p@ and a list @xs@, returns a tuple:
+-- the first component is the longest prefix (possibly empty) of @xs@ whose elements
+-- satisfy @p@;
+-- the second component is the remainder of the list.
+--
+-- See also 'TakeWhile', 'DropWhile', and 'Break'.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Span (Flip (<) 3) [1,2,3,4,1,2])
+-- Eval (Span (Flip (<) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
+-- = '([1, 2], [3, 4, 1, 2])
+--
+-- >>> :kind! Eval (Span (Flip (<) 9) [1,2,3])
+-- Eval (Span (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
+-- = '([1, 2, 3], '[])
+--
+-- >>> :kind! Eval (Span (Flip (<) 0) [1,2,3])
+-- Eval (Span (Flip (<) 0) [1,2,3]) :: ([Natural], [Natural])
+-- = '( '[], [1, 2, 3])
+data Span :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
+type instance Eval (Span p lst) = '( Eval (TakeWhile p lst), Eval (DropWhile p lst))
+
+
+-- | 'Break', applied to a predicate @p@ and a list @xs@, returns a tuple:
+-- the first component is the longest prefix (possibly empty) of @xs@ whose elements
+-- /do not satisfy/ @p@; the second component is the remainder of the list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Break (Flip (>) 3) [1,2,3,4,1,2])
+-- Eval (Break (Flip (>) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
+-- = '([1, 2, 3], [4, 1, 2])
+--
+-- >>> :kind! Eval (Break (Flip (<) 9) [1,2,3])
+-- Eval (Break (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
+-- = '( '[], [1, 2, 3])
+--
+-- >>> :kind! Eval (Break (Flip (>) 9) [1,2,3])
+-- Eval (Break (Flip (>) 9) [1,2,3]) :: ([Natural], [Natural])
+-- = '([1, 2, 3], '[])
+data Break :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
+type instance Eval (Break p lst) = Eval (Span (Not <=< p) lst)
+
+
+-- | List of suffixes of a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Tails [0,1,2,3])
+-- Eval (Tails [0,1,2,3]) :: [[Natural]]
+-- = [[0, 1, 2, 3], [1, 2, 3], [2, 3], '[3]]
+data Tails :: [a] -> Exp [[a]]
+type instance Eval (Tails '[]) = '[]
+type instance Eval (Tails (a ': as)) = (a ': as) ': Eval (Tails as)
+
+
+-- | Return @True@ when the first list is a prefix of the second.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5])
+-- Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5]) :: Bool
+-- = True
+--
+-- >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5])
+-- Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
+-- = False
+--
+-- >>> :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
+-- Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
+-- = True
+--
+-- >>> :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
+-- Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
+-- = False
+data IsPrefixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsPrefixOf xs ys) = IsPrefixOf_ xs ys
+
+-- helper for IsPrefixOf
+type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where
+  IsPrefixOf_ '[] _ = 'True
+  IsPrefixOf_ _ '[] = 'False
+  IsPrefixOf_ (x ': xs) (y ': ys) =
+     Eval ((Eval (TyEq x y)) && IsPrefixOf_ xs ys)
+
+
+-- | Return @True@ when the first list is a suffix of the second.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5])
+-- Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5]) :: Bool
+-- = True
+--
+-- >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5])
+-- Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5]) :: Bool
+-- = False
+--
+-- >>> :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
+-- Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
+-- = True
+--
+-- >>> :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
+-- Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
+-- = False
+data IsSuffixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsSuffixOf xs ys) =
+  Eval (IsPrefixOf (Reverse @@ xs) (Reverse @@ ys))
+
+
+-- | Return @True@ when the first list is contained within the second.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6])
+-- Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6]) :: Bool
+-- = True
+--
+-- >>> :kind! Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6])
+-- Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6]) :: Bool
+-- = False
+data IsInfixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsInfixOf xs ys) = Eval (Any (IsPrefixOf xs) =<< Tails ys)
+
+
+-- | Return @True@ if an element is in a list.
+--
+-- See also 'FindIndex'.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Elem 1 [1,2,3])
+-- Eval (Elem 1 [1,2,3]) :: Bool
+-- = True
+-- >>> :kind! Eval (Elem 1 [2,3])
+-- Eval (Elem 1 [2,3]) :: Bool
+-- = False
+--
+data Elem :: a -> [a] -> Exp Bool
+type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)
+
+-- | Find an element associated with a key in an association list.
+data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
+type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =
+  Eval (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
+
+
+-- | Find @Just@ the first element satisfying a predicate, or evaluate to
+-- @Nothing@ if no element satisfies the predicate.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Find (TyEq 0) [1,2,3])
+-- Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
+-- = Nothing
+--
+-- >>> :kind! Eval (Find (TyEq 0) [1,2,3,0])
+-- Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
+-- = Just 0
+data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
+type instance Eval (Find _p '[]) = 'Nothing
+type instance Eval (Find p (a ': as)) =
+  Eval (If (Eval (p a))
+    (Pure ('Just a))
+    (Find p as))
+
+
+-- | Keep all elements that satisfy a predicate, remove all that don't.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Filter ((>) 3) [1,2,3,0])
+-- Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural]
+-- = [1, 2, 0]
+data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
+type instance Eval (Filter _p '[]) = '[]
+type instance Eval (Filter p (a ': as)) =
+  Eval (If (Eval (p a))
+    ('(:) a <$> Filter p as)
+    (Filter p as))
+
+
+-- | Split a list into one where all elements satisfy a predicate,
+-- and a second where no elements satisfy it.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Partition ((>=) 35) [20, 30, 40, 50])
+-- Eval (Partition ((>=) 35) [20, 30, 40, 50]) :: ([Natural],
+--                                                 [Natural])
+-- = '([20, 30], [40, 50])
+data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
+type instance Eval (Partition p lst) = Eval (Foldr (PartHelp p) '( '[], '[]) lst)
+
+-- | Helper for 'Partition'.
+data PartHelp :: (a -> Exp Bool) -> a -> ([a],[a]) -> Exp ([a],[a])
+type instance Eval (PartHelp p a '(xs,ys)) =
+  If (Eval (p a))
+    '(a ': xs, ys)
+    '(xs, a ': ys)
+
+
+-- | Find the index of an element satisfying the predicate.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
+-- Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural
+-- = Just 2
+--
+-- >>> :kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
+-- Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural
+-- = Nothing
+data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
+type instance Eval (FindIndex _p '[]) = 'Nothing
+type instance Eval (FindIndex p (a ': as)) =
+  Eval (If (Eval (p a))
+    (Pure ('Just 0))
+    (Map ((+) 1) =<< FindIndex p as))
+
+
+-- | Modify an element at a given index.
+--
+-- The list is unchanged if the index is out of bounds.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (SetIndex 2 7 [1,2,3])
+-- Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
+-- = [1, 2, 7]
+data SetIndex :: Nat -> a -> [a] -> Exp [a]
+type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
+
+type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
+  SetIndexImpl _n _a' '[] = '[]
+  SetIndexImpl 0 a' (_a ': as) = a' ': as
+  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as
+
+-- | Combine elements of two lists pairwise.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
+-- Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
+-- = [2, 3, 4]
+data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
+type instance Eval (ZipWith _f '[] _bs) = '[]
+type instance Eval (ZipWith _f _as '[]) = '[]
+type instance Eval (ZipWith f (a ': as) (b ': bs)) =
+  Eval (f a b) ': Eval (ZipWith f as bs)
+
+data Zip :: [a] -> [b] -> Exp [(a, b)]
+type instance Eval (Zip as bs) = Eval (ZipWith (Pure2 '(,)) as bs)
+
+data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
+type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
diff --git a/src/Fcf/Utils.hs b/src/Fcf/Utils.hs
--- a/src/Fcf/Utils.hs
+++ b/src/Fcf/Utils.hs
@@ -1,136 +1,170 @@
-{-# LANGUAGE
-    AllowAmbiguousTypes,
-    ConstraintKinds,
-    DataKinds,
-    PolyKinds,
-    RankNTypes,
-    TypeFamilies,
-    TypeOperators,
-    UndecidableInstances #-}
-
--- | Miscellaneous families.
-module Fcf.Utils
-  ( Error
-  , TError
-  , Constraints
-  , TyEq
-  , Stuck
-  , IsBool(_If)
-  , Case
-  , Match()
-  , type (-->)
-  , Is
-  , Any
-  , Else
-
-    -- * From "Data.Type.Bool"
-  , If
-  ) where
-
-import Data.Kind (Constraint)
-import Data.Type.Bool (If)
-import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))
-
-import Fcf.Core
-import Fcf.Combinators (Pure)
-
--- | Type-level 'error'.
-data Error :: Symbol -> Exp a
-type instance Eval (Error msg) = TypeError ('Text msg)
-
--- | 'TypeError' as a fcf.
-data TError :: ErrorMessage -> Exp a
-type instance Eval (TError msg) = TypeError msg
-
--- | Conjunction of a list of constraints.
-data Constraints :: [Constraint] -> Exp Constraint
-type instance Eval (Constraints '[]) = (() :: Constraint)
-type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))
-
--- | Type equality.
---
--- === __Details__
---
--- The base library also defines a similar @('Type.Equality.==')@;
--- it differs from 'TyEq' in the following ways:
---
--- * 'TyEq' is heterogeneous: its arguments may have different kinds;
--- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is
---   a variable.
-data TyEq :: a -> b -> Exp Bool
-type instance Eval (TyEq a b) = TyEqImpl a b
-
-type family TyEqImpl (a :: k) (b :: l) :: Bool where
-  TyEqImpl a a = 'True
-  TyEqImpl a b = 'False
-
--- | A stuck type that can be used like a type-level 'undefined'.
-type family Stuck :: a
-
--- * Reification
-
-class IsBool (b :: Bool) where
-  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r
-
-instance IsBool 'True  where _If a _ = a
-instance IsBool 'False where _If _ b = b
-
--- * Case splitting
-
-infix 0 -->
-
-data Match j k
-  = Match_ j k
-  | Is_ (j -> Exp Bool) k
-  | Any_ k
-  | Else_ (j -> Exp k)
-
--- | (Limited) equivalent of @\\case { .. }@ syntax. Supports matching of exact
--- values ('-->') and final matches for any value ('Any') or for passing value
--- to subcomputation ('Else'). Examples:
---
--- @
--- type BoolToNat = 'Case'
---   [ 'True  '-->' 0
---   , 'False '-->' 1
---   ]
---
--- type NatToBool = 'Case'
---   [ 0 '-->' 'False
---   , 'Any'   'True
---   ]
---
--- type ZeroOneOrSucc = 'Case'
---   [ 0  '-->' 0
---   , 1  '-->' 1
---   , 'Else'   (('+') 1)
---   ]
--- @
-data Case :: [Match j k] -> j -> Exp k
-type instance Eval (Case ms a) = Case_ ms a
-
-type family Case_ (ms :: [Match j k]) (a :: j) :: k where
-  Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a))
-  Case_ ('Is_ p b    : ms) a = Case_ [ 'True  --> b
-                                     , 'False --> Case_ ms a
-                                     ] (p @@ a)
-  Case_ ('Any_ b     : _ ) _ = b
-  Case_ ('Else_ f    : _ ) a = f @@ a
-
--- | Match concrete type in 'Case'.
-type (-->) = ('Match_ :: j -> k -> Match j k)
-
--- | Match on predicate being successful with type in 'Case'.
-type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)
-
--- | Match any type in 'Case'. Should be used as a final branch.
---
--- Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable")
--- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").
---
--- We recommend importing this one qualified.
-type Any = ('Any_ :: k -> Match j k)
-
--- | Pass type being matched in 'Case' to subcomputation. Should be used as a
--- final branch.
-type Else = ('Else_ :: (j -> Exp k) -> Match j k)
+{-# LANGUAGE
+    AllowAmbiguousTypes,
+    ConstraintKinds,
+    DataKinds,
+    PolyKinds,
+    RankNTypes,
+    TypeFamilies,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Miscellaneous families.
+module Fcf.Utils
+  ( Error
+  , TError
+  , Constraints
+  , TyEq
+  , Stuck
+  , IsBool(_If)
+  , Case
+  , Match()
+  , type (-->)
+  , Is
+  , Any
+  , Else
+
+    -- * From "Data.Type.Bool"
+  , If
+
+    -- * Compile-time asserts
+  , Assert
+  , AssertNot
+
+    -- * Reexports
+  , GHC.TypeLits.ErrorMessage(Text, ShowType, type (:<>:), type (:$$:))
+  , GHC.TypeLits.TypeError
+  ) where
+
+import Data.Kind (Constraint)
+import Data.Type.Bool (If)
+import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))
+
+import Fcf.Core
+import Fcf.Combinators (Pure, type (=<<))
+import Fcf.Data.Bool (Not)
+
+-- | Type-level 'error'.
+data Error :: Symbol -> Exp a
+type instance Eval (Error msg) = TypeError ('Text msg)
+
+-- | 'TypeError' as a fcf.
+data TError :: ErrorMessage -> Exp a
+type instance Eval (TError msg) = TypeError msg
+
+-- | Conjunction of a list of constraints.
+data Constraints :: [Constraint] -> Exp Constraint
+type instance Eval (Constraints '[]) = (() :: Constraint)
+type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))
+
+-- | Type equality.
+--
+-- === __Details__
+--
+-- The base library also defines a similar @('Type.Equality.==')@;
+-- it differs from 'TyEq' in the following ways:
+--
+-- * 'TyEq' is heterogeneous: its arguments may have different kinds;
+-- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is
+--   a variable.
+data TyEq :: a -> b -> Exp Bool
+type instance Eval (TyEq a b) = TyEqImpl a b
+
+type family TyEqImpl (a :: k) (b :: l) :: Bool where
+  TyEqImpl a a = 'True
+  TyEqImpl a b = 'False
+
+-- | A stuck type that can be used like a type-level 'undefined'.
+type family Stuck :: a
+
+-- * Reification
+
+class IsBool (b :: Bool) where
+  _If :: ((b ~ 'True) => r) -> ((b ~ 'False) => r) -> r
+
+instance IsBool 'True  where _If a _ = a
+instance IsBool 'False where _If _ b = b
+
+-- * Case splitting
+
+infix 0 -->
+
+data Match j k
+  = Match_ j k
+  | Is_ (j -> Exp Bool) k
+  | Any_ k
+  | Else_ (j -> Exp k)
+
+-- | (Limited) equivalent of @\\case { .. }@ syntax. Supports matching of exact
+-- values ('-->') and final matches for any value ('Any') or for passing value
+-- to subcomputation ('Else'). Examples:
+--
+-- @
+-- type BoolToNat = 'Case'
+--   [ 'True  '-->' 0
+--   , 'False '-->' 1
+--   ]
+--
+-- type NatToBool = 'Case'
+--   [ 0 '-->' 'False
+--   , 'Any'   'True
+--   ]
+--
+-- type ZeroOneOrSucc = 'Case'
+--   [ 0  '-->' 0
+--   , 1  '-->' 1
+--   , 'Else'   (('+') 1)
+--   ]
+-- @
+data Case :: [Match j k] -> j -> Exp k
+type instance Eval (Case ms a) = Case_ ms a
+
+type family Case_ (ms :: [Match j k]) (a :: j) :: k where
+  Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a))
+  Case_ ('Is_ p b    : ms) a = Case_ [ 'True  --> b
+                                     , 'False --> Case_ ms a
+                                     ] (p @@ a)
+  Case_ ('Any_ b     : _ ) _ = b
+  Case_ ('Else_ f    : _ ) a = f @@ a
+
+-- | Match concrete type in 'Case'.
+type (-->) = ('Match_ :: j -> k -> Match j k)
+
+-- | Match on predicate being successful with type in 'Case'.
+type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)
+
+-- | Match any type in 'Case'. Should be used as a final branch.
+--
+-- Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable")
+-- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").
+--
+-- We recommend importing this one qualified.
+type Any = ('Any_ :: k -> Match j k)
+
+-- | Pass type being matched in 'Case' to subcomputation. Should be used as a
+-- final branch.
+type Else = ('Else_ :: (j -> Exp k) -> Match j k)
+
+-- | A compile-time assert.
+--
+-- Raises the provided `TypeError`, whenever the condition evaluates to `False`.
+--
+-- Usage example:
+-- @
+-- type ExampleAssertionFailure = Eval (
+--   Pure '["foo", "bar"]
+--   >>= Length
+--   >>= Assert ('Text "Assertion") (TyEq Int Void)
+--   )
+-- @
+data Assert :: ErrorMessage -> Exp Bool -> r -> Exp r
+type instance Eval (Assert msg mcond k)
+  = Eval (If (Eval mcond) (Pure k) (TError msg))
+
+-- | Compile-time assert, with condition negated.
+--
+-- Raises the provided `TypeError`, whenever the condition evaluates to `True`.
+--
+-- Also see 'Assert'.
+data AssertNot :: forall r. ErrorMessage -> Exp Bool -> r -> Exp r
+type instance Eval (AssertNot err mcond k)
+  = Eval (Assert err (Not =<< mcond) k)
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -1,100 +1,106 @@
-{-# LANGUAGE
-    CPP,
-    DataKinds,
-    KindSignatures,
-    TypeOperators #-}
-
-import Data.Type.Equality ((:~:)(Refl))
-import qualified Data.Monoid as Monoid
-
-import Fcf.Core (Eval, type (@@))
-import Fcf.Combinators
-import Fcf.Utils (Case, type (-->), Error)
-import qualified Fcf.Utils as Case
-
-import Fcf.Class.Bifunctor
-import Fcf.Class.Foldable
-import Fcf.Class.Monoid
-import Fcf.Class.Ord
-
-import Fcf.Data.Function
-import Fcf.Data.List
-import Fcf.Data.Nat (type (+))
-
-type UnitPrefix = Case
-  [ 0 --> ""
-  , 1 --> "deci"
-  , 2 --> "hecto"
-  , 3 --> "kilo"
-  , 6 --> "mega"
-  , 9 --> "giga"
-  , Case.Any   (Error @@ "Something Else")
-  ]
-
--- Compile-time tests
-
-_ = Refl :: Eval (UnitPrefix 0) :~: ""
-_ = Refl :: Eval (UnitPrefix 3) :~: "kilo"
-
--- * Class
-
--- ** Ord
-
-_ = Refl :: Eval (Compare '( '(), 0 ) '( '(), 1 )) :~: 'LT
-_ = Refl :: Eval (Compare '( 1, 3 ) '( 1, 2 )) :~: 'GT
-_ = Refl :: Eval (Compare ('Left '()) ('Right 'LT)) :~: 'LT
-_ = Refl :: Eval (Compare ('Right 'EQ) ('Right 'EQ)) :~: 'EQ
-_ = Refl :: Eval (Compare '[ 'LT, 'EQ, 'GT ] '[ 'LT, 'EQ, 'GT ]) :~: 'EQ
-_ = Refl :: Eval (Compare 'True 'True) :~: 'EQ
-_ = Refl :: Eval (Compare "A" "B") :~: 'LT
-
-_ = Refl :: Eval (1 <= 1) :~: 'True
-_ = Refl :: Eval (2 <= 1) :~: 'False
-_ = Refl :: Eval (1 < 1) :~: 'False
-_ = Refl :: Eval (1 < 2) :~: 'True
-_ = Refl :: Eval (1 >= 1) :~: 'True
-_ = Refl :: Eval (1 >= 2) :~: 'False
-_ = Refl :: Eval (1 > 1) :~: 'False
-_ = Refl :: Eval (2 > 1) :~: 'True
-
--- ** Monoid
-
-_ = Refl :: Eval ('( '(), '[ 'LT, 'EQ ]) .<> '( '(), '[ 'GT ])) :~: '( '(), '[ 'LT, 'EQ, 'GT ])
-_ = Refl :: Eval ('Nothing .<> 'Just '[]) :~: 'Just '[]
-_ = Refl :: Eval ('LT .<> 'GT) :~: 'LT
-_ = Refl :: Eval ('EQ .<> 'GT) :~: 'GT
-_ = Refl :: Eval ('Monoid.All 'True .<> 'Monoid.All 'False) :~: 'Monoid.All 'False
-_ = Refl :: Eval ('Monoid.Any 'True .<> 'Monoid.Any 'False) :~: 'Monoid.Any 'True
-#if __GLASGOW_HASKELL__ >= 802
-_ = Refl :: Eval ("a" .<> MEmpty) :~: "a"
-#endif
-
--- ** Foldable
-
-_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) '[ 'True, 'False ]) :~: 'Monoid.All 'False
-_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) 'Nothing) :~: 'Monoid.All 'True
-_ = Refl :: Eval (Foldr (.<>) 'LT '[ 'EQ, 'EQ ]) :~: 'LT
-_ = Refl :: Eval (And '[ 'False, 'False ]) :~: 'False
-_ = Refl :: Eval (Or '[ 'False, 'False ]) :~: 'False
-_ = Refl :: Eval (Concat ('Right 'LT)) :~: 'LT
-
-_ = Refl :: FoldMapDefault_ (Pure1 'Monoid.All) 'Nothing :~: 'Monoid.All 'True
-_ = Refl :: FoldrDefault_ (.<>) 'LT '[ 'EQ, 'EQ ] :~: 'LT
-
--- ** Functor
-
-_ = Refl :: Eval (Bimap ((+) 1) (Pure2 '(:) '()) '(8, '[])) :~: '(9, '[ '()])
-_ = Refl :: Eval (First ((+) 1) ('Left 8)) :~: 'Left 9
-_ = Refl :: Eval (First ((+) 1) ('Right 0)) :~: 'Right 0
-_ = Refl :: Eval (Second ((+) 1) ('Left 0)) :~: 'Left 0
-_ = Refl :: Eval (Second ((+) 1) ('Right 8)) :~: 'Right 9
-
--- ** Function
-
-_ = Refl :: Eval (3 & Pure) :~: 3
-_ = Refl :: Eval (((+) `On` Length) '[1,2,3] '[1,2]) :~: 5
-
--- Dummy
-
-main :: IO ()
-main = pure ()
+{-# LANGUAGE
+    CPP,
+    DataKinds,
+    KindSignatures,
+    TypeOperators #-}
+
+import Data.Type.Equality ((:~:)(Refl))
+import qualified Data.Monoid as Monoid
+
+import Fcf.Core (Eval, type (@@))
+import Fcf.Combinators
+import Fcf.Utils (Assert, AssertNot, Case, type (-->), Error, ErrorMessage (Text), TypeError)
+import qualified Fcf.Utils as Utils
+
+import Fcf.Class.Bifunctor
+import Fcf.Class.Foldable
+import Fcf.Class.Monoid
+import Fcf.Class.Ord
+
+import Fcf.Data.Function
+import Fcf.Data.List
+import Fcf.Data.Nat (type (+))
+
+type UnitPrefix = Case
+  [ 0 --> ""
+  , 1 --> "deci"
+  , 2 --> "hecto"
+  , 3 --> "kilo"
+  , 6 --> "mega"
+  , 9 --> "giga"
+  , Utils.Any   (Error @@ "Something Else")
+  ]
+
+-- Compile-time tests
+
+_ = Refl :: Eval (UnitPrefix 0) :~: ""
+_ = Refl :: Eval (UnitPrefix 3) :~: "kilo"
+
+-- * Class
+
+-- ** Ord
+
+_ = Refl :: Eval (Compare '( '(), 0 ) '( '(), 1 )) :~: 'LT
+_ = Refl :: Eval (Compare '( 1, 3 ) '( 1, 2 )) :~: 'GT
+_ = Refl :: Eval (Compare ('Left '()) ('Right 'LT)) :~: 'LT
+_ = Refl :: Eval (Compare ('Right 'EQ) ('Right 'EQ)) :~: 'EQ
+_ = Refl :: Eval (Compare '[ 'LT, 'EQ, 'GT ] '[ 'LT, 'EQ, 'GT ]) :~: 'EQ
+_ = Refl :: Eval (Compare 'True 'True) :~: 'EQ
+_ = Refl :: Eval (Compare "A" "B") :~: 'LT
+
+_ = Refl :: Eval (1 <= 1) :~: 'True
+_ = Refl :: Eval (2 <= 1) :~: 'False
+_ = Refl :: Eval (1 < 1) :~: 'False
+_ = Refl :: Eval (1 < 2) :~: 'True
+_ = Refl :: Eval (1 >= 1) :~: 'True
+_ = Refl :: Eval (1 >= 2) :~: 'False
+_ = Refl :: Eval (1 > 1) :~: 'False
+_ = Refl :: Eval (2 > 1) :~: 'True
+
+-- ** Monoid
+
+_ = Refl :: Eval ('( '(), '[ 'LT, 'EQ ]) .<> '( '(), '[ 'GT ])) :~: '( '(), '[ 'LT, 'EQ, 'GT ])
+_ = Refl :: Eval ('Nothing .<> 'Just '[]) :~: 'Just '[]
+_ = Refl :: Eval ('LT .<> 'GT) :~: 'LT
+_ = Refl :: Eval ('EQ .<> 'GT) :~: 'GT
+_ = Refl :: Eval ('Monoid.All 'True .<> 'Monoid.All 'False) :~: 'Monoid.All 'False
+_ = Refl :: Eval ('Monoid.Any 'True .<> 'Monoid.Any 'False) :~: 'Monoid.Any 'True
+#if __GLASGOW_HASKELL__ >= 802
+_ = Refl :: Eval ("a" .<> MEmpty) :~: "a"
+#endif
+
+-- ** Foldable
+
+_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) '[ 'True, 'False ]) :~: 'Monoid.All 'False
+_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) 'Nothing) :~: 'Monoid.All 'True
+_ = Refl :: Eval (Foldr (.<>) 'LT '[ 'EQ, 'EQ ]) :~: 'LT
+_ = Refl :: Eval (And '[ 'False, 'False ]) :~: 'False
+_ = Refl :: Eval (Or '[ 'False, 'False ]) :~: 'False
+_ = Refl :: Eval (Concat ('Right 'LT)) :~: 'LT
+
+_ = Refl :: FoldMapDefault_ (Pure1 'Monoid.All) 'Nothing :~: 'Monoid.All 'True
+_ = Refl :: FoldrDefault_ (.<>) 'LT '[ 'EQ, 'EQ ] :~: 'LT
+
+-- ** Functor
+
+_ = Refl :: Eval (Bimap ((+) 1) (Pure2 '(:) '()) '(8, '[])) :~: '(9, '[ '()])
+_ = Refl :: Eval (First ((+) 1) ('Left 8)) :~: 'Left 9
+_ = Refl :: Eval (First ((+) 1) ('Right 0)) :~: 'Right 0
+_ = Refl :: Eval (Second ((+) 1) ('Left 0)) :~: 'Left 0
+_ = Refl :: Eval (Second ((+) 1) ('Right 8)) :~: 'Right 9
+
+-- ** Function
+
+_ = Refl :: Eval (3 & Pure) :~: 3
+_ = Refl :: Eval (((+) `On` Length) '[1,2,3] '[1,2]) :~: 5
+
+-- ** Asserts
+
+_ = Refl :: Eval (Pure Monoid.First >>= Assert ('Text "no error") (Pure True)) :~: Monoid.First
+_ = Refl :: Eval (Pure Int >>= AssertNot ('Text "no error") (Pure False)) :~: Int
+-- negative tests (asserts firing at compile time) are a challenge to test. tried, but omitted
+
+-- Dummy
+
+main :: IO ()
+main = pure ()