diff --git a/Build.hs b/Build.hs
--- a/Build.hs
+++ b/Build.hs
@@ -75,6 +75,9 @@
       removeFilesAfter "samples" ["/*.o"]
       cmd "stack ghc"
         "--stack-yaml stack.yaml"
+        "--package mnist-idx"
+        "--package singletons"
+        "--package one-liner-instances"
         "--"
         ("samples" </> src)
         "-o" f
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,28 @@
 Changelog
 =========
 
+Version 0.2.5.0
+---------------
+
+*June 19, 2018*
+
+<https://github.com/mstksg/backprop/releases/tag/v0.2.5.0>
+
+*   Since *type-combinators* has been unmaintained for over two years, and is
+    no longer compatible with modern GHC, the library internals was rewritten
+    to be built on the type-level combinators in the *vinyl* library instead.
+    The main external API change is basically `Every` is replaced with
+    `AllConstrained`, and `Known Length` is replaced with `RecApplicative`.
+
+    To most users, this should make no difference API-wise.  The only users
+    affected should be those using the "-N" family of functions (`backpropN`),
+    who have to pass in heterogeneous lists.  Heterogeneous lists now must be
+    passed in using *vinyl* syntax and operators instead of the previous
+    *type-combinators* interface.
+*   `bpOp` added, to allow for non-rank-N storage of backpropagatable
+    functions in containers without impredicative types.
+*   Benchmarks use *microlens* and *microlens-th* instead of *lens*.
+
 Version 0.2.4.0
 ---------------
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -7,7 +7,6 @@
 [![Build Status](https://travis-ci.org/mstksg/backprop.svg?branch=master)](https://travis-ci.org/mstksg/backprop)
 
 [![Join the chat at https://gitter.im/haskell-backprop/Lobby](https://badges.gitter.im/haskell-backprop/Lobby.svg)](https://gitter.im/haskell-backprop/Lobby?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
-[![Beerpay](https://beerpay.io/mstksg/backprop/badge.svg?style=beer-square)](https://beerpay.io/mstksg/backprop)
 
 [**Documentation and Walkthrough**][docs]
 
@@ -43,8 +42,8 @@
 [blog]: https://blog.jle.im/entry/introducing-the-backprop-library.html
 [gitter]: https://gitter.im/haskell-backprop/Lobby
 
-If you want to provide *backprop* for users of your library, see this **[guide
-to equipping your library with backprop][library]**.
+If you want to provide *backprop* for users of your library, see this [guide
+to equipping your library with backprop][library].
 
 [library]: https://backprop.jle.im/08-equipping-your-library.html
 
diff --git a/backprop.cabal b/backprop.cabal
--- a/backprop.cabal
+++ b/backprop.cabal
@@ -2,10 +2,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: a0a5c07fc3725b8c05a80eee56361aced820e46da1abe7c71526e36fdf63e6e8
+-- hash: 3b204e36b38185be2d92ef4a0e6c3d9ad3cc90fbbf5cf0ccfc4b936a65fb7cac
 
 name:           backprop
-version:        0.2.4.0
+version:        0.2.5.0
 synopsis:       Heterogeneous automatic differentation
 description:    Write your functions to compute your result, and the library will
                 automatically generate functions to compute your gradient.
@@ -63,8 +63,8 @@
     , reflection
     , simple-reflect
     , transformers
-    , type-combinators
     , vector
+    , vinyl >=0.6
   exposed-modules:
       Numeric.Backprop
       Numeric.Backprop.Class
@@ -92,7 +92,8 @@
     , deepseq
     , directory
     , hmatrix >=0.18
-    , lens
+    , microlens
+    , microlens-th
     , mwc-random
     , time
     , vector
diff --git a/bench/bench.hs b/bench/bench.hs
--- a/bench/bench.hs
+++ b/bench/bench.hs
@@ -16,13 +16,15 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 import           Control.DeepSeq
-import           Control.Lens hiding          ((:<), (<.>))
 import           Criterion.Main
 import           Criterion.Types
 import           Data.Char
+import           Data.Functor.Identity
 import           Data.Time
 import           GHC.Generics                 (Generic)
 import           GHC.TypeLits
+import           Lens.Micro
+import           Lens.Micro.TH
 import           Numeric.Backprop
 import           Numeric.Backprop.Class
 import           Numeric.LinearAlgebra.Static
diff --git a/doc/01-getting-started.md b/doc/01-getting-started.md
--- a/doc/01-getting-started.md
+++ b/doc/01-getting-started.md
@@ -13,6 +13,8 @@
 {-# LANGUAGE ViewPatterns     #-}
 
 
+import           Data.List
+import           Debug.SimpleReflect
 import           GHC.Generics (Generic)
 import           GHC.TypeNats
 import           Inliterate.Import
@@ -51,6 +53,24 @@
 gradBP myFunc (9 :: Double)
 ```
 
+We can even be cute with with the *[simple-reflect][]* library:
+
+[simple-reflect]: https://hackage.haskell.org/package/simple-reflect
+
+```haskell top hide
+instance AskInliterate Expr
+```
+
+```haskell eval
+evalBP myFunc (x :: Expr)
+```
+
+
+```haskell eval
+gradBP myFunc (x :: Expr)
+```
+
+
 And that's the gist of the entire library: write your functions to compute your
 things, and `gradBP` will give you the gradients and derivatives of those
 functions.
@@ -159,9 +179,13 @@
 instance KnownNat n => AskInliterate (R n) where
     askInliterate = answerWith (show . H.extract)
 instance AskInliterate Net where
-    askInliterate = answerWith (unlines . ((++ ["-- ..."]) . map lim) . take 5 . lines . show)
+    askInliterate = answerWith $ intercalate "\n"
+                               . ((++ ["-- ..."]) . map lim)
+                               . take 5
+                               . lines
+                               . show
       where
-        lim = (++ " -- ...") . take 200
+        lim = (++ " -- ...") . take 100
 ```
 
 ```haskell eval
diff --git a/doc/index.md b/doc/index.md
--- a/doc/index.md
+++ b/doc/index.md
@@ -52,8 +52,6 @@
 
 [![Join the chat at https://gitter.im/haskell-backprop/Lobby](https://badges.gitter.im/haskell-backprop/Lobby.svg)](https://gitter.im/haskell-backprop/Lobby?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
 
-[![Beerpay](https://beerpay.io/mstksg/backprop/badge.svg?style=beer-square)](https://beerpay.io/mstksg/backprop)
-
 [![backprop on Hackage](https://img.shields.io/hackage/v/backprop.svg?maxAge=86400)](https://hackage.haskell.org/package/backprop)
 [![backprop on Stackage LTS 11](http://stackage.org/package/backprop/badge/lts-11)](http://stackage.org/lts-11/package/backprop)
 [![backprop on Stackage Nightly](http://stackage.org/package/backprop/badge/nightly)](http://stackage.org/nightly/package/backprop)
diff --git a/samples/backprop-mnist.lhs b/samples/backprop-mnist.lhs
--- a/samples/backprop-mnist.lhs
+++ b/samples/backprop-mnist.lhs
@@ -31,24 +31,23 @@
 *   one-liner-instances
 *   split
 
-> {-# LANGUAGE BangPatterns                     #-}
-> {-# LANGUAGE DataKinds                        #-}
-> {-# LANGUAGE DeriveGeneric                    #-}
-> {-# LANGUAGE FlexibleContexts                 #-}
-> {-# LANGUAGE GADTs                            #-}
-> {-# LANGUAGE LambdaCase                       #-}
-> {-# LANGUAGE ScopedTypeVariables              #-}
-> {-# LANGUAGE TemplateHaskell                  #-}
-> {-# LANGUAGE TupleSections                    #-}
-> {-# LANGUAGE TypeApplications                 #-}
-> {-# LANGUAGE ViewPatterns                     #-}
-> {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
-> {-# OPTIONS_GHC -fno-warn-orphans             #-}
-> {-# OPTIONS_GHC -fno-warn-unused-top-binds    #-}
+> {-# LANGUAGE BangPatterns                #-}
+> {-# LANGUAGE DataKinds                   #-}
+> {-# LANGUAGE DeriveGeneric               #-}
+> {-# LANGUAGE FlexibleContexts            #-}
+> {-# LANGUAGE GADTs                       #-}
+> {-# LANGUAGE LambdaCase                  #-}
+> {-# LANGUAGE ScopedTypeVariables         #-}
+> {-# LANGUAGE TemplateHaskell             #-}
+> {-# LANGUAGE TupleSections               #-}
+> {-# LANGUAGE TypeApplications            #-}
+> {-# LANGUAGE ViewPatterns                #-}
+> {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+> {-# OPTIONS_GHC -Wno-orphans             #-}
+> {-# OPTIONS_GHC -Wno-unused-top-binds    #-}
 >
 > import           Control.DeepSeq
 > import           Control.Exception
-> import           Control.Lens hiding ((<.>))
 > import           Control.Monad
 > import           Control.Monad.IO.Class
 > import           Control.Monad.Trans.Maybe
@@ -62,6 +61,8 @@
 > import           Data.Tuple
 > import           GHC.Generics                        (Generic)
 > import           GHC.TypeLits
+> import           Lens.Micro
+> import           Lens.Micro.TH
 > import           Numeric.Backprop
 > import           Numeric.Backprop.Class
 > import           Numeric.LinearAlgebra.Static
diff --git a/samples/extensible-neural.lhs b/samples/extensible-neural.lhs
--- a/samples/extensible-neural.lhs
+++ b/samples/extensible-neural.lhs
@@ -21,26 +21,24 @@
 *   singletons
 *   split
 
-> {-# LANGUAGE BangPatterns         #-}
-> {-# LANGUAGE DataKinds            #-}
-> {-# LANGUAGE DeriveGeneric        #-}
-> {-# LANGUAGE FlexibleContexts     #-}
-> {-# LANGUAGE GADTs                #-}
-> {-# LANGUAGE InstanceSigs         #-}
-> {-# LANGUAGE LambdaCase           #-}
-> {-# LANGUAGE LambdaCase           #-}
-> {-# LANGUAGE RankNTypes           #-}
-> {-# LANGUAGE ScopedTypeVariables  #-}
-> {-# LANGUAGE TemplateHaskell      #-}
-> {-# LANGUAGE TypeApplications     #-}
-> {-# LANGUAGE TypeInType           #-}
-> {-# LANGUAGE TypeOperators        #-}
-> {-# LANGUAGE ViewPatterns         #-}
-> {-# OPTIONS_GHC -fno-warn-orphans #-}
+> {-# LANGUAGE BangPatterns        #-}
+> {-# LANGUAGE DataKinds           #-}
+> {-# LANGUAGE DeriveGeneric       #-}
+> {-# LANGUAGE FlexibleContexts    #-}
+> {-# LANGUAGE GADTs               #-}
+> {-# LANGUAGE InstanceSigs        #-}
+> {-# LANGUAGE LambdaCase          #-}
+> {-# LANGUAGE RankNTypes          #-}
+> {-# LANGUAGE ScopedTypeVariables #-}
+> {-# LANGUAGE TemplateHaskell     #-}
+> {-# LANGUAGE TypeApplications    #-}
+> {-# LANGUAGE TypeInType          #-}
+> {-# LANGUAGE TypeOperators       #-}
+> {-# LANGUAGE ViewPatterns        #-}
+> {-# OPTIONS_GHC -Wno-orphans     #-}
 >
 > import           Control.DeepSeq
 > import           Control.Exception
-> import           Control.Lens hiding             ((<.>))
 > import           Control.Monad
 > import           Control.Monad.IO.Class
 > import           Control.Monad.Primitive
@@ -58,6 +56,8 @@
 > import           Data.Traversable
 > import           Data.Tuple
 > import           GHC.Generics                    (Generic)
+> import           Lens.Micro
+> import           Lens.Micro.TH
 > import           Numeric.Backprop
 > import           Numeric.Backprop.Class
 > import           Numeric.LinearAlgebra.Static
diff --git a/src/Data/Type/Util.hs b/src/Data/Type/Util.hs
--- a/src/Data/Type/Util.hs
+++ b/src/Data/Type/Util.hs
@@ -1,156 +1,138 @@
 {-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE GADTs                  #-}
 {-# LANGUAGE LambdaCase             #-}
+{-# LANGUAGE PatternSynonyms        #-}
 {-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE RankNTypes             #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
 {-# LANGUAGE TupleSections          #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType             #-}
 {-# LANGUAGE TypeOperators          #-}
 
 module Data.Type.Util (
-    Replicate
-  , unzipP
-  , zipP
-  , zipWithPM_
-  , zipWithPM3_
-  , vecToProd
-  , vecLen
-  , lengthProd
-  , listToVecDef
-  , fillProd
+    runzipWith
+  , rzipWithM_
+  , Replicate
+  , VecT(.., (:+)), Vec
+  , vmap
+  , withVec
+  , vecToRec
+  , fillRec
+  , rtraverse_
   , zipVecList
-  , splitProd
-  , traverse1_
+  , splitRec
   , p1, p2, s1, s2
   ) where
 
 import           Data.Bifunctor
-import           Data.Foldable
-import           Data.Type.Conjunction hiding ((:*:))
-import           Data.Type.Length
-import           Data.Type.Nat
-import           Data.Type.Product
-import           Data.Type.Vector
+import           Data.Functor.Identity
+import           Data.Kind
+import           Data.Proxy
+import           Data.Vinyl.Core
+import           Data.Vinyl.TypeLevel
 import           GHC.Generics
 import           Lens.Micro
-import           Type.Class.Higher
-import           Type.Class.Witness
-import           Type.Family.List
-import           Type.Family.Nat
 
--- | @'Replicate' n a@ is a list of @a@s repeated @n@ times.
---
--- >>> :kind! Replicate N3 Int
--- '[Int, Int, Int]
--- >>> :kind! Replicate N5 Double
--- '[Double, Double, Double, Double, Double]
-type family Replicate (n :: N) (a :: k) = (as :: [k]) | as -> n where
-    Replicate 'Z     a = '[]
-    Replicate ('S n) a = a ': Replicate n a
+runzipWith
+    :: forall f g h. ()
+    => (forall x. f x -> (g x, h x))
+    -> (forall xs. Rec f xs -> (Rec g xs, Rec h xs))
+runzipWith f = go
+  where
+    go :: forall ys. Rec f ys -> (Rec g ys, Rec h ys)
+    go = \case
+      RNil    -> (RNil, RNil)
+      x :& xs -> let (y , z ) = f x
+                     (ys, zs) = go xs
+                 in  (y :& ys, z :& zs)
+{-# INLINE runzipWith #-}
 
-vecToProd
-    :: VecT n f a
-    -> Prod f (Replicate n a)
-vecToProd = \case
-    ØV      -> Ø
-    x :* xs -> x :< vecToProd xs
+data VecT :: Nat -> (k -> Type) -> k -> Type where
+    VNil :: VecT 'Z f a
+    (:*) :: !(f a) -> VecT n f a -> VecT ('S n) f a
 
-vecLen
-    :: VecT n f a
-    -> Nat n
-vecLen = \case
-    ØV      -> Z_
-    _ :* xs -> S_ (vecLen xs)
+type Vec n = VecT n Identity
 
-zipWithPM_
-    :: forall h f g as. Applicative h
-    => (forall a. f a -> g a -> h ())
-    -> Prod f as
-    -> Prod g as
-    -> h ()
-zipWithPM_ f = go
-  where
-    go :: forall bs. Prod f bs -> Prod g bs -> h ()
-    go = \case
-      Ø -> \case
-        Ø -> pure ()
-      x :< xs -> \case
-        y :< ys -> f x y *> go xs ys
+pattern (:+) :: a -> Vec n a -> Vec ('S n) a
+pattern x :+ xs = Identity x :* xs
 
-zipWithPM3_
-    :: forall m f g h as. Applicative m
-    => (forall a. f a -> g a -> h a -> m ())
-    -> Prod f as
-    -> Prod g as
-    -> Prod h as
-    -> m ()
-zipWithPM3_ f = go
+vmap
+    :: forall n f g a. ()
+    => (f a -> g a) -> VecT n f a -> VecT n g a
+vmap f = go
   where
-    go :: forall bs. Prod f bs -> Prod g bs -> Prod h bs -> m ()
+    go :: VecT m f a -> VecT m g a
     go = \case
-      Ø -> \case
-        Ø -> \case
-          Ø -> pure ()
-      x :< xs -> \case
-        y :< ys -> \case
-          z :< zs -> f x y z *> go xs ys zs
-
-zipP
-    :: Prod f as
-    -> Prod g as
-    -> Prod (f :&: g) as
-zipP = \case
-    Ø -> \case
-      Ø       -> Ø
-    x :< xs -> \case
-      y :< ys -> x :&: y :< zipP xs ys
-{-# INLINE zipP #-}
+      VNil -> VNil
+      x :* xs -> f x :* go xs
+{-# INLINE vmap #-}
 
-unzipP
-    :: Prod (f :&: g) as
-    -> (Prod f as, Prod g as)
-unzipP = \case
-    Ø               -> (Ø, Ø)
-    (x :&: y) :< zs -> bimap (x :<) (y :<) (unzipP zs)
+withVec
+    :: [f a]
+    -> (forall n. VecT n f a -> r)
+    -> r
+withVec = \case
+    []   -> ($ VNil)
+    x:xs -> \f -> withVec xs (f . (x :*))
+{-# INLINE withVec #-}
 
-lengthProd
-    :: (forall a. f a)
-    -> Length as
-    -> Prod f as
-lengthProd x = \case
-    LZ   -> Ø
-    LS l -> x :< lengthProd x l
+type family Replicate (n :: Nat) (a :: k) = (as :: [k]) | as -> n where
+    Replicate 'Z     a = '[]
+    Replicate ('S n) a = a ': Replicate n a
 
-listToVecDef
-    :: forall f a n. ()
-    => f a
-    -> Nat n
-    -> [f a]
-    -> VecT n f a
-listToVecDef d = go
-  where
-    go :: Nat m -> [f a] -> VecT m f a
-    go = \case
-      Z_   -> const ØV
-      S_ n -> \case
-        []   -> d :* vrep d \\ n
-        x:xs -> x :* go n xs
+vecToRec
+    :: VecT n f a
+    -> Rec f (Replicate n a)
+vecToRec = \case
+    VNil    -> RNil
+    x :* xs -> x :& vecToRec xs
+{-# INLINE vecToRec #-}
 
-fillProd
+fillRec
     :: forall f g as c. ()
     => (forall a. f a -> c -> g a)
-    -> Prod f as
+    -> Rec f as
     -> [c]
-    -> Maybe (Prod g as)
-fillProd f = go
+    -> Maybe (Rec g as)
+fillRec f = go
   where
-    go :: Prod f bs -> [c] -> Maybe (Prod g bs)
+    go :: Rec f bs -> [c] -> Maybe (Rec g bs)
     go = \case
-      Ø -> \_ -> Just Ø
-      x :< xs -> \case
+      RNil -> \_ -> Just RNil
+      x :& xs -> \case
         []   -> Nothing
-        y:ys -> (f x y :<) <$> go xs ys
+        y:ys -> (f x y :&) <$> go xs ys
+{-# INLINE fillRec #-}
 
+rtraverse_
+    :: forall f g. Applicative g
+    => (forall x. f x -> g ())
+    -> (forall xs. Rec f xs -> g ())
+rtraverse_ f = go
+  where
+    go :: Rec f ys -> g ()
+    go = \case
+      RNil    -> pure ()
+      x :& xs -> f x *> go xs
+{-# INLINE rtraverse_ #-}
+
+rzipWithM_
+    :: forall h f g as. Applicative h
+    => (forall a. f a -> g a -> h ())
+    -> Rec f as
+    -> Rec g as
+    -> h ()
+rzipWithM_ f = go
+  where
+    go :: forall bs. Rec f bs -> Rec g bs -> h ()
+    go = \case
+      RNil -> \case
+        RNil -> pure ()
+      x :& xs -> \case
+        y :& ys -> f x y *> go xs ys
+{-# INLINE rzipWithM_ #-}
+
 zipVecList
     :: forall a b c f g n. ()
     => (f a -> Maybe b -> g c)
@@ -161,27 +143,24 @@
   where
     go :: VecT m f a -> [b] -> VecT m g c
     go = \case
-      ØV -> const ØV
+      VNil -> const VNil
       x :* xs -> \case
         []   -> f x Nothing  :* go xs []
         y:ys -> f x (Just y) :* go xs ys
-
-traverse1_
-    :: (Foldable1 t, Applicative g)
-    => (forall a. f a -> g ())
-    -> t f as
-    -> g ()
-traverse1_ f = sequenceA_ . foldMap1 ((:[]) . f)
+{-# INLINE zipVecList #-}
 
-splitProd
-    :: Length as
-    -> Prod f (as ++ bs)
-    -> (Prod f as, Prod f bs)
-splitProd = \case
-    LZ   -> (Ø,)
-    LS l -> \case
-      x :< xs -> first (x :<) $ splitProd l xs
-{-# INLINE splitProd #-}
+splitRec
+    :: forall f as bs. (RecApplicative as)
+    => Rec f (as ++ bs)
+    -> (Rec f as, Rec f bs)
+splitRec = go (rpure Proxy)
+  where
+    go :: Rec Proxy as' -> Rec f (as' ++ bs) -> (Rec f as', Rec f bs)
+    go = \case
+      RNil -> (RNil,)
+      _ :& ps -> \case
+        x :& xs -> first (x :&) $ go ps xs
+{-# INLINE splitRec #-}
 
 p1 :: Lens' ((f :*: g) a) (f a)
 p1 f (x :*: y) = (:*: y) <$> f x
diff --git a/src/Numeric/Backprop.hs b/src/Numeric/Backprop.hs
--- a/src/Numeric/Backprop.hs
+++ b/src/Numeric/Backprop.hs
@@ -75,7 +75,7 @@
   , backprop, E.evalBP, gradBP, backpropWith
     -- ** Multiple inputs
   , backprop2, E.evalBP2, gradBP2, backpropWith2
-  , backpropN, E.evalBPN, gradBPN, backpropWithN, Every
+  , backpropN, E.evalBPN, gradBPN, backpropWithN
     -- * Manipulating 'BVar'
   , E.evalBP0
   , E.constVar, E.auto, E.coerceVar
@@ -100,7 +100,7 @@
   , Op(..)
     -- ** Creation
   , op0, opConst, idOp
-  , opConst'
+  , bpOp
     -- *** Giving gradients directly
   , op1, op2, op3
     -- *** From Isomorphisms
@@ -108,24 +108,19 @@
     -- *** No gradients
   , noGrad1, noGrad
     -- * Utility
-    -- ** Inductive tuples/heterogeneous lists
-  , Prod(..), pattern (:>), only, head'
-  , Tuple, pattern (::<), only_
-  , I(..)
-    -- ** Misc
-  , Reifies
+  , Rec(..), Reifies
   ) where
 
+import           Data.Functor.Identity
 import           Data.Maybe
 import           Data.Reflection
-import           Data.Type.Index
-import           Data.Type.Length
+import           Data.Vinyl
+import           Data.Vinyl.TypeLevel
 import           GHC.Generics
 import           Lens.Micro
 import           Numeric.Backprop.Class
 import           Numeric.Backprop.Explicit (BVar, W)
 import           Numeric.Backprop.Op
-import           Type.Class.Known
 import qualified Numeric.Backprop.Explicit as E
 
 -- $liftops
@@ -180,26 +175,23 @@
 -- arguments or a giant tuple.  However, this could potentially also be
 -- more performant.
 --
--- A @'Prod' ('BVar' s) '[Double, Float, Double]@, for instance, is a tuple
+-- A @'Rec' ('BVar' s) '[Double, Float, Double]@, for instance, is a tuple
 -- of @'BVar' s 'Double'@, @'BVar' s 'Float'@, and @'BVar' s 'Double'@, and
 -- can be pattern matched on using ':<' (cons) and 'Ø' (nil).
 --
--- Tuples can be built and pattern matched on using '::<' (cons) and 'Ø'
--- (nil), as well.
---
--- The @'Every' 'Backprop' as@ in the constraint says that every value in
--- the type-level list @as@ must have a 'Backprop' instance.  This means
--- you can use, say, @'[Double, Float, Int]@, but not @'[Double, Bool,
--- String]@.
+-- The @'AllConstrained' 'Backprop' as@ in the constraint says that every
+-- value in the type-level list @as@ must have a 'Backprop' instance.  This
+-- means you can use, say, @'[Double, Float, Int]@, but not @'[Double,
+-- Bool, String]@.
 --
 -- If you stick to /concerete/, monomorphic usage of this (with specific
--- types, typed into source code, known at compile-time), then @'Every'
--- 'Backprop' as@ should be fulfilled automatically.
+-- types, typed into source code, known at compile-time), then
+-- @'AllConstrained' 'Backprop' as@ should be fulfilled automatically.
 backpropN
-    :: (Every Backprop as, Known Length as, Backprop b)
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> (b, Tuple as)
+    :: (AllConstrained Backprop as, RecApplicative as, Backprop b)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> (b, Rec Identity as)
 backpropN = E.backpropN E.zeroFuncs E.oneFunc
 {-# INLINE backpropN #-}
 
@@ -211,10 +203,10 @@
 --
 -- @since 0.2.0.0
 backpropWithN
-    :: (Every Backprop as, Known Length as)
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> (b, b -> Tuple as)
+    :: (AllConstrained Backprop as, RecApplicative as)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> (b, b -> Rec Identity as)
 backpropWithN = E.backpropWithN E.zeroFuncs
 {-# INLINE backpropWithN #-}
 
@@ -283,10 +275,10 @@
 -- | 'gradBP' generalized to multiple inputs of different types.  See
 -- documentation for 'backpropN' for more details.
 gradBPN
-    :: (Every Backprop as, Known Length as, Backprop b)
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> Tuple as
+    :: (AllConstrained Backprop as, RecApplicative as, Backprop b)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> Rec Identity as
 gradBPN = E.gradBPN E.zeroFuncs E.oneFunc
 {-# INLINE gradBPN #-}
 
@@ -332,6 +324,22 @@
 gradBP2 = E.gradBP2 E.zeroFunc E.zeroFunc E.oneFunc
 {-# INLINE gradBP2 #-}
 
+-- | Create an 'Op' from a backpropagatable function.  Can be useful for
+-- "storing" an otherwise Rank-N backpropagatable function in order to
+-- avoid impredicative types.  But this is pretty uncommon, so this is
+-- mostly just used for low-level internal situations.
+--
+-- @
+-- 'liftOp' . 'bpOp' = 'id'
+-- 'bpOp' . 'liftOp' = 'id'
+-- @
+bpOp
+    :: (AllConstrained Backprop as, RecApplicative as)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Op as b
+bpOp = E.bpOp E.zeroFuncs
+{-# INLINE bpOp #-}
+
 -- | An infix version of 'viewVar', meant to evoke parallels to '^.' from
 -- lens.
 --
@@ -412,6 +420,9 @@
 --
 -- This is the main way to set values inside 'BVar's of container types.
 --
+-- Note that this does not incurr the performance overhead issues of
+-- 'viewVar' and '^^.', and is fairly cheap.
+--
 (.~~)
     :: (Backprop a, Backprop b, Reifies s W)
     => Lens' b a
@@ -435,7 +446,7 @@
 setVar = E.setVar E.addFunc E.addFunc E.zeroFunc
 {-# INLINE setVar #-}
 
--- | An infix version of 'overVar', meant to evoke parallels to '%~~' from
+-- | An infix version of 'overVar', meant to evoke parallels to '%~' from
 -- lens.
 --
 -- With normal values, you can set modify in a value with a lens:
@@ -657,11 +668,11 @@
 --
 -- See "Numeric.Backprop#liftops" and documentation for 'liftOp' for more
 -- information, and "Numeric.Backprop.Op#prod" for a mini-tutorial on using
--- 'Prod' and 'Tuple'.
+-- 'Rec'.
 liftOp
-    :: (Every Backprop as, Known Length as, Reifies s W)
+    :: (AllConstrained Backprop as, RecApplicative as, Reifies s W)
     => Op as b
-    -> Prod (BVar s) as
+    -> Rec (BVar s) as
     -> BVar s b
 liftOp = E.liftOp E.addFuncs
 {-# INLINE liftOp #-}
@@ -778,10 +789,10 @@
 --
 -- @since 0.1.4.0
 isoVarN
-    :: (Every Backprop as, Known Length as, Reifies s W)
-    => (Tuple as -> b)
-    -> (b -> Tuple as)
-    -> Prod (BVar s) as
+    :: (AllConstrained Backprop as, RecApplicative as, Reifies s W)
+    => (Rec Identity as -> b)
+    -> (b -> Rec Identity as)
+    -> Rec (BVar s) as
     -> BVar s b
 isoVarN = E.isoVarN E.addFuncs
 {-# INLINE isoVarN #-}
@@ -949,8 +960,8 @@
        , E.BVGroup s as (Rep (z f)) (Rep (z (BVar s)))
        , Backprop (z f)
        , Backprop (Rep (z f) ())
-       , Every Backprop as
-       , Known Length as
+       , AllConstrained Backprop as
+       , RecApplicative as
        , Reifies s W
        )
     => BVar s (z f)             -- ^ 'BVar' of value
@@ -984,8 +995,8 @@
        , E.BVGroup s as (Rep (z f)) (Rep (z (BVar s)))
        , Backprop (z f)
        , Backprop (Rep (z f) ())
-       , Every Backprop as
-       , Known Length as
+       , AllConstrained Backprop as
+       , RecApplicative as
        , Reifies s W
        )
     => z (BVar s)           -- ^ 'BVar's of fields
@@ -1003,8 +1014,8 @@
        , E.BVGroup s as (Rep (z f)) (Rep (z (BVar s)))
        , Backprop (Rep (z f) ())
        , Backprop (z f)
-       , Every Backprop as
-       , Known Length as
+       , AllConstrained Backprop as
+       , RecApplicative as
        , Reifies s W
        )
 #if MIN_VERSION_base(4,10,0)
diff --git a/src/Numeric/Backprop/Class.hs b/src/Numeric/Backprop/Class.hs
--- a/src/Numeric/Backprop/Class.hs
+++ b/src/Numeric/Backprop/Class.hs
@@ -53,37 +53,29 @@
 import           Data.Coerce
 import           Data.Complex
 import           Data.Data
-import           Data.Foldable hiding         (toList)
+import           Data.Foldable hiding     (toList)
+import           Data.Functor.Compose
 import           Data.Functor.Identity
-import           Data.List.NonEmpty           (NonEmpty(..))
+import           Data.List.NonEmpty       (NonEmpty(..))
 import           Data.Monoid
 import           Data.Ratio
-import           Data.Type.Combinator hiding  ((:.:), Comp1)
-import           Data.Type.Conjunction hiding ((:*:))
-import           Data.Type.Option
-import           Data.Type.Product hiding     (toList)
 import           Data.Void
 import           Data.Word
 import           Debug.SimpleReflect.Expr
 import           GHC.Exts
 import           GHC.Generics
 import           Numeric.Natural
-import           Type.Family.List
-import qualified Control.Arrow                as Arr
-import qualified Data.Functor.Compose         as DFC
-import qualified Data.Functor.Product         as DFP
-import qualified Data.IntMap                  as IM
-import qualified Data.Map                     as M
-import qualified Data.Semigroup               as SG
-import qualified Data.Sequence                as Seq
-import qualified Data.Type.Combinator         as TC
-import qualified Data.Type.Conjunction        as TC
-import qualified Data.Vector                  as V
-import qualified Data.Vector.Generic          as VG
-import qualified Data.Vector.Primitive        as VP
-import qualified Data.Vector.Storable         as VS
-import qualified Data.Vector.Unboxed          as VU
-import qualified Type.Family.Maybe            as M
+import qualified Control.Arrow            as Arr
+import qualified Data.Functor.Product     as DFP
+import qualified Data.IntMap              as IM
+import qualified Data.Map                 as M
+import qualified Data.Semigroup           as SG
+import qualified Data.Sequence            as Seq
+import qualified Data.Vector              as V
+import qualified Data.Vector.Generic      as VG
+import qualified Data.Vector.Primitive    as VP
+import qualified Data.Vector.Storable     as VS
+import qualified Data.Vector.Unboxed      as VU
 
 -- | Class of values that can be backpropagated in general.
 --
@@ -827,13 +819,13 @@
     one (Identity x) = Identity (one x)
     {-# INLINE one #-}
 
-instance Backprop a => Backprop (I a) where
-    zero (I x) = I (zero x)
-    {-# INLINE zero #-}
-    add (I x) (I y) = I (add x y)
-    {-# INLINE add #-}
-    one (I x) = I (one x)
-    {-# INLINE one #-}
+-- instance Backprop a => Backprop (I a) where
+--     zero (I x) = I (zero x)
+--     {-# INLINE zero #-}
+--     add (I x) (I y) = I (add x y)
+--     {-# INLINE add #-}
+--     one (I x) = I (one x)
+--     {-# INLINE one #-}
 
 instance Backprop (Proxy a) where
     zero _ = Proxy
@@ -877,163 +869,163 @@
     one  = oneFunctor
     {-# INLINE one #-}
 
-instance ListC (Backprop <$> (f <$> as)) => Backprop (Prod f as) where
-    zero = \case
-      Ø -> Ø
-      x :< xs -> zero x :< zero xs
-    {-# INLINE zero #-}
-    add = \case
-      Ø -> \case
-        Ø -> Ø
-      x :< xs -> \case
-        y :< ys -> add x y :< add xs ys
-    {-# INLINE add #-}
-    one = \case
-      Ø       -> Ø
-      x :< xs -> one x :< one xs
-    {-# INLINE one #-}
+-- instance ListC (Backprop <$> (f <$> as)) => Backprop (Prod f as) where
+--     zero = \case
+--       Ø -> Ø
+--       x :< xs -> zero x :< zero xs
+--     {-# INLINE zero #-}
+--     add = \case
+--       Ø -> \case
+--         Ø -> Ø
+--       x :< xs -> \case
+--         y :< ys -> add x y :< add xs ys
+--     {-# INLINE add #-}
+--     one = \case
+--       Ø       -> Ø
+--       x :< xs -> one x :< one xs
+--     {-# INLINE one #-}
 
-instance M.MaybeC (Backprop M.<$> (f M.<$> a)) => Backprop (Option f a) where
-    zero = \case
-      Nothing_ -> Nothing_
-      Just_ x  -> Just_ (zero x)
-    {-# INLINE zero #-}
-    add = \case
-      Nothing_ -> \case
-        Nothing_ -> Nothing_
-      Just_ x -> \case
-        Just_ y -> Just_ (add x y)
-    {-# INLINE add #-}
-    one = \case
-      Nothing_ -> Nothing_
-      Just_ x  -> Just_ (one x)
-    {-# INLINE one #-}
+-- instance M.MaybeC (Backprop M.<$> (f M.<$> a)) => Backprop (Option f a) where
+--     zero = \case
+--       Nothing_ -> Nothing_
+--       Just_ x  -> Just_ (zero x)
+--     {-# INLINE zero #-}
+--     add = \case
+--       Nothing_ -> \case
+--         Nothing_ -> Nothing_
+--       Just_ x -> \case
+--         Just_ y -> Just_ (add x y)
+--     {-# INLINE add #-}
+--     one = \case
+--       Nothing_ -> Nothing_
+--       Just_ x  -> Just_ (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance (Backprop (f a), Backprop (g a)) => Backprop ((f :&: g) a) where
-    zero (x :&: y) = zero x :&: zero y
-    {-# INLINE zero #-}
-    add (x1 :&: y1) (x2 :&: y2) = add x1 x2 :&: add y1 y2
-    {-# INLINE add #-}
-    one (x :&: y) = one x :&: one y
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance (Backprop (f a), Backprop (g a)) => Backprop ((f :&: g) a) where
+--     zero (x :&: y) = zero x :&: zero y
+--     {-# INLINE zero #-}
+--     add (x1 :&: y1) (x2 :&: y2) = add x1 x2 :&: add y1 y2
+--     {-# INLINE add #-}
+--     one (x :&: y) = one x :&: one y
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance (Backprop (f a), Backprop (g b)) => Backprop ((f TC.:*: g) '(a, b)) where
-    zero (x TC.:*: y) = zero x TC.:*: zero y
-    {-# INLINE zero #-}
-    add (x1 TC.:*: y1) (x2 TC.:*: y2) = add x1 x2 TC.:*: add y1 y2
-    {-# INLINE add #-}
-    one (x TC.:*: y) = one x TC.:*: one y
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance (Backprop (f a), Backprop (g b)) => Backprop ((f TC.:*: g) '(a, b)) where
+--     zero (x TC.:*: y) = zero x TC.:*: zero y
+--     {-# INLINE zero #-}
+--     add (x1 TC.:*: y1) (x2 TC.:*: y2) = add x1 x2 TC.:*: add y1 y2
+--     {-# INLINE add #-}
+--     one (x TC.:*: y) = one x TC.:*: one y
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (f (g h) a) => Backprop (TC.Comp1 f g h a) where
-    zero (TC.Comp1 x) = TC.Comp1 (zero x)
-    {-# INLINE zero #-}
-    add (TC.Comp1 x) (TC.Comp1 y) = TC.Comp1 (add x y)
-    {-# INLINE add #-}
-    one (TC.Comp1 x) = TC.Comp1 (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (f (g h) a) => Backprop (TC.Comp1 f g h a) where
+--     zero (TC.Comp1 x) = TC.Comp1 (zero x)
+--     {-# INLINE zero #-}
+--     add (TC.Comp1 x) (TC.Comp1 y) = TC.Comp1 (add x y)
+--     {-# INLINE add #-}
+--     one (TC.Comp1 x) = TC.Comp1 (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (f (g a)) => Backprop ((f TC.:.: g) a) where
-    zero (Comp x) = Comp (zero x)
-    {-# INLINE zero #-}
-    add (Comp x) (Comp y) = Comp (add x y)
-    {-# INLINE add #-}
-    one (Comp x) = Comp (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (f (g a)) => Backprop ((f TC.:.: g) a) where
+--     zero (Comp x) = Comp (zero x)
+--     {-# INLINE zero #-}
+--     add (Comp x) (Comp y) = Comp (add x y)
+--     {-# INLINE add #-}
+--     one (Comp x) = Comp (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop w => Backprop (TC.C w a) where
-    zero (TC.C x) = TC.C (zero x)
-    {-# INLINE zero #-}
-    add (TC.C x) (TC.C y) = TC.C (add x y)
-    {-# INLINE add #-}
-    one (TC.C x) = TC.C (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop w => Backprop (TC.C w a) where
+--     zero (TC.C x) = TC.C (zero x)
+--     {-# INLINE zero #-}
+--     add (TC.C x) (TC.C y) = TC.C (add x y)
+--     {-# INLINE add #-}
+--     one (TC.C x) = TC.C (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (p a b) => Backprop (Flip p b a) where
-    zero (Flip x) = Flip (zero x)
-    {-# INLINE zero #-}
-    add (Flip x) (Flip y) = Flip (add x y)
-    {-# INLINE add #-}
-    one (Flip x) = Flip (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (p a b) => Backprop (Flip p b a) where
+--     zero (Flip x) = Flip (zero x)
+--     {-# INLINE zero #-}
+--     add (Flip x) (Flip y) = Flip (add x y)
+--     {-# INLINE add #-}
+--     one (Flip x) = Flip (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (p '(a, b)) => Backprop (Cur p a b) where
-    zero (Cur x) = Cur (zero x)
-    {-# INLINE zero #-}
-    add (Cur x) (Cur y) = Cur (add x y)
-    {-# INLINE add #-}
-    one (Cur x) = Cur (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (p '(a, b)) => Backprop (Cur p a b) where
+--     zero (Cur x) = Cur (zero x)
+--     {-# INLINE zero #-}
+--     add (Cur x) (Cur y) = Cur (add x y)
+--     {-# INLINE add #-}
+--     one (Cur x) = Cur (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (p a b) => Backprop (Uncur p '(a, b)) where
-    zero (Uncur x) = Uncur (zero x)
-    {-# INLINE zero #-}
-    add (Uncur x) (Uncur y) = Uncur (add x y)
-    {-# INLINE add #-}
-    one (Uncur x) = Uncur (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (p a b) => Backprop (Uncur p '(a, b)) where
+--     zero (Uncur x) = Uncur (zero x)
+--     {-# INLINE zero #-}
+--     add (Uncur x) (Uncur y) = Uncur (add x y)
+--     {-# INLINE add #-}
+--     one (Uncur x) = Uncur (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (p '(a, b, c)) => Backprop (Cur3 p a b c) where
-    zero (Cur3 x) = Cur3 (zero x)
-    {-# INLINE zero #-}
-    add (Cur3 x) (Cur3 y) = Cur3 (add x y)
-    {-# INLINE add #-}
-    one (Cur3 x) = Cur3 (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (p '(a, b, c)) => Backprop (Cur3 p a b c) where
+--     zero (Cur3 x) = Cur3 (zero x)
+--     {-# INLINE zero #-}
+--     add (Cur3 x) (Cur3 y) = Cur3 (add x y)
+--     {-# INLINE add #-}
+--     one (Cur3 x) = Cur3 (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (p a b c) => Backprop (Uncur3 p '(a, b, c)) where
-    zero (Uncur3 x) = Uncur3 (zero x)
-    {-# INLINE zero #-}
-    add (Uncur3 x) (Uncur3 y) = Uncur3 (add x y)
-    {-# INLINE add #-}
-    one (Uncur3 x) = Uncur3 (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (p a b c) => Backprop (Uncur3 p '(a, b, c)) where
+--     zero (Uncur3 x) = Uncur3 (zero x)
+--     {-# INLINE zero #-}
+--     add (Uncur3 x) (Uncur3 y) = Uncur3 (add x y)
+--     {-# INLINE add #-}
+--     one (Uncur3 x) = Uncur3 (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (f a a) => Backprop (Join f a) where
-    zero (Join x) = Join (zero x)
-    {-# INLINE zero #-}
-    add (Join x) (Join y) = Join (add x y)
-    {-# INLINE add #-}
-    one (Join x) = Join (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (f a a) => Backprop (Join f a) where
+--     zero (Join x) = Join (zero x)
+--     {-# INLINE zero #-}
+--     add (Join x) (Join y) = Join (add x y)
+--     {-# INLINE add #-}
+--     one (Join x) = Join (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (t (Flip f b) a) => Backprop (Conj t f a b) where
-    zero (Conj x) = Conj (zero x)
-    {-# INLINE zero #-}
-    add (Conj x) (Conj y) = Conj (add x y)
-    {-# INLINE add #-}
-    one (Conj x) = Conj (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (t (Flip f b) a) => Backprop (Conj t f a b) where
+--     zero (Conj x) = Conj (zero x)
+--     {-# INLINE zero #-}
+--     add (Conj x) (Conj y) = Conj (add x y)
+--     {-# INLINE add #-}
+--     one (Conj x) = Conj (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (c (f a)) => Backprop (LL c a f) where
-    zero (LL x) = LL (zero x)
-    {-# INLINE zero #-}
-    add (LL x) (LL y) = LL (add x y)
-    {-# INLINE add #-}
-    one (LL x) = LL (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (c (f a)) => Backprop (LL c a f) where
+--     zero (LL x) = LL (zero x)
+--     {-# INLINE zero #-}
+--     add (LL x) (LL y) = LL (add x y)
+--     {-# INLINE add #-}
+--     one (LL x) = LL (one x)
+--     {-# INLINE one #-}
 
--- | @since 0.2.2.0
-instance Backprop (c (f a)) => Backprop (RR c f a) where
-    zero (RR x) = RR (zero x)
-    {-# INLINE zero #-}
-    add (RR x) (RR y) = RR (add x y)
-    {-# INLINE add #-}
-    one (RR x) = RR (one x)
-    {-# INLINE one #-}
+-- -- | @since 0.2.2.0
+-- instance Backprop (c (f a)) => Backprop (RR c f a) where
+--     zero (RR x) = RR (zero x)
+--     {-# INLINE zero #-}
+--     add (RR x) (RR y) = RR (add x y)
+--     {-# INLINE add #-}
+--     one (RR x) = RR (one x)
+--     {-# INLINE one #-}
 
 -- | @since 0.2.2.0
 instance Backprop a => Backprop (K1 i a p)
@@ -1081,7 +1073,7 @@
 instance (Backprop (f a), Backprop (g a)) => Backprop (DFP.Product f g a)
 
 -- | @since 0.2.2.0
-instance Backprop (f (g a)) => Backprop (DFC.Compose f g a)
+instance Backprop (f (g a)) => Backprop (Compose f g a)
 
 -- | 'add' adds together results; 'zero' and 'one' act on results.
 --
diff --git a/src/Numeric/Backprop/Explicit.hs b/src/Numeric/Backprop/Explicit.hs
--- a/src/Numeric/Backprop/Explicit.hs
+++ b/src/Numeric/Backprop/Explicit.hs
@@ -54,7 +54,7 @@
     -- ** Multiple inputs
   , evalBP0
   , backprop2, evalBP2, gradBP2, backpropWith2
-  , backpropN, evalBPN, gradBPN, backpropWithN, Every
+  , backpropN, evalBPN, gradBPN, backpropWithN, RecApplicative, AllConstrained
     -- * Manipulating 'BVar'
   , constVar, auto, coerceVar
   , viewVar, setVar, overVar
@@ -73,7 +73,7 @@
   , Op(..)
     -- ** Creation
   , op0, opConst, idOp
-  , opConst'
+  , bpOp
     -- *** Giving gradients directly
   , op1, op2, op3
     -- *** From Isomorphisms
@@ -81,37 +81,29 @@
     -- *** No gradients
   , noGrad1, noGrad
     -- * Utility
-    -- ** Inductive tuples/heterogeneous lists
-  , Prod(..), pattern (:>), only, head'
-  , Tuple, pattern (::<), only_
-  , I(..)
-    -- ** Misc
-  , Reifies
+  , Rec(..), Reifies
   ) where
 
 import           Data.Bifunctor
+import           Data.Functor.Identity
+import           Data.Proxy
 import           Data.Reflection
-import           Data.Type.Index
-import           Data.Type.Length
-import           Data.Type.Product
 import           Data.Type.Util
+import           Data.Vinyl.Core
+import           Data.Vinyl.TypeLevel
 import           GHC.Generics              as G
 import           Lens.Micro
 import           Numeric.Backprop.Class
 import           Numeric.Backprop.Internal
 import           Numeric.Backprop.Op
-import           Type.Class.Higher
-import           Type.Class.Known
-import           Type.Class.Witness
-import           Type.Family.List
 import           Unsafe.Coerce
 
 -- | 'ZeroFunc's for every item in a type level list based on their
 -- 'Num' instances
 --
 -- @since 0.2.0.0
-zfNums :: (Every Num as, Known Length as) => Prod ZeroFunc as
-zfNums = map1 (\i -> zfNum \\ every @_ @Num i) indices
+zfNums :: (RecApplicative as, AllConstrained Num as) => Rec ZeroFunc as
+zfNums = rpureConstrained (Proxy @Num) zfNum
 
 -- | 'zeroFunc' for instances of 'Functor'
 --
@@ -124,15 +116,15 @@
 -- 'Num' instances
 --
 -- @since 0.2.0.0
-afNums :: (Every Num as, Known Length as) => Prod AddFunc as
-afNums = map1 (\i -> afNum \\ every @_ @Num i) indices
+afNums :: (RecApplicative as, AllConstrained Num as) => Rec AddFunc as
+afNums = rpureConstrained (Proxy @Num) afNum
 
 -- | 'ZeroFunc's for every item in a type level list based on their
 -- 'Num' instances
 --
 -- @since 0.2.0.0
-ofNums :: (Every Num as, Known Length as) => Prod OneFunc as
-ofNums = map1 (\i -> ofNum \\ every @_ @Num i) indices
+ofNums :: (RecApplicative as, AllConstrained Num as) => Rec OneFunc as
+ofNums = rpureConstrained (Proxy @Num) ofNum
 
 -- | 'OneFunc' for instances of 'Functor'
 --
@@ -145,22 +137,22 @@
 -- type has an instance of 'Backprop'.
 --
 -- @since 0.2.0.0
-zeroFuncs :: (Every Backprop as, Known Length as) => Prod ZeroFunc as
-zeroFuncs = map1 (\i -> zeroFunc \\ every @_ @Backprop i) indices
+zeroFuncs :: (RecApplicative as, AllConstrained Backprop as) => Rec ZeroFunc as
+zeroFuncs = rpureConstrained (Proxy @Backprop) zeroFunc
 
 -- | Generate an 'AddFunc' for every type in a type-level list, if every
 -- type has an instance of 'Backprop'.
 --
 -- @since 0.2.0.0
-addFuncs :: (Every Backprop as, Known Length as) => Prod AddFunc as
-addFuncs = map1 (\i -> addFunc \\ every @_ @Backprop i) indices
+addFuncs :: (RecApplicative as, AllConstrained Backprop as) => Rec AddFunc as
+addFuncs = rpureConstrained (Proxy @Backprop) addFunc
 
 -- | Generate an 'OneFunc' for every type in a type-level list, if every
 -- type has an instance of 'Backprop'.
 --
 -- @since 0.2.0.0
-oneFuncs :: (Every Backprop as, Known Length as) => Prod OneFunc as
-oneFuncs = map1 (\i -> oneFunc \\ every @_ @Backprop i) indices
+oneFuncs :: (RecApplicative as, AllConstrained Backprop as) => Rec OneFunc as
+oneFuncs = rpureConstrained (Proxy @Backprop) oneFunc
 
 -- | Shorter alias for 'constVar', inspired by the /ad/ library.
 --
@@ -172,11 +164,11 @@
 -- | 'Numeric.Backprop.backpropN', but with explicit 'zero' and 'one'.
 backpropN
     :: forall as b. ()
-    => Prod ZeroFunc as
+    => Rec ZeroFunc as
     -> OneFunc b
-    -> (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> (b, Tuple as)
+    -> (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> (b, Rec Identity as)
 backpropN zfs ob f xs = case backpropWithN zfs f xs of
     (y, g) -> (y, g (runOF ob y))
 {-# INLINE backpropN #-}
@@ -188,9 +180,10 @@
     -> (forall s. Reifies s W => BVar s a -> BVar s b)
     -> a
     -> (b, a)
-backprop zfa ofb f = second (getI . head')
-                   . backpropN (zfa :< Ø) ofb (f . head')
-                   . only_
+backprop zfa ofb f = second (\case Identity x :& RNil -> x)
+                   . backpropN (zfa :& RNil) ofb (f . (\case x :& RNil -> x))
+                   . (:& RNil)
+                   . Identity
 {-# INLINE backprop #-}
 
 -- | 'Numeric.Backprop.backpropWith', but with explicit 'zero'.
@@ -201,15 +194,16 @@
     -> (forall s. Reifies s W => BVar s a -> BVar s b)
     -> a
     -> (b, b -> a)
-backpropWith zfa f = second ((getI . head') .)
-                   . backpropWithN (zfa :< Ø) (f . head')
-                   . only_
+backpropWith zfa f = second ((\case Identity x :& RNil -> x) .)
+                   . backpropWithN (zfa :& RNil) (f . (\case x :& RNil -> x))
+                   . (:& RNil)
+                   . Identity
 {-# INLINE backpropWith #-}
 
 -- | 'evalBP' but with no arguments.  Useful when everything is just given
 -- through 'constVar'.
 evalBP0 :: (forall s. Reifies s W => BVar s a) -> a
-evalBP0 x = evalBPN (const x) Ø
+evalBP0 x = evalBPN (const x) RNil
 {-# INLINE evalBP0 #-}
 
 -- | Turn a function @'BVar' s a -> 'BVar' s b@ into the function @a -> b@
@@ -221,7 +215,7 @@
 --
 -- See documentation of 'Numeric.Backprop.backprop' for more information.
 evalBP :: (forall s. Reifies s W => BVar s a -> BVar s b) -> a -> b
-evalBP f = evalBPN (f . head') . only_
+evalBP f = evalBPN (f . (\case x :& RNil -> x)) . (:& RNil)  . Identity
 {-# INLINE evalBP #-}
 
 -- | 'Numeric.Backprop.gradBP', but with explicit 'zero' and 'one'.
@@ -236,11 +230,11 @@
 
 -- | 'Numeric.Backprop.gradBP', Nbut with explicit 'zero' and 'one'.
 gradBPN
-    :: Prod ZeroFunc as
+    :: Rec ZeroFunc as
     -> OneFunc b
-    -> (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> Tuple as
+    -> (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> Rec Identity as
 gradBPN zfas ofb f = snd . backpropN zfas ofb f
 {-# INLINE gradBPN #-}
 
@@ -253,10 +247,10 @@
     -> a
     -> b
     -> (c, (a, b))
-backprop2 zfa zfb ofc f x y = second (\(dx ::< dy ::< Ø) -> (dx, dy)) $
-    backpropN (zfa :< zfb :< Ø) ofc
-        (\(x' :< y' :< Ø) -> f x' y')
-        (x ::< y ::< Ø)
+backprop2 zfa zfb ofc f x y = second (\(Identity dx :& Identity dy :& RNil) -> (dx, dy)) $
+    backpropN (zfa :& zfb :& RNil) ofc
+        (\(x' :& y' :& RNil) -> f x' y')
+        (Identity x :& Identity y :& RNil)
 {-# INLINE backprop2 #-}
 
 -- | 'Numeric.Backprop.backpropWith2', but with explicit 'zero'.
@@ -271,10 +265,10 @@
     -> a
     -> b
     -> (c, c -> (a, b))
-backpropWith2 zfa zfb f x y = second ((\(dx ::< dy ::< Ø) -> (dx, dy)) .) $
-    backpropWithN (zfa :< zfb :< Ø)
-        (\(x' :< y' :< Ø) -> f x' y')
-        (x ::< y ::< Ø)
+backpropWith2 zfa zfb f x y = second ((\(Identity dx :& Identity dy :& RNil) -> (dx, dy)) .) $
+    backpropWithN (zfa :& zfb :& RNil)
+        (\(x' :& y' :& RNil) -> f x' y')
+        (Identity x :& Identity y :& RNil)
 {-# INLINE backpropWith2 #-}
 
 -- | 'evalBP' for a two-argument function.  See
@@ -284,11 +278,12 @@
     -> a
     -> b
     -> c
-evalBP2 f x y = evalBPN (\(x' :< y' :< Ø) -> f x' y') (x ::< y ::< Ø)
+evalBP2 f x y = evalBPN (\(x' :& y' :& RNil) -> f x' y') $ Identity x
+                                                        :& Identity y
+                                                        :& RNil
 {-# INLINE evalBP2 #-}
 
--- | 'gradBP' for a two-argument function.  See
--- 'Numeric.Backprop.backprop2' for notes.
+-- | 'Numeric.Backprop.gradBP2' with explicit 'zero' and 'one'.
 gradBP2
     :: ZeroFunc a
     -> ZeroFunc b
@@ -300,6 +295,14 @@
 gradBP2 zfa zfb ofc f x = snd . backprop2 zfa zfb ofc f x
 {-# INLINE gradBP2 #-}
 
+-- | 'Numeric.Backprop.bpOp' with explicit 'zero'.
+bpOp
+    :: Rec ZeroFunc as
+    -> (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Op as b
+bpOp zfs f = Op (backpropWithN zfs f)
+{-# INLINE bpOp #-}
+
 -- | 'Numeric.Backprop.overVar' with explicit 'add' and 'zero'.
 --
 -- @since 0.2.4.0
@@ -358,10 +361,10 @@
 -- | 'Numeric.Backprop.isoVarN' with explicit 'add' and 'zero'.
 isoVarN
     :: Reifies s W
-    => Prod AddFunc as
-    -> (Tuple as -> b)
-    -> (b -> Tuple as)
-    -> Prod (BVar s) as
+    => Rec AddFunc as
+    -> (Rec Identity as -> b)
+    -> (b -> Rec Identity as)
+    -> Rec (BVar s) as
     -> BVar s b
 isoVarN afs f g = liftOp afs (opIsoN f g)
 {-# INLINE isoVarN #-}
@@ -379,10 +382,10 @@
 class BVGroup s as i o | o -> i, i -> as where
     -- | Helper method for generically "splitting" 'BVar's out of
     -- constructors inside a 'BVar'.  See 'splitBV'.
-    gsplitBV :: Prod AddFunc as -> Prod ZeroFunc as -> BVar s (i ()) -> o ()
+    gsplitBV :: Rec AddFunc as -> Rec ZeroFunc as -> BVar s (i ()) -> o ()
     -- | Helper method for generically "joining" 'BVar's inside
     -- a constructor into a 'BVar'.  See 'joinBV'.
-    gjoinBV  :: Prod AddFunc as -> Prod ZeroFunc as -> o () -> BVar s (i ())
+    gjoinBV  :: Rec AddFunc as -> Rec ZeroFunc as -> o () -> BVar s (i ())
 
 instance BVGroup s '[] (K1 i a) (K1 i (BVar s a)) where
     gsplitBV _ _ = K1 . coerceVar
@@ -413,23 +416,23 @@
          , BVGroup s as i1 o1
          , BVGroup s bs i2 o2
          , cs ~ (as ++ bs)
-         , Known Length as
+         , RecApplicative as
          ) => BVGroup s (i1 () ': i2 () ': cs) (i1 :*: i2) (o1 :*: o2) where
-    gsplitBV (afa :< afb :< afs) (zfa :< zfb :< zfs) xy = x :*: y
+    gsplitBV (afa :& afb :& afs) (zfa :& zfb :& zfs) xy = x :*: y
       where
-        (afas, afbs) = splitProd known afs
-        (zfas, zfbs) = splitProd known zfs
+        (afas, afbs) = splitRec afs
+        (zfas, zfbs) = splitRec zfs
         zfab = ZF $ \(xx :*: yy) -> runZF zfa xx :*: runZF zfb yy
         x = gsplitBV afas zfas . viewVar afa zfab p1 $ xy
         y = gsplitBV afbs zfbs . viewVar afb zfab p2 $ xy
     {-# INLINE gsplitBV #-}
-    gjoinBV (afa :< afb :< afs) (_ :< _ :< zfs) (x :*: y)
+    gjoinBV (afa :& afb :& afs) (_ :& _ :& zfs) (x :*: y)
         = isoVar2 afa afb (:*:) unP
             (gjoinBV afas zfas x)
             (gjoinBV afbs zfbs y)
       where
-        (afas, afbs) = splitProd known afs
-        (zfas, zfbs) = splitProd known zfs
+        (afas, afbs) = splitRec afs
+        (zfas, zfbs) = splitRec zfs
         unP (xx :*: yy) = (xx, yy)
     {-# INLINE gjoinBV #-}
 
@@ -438,9 +441,9 @@
          , BVGroup s as i1 o1
          , BVGroup s bs i2 o2
          , cs ~ (as ++ bs)
-         , Known Length as
+         , RecApplicative as
          ) => BVGroup s (i1 () ': i2 () ': cs) (i1 :+: i2) (o1 :+: o2) where
-    gsplitBV (afa :< afb :< afs) (zfa :< zfb :< zfs) xy =
+    gsplitBV (afa :& afb :& afs) (zfa :& zfb :& zfs) xy =
         case previewVar afa zf s1 xy of
           Just x -> L1 $ gsplitBV afas zfas x
           Nothing -> case previewVar afb zf s2 xy of
@@ -450,17 +453,17 @@
         zf = ZF $ \case
             L1 xx -> L1 $ runZF zfa xx
             R1 yy -> R1 $ runZF zfb yy
-        (afas, afbs) = splitProd known afs
-        (zfas, zfbs) = splitProd known zfs
+        (afas, afbs) = splitRec afs
+        (zfas, zfbs) = splitRec zfs
     {-# INLINE gsplitBV #-}
-    gjoinBV (afa :< afb :< afs) (zfa :< zfb :< zfs) = \case
+    gjoinBV (afa :& afb :& afs) (zfa :& zfb :& zfs) = \case
         L1 x -> liftOp1 afa (op1 (\xx -> (L1 xx, \case L1 d -> d; R1 _ -> runZF zfa xx)))
                     (gjoinBV afas zfas x)
         R1 y -> liftOp1 afb (op1 (\yy -> (R1 yy, \case L1 _ -> runZF zfb yy; R1 d -> d)))
                     (gjoinBV afbs zfbs y)
       where
-        (afas, afbs) = splitProd known afs
-        (zfas, zfbs) = splitProd known zfs
+        (afas, afbs) = splitRec afs
+        (zfas, zfbs) = splitRec zfs
     {-# INLINE gjoinBV #-}
 
 -- | 'Numeric.Backprop.splitBV' with explicit 'add' and 'zero'.
@@ -474,9 +477,9 @@
        , Reifies s W
        )
     => AddFunc (Rep (z f) ())
-    -> Prod AddFunc as
+    -> Rec AddFunc as
     -> ZeroFunc (z f)
-    -> Prod ZeroFunc as
+    -> Rec ZeroFunc as
     -> BVar s (z f)             -- ^ 'BVar' of value
     -> z (BVar s)               -- ^ 'BVar's of fields
 splitBV af afs zf zfs =
@@ -496,9 +499,9 @@
        , Reifies s W
        )
     => AddFunc (z f)
-    -> Prod AddFunc as
+    -> Rec AddFunc as
     -> ZeroFunc (Rep (z f) ())
-    -> Prod ZeroFunc as
+    -> Rec ZeroFunc as
     -> z (BVar s)           -- ^ 'BVar's of fields
     -> BVar s (z f)         -- ^ 'BVar' of combined value
 joinBV af afs zf zfs =
diff --git a/src/Numeric/Backprop/Internal.hs b/src/Numeric/Backprop/Internal.hs
--- a/src/Numeric/Backprop/Internal.hs
+++ b/src/Numeric/Backprop/Internal.hs
@@ -54,28 +54,26 @@
 import           Data.Coerce
 import           Data.Foldable
 import           Data.Function
+import           Data.Functor.Identity
 import           Data.IORef
 import           Data.Kind
 import           Data.Maybe
-import           Data.Monoid hiding           (Any(..))
+import           Data.Monoid hiding        (Any(..))
 import           Data.Proxy
 import           Data.Reflection
-import           Data.Type.Conjunction hiding ((:*:))
-import           Data.Type.Product hiding     (toList)
 import           Data.Type.Util
-import           Data.Type.Vector hiding      (itraverse)
 import           Data.Typeable
-import           GHC.Exts                     (Any)
-import           GHC.Generics                 as G
+import           Data.Vinyl.Core
+import           GHC.Exts                  (Any)
+import           GHC.Generics              as G
 import           Lens.Micro
 import           Lens.Micro.Extras
 import           Numeric.Backprop.Class
 import           Numeric.Backprop.Op
 import           System.IO.Unsafe
-import           Type.Class.Higher
 import           Unsafe.Coerce
-import qualified Data.Vector                  as V
-import qualified Data.Vector.Mutable          as MV
+import qualified Data.Vector               as V
+import qualified Data.Vector.Mutable       as MV
 
 -- | "Zero out" all components of a value.  For scalar values, this should
 -- just be @'const' 0@.  For vectors and matrices, this should set all
@@ -229,13 +227,13 @@
 debugIR IR{..} = show (_bvRef _irIx)
 
 data TapeNode :: Type -> Type where
-    TN :: { _tnInputs :: !(Prod InpRef as)
-          , _tnGrad   :: !(a -> Tuple as)
+    TN :: { _tnInputs :: !(Rec InpRef as)
+          , _tnGrad   :: !(a -> Rec Identity as)
           }
        -> TapeNode a
 
 forceTapeNode :: TapeNode a -> ()
-forceTapeNode (TN inps !_) = foldMap1 forceInpRef inps `seq` ()
+forceTapeNode (TN inps !_) = rfoldMap forceInpRef inps `seq` ()
 {-# INLINE forceTapeNode #-}
 
 data SomeTapeNode :: Type where
@@ -245,7 +243,7 @@
 
 -- | Debugging string for a 'SomeTapeMode'.
 debugSTN :: SomeTapeNode -> String
-debugSTN (STN TN{..}) = show . foldMap1 ((:[]) . debugIR) $ _tnInputs
+debugSTN (STN TN{..}) = show . rfoldMap ((:[]) . debugIR) $ _tnInputs
 
 -- | An ephemeral Wengert Tape in the environment.  Used internally to
 -- track of the computational graph of variables.
@@ -279,29 +277,29 @@
 
 liftOp_
     :: forall s as b. Reifies s W
-    => Prod AddFunc as
+    => Rec AddFunc as
     -> Op as b
-    -> Prod (BVar s) as
+    -> Rec (BVar s) as
     -> IO (BVar s b)
-liftOp_ afs o !vs = case traverse1 (fmap I . bvConst) vs of
+liftOp_ afs o !vs = case rtraverse (fmap Identity . bvConst) vs of
     Just xs -> return $ constVar (evalOp o xs)
     Nothing -> insertNode tn y (reflect (Proxy @s))
   where
-    (y,g) = runOpWith o (map1 (I . _bvVal) vs)
-    tn = TN { _tnInputs = map1 go (zipP afs vs)
+    (y,g) = runOpWith o (rmap (Identity . _bvVal) vs)
+    tn = TN { _tnInputs = rzipWith go afs vs
             , _tnGrad   = g
             }
-    go :: forall a. (AddFunc :&: BVar s) a -> InpRef a
-    go (af :&: (!v)) = forceBVar v `seq` IR v (runAF af) id
+    go :: forall a. AddFunc a -> BVar s a -> InpRef a
+    go af !v = forceBVar v `seq` IR v (runAF af) id
     {-# INLINE go #-}
 {-# INLINE liftOp_ #-}
 
 -- | 'Numeric.Backprop.liftOp', but with explicit 'add' and 'zero'.
 liftOp
     :: forall as b s. Reifies s W
-    => Prod AddFunc as
+    => Rec AddFunc as
     -> Op as b
-    -> Prod (BVar s) as
+    -> Rec (BVar s) as
     -> BVar s b
 liftOp afs o !vs = unsafePerformIO $ liftOp_ afs o vs
 {-# INLINE liftOp #-}
@@ -312,11 +310,11 @@
     -> Op '[a] b
     -> BVar s a
     -> IO (BVar s b)
-liftOp1_ _  o (bvConst->Just x) = return . constVar . evalOp o $ (x ::< Ø)
+liftOp1_ _  o (bvConst->Just x) = return . constVar . evalOp o $ (Identity x :& RNil)
 liftOp1_ af o v = forceBVar v `seq` insertNode tn y (reflect (Proxy @s))
   where
-    (y,g) = runOpWith o (_bvVal v ::< Ø)
-    tn = TN { _tnInputs = IR v (runAF af) id :< Ø
+    (y,g) = runOpWith o (Identity (_bvVal v) :& RNil)
+    tn = TN { _tnInputs = IR v (runAF af) id :& RNil
             , _tnGrad   = g
             }
 {-# INLINE liftOp1_ #-}
@@ -340,13 +338,15 @@
     -> BVar s b
     -> IO (BVar s c)
 liftOp2_ _ _ o (bvConst->Just x) (bvConst->Just y)
-    = return . constVar . evalOp o $ x ::< y ::< Ø
+    = return . constVar . evalOp o $ Identity x :& Identity y :& RNil
 liftOp2_ afa afb o v u = forceBVar v
                    `seq` forceBVar u
                    `seq` insertNode tn y (reflect (Proxy @s))
   where
-    (y,g) = runOpWith o (_bvVal v ::< _bvVal u ::< Ø)
-    tn = TN { _tnInputs = IR v (runAF afa) id :< IR u (runAF afb) id :< Ø
+    (y,g) = runOpWith o $ Identity (_bvVal v)
+                       :& Identity (_bvVal u)
+                       :& RNil
+    tn = TN { _tnInputs = IR v (runAF afa) id :& IR u (runAF afb) id :& RNil
             , _tnGrad   = g
             }
 {-# INLINE liftOp2_ #-}
@@ -374,17 +374,23 @@
     -> BVar s c
     -> IO (BVar s d)
 liftOp3_ _ _ _ o (bvConst->Just x) (bvConst->Just y) (bvConst->Just z)
-    = return . constVar . evalOp o $ x ::< y ::< z ::< Ø
+    = return . constVar . evalOp o $ Identity x
+                                  :& Identity y
+                                  :& Identity z
+                                  :& RNil
 liftOp3_ afa afb afc o v u w = forceBVar v
                          `seq` forceBVar u
                          `seq` forceBVar w
                          `seq` insertNode tn y (reflect (Proxy @s))
   where
-    (y, g) = runOpWith o (_bvVal v ::< _bvVal u ::< _bvVal w ::< Ø)
+    (y, g) = runOpWith o $ Identity (_bvVal v)
+                        :& Identity (_bvVal u)
+                        :& Identity (_bvVal w)
+                        :& RNil
     tn = TN { _tnInputs = IR v (runAF afa) id
-                       :< IR u (runAF afb) id
-                       :< IR w (runAF afc) id
-                       :< Ø
+                       :& IR u (runAF afb) id
+                       :& IR w (runAF afc) id
+                       :& RNil
             , _tnGrad   = g
             }
 {-# INLINE liftOp3_ #-}
@@ -416,8 +422,8 @@
     x = _bvVal v
     y = x ^. l
     tn = TN { _tnInputs = IR v (over l . runAF af) (\g -> set l g (runZF z x))
-                       :< Ø
-            , _tnGrad   = only_
+                       :& RNil
+            , _tnGrad   = (:& RNil) . Identity
             }
 {-# INLINE viewVar_ #-}
 
@@ -448,10 +454,10 @@
   where
     y = _bvVal v & l .~ _bvVal w
     tn = TN { _tnInputs = IR w (runAF afa) id
-                       :< IR v (runAF afb) id
-                       :< Ø
+                       :& IR v (runAF afb) id
+                       :& RNil
             , _tnGrad   = \d -> let (dw,dv) = l (\x -> (x, runZF za x)) d
-                                in  dw ::< dv ::< Ø
+                                in  Identity dw :& Identity dv :& RNil
             }
 {-# INLINE setVar_ #-}
 
@@ -486,12 +492,12 @@
     -> ZeroFunc a
     -> t (BVar s a)
     -> IO (BVar s (t a))
-collectVar_ af z !vs = withV (toList vs) $ \(vVec :: Vec n (BVar s a)) -> do
+collectVar_ af z !vs = withVec (toList vs) $ \(vVec :: VecT n (BVar s) a) -> do
     let tn :: TapeNode (t a)
         tn = TN
-          { _tnInputs = vecToProd (vmap ((\v -> IR v (runAF af) id) . getI) vVec)
-          , _tnGrad   = vecToProd
-                      . zipVecList (\(I v) -> I . fromMaybe (runZF z (_bvVal v))) vVec
+          { _tnInputs = vecToRec (vmap (\v -> IR v (runAF af) id) vVec)
+          , _tnGrad   = vecToRec
+                      . zipVecList (\v -> Identity . fromMaybe (runZF z (_bvVal v))) vVec
                       . toList
           }
     traverse_ (evaluate . forceBVar) vs
@@ -525,8 +531,8 @@
       where
         tn = TN { _tnInputs = IR v (over (ixt t i) . runAF af)
                                    (\g -> set (ixt t i) g (runZF z x))
-                           :< Ø
-                , _tnGrad   = only_
+                           :& RNil
+                , _tnGrad   = (:& RNil) . Identity
                 }
     {-# INLINE go #-}
 {-# INLINE traverseVar' #-}
@@ -598,10 +604,10 @@
       delt <- MV.read _rDelta i
       forM_ delt $ \d -> do
         let gs = _tnGrad (unsafeCoerce d)
-        zipWithPM_ propagate _tnInputs gs
+        rzipWithM_ propagate _tnInputs gs
     {-# INLINE go #-}
-    propagate :: forall x. InpRef x -> I x -> ST s ()
-    propagate (IR v (+*) e) (I d) = case _bvRef v of
+    propagate :: forall x. InpRef x -> Identity x -> ST s ()
+    propagate (IR v (+*) e) (Identity d) = case _bvRef v of
       BRInp i -> flip (MV.modify _rInputs) i $
         unsafeCoerce . bumpMaybe d (+*) e . unsafeCoerce
       BRIx i -> flip (MV.modify _rDelta) i $
@@ -628,28 +634,26 @@
 -- @since 0.2.0.0
 backpropWithN
     :: forall as b. ()
-    => Prod ZeroFunc as
-    -> (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> (b, b -> Tuple as)
+    => Rec ZeroFunc as
+    -> (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> (b, b -> Rec Identity as)
 backpropWithN zfs f !xs = (y, g)
   where
     !(!tp@(!_,!_),!y) = unsafePerformIO $ fillWengert f xs
-    g :: b -> Tuple as
+    g :: b -> Rec Identity as
     g o = runST $ do
         r <- initRunner tp $ bimap getSum (`appEndo` [])
                            . fst
-                           $ traverse1_ go xs
-                           -- zipWithPM_ go zfs xs
+                           $ rtraverse_ go xs
         gradRunner o r tp
         delts <- toList <$> V.freeze (_rInputs r)
         return . fromMaybe (internalError "backpropN") $
-          fillProd (\(zf :&: I x) d -> I $ maybe (runZF zf x) unsafeCoerce d
-                   )
-            (zipP zfs xs)
+          fillRec (\z -> maybe z (Identity . unsafeCoerce))
+            (rzipWith (fmap . runZF) zfs xs)
             delts
       where
-        go :: forall a. I a -> ((Sum Int, Endo [Maybe Any]),())
+        go :: forall a. Identity a -> ((Sum Int, Endo [Maybe Any]),())
         go _ = ((1, Endo (unsafeCoerce (Nothing @a) :)), ())
         {-# INLINE go #-}
 {-# INLINE backpropWithN #-}
@@ -658,33 +662,33 @@
 -- documentation for 'Numeric.Backprop.backpropN' for more details.
 evalBPN
     :: forall as b. ()
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
     -> b
 evalBPN f = snd . unsafePerformIO . fillWengert f
 {-# INLINE evalBPN #-}
 
 fillWengert
     :: forall as b. ()
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
     -> IO ((Int, [SomeTapeNode]), b)
 fillWengert f xs = do
     w <- initWengert
     o <- reify w $ \(Proxy :: Proxy s) -> do
-      let oVar = f (inpProd @s)
+      let oVar = f (inpRec @s)
       evaluate (forceBVar oVar)
       return (_bvVal oVar)
     t <- readIORef (wRef w)
     return (t, o)
   where
-    inpProd :: forall s. Prod (BVar s) as
-    inpProd = evalState (traverse1 (state . go . getI) xs) 0
+    inpRec :: forall s. Rec (BVar s) as
+    inpRec = evalState (rtraverse (state . go . runIdentity) xs) 0
       where
         go :: a -> Int -> (BVar s a, Int)
         go x i = (BV (BRInp i) x, i + 1)
         {-# INLINE go #-}
-    {-# INLINE inpProd #-}
+    {-# INLINE inpRec #-}
 {-# INLINE fillWengert #-}
 
 
diff --git a/src/Numeric/Backprop/Num.hs b/src/Numeric/Backprop/Num.hs
--- a/src/Numeric/Backprop/Num.hs
+++ b/src/Numeric/Backprop/Num.hs
@@ -33,15 +33,11 @@
 -- If you have external types that are not 'Num' instances, consider
 -- instead "Numeric.Backprop.External".
 --
--- If you need a 'Num' instance for tuples, you can use the canonical 2-
--- and 3-tuples for the library in "Numeric.Backprop.Tuple".  If you need
--- one for larger tuples, consider making a custom product type instead
--- (making Num instances with something like
--- <https://hackage.haskell.org/package/one-liner-instances
--- one-liner-instances>).  You can also use the orphan instances in the
--- <https://hackage.haskell.org/package/NumInstances NumInstances> package
--- (in particular, "Data.NumInstances.Tuple") if you are writing an
--- application and do not have to worry about orphan instances.
+-- If you need a 'Num' instance for tuples, you can use the orphan
+-- instances in the <https://hackage.haskell.org/package/NumInstances
+-- NumInstances> package (in particular, "Data.NumInstances.Tuple") if you
+-- are writing an application and do not have to worry about orphan
+-- instances.
 --
 -- See "Numeric.Backprop" for fuller documentation on using these
 -- functions.
@@ -56,7 +52,7 @@
     -- ** Multiple inputs
   , E.evalBP0
   , backprop2, E.evalBP2, gradBP2, backpropWith2
-  , backpropN, E.evalBPN, gradBPN, backpropWithN, Every
+  , backpropN, E.evalBPN, gradBPN, backpropWithN
     -- * Manipulating 'BVar'
   , E.constVar, E.auto, E.coerceVar
   , (^^.), (.~~), (%~~), (^^?), (^^..), (^^?!)
@@ -72,7 +68,7 @@
   , Op(..)
     -- ** Creation
   , op0, opConst, idOp
-  , opConst'
+  , bpOp
     -- *** Giving gradients directly
   , op1, op2, op3
     -- *** From Isomorphisms
@@ -80,56 +76,51 @@
     -- *** No gradients
   , noGrad1, noGrad
     -- * Utility
-    -- ** Inductive tuples/heterogeneous lists
-  , Prod(..), pattern (:>), only, head'
-  , Tuple, pattern (::<), only_
-  , I(..)
-    -- ** Misc
-  , Reifies
+  , Rec(..), Reifies
   ) where
 
+import           Data.Functor.Identity
 import           Data.Maybe
 import           Data.Reflection
-import           Data.Type.Index
-import           Data.Type.Length
+import           Data.Vinyl
+import           Data.Vinyl.TypeLevel
 import           Lens.Micro
 import           Numeric.Backprop.Explicit (BVar, W)
 import           Numeric.Backprop.Op
-import           Type.Class.Known
 import qualified Numeric.Backprop.Explicit as E
 
 -- | 'Numeric.Backprop.backpropN', but with 'Num' constraints instead of
 -- 'Backprop' constraints.
 --
--- The @'Every' 'Num' as@ in the constraint says that every value in the
+-- The @'AllConstrained' 'Num' as@ in the constraint says that every value in the
 -- type-level list @as@ must have a 'Num' instance.  This means you can
 -- use, say, @'[Double, Float, Int]@, but not @'[Double, Bool, String]@.
 --
 -- If you stick to /concerete/, monomorphic usage of this (with specific
--- types, typed into source code, known at compile-time), then @'Every'
+-- types, typed into source code, known at compile-time), then @'AllConstrained'
 -- 'Num' as@ should be fulfilled automatically.
 --
 backpropN
-    :: (Every Num as, Known Length as, Num b)
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> (b, Tuple as)
+    :: (AllConstrained Num as, RecApplicative as, Num b)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> (b, Rec Identity as)
 backpropN = E.backpropN E.zfNums E.ofNum
 {-# INLINE backpropN #-}
 
 -- | 'Numeric.Backprop.backpropWithN', but with 'Num' constraints instead
 -- of 'Backprop' constraints.
 --
--- See 'backpropN' for information on the 'Every' constraint.
+-- See 'backpropN' for information on the 'AllConstrained' constraint.
 --
 -- Note that argument order changed in v0.2.4.
 --
 -- @since 0.2.0.0
 backpropWithN
-    :: (Every Num as, Known Length as)
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> (b, b -> Tuple as)
+    :: (AllConstrained Num as, RecApplicative as)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> (b, b -> Rec Identity as)
 backpropWithN = E.backpropWithN E.zfNums
 {-# INLINE backpropWithN #-}
 
@@ -176,10 +167,10 @@
 -- | 'Numeric.Backprop.gradBPN', but with 'Num' constraints instead of
 -- 'Backprop' constraints.
 gradBPN
-    :: (Every Num as, Known Length as, Num b)
-    => (forall s. Reifies s W => Prod (BVar s) as -> BVar s b)
-    -> Tuple as
-    -> Tuple as
+    :: (AllConstrained Num as, RecApplicative as, Num b)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Rec Identity as
+    -> Rec Identity as
 gradBPN = E.gradBPN E.zfNums E.ofNum
 {-# INLINE gradBPN #-}
 
@@ -220,6 +211,15 @@
 gradBP2 = E.gradBP2 E.zfNum E.zfNum E.ofNum
 {-# INLINE gradBP2 #-}
 
+-- | 'Numeric.Backprop.bpOp', but with 'Num' constraints instead of
+-- 'Backprop' constraints.
+bpOp
+    :: (AllConstrained Num as, RecApplicative as)
+    => (forall s. Reifies s W => Rec (BVar s) as -> BVar s b)
+    -> Op as b
+bpOp = E.bpOp E.zfNums
+{-# INLINE bpOp #-}
+
 -- | 'Numeric.Backprop.^^.', but with 'Num' constraints instead of
 -- 'Backprop' constraints.
 (^^.)
@@ -394,9 +394,9 @@
 -- | 'Numeric.Backprop.liftOp', but with 'Num' constraints instead of
 -- 'Backprop' constraints.
 liftOp
-    :: (Every Num as, Known Length as, Reifies s W)
+    :: (AllConstrained Num as, RecApplicative as, Reifies s W)
     => Op as b
-    -> Prod (BVar s) as
+    -> Rec (BVar s) as
     -> BVar s b
 liftOp = E.liftOp E.afNums
 {-# INLINE liftOp #-}
@@ -473,10 +473,10 @@
 -- | 'Numeric.Backprop.isoVarN', but with 'Num' constraints instead of
 -- 'Backprop' constraints.
 isoVarN
-    :: (Every Num as, Known Length as, Reifies s W)
-    => (Tuple as -> b)
-    -> (b -> Tuple as)
-    -> Prod (BVar s) as
+    :: (AllConstrained Num as, RecApplicative as, Reifies s W)
+    => (Rec Identity as -> b)
+    -> (b -> Rec Identity as)
+    -> Rec (BVar s) as
     -> BVar s b
 isoVarN = E.isoVarN E.afNums
 {-# INLINE isoVarN #-}
diff --git a/src/Numeric/Backprop/Op.hs b/src/Numeric/Backprop/Op.hs
--- a/src/Numeric/Backprop/Op.hs
+++ b/src/Numeric/Backprop/Op.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE LambdaCase           #-}
 {-# LANGUAGE PatternSynonyms      #-}
 {-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE TypeApplications     #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -51,13 +52,13 @@
     Op(..)
   -- ** Tuple Types#prod#
   -- $prod
-  , Prod(..), Tuple, I(..)
+  , Rec(..)
   -- * Running
   -- ** Pure
   , runOp, evalOp, gradOp, gradOpWith
   -- * Creation
   , op0, opConst, idOp
-  , opConst', opLens
+  , opLens
   -- ** Giving gradients directly
   , op1, op2, op3
   -- ** From Isomorphisms
@@ -66,10 +67,7 @@
   , noGrad1, noGrad
   -- * Manipulation
   , composeOp, composeOp1, (~.)
-  , composeOp', composeOp1'
   -- * Utility
-  , pattern (:>), only, head'
-  , pattern (::<), only_
   -- ** Numeric Ops#numops#
   -- $numops
   , (+.), (-.), (*.), negateOp, absOp, signumOp
@@ -79,19 +77,17 @@
   , sinhOp, coshOp, tanhOp, asinhOp, acoshOp, atanhOp
   ) where
 
+import           Control.Applicative
 import           Data.Bifunctor
 import           Data.Coerce
-import           Data.Type.Combinator
-import           Data.Type.Conjunction
-import           Data.Type.Index
-import           Data.Type.Length
-import           Data.Type.Product
+import           Data.Functor.Identity
+import           Data.List
+import           Data.Proxy
 import           Data.Type.Util
+import           Data.Vinyl.Core
+import           Data.Vinyl.TypeLevel
 import           Lens.Micro
 import           Lens.Micro.Extras
-import           Type.Class.Higher
-import           Type.Class.Known
-import           Type.Class.Witness
 
 -- $opdoc
 -- 'Op's contain information on a function as well as its gradient, but
@@ -135,7 +131,7 @@
 -- a function that returns a tuple, containing:
 --
 --     1. An @a@: The result of the function
---     2. An @a -> Tuple as@:  A function that, when given
+--     2. An @a -> Rec Identity as@:  A function that, when given
 --     \(\frac{dz}{dy}\), returns the total gradient
 --     \(\nabla_z \mathbf{x}\).
 --
@@ -155,8 +151,8 @@
 -- For examples of 'Op's implemented from scratch, see the implementations
 -- of '+.', '-.', 'recipOp', 'sinOp', etc.
 --
--- See "Numeric.Backprop.Op#prod" for a mini-tutorial on using 'Prod' and
--- 'Tuple'.
+-- See "Numeric.Backprop.Op#prod" for a mini-tutorial on using 'Rec' and
+-- 'Rec Identity'.
 
 -- | An @'Op' as a@ describes a differentiable function from @as@ to @a@.
 --
@@ -181,8 +177,8 @@
 -- It is simpler to not use this type constructor directly, and instead use
 -- the 'op2', 'op1', 'op2', and 'op3' helper smart constructors.
 --
--- See "Numeric.Backprop.Op#prod" for a mini-tutorial on using 'Prod' and
--- 'Tuple'.
+-- See "Numeric.Backprop.Op#prod" for a mini-tutorial on using 'Rec' and
+-- 'Rec Identity'.
 --
 -- To /use/ an 'Op' with the backprop library, see 'liftOp', 'liftOp1',
 -- 'liftOp2', and 'liftOp3'.
@@ -197,42 +193,11 @@
          -- a continuation to compute the gradient, given the total
          -- derivative of @a@.  See documentation for "Numeric.Backprop.Op"
          -- for more information.
-         runOpWith :: Tuple as -> (a, a -> Tuple as)
+         runOpWith :: Rec Identity as -> (a, a -> Rec Identity as)
        }
 
 -- | Helper wrapper used for the implementation of 'composeOp'.
-newtype OpCont as a = OC { runOpCont :: a -> Tuple as }
-
--- | A version of 'composeOp' taking explicit 'Length', indicating the
--- number of inputs expected and their types.
---
--- Requiring an explicit 'Length' is mostly useful for rare "extremely
--- polymorphic" situations, where GHC can't infer the type and length of
--- the the expected input tuple.  If you ever actually explicitly write
--- down @as@ as a list of types, you should be able to just use
--- 'composeOp'.
-composeOp'
-    :: Every Num as
-    => Length as
-    -> Prod (Op as) bs   -- ^ 'Prod' of 'Op's taking @as@ and returning
-                         --     different @b@ in @bs@
-    -> Op bs c           -- ^ 'OpM' taking eac of the @bs@ from the
-                         --     input 'Prod'.
-    -> Op as c           -- ^ Composed 'Op'
-composeOp' l os o = Op $ \xs ->
-    let (ys, conts) = unzipP
-                    . map1 ((\(x, c) -> I x :&: OC c) . flip runOpWith xs)
-                    $ os
-        (z, gFz) = runOpWith o ys
-        gFunc g0 =
-          let g1 = gFz g0
-              g2s = toList (\(oc :&: I g) -> runOpCont oc g)
-                  $ conts `zipP` g1
-          in  imap1 (\i gs -> I (sum gs) \\ every @_ @Num i)
-                 . foldr (\x -> map1 (uncurryFan (\(I y) -> (y:))) . zipP x)
-                         (lengthProd [] l)
-                 $ g2s
-    in (z, gFunc)
+newtype OpCont as a = OC { runOpCont :: a -> Rec Identity as }
 
 -- | Compose 'Op's together, like 'sequence' for functions, or @liftAN@.
 --
@@ -240,39 +205,39 @@
 -- can compose them with an @'Op' '[b1,b2,b3] c@ to create an @'Op' as
 -- c@.
 composeOp
-    :: (Every Num as, Known Length as)
-    => Prod (Op as) bs   -- ^ 'Prod' of 'Op's taking @as@ and returning
+    :: forall as bs c. (AllConstrained Num as, RecApplicative as)
+    => Rec (Op as) bs   -- ^ 'Rec' of 'Op's taking @as@ and returning
                          --     different @b@ in @bs@
-    -> Op bs c           -- ^ 'Op' taking eac of the @bs@ from the
-                         --     input 'Prod'.
+    -> Op bs c           -- ^ 'OpM' taking eac of the @bs@ from the
+                         --     input 'Rec'.
     -> Op as c           -- ^ Composed 'Op'
-composeOp = composeOp' known
-
--- | A version of 'composeOp1' taking explicit 'Length', indicating the
--- number of inputs expected and their types.
---
--- Requiring an explicit 'Length' is mostly useful for rare "extremely
--- polymorphic" situations, where GHC can't infer the type and length of
--- the the expected input tuple.  If you ever actually explicitly write
--- down @as@ as a list of types, you should be able to just use
--- 'composeOp1'.
-composeOp1'
-    :: Every Num as
-    => Length as
-    -> Op as b
-    -> Op '[b] c
-    -> Op as c
-composeOp1' l = composeOp' l . only
+composeOp os o = Op $ \xs ->
+    let (ys, conts) = runzipWith (bimap Identity OC . flip runOpWith xs) os
+        (z, gFz) = runOpWith o ys
+        gFunc g0 =
+          let g1 = gFz g0
+              g2s :: Rec (Const (Rec Identity as)) bs
+              g2s = rzipWith (\oc (Identity g) -> Const $ runOpCont oc g)
+                        conts g1
+          in  rmap (\(Dict x) -> Identity x)
+                . foldl' (rzipWith (\(Dict !x) (Identity y) ->
+                                        let q = x + y in q `seq` Dict q
+                                   )
+                         )
+                    (rpureConstrained (Proxy @Num) (Dict @Num 0))
+                . rfoldMap ((:[]) . getConst)
+                $ g2s
+    in (z, gFunc)
 
 -- | Convenient wrapper over 'composeOp' for the case where the second
 -- function only takes one input, so the two 'Op's can be directly piped
 -- together, like for '.'.
 composeOp1
-    :: (Every Num as, Known Length as)
+    :: (AllConstrained Num as, RecApplicative as)
     => Op as b
     -> Op '[b] c
     -> Op as c
-composeOp1 = composeOp1' known
+composeOp1 = composeOp . (:& RNil)
 
 -- | Convenient infix synonym for (flipped) 'composeOp1'.  Meant to be used
 -- just like '.':
@@ -285,7 +250,7 @@
 -- @
 infixr 9 ~.
 (~.)
-    :: (Known Length as, Every Num as)
+    :: (AllConstrained Num as, RecApplicative as)
     => Op '[b] c
     -> Op as b
     -> Op as c
@@ -295,18 +260,18 @@
 
 -- | Run the function that an 'Op' encodes, to get the result.
 --
--- >>> runOp (op2 (*)) (3 ::< 5 ::< Ø)
+-- >>> runOp (op2 (*)) (3 :& 5 :& RNil)
 -- 15
-evalOp :: Op as a -> Tuple as -> a
+evalOp :: Op as a -> Rec Identity as -> a
 evalOp o = fst . runOpWith o
 {-# INLINE evalOp #-}
 
 -- | Run the function that an 'Op' encodes, to get the resulting output and
 -- also its gradient with respect to the inputs.
 --
--- >>> gradOp' (op2 (*)) (3 ::< 5 ::< Ø)
--- (15, 5 ::< 3 ::< Ø)
-runOp :: Num a => Op as a -> Tuple as -> (a, Tuple as)
+-- >>> gradOp' (op2 (*)) (3 :& 5 :& RNil)
+-- (15, 5 :& 3 :& RNil)
+runOp :: Num a => Op as a -> Rec Identity as -> (a, Rec Identity as)
 runOp o = second ($ 1) . runOpWith o
 {-# INLINE runOp #-}
 
@@ -317,24 +282,24 @@
 -- information.
 gradOpWith
     :: Op as a      -- ^ 'Op' to run
-    -> Tuple as     -- ^ Inputs to run it with
+    -> Rec Identity as     -- ^ Inputs to run it with
     -> a            -- ^ The total derivative of the result.
-    -> Tuple as     -- ^ The gradient
+    -> Rec Identity as     -- ^ The gradient
 gradOpWith o = snd . runOpWith o
 {-# INLINE gradOpWith #-}
 
 -- | Run the function that an 'Op' encodes, and get the gradient of the
 -- output with respect to the inputs.
 --
--- >>> gradOp (op2 (*)) (3 ::< 5 ::< Ø)
--- 5 ::< 3 ::< Ø
+-- >>> gradOp (op2 (*)) (3 :& 5 :& RNil)
+-- 5 :& 3 :& RNil
 -- -- the gradient of x*y is (y, x)
 --
 -- @
 -- 'gradOp' o xs = 'gradOpWith' o xs 1
 -- @
 --
-gradOp :: Num a => Op as a -> Tuple as -> Tuple as
+gradOp :: Num a => Op as a -> Rec Identity as -> Rec Identity as
 gradOp o i = gradOpWith o i 1
 {-# INLINE gradOp #-}
 
@@ -381,7 +346,7 @@
 -- result is used in the final result.
 --
 -- @since 0.1.3.0
-noGrad :: (Tuple as -> b) -> Op as b
+noGrad :: (Rec Identity as -> b) -> Op as b
 noGrad f = Op (\xs -> (f xs, \_ -> error "noGrad: no gradient defined"))
 {-# INLINE noGrad #-}
 
@@ -397,9 +362,9 @@
 
 -- | An 'Op' that takes @as@ and returns exactly the input tuple.
 --
--- >>> gradOp' opTup (1 ::< 2 ::< 3 ::< Ø)
--- (1 ::< 2 ::< 3 ::< Ø, 1 ::< 1 ::< 1 ::< Ø)
-opTup :: Op as (Tuple as)
+-- >>> gradOp' opTup (1 :& 2 :& 3 :& RNil)
+-- (1 :& 2 :& 3 :& RNil, 1 :& 1 :& 1 :& RNil)
+opTup :: Op as (Rec Identity as)
 opTup = Op $ \xs -> (xs, id)
 {-# INLINE opTup #-}
 
@@ -435,7 +400,7 @@
 -- "Numeric.Backprop" since version 0.1.3.0.
 --
 -- @since 0.1.2.0
-opIsoN :: (Tuple as -> b) -> (b -> Tuple as) -> Op as b
+opIsoN :: (Rec Identity as -> b) -> (b -> Rec Identity as) -> Op as b
 opIsoN to' from' = Op $ \xs -> (to' xs, from')
 {-# INLINE opIsoN #-}
 
@@ -448,26 +413,17 @@
 opLens l = op1 $ \x -> (view l x, \d -> set l d 0)
 {-# INLINE opLens #-}
 
--- | A version of 'opConst' taking explicit 'Length', indicating the
--- number of inputs and their types.
---
--- Requiring an explicit 'Length' is mostly useful for rare "extremely
--- polymorphic" situations, where GHC can't infer the type and length of
--- the the expected input tuple.  If you ever actually explicitly write
--- down @as@ as a list of types, you should be able to just use
--- 'opConst'.
-opConst' :: Every Num as => Length as -> a -> Op as a
-opConst' l x = Op $ const
-    (x , const $ map1 ((0 \\) . every @_ @Num) (indices' l))
-{-# INLINE opConst' #-}
-
 -- | An 'Op' that ignores all of its inputs and returns a given constant
 -- value.
 --
--- >>> gradOp' (opConst 10) (1 ::< 2 ::< 3 ::< Ø)
--- (10, 0 ::< 0 ::< 0 ::< Ø)
-opConst :: (Every Num as, Known Length as) => a -> Op as a
-opConst = opConst' known
+-- >>> gradOp' (opConst 10) (1 :& 2 :& 3 :& RNil)
+-- (10, 0 :& 0 :& 0 :& RNil)
+opConst
+    :: forall as a. (AllConstrained Num as, RecApplicative as)
+    => a
+    -> Op as a
+opConst x = Op $ const
+    (x , const $ rpureConstrained (Proxy @Num) 0)
 {-# INLINE opConst #-}
 
 -- | Create an 'Op' that takes no inputs and always returns the given
@@ -476,14 +432,14 @@
 -- There is no gradient, of course (using 'gradOp' will give you an empty
 -- tuple), because there is no input to have a gradient of.
 --
--- >>> runOp (op0 10) Ø
--- (10, Ø)
+-- >>> runOp (op0 10) RNil
+-- (10, RNil)
 --
 -- For a constant 'Op' that takes input and ignores it, see 'opConst' and
 -- 'opConst''.
 op0 :: a -> Op '[] a
 op0 x = Op $ \case
-    Ø -> (x, const Ø)
+    RNil -> (x, const RNil)
 {-# INLINE op0 #-}
 
 -- | Create an 'Op' of a function taking one input, by giving its explicit
@@ -525,9 +481,9 @@
     :: (a -> (b, b -> a))
     -> Op '[a] b
 op1 f = Op $ \case
-    I x :< Ø ->
+    Identity x :& RNil ->
       let (y, dx) = f x
-      in  (y, \(!d) -> only_ . dx $ d)
+      in  (y, \(!d) -> (:& RNil) . Identity . dx $ d)
 {-# INLINE op1 #-}
 
 -- | Create an 'Op' of a function taking two inputs, by giving its explicit
@@ -571,9 +527,9 @@
     :: (a -> b -> (c, c -> (a, b)))
     -> Op '[a,b] c
 op2 f = Op $ \case
-    I x :< I y :< Ø ->
+    Identity x :& Identity y :& RNil ->
       let (z, dxdy) = f x y
-      in  (z, (\(!dx,!dy) -> dx ::< dy ::< Ø) . dxdy)
+      in  (z, (\(!dx,!dy) -> Identity dx :& Identity dy :& RNil) . dxdy)
 {-# INLINE op2 #-}
 
 -- | Create an 'Op' of a function taking three inputs, by giving its explicit
@@ -582,70 +538,70 @@
     :: (a -> b -> c -> (d, d -> (a, b, c)))
     -> Op '[a,b,c] d
 op3 f = Op $ \case
-    I x :< I y :< I z :< Ø ->
+    Identity x :& Identity y :& Identity z :& RNil ->
       let (q, dxdydz) = f x y z
-      in  (q, (\(!dx, !dy, !dz) -> dx ::< dy ::< dz ::< Ø) . dxdydz)
+      in  (q, (\(!dx, !dy, !dz) -> Identity dx :& Identity dy :& Identity dz :& RNil) . dxdydz)
 {-# INLINE op3 #-}
 
-instance (Known Length as, Every Num as, Num a) => Num (Op as a) where
-    o1 + o2       = composeOp (o1 :< o2 :< Ø) (+.)
+instance (RecApplicative as, AllConstrained Num as, Num a) => Num (Op as a) where
+    o1 + o2       = composeOp (o1 :& o2 :& RNil) (+.)
     {-# INLINE (+) #-}
-    o1 - o2       = composeOp (o1 :< o2 :< Ø) (-.)
+    o1 - o2       = composeOp (o1 :& o2 :& RNil) (-.)
     {-# INLINE (-) #-}
-    o1 * o2       = composeOp (o1 :< o2 :< Ø) (*.)
+    o1 * o2       = composeOp (o1 :& o2 :& RNil) (*.)
     {-# INLINE (*) #-}
-    negate o      = composeOp (o  :< Ø)       negateOp
+    negate o      = composeOp (o  :& RNil)       negateOp
     {-# INLINE negate #-}
-    signum o      = composeOp (o  :< Ø)       signumOp
+    signum o      = composeOp (o  :& RNil)       signumOp
     {-# INLINE signum #-}
-    abs    o      = composeOp (o  :< Ø)       absOp
+    abs    o      = composeOp (o  :& RNil)       absOp
     {-# INLINE abs #-}
     fromInteger x = opConst (fromInteger x)
     {-# INLINE fromInteger #-}
 
-instance (Known Length as, Every Fractional as, Every Num as, Fractional a) => Fractional (Op as a) where
-    o1 / o2        = composeOp (o1 :< o2 :< Ø) (/.)
-    recip o        = composeOp (o  :< Ø)       recipOp
+instance (RecApplicative as, AllConstrained Num as, Fractional a) => Fractional (Op as a) where
+    o1 / o2        = composeOp (o1 :& o2 :& RNil) (/.)
+    recip o        = composeOp (o  :& RNil)       recipOp
     {-# INLINE recip #-}
     fromRational x = opConst (fromRational x)
     {-# INLINE fromRational #-}
 
-instance (Known Length as, Every Floating as, Every Fractional as, Every Num as, Floating a) => Floating (Op as a) where
+instance (RecApplicative as, AllConstrained Floating as, AllConstrained Fractional as, AllConstrained Num as, Floating a) => Floating (Op as a) where
     pi            = opConst pi
     {-# INLINE pi #-}
-    exp   o       = composeOp (o  :< Ø)       expOp
+    exp   o       = composeOp (o  :& RNil)       expOp
     {-# INLINE exp #-}
-    log   o       = composeOp (o  :< Ø)       logOp
+    log   o       = composeOp (o  :& RNil)       logOp
     {-# INLINE log #-}
-    sqrt  o       = composeOp (o  :< Ø)       sqrtOp
+    sqrt  o       = composeOp (o  :& RNil)       sqrtOp
     {-# INLINE sqrt #-}
-    o1 ** o2      = composeOp (o1 :< o2 :< Ø) (**.)
+    o1 ** o2      = composeOp (o1 :& o2 :& RNil) (**.)
     {-# INLINE (**) #-}
-    logBase o1 o2 = composeOp (o1 :< o2 :< Ø) logBaseOp
+    logBase o1 o2 = composeOp (o1 :& o2 :& RNil) logBaseOp
     {-# INLINE logBase #-}
-    sin   o       = composeOp (o  :< Ø)       sinOp
+    sin   o       = composeOp (o  :& RNil)       sinOp
     {-# INLINE sin #-}
-    cos   o       = composeOp (o  :< Ø)       cosOp
+    cos   o       = composeOp (o  :& RNil)       cosOp
     {-# INLINE cos #-}
-    tan   o       = composeOp (o  :< Ø)       tanOp
+    tan   o       = composeOp (o  :& RNil)       tanOp
     {-# INLINE tan #-}
-    asin  o       = composeOp (o  :< Ø)       asinOp
+    asin  o       = composeOp (o  :& RNil)       asinOp
     {-# INLINE asin #-}
-    acos  o       = composeOp (o  :< Ø)       acosOp
+    acos  o       = composeOp (o  :& RNil)       acosOp
     {-# INLINE acos #-}
-    atan  o       = composeOp (o  :< Ø)       atanOp
+    atan  o       = composeOp (o  :& RNil)       atanOp
     {-# INLINE atan #-}
-    sinh  o       = composeOp (o  :< Ø)       sinhOp
+    sinh  o       = composeOp (o  :& RNil)       sinhOp
     {-# INLINE sinh #-}
-    cosh  o       = composeOp (o  :< Ø)       coshOp
+    cosh  o       = composeOp (o  :& RNil)       coshOp
     {-# INLINE cosh #-}
-    tanh  o       = composeOp (o  :< Ø)       tanhOp
+    tanh  o       = composeOp (o  :& RNil)       tanhOp
     {-# INLINE tanh #-}
-    asinh o       = composeOp (o  :< Ø)       asinhOp
+    asinh o       = composeOp (o  :& RNil)       asinhOp
     {-# INLINE asinh #-}
-    acosh o       = composeOp (o  :< Ø)       acoshOp
+    acosh o       = composeOp (o  :& RNil)       acoshOp
     {-# INLINE acosh #-}
-    atanh o       = composeOp (o  :< Ø)       atanhOp
+    atanh o       = composeOp (o  :& RNil)       atanhOp
     {-# INLINE atanh #-}
 
 -- $numops
@@ -793,50 +749,26 @@
 
 -- $prod
 --
--- 'Prod', from the <http://hackage.haskell.org/package/type-combinators
--- type-combinators> library (in "Data.Type.Product") is a heterogeneous
--- list/tuple type, which allows you to tuple together multiple values of
--- different types and operate on them generically.
+-- 'Rec', from the <http://hackage.haskell.org/package/vinyl vinyl> library
+-- (in "Data.Vinyl.Core") is a heterogeneous list/tuple type, which allows
+-- you to tuple together multiple values of different types and operate on
+-- them generically.
 --
--- A @'Prod' f '[a, b, c]@ contains an @f a@, an @f b@, and an @f c@, and
--- is constructed by consing them together with ':<' (using 'Ø' as nil):
+-- A @'Rec' f '[a, b, c]@ contains an @f a@, an @f b@, and an @f c@, and
+-- is constructed by consing them together with ':&' (using 'RNil' as nil):
 --
 -- @
--- 'I' "hello" ':<' I True :< I 7.8 :< Ø    :: 'Prod' 'I' '[String, Bool, Double]
--- 'C' "hello" :< C "world" :< C "ok" :< Ø  :: 'Prod' ('C' String) '[a, b, c]
--- 'Proxy' :< Proxy :< Proxy :< Ø           :: 'Prod' 'Proxy' '[a, b, c]
+-- 'Identity' "hello" ':&' Identity True :& Identity 7.8 :& RNil    :: 'Rec' 'I' '[String, Bool, Double]
+-- 'Const' "hello" :& Const "world" :& Const "ok" :& RNil  :: 'Rec' ('C' String) '[a, b, c]
+-- 'Proxy' :& Proxy :& Proxy :& RNil           :: 'Rec' 'Proxy' '[a, b, c]
 -- @
 --
--- ('I' is the identity functor, and 'C' is the constant functor)
---
 -- So, in general:
 --
 -- @
 -- x :: f a
 -- y :: f b
 -- z :: f c
--- x :< y :< z :< Ø :: Prod f '[a, b, c]
--- @
---
--- If you're having problems typing 'Ø', you can use 'only':
---
--- @
--- only z           :: Prod f '[c]
--- x :< y :< only z :: Prod f '[a, b, c]
+-- x :& y :& z :& RNil :: Rec f '[a, b, c]
 -- @
 --
--- 'Tuple' is provided as a convenient type synonym for 'Prod' 'I', and has
--- a convenient pattern synonym '::<' (and 'only_'), which can also be used
--- for pattern matching:
---
--- @
--- x :: a
--- y :: b
--- z :: c
---
--- 'only_' z             :: 'Tuple' '[c]
--- x '::<' y ::< z ::< Ø :: 'Tuple' '[a, b, c]
--- x ::< y ::< only_ z :: 'Tuple' '[a, b, c]
--- @
-
-