diff --git a/Math/LinearMap/Category.hs b/Math/LinearMap/Category.hs
--- a/Math/LinearMap/Category.hs
+++ b/Math/LinearMap/Category.hs
@@ -19,6 +19,7 @@
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE UnicodeSyntax        #-}
 {-# LANGUAGE TupleSections        #-}
+{-# LANGUAGE TypeApplications     #-}
 {-# LANGUAGE ConstraintKinds      #-}
 {-# LANGUAGE ExplicitNamespaces   #-}
 
@@ -315,11 +316,13 @@
 type Seminorm v = Norm v
 
 -- | @(m<>n|$|v)^2 ⩵ (m|$|v)^2 + (n|$|v)^2@
-instance LSpace v => Semigroup (Norm v) where
-  Norm m <> Norm n = Norm $ m^+^n
+instance ∀ v . LSpace v => Semigroup (Norm v) where
+  Norm m <> Norm n = case dualSpaceWitness @v of
+    DualSpaceWitness -> Norm $ m^+^n
 -- | @mempty|$|v ≡ 0@
-instance LSpace v => Monoid (Seminorm v) where
-  mempty = Norm zeroV
+instance ∀ v . LSpace v => Monoid (Seminorm v) where
+  mempty = case dualSpaceWitness @v of
+    DualSpaceWitness -> Norm zeroV
   mappend = (<>)
 
 -- | A multidimensional variance of points @v@ with some distribution can be
diff --git a/Math/LinearMap/Category/Class.hs b/Math/LinearMap/Category/Class.hs
--- a/Math/LinearMap/Category/Class.hs
+++ b/Math/LinearMap/Category/Class.hs
@@ -365,8 +365,7 @@
 --   'LinearSpace', but makes the condition explicit that the scalar and dual vectors
 --   also form a linear space. 'LinearSpace' only stores that constraint in
 --   'dualSpaceWitness' (to avoid UndecidableSuperclasses).
-type LSpace v = ( LinearSpace v, LinearSpace (Scalar v), LinearSpace (DualVector v)
-                , Num' (Scalar v) )
+type LSpace v = ( LinearSpace v, Num' (Scalar v) )
 
 instance (LinearSpace v, TensorSpace w, Scalar v~s, Scalar w~s)
                => AdditiveGroup (LinearMap s v w) where
diff --git a/Math/LinearMap/Category/Instances/Deriving.hs b/Math/LinearMap/Category/Instances/Deriving.hs
--- a/Math/LinearMap/Category/Instances/Deriving.hs
+++ b/Math/LinearMap/Category/Instances/Deriving.hs
@@ -25,545 +25,1610 @@
 {-# LANGUAGE TemplateHaskell            #-}
 {-# LANGUAGE CPP                        #-}
 {-# LANGUAGE TupleSections              #-}
-
-module Math.LinearMap.Category.Instances.Deriving
-   ( makeLinearSpaceFromBasis, makeFiniteDimensionalFromBasis
-   -- * The instantiated classes
-   , AffineSpace(..), Semimanifold(..), PseudoAffine(..)
-   , TensorSpace(..), LinearSpace(..), FiniteDimensional(..), SemiInner(..)
-   -- * Internals
-   , BasisGeneratedSpace(..), LinearSpaceFromBasisDerivationConfig, def ) where
-
-import Math.LinearMap.Category.Class
-import Math.VectorSpace.Docile
-
-import Data.VectorSpace
-import Data.AffineSpace
-import Data.Basis
-import qualified Data.Map as Map
-import Data.MemoTrie
-import Data.Hashable
-
-import Prelude ()
-import qualified Prelude as Hask
-
-import Control.Category.Constrained.Prelude
-import Control.Arrow.Constrained
-
-import Data.Coerce
-import Data.Type.Coercion
-import Data.Tagged
-import Data.Traversable (traverse)
-import Data.Default.Class
-
-import Math.Manifold.Core.PseudoAffine
-import Math.LinearMap.Asserted
-import Math.VectorSpace.ZeroDimensional
-import Data.VectorSpace.Free
-
-import Language.Haskell.TH
-
--- | Given a type @V@ that is already a 'VectorSpace' and 'HasBasis', generate
---   the other class instances that are needed to use the type with this
---   library.
---
---   Prerequisites: (these can often be derived automatically,
---   using either the @newtype@ \/ @via@ strategy or generics \/ anyclass)
---
--- @
--- instance 'AdditiveGroup' V
---
--- instance 'VectorSpace' V where
---   type Scalar V = -- a simple number type, usually 'Double'
---
--- instance 'HasBasis' V where
---   type Basis V = -- a type with an instance of 'HasTrie'
--- @
---
---   Note that the 'Basis' does /not/ need to be orthonormal – in fact it
---   is not necessary to have a scalar product (i.e. an 'InnerSpace' instance)
---   at all.
---
---   This macro, invoked like
--- @
--- makeLinearSpaceFromBasis [t| V |]
--- @
---
---   will then generate @V@-instances for the classes 'Semimanifold',
---   'PseudoAffine', 'AffineSpace', 'TensorSpace' and 'LinearSpace'.
-makeLinearSpaceFromBasis :: Q Type -> DecsQ
-makeLinearSpaceFromBasis v
-   = makeLinearSpaceFromBasis' def $ deQuantifyType v
-
-data LinearSpaceFromBasisDerivationConfig = LinearSpaceFromBasisDerivationConfig
-instance Default LinearSpaceFromBasisDerivationConfig where
-  def = LinearSpaceFromBasisDerivationConfig
-
--- | More general version of 'makeLinearSpaceFromBasis', that can be used with
---   parameterised types.
-makeLinearSpaceFromBasis' :: LinearSpaceFromBasisDerivationConfig
-                -> Q (Cxt, Type) -> DecsQ
-makeLinearSpaceFromBasis' _ cxtv = do
- (cxt,v) <- do
-   (cxt', v') <- cxtv
-   return (pure cxt', pure v')
- 
- exts <- extsEnabled
- if not $ all (`elem`exts) [TypeFamilies, ScopedTypeVariables, TypeApplications]
-   then reportError "This macro requires -XTypeFamilies, -XScopedTypeVariables and -XTypeApplications."
-   else pure ()
- 
- sequence
-  [ InstanceD Nothing <$> cxt <*> [t|Semimanifold $v|] <*> [d|
-         type instance Needle $v = $v
-#if !MIN_VERSION_manifolds_core(0,6,0)
-         type instance Interior $v = $v
-         $(varP 'toInterior) = pure
-         $(varP 'fromInterior) = id
-         $(varP 'translateP) = Tagged (^+^)
-         $(varP 'semimanifoldWitness) = SemimanifoldWitness BoundarylessWitness
-#endif
-         $(varP '(.+~^)) = (^+^)
-      |]
-  , InstanceD Nothing <$> cxt <*> [t|PseudoAffine $v|] <*> do
-      [d|
-         $(varP '(.-~!)) = (^-^)
-         $(varP '(.-~.)) = \p q -> pure (p^-^q)
-       |]
-  , InstanceD Nothing <$> cxt <*> [t|AffineSpace $v|] <*> [d|
-         type instance Diff $v = $v
-         $(varP '(.+^)) = (^+^)
-         $(varP '(.-.)) = (^-^)
-       |]
-  , InstanceD Nothing <$> cxt <*> [t|TensorSpace $v|] <*> [d|
-         type instance TensorProduct $v w = Basis $v :->: w
-         $(varP 'wellDefinedVector) = \v
-            -> if v==v then Just v else Nothing
-         $(varP 'wellDefinedTensor) = \(Tensor v)
-            -> fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v
-         $(varP 'zeroTensor) = Tensor . trie $ const zeroV
-         $(varP 'toFlatTensor) = LinearFunction $ Tensor . trie . decompose'
-         $(varP 'fromFlatTensor) = LinearFunction $ \(Tensor t)
-                 -> recompose $ enumerate t
-         $(varP 'scalarSpaceWitness) = ScalarSpaceWitness
-         $(varP 'linearManifoldWitness) = LinearManifoldWitness
-#if !MIN_VERSION_manifolds_core(0,6,0)
-                                 BoundarylessWitness
-#endif
-         $(varP 'addTensors) = \(Tensor v) (Tensor w)
-             -> Tensor $ (^+^) <$> v <*> w
-         $(varP 'subtractTensors) = \(Tensor v) (Tensor w)
-             -> Tensor $ (^-^) <$> v <*> w
-         $(varP 'tensorProduct) = bilinearFunction
-           $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w
-         $(varP 'transposeTensor) = LinearFunction $ \(Tensor t)
-              -> sumV [ (tensorProduct-+$>w)-+$>basisValue b
-                      | (b,w) <- enumerate t ]
-         $(varP 'fmapTensor) = bilinearFunction
-           $ \(LinearFunction f) (Tensor t)
-                -> Tensor $ fmap f t
-         $(varP 'fzipTensorWith) = bilinearFunction
-           $ \(LinearFunction f) (Tensor tv, Tensor tw)
-                -> Tensor $ liftA2 (curry f) tv tw
-         $(varP 'coerceFmapTensorProduct) = \_ Coercion
-           -> error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"
-       |]
-  , InstanceD Nothing <$> cxt <*> [t|BasisGeneratedSpace $v|] <*> do
-      [d|
-         $(varP 'proveTensorProductIsTrie) = \φ -> φ
-       |]
-  , InstanceD Nothing <$> cxt <*> [t|LinearSpace $v|] <*> [d|
-         type instance DualVector $v = DualVectorFromBasis $v
-         $(varP 'dualSpaceWitness) = case closedScalarWitness @(Scalar $v) of
-              ClosedScalarWitness -> DualSpaceWitness
-         $(varP 'linearId) = LinearMap . trie $ basisValue
-         $(varP 'tensorId) = tid
-             where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar $v)
-                     => ($v⊗w) +> ($v⊗w)
-                   tid = case dualSpaceWitness @w of
-                    DualSpaceWitness -> LinearMap . trie $ Tensor . \i
-                     -> getTensorProduct $
-                       (fmapTensor @(DualVector w)
-                           -+$>(LinearFunction $ \w -> Tensor . trie
-                                        $ (\j -> if i==j then w else zeroV)
-                                         :: $v⊗w))
-                        -+$> case linearId @w of
-                              LinearMap lw -> Tensor lw :: DualVector w⊗w
-         $(varP 'applyDualVector) = bilinearFunction
-              $ \(DualVectorFromBasis f) v
-                    -> sum [decompose' f i * vi | (i,vi) <- decompose v]
-         $(varP 'applyLinear) = bilinearFunction
-              $ \(LinearMap f) v
-                    -> sumV [vi *^ untrie f i | (i,vi) <- decompose v]
-         $(varP 'applyTensorFunctional) = atf
-             where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar $v)
-                    => Bilinear (DualVector ($v ⊗ u))
-                                   ($v ⊗ u) (Scalar $v)
-                   atf = case dualSpaceWitness @u of
-                    DualSpaceWitness -> bilinearFunction
-                     $ \(LinearMap f) (Tensor t)
-                       -> sum [ (applyDualVector-+$>fi)-+$>untrie t i
-                              | (i, fi) <- enumerate f ]
-         $(varP 'applyTensorLinMap) = atlm
-             where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w
-                                   , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v )
-                            => Bilinear (($v ⊗ u) +> w) ($v ⊗ u) w
-                   atlm = case dualSpaceWitness @u of
-                     DualSpaceWitness -> bilinearFunction
-                       $ \(LinearMap f) (Tensor t)
-                        -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))
-                                   -+$> untrie t i
-                                | (i, Tensor fi) <- enumerate f ]
-         $(varP 'useTupleLinearSpaceComponents) = \_ -> usingNonTupleTypeAsTupleError
- 
-       |]
-  ]
-
-data FiniteDimensionalFromBasisDerivationConfig
-         = FiniteDimensionalFromBasisDerivationConfig
-instance Default FiniteDimensionalFromBasisDerivationConfig where
-  def = FiniteDimensionalFromBasisDerivationConfig
-
--- | Like 'makeLinearSpaceFromBasis', but additionally generate instances for
---   'FiniteDimensional' and 'SemiInner'.
-makeFiniteDimensionalFromBasis :: Q Type -> DecsQ
-makeFiniteDimensionalFromBasis v
-   = makeFiniteDimensionalFromBasis' def $ deQuantifyType v
-
-makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig
-              -> Q (Cxt, Type) -> DecsQ
-makeFiniteDimensionalFromBasis' _ cxtv = do
- generalInsts <- makeLinearSpaceFromBasis' def cxtv
- (cxt,v) <- do
-   (cxt', v') <- cxtv
-   return (pure cxt', pure v')
- vtnameHash <- abs . hash . show <$> v
- 
- fdInsts <- sequence
-  [ InstanceD Nothing <$> cxt <*> [t|FiniteDimensional $v|] <*> do
-    
-    -- This is a hack. Ideally, @newName@ should generate globally unique names,
-    -- but it doesn't, so we append a hash of the vector space type.
-    -- Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/13054
-    subBasisCstr <- newName $ "CompleteBasis"++show vtnameHash
-
-    tySyns <- sequence [
-#if MIN_VERSION_template_haskell(2,15,0)
-       DataInstD [] Nothing
-          <$> (AppT (ConT ''SubBasis) <$> v)
-          <*> pure Nothing
-          <*> pure [NormalC subBasisCstr []]
-          <*> pure []
-#else
-       DataInstD [] ''SubBasis
-          <$> ((:[]) <$> v)
-          <*> pure Nothing
-          <*> pure [NormalC subBasisCstr []]
-          <*> pure []
-#endif
-     ]
-    methods <- [d|
-        $(varP 'entireBasis) = $(conE subBasisCstr)
-        $(varP 'enumerateSubBasis) =
-            \ $(conP subBasisCstr []) -> basisValue . fst <$> enumerate (trie $ const ())
-        $(varP 'tensorEquality)
-          = \(Tensor t) (Tensor t')  -> and [ti == untrie t' i | (i,ti) <- enumerate t]
-        $(varP 'decomposeLinMap) = dlm
-           where dlm :: ∀ w . ($v+>w)
-                       -> (SubBasis $v, [w]->[w])
-                 dlm (LinearMap f) = 
-                         ( $(conE subBasisCstr)
-                         , (map snd (enumerate f) ++) )
-        $(varP 'decomposeLinMapWithin) = dlm
-           where dlm :: ∀ w . SubBasis $v
-                        -> ($v+>w)
-                        -> Either (SubBasis $v, [w]->[w])
-                                  ([w]->[w])
-                 dlm $(conP subBasisCstr []) (LinearMap f) = 
-                         (Right (map snd (enumerate f) ++) )
-        $(varP 'recomposeSB) = rsb
-           where rsb :: SubBasis $v
-                        -> [Scalar $v]
-                        -> ($v, [Scalar $v])
-                 rsb $(conP subBasisCstr []) cs = first recompose
-                           $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs
-        $(varP 'recomposeSBTensor) = rsbt
-           where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar $v)
-                     => SubBasis $v -> SubBasis w
-                        -> [Scalar $v]
-                        -> ($v⊗w, [Scalar $v])
-                 rsbt $(conP subBasisCstr []) sbw ws = 
-                         (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))
-                           $ zipConsumeWith' (\i cs' -> first (\c->(i,c))
-                                                       $ recomposeSB sbw cs')
-                                 (fst <$> enumerate (trie $ const ())) ws)
-        $(varP 'recomposeLinMap) = rlm
-           where rlm :: ∀ w . SubBasis $v
-                        -> [w]
-                        -> ($v+>w, [w])
-                 rlm $(conP subBasisCstr []) ws = 
-                    (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))
-                      $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)
-        $(varP 'recomposeContraLinMap) = rclm
-           where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar $v, Hask.Functor f)
-                      => (f (Scalar w) -> w) -> f (DualVectorFromBasis $v)
-                        -> ($v+>w)
-                 rclm f vs = 
-                       (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))
-        $(varP 'recomposeContraLinMapTensor) = rclm
-           where rclm :: ∀ u w f
-                   . ( FiniteDimensional u, LinearSpace w
-                     , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v, Hask.Functor f
-                     )
-                      => (f (Scalar w) -> w) -> f ($v+>DualVector u)
-                        -> (($v⊗u)+>w)
-                 rclm f vus = case dualSpaceWitness @u of
-                   DualSpaceWitness -> 
-                              (
-                       (LinearMap $ trie
-                           (\i -> case recomposeContraLinMap @u @w @f f
-                                      $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis $v)) vus of
-                              LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))
-        $(varP 'uncanonicallyFromDual) = LinearFunction getDualVectorFromBasis
-        $(varP 'uncanonicallyToDual) = LinearFunction DualVectorFromBasis
-
-      |]
-    return $ tySyns ++ methods
-  , InstanceD Nothing <$> cxt <*> [t|SemiInner $v|] <*> do
-     [d|
-        $(varP 'dualBasisCandidates)
-           = cartesianDualBasisCandidates
-               (enumerateSubBasis CompleteDualVBasis)
-               (\v -> map (abs . realToFrac . decompose' v . fst)
-                       $ enumerate (trie $ const ()) )
-      |]
-  ]
- return $ generalInsts ++ fdInsts
-
-
-deQuantifyType :: Q Type -> Q (Cxt, Type)
-deQuantifyType t = do
-   t' <- t
-   return $ case t' of
-     ForallT _ cxt instT -> (cxt, instT)
-     _ -> ([], t')
-
-
-newtype DualVectorFromBasis v = DualVectorFromBasis { getDualVectorFromBasis :: v }
-  deriving newtype (Eq, AdditiveGroup, VectorSpace, HasBasis)
-
-instance AdditiveGroup v => Semimanifold (DualVectorFromBasis v) where
-  type Needle (DualVectorFromBasis v) = DualVectorFromBasis v
-#if !MIN_VERSION_manifolds_core(0,6,0)
-  type Interior (DualVectorFromBasis v) = DualVectorFromBasis v
-  toInterior = pure
-  fromInterior = id
-  translateP = Tagged (^+^)
-  semimanifoldWitness = SemimanifoldWitness BoundarylessWitness
-#endif
-  (.+~^) = (^+^)
-
-instance AdditiveGroup v => AffineSpace (DualVectorFromBasis v) where
-  type Diff (DualVectorFromBasis v) = DualVectorFromBasis v
-  (.+^) = (^+^)
-  (.-.) = (^-^)
-
-instance AdditiveGroup v => PseudoAffine (DualVectorFromBasis v) where
-  (.-~!) = (^-^)
-  p.-~.q = pure (p^-^q)
-
-instance ∀ v . ( HasBasis v, Num' (Scalar v)
-               , Scalar (Scalar v) ~ Scalar v
-               , HasTrie (Basis v)
-               , Eq v )
-     => TensorSpace (DualVectorFromBasis v) where
-  type TensorProduct (DualVectorFromBasis v) w = Basis v :->: w
-  wellDefinedVector v
-   | v==v       = Just v
-   | otherwise  = Nothing
-  wellDefinedTensor (Tensor v)
-     = fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v
-  zeroTensor = Tensor . trie $ const zeroV
-  toFlatTensor = LinearFunction $ Tensor . trie . decompose'
-  fromFlatTensor = LinearFunction $ \(Tensor t)
-          -> recompose $ enumerate t
-  scalarSpaceWitness = ScalarSpaceWitness
-  linearManifoldWitness = LinearManifoldWitness
-#if !MIN_VERSION_manifolds_core(0,6,0)
-        BoundarylessWitness
-#endif
-  addTensors (Tensor v) (Tensor w) = Tensor $ (^+^) <$> v <*> w
-  subtractTensors (Tensor v) (Tensor w) = Tensor $ (^-^) <$> v <*> w
-  tensorProduct = bilinearFunction
-    $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w
-  transposeTensor = LinearFunction $ \(Tensor t)
-       -> sumV [ (tensorProduct-+$>w)-+$>basisValue b
-               | (b,w) <- enumerate t ]
-  fmapTensor = bilinearFunction
-    $ \(LinearFunction f) (Tensor t)
-         -> Tensor $ fmap f t
-  fzipTensorWith = bilinearFunction
-    $ \(LinearFunction f) (Tensor tv, Tensor tw)
-         -> Tensor $ liftA2 (curry f) tv tw
-  coerceFmapTensorProduct _ Coercion
-    = error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"
-
-
--- | Do not manually instantiate this class. It is used internally
---   by 'makeLinearSpaceFromBasis'.
-class ( HasBasis v, Num' (Scalar v)
-      , LinearSpace v, DualVector v ~ DualVectorFromBasis v)
-    => BasisGeneratedSpace v where
-  proveTensorProductIsTrie
-    :: ∀ w φ . (TensorProduct v w ~ (Basis v :->: w) => φ) -> φ
-
-instance ∀ v . ( BasisGeneratedSpace v
-               , Scalar (Scalar v) ~ Scalar v
-               , HasTrie (Basis v)
-               , Eq v, Eq (Basis v) )
-     => LinearSpace (DualVectorFromBasis v) where
-  type DualVector (DualVectorFromBasis v) = v
-  dualSpaceWitness = case closedScalarWitness @(Scalar v) of
-    ClosedScalarWitness -> DualSpaceWitness
-  linearId = proveTensorProductIsTrie @v @(DualVectorFromBasis v)
-     (LinearMap . trie $ DualVectorFromBasis . basisValue)
-  tensorId = tid
-   where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar v)
-           => (DualVectorFromBasis v⊗w) +> (DualVectorFromBasis v⊗w)
-         tid = proveTensorProductIsTrie @v @(DualVector w⊗(DualVectorFromBasis v⊗w))
-                    ( case dualSpaceWitness @w of
-          DualSpaceWitness -> LinearMap . trie $ Tensor . \i
-           -> getTensorProduct $
-             (fmapTensor @(DualVector w)
-                 -+$>(LinearFunction $ \w -> Tensor . trie
-                              $ (\j -> if i==j then w else zeroV)
-                               :: DualVectorFromBasis v⊗w))
-              -+$> case linearId @w of
-                    LinearMap lw -> Tensor lw :: DualVector w⊗w )
-  applyDualVector = proveTensorProductIsTrie @v @(DualVectorFromBasis v)
-     ( bilinearFunction $ \f (DualVectorFromBasis v)
-          -> sum [decompose' f i * vi | (i,vi) <- decompose v] )
-  applyLinear = ali
-   where ali :: ∀ w . (TensorSpace w, Scalar w~Scalar v)
-           => Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
-         ali = proveTensorProductIsTrie @v @w ( bilinearFunction
-            $ \(LinearMap f) (DualVectorFromBasis v)
-                -> sumV [vi *^ untrie f i | (i,vi) <- decompose v] )
-  applyTensorFunctional = atf
-   where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar v)
-          => Bilinear (DualVector (DualVectorFromBasis v ⊗ u))
-                         (DualVectorFromBasis v ⊗ u) (Scalar v)
-         atf = proveTensorProductIsTrie @v @(DualVector u) (case dualSpaceWitness @u of
-          DualSpaceWitness -> bilinearFunction
-           $ \(LinearMap f) (Tensor t)
-             -> sum [ (applyDualVector-+$>fi)-+$>untrie t i
-                    | (i, fi) <- enumerate f ]
-               )
-  applyTensorLinMap = atlm
-   where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w
-                         , Scalar u ~ Scalar v, Scalar w ~ Scalar v )
-                  => Bilinear ((DualVectorFromBasis v ⊗ u) +> w)
-                               (DualVectorFromBasis v ⊗ u) w
-         atlm = proveTensorProductIsTrie @v @(DualVector u⊗w) (
-          case dualSpaceWitness @u of
-           DualSpaceWitness -> bilinearFunction
-             $ \(LinearMap f) (Tensor t)
-              -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))
-                         -+$> untrie t i
-                      | (i, Tensor fi) <- enumerate f ]
-          )
-  useTupleLinearSpaceComponents _ = usingNonTupleTypeAsTupleError
-
-
-zipWith' :: (a -> b -> c) -> [a] -> [b] -> ([c], [b])
-zipWith' _ _ [] = ([], [])
-zipWith' _ [] ys = ([], ys)
-zipWith' f (x:xs) (y:ys) = first (f x y :) $ zipWith' f xs ys
-
-zipConsumeWith' :: (a -> [b] -> (c,[b])) -> [a] -> [b] -> ([c], [b])
-zipConsumeWith' _ _ [] = ([], [])
-zipConsumeWith' _ [] ys = ([], ys)
-zipConsumeWith' f (x:xs) ys
-    = case f x ys of
-       (z, ys') -> first (z :) $ zipConsumeWith' f xs ys'
-
-instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v
-               , Scalar (Scalar v) ~ Scalar v
-               , HasTrie (Basis v), Ord (Basis v)
-               , Eq v, Eq (Basis v) )
-     => FiniteDimensional (DualVectorFromBasis v) where
-  data SubBasis (DualVectorFromBasis v) = CompleteDualVBasis
-  entireBasis = CompleteDualVBasis
-  enumerateSubBasis CompleteDualVBasis
-      = basisValue . fst <$> enumerate (trie $ const ())
-  tensorEquality (Tensor t) (Tensor t')
-      = and [ti == untrie t' i | (i,ti) <- enumerate t]
-  decomposeLinMap = dlm
-   where dlm :: ∀ w . (DualVectorFromBasis v+>w)
-               -> (SubBasis (DualVectorFromBasis v), [w]->[w])
-         dlm (LinearMap f) = proveTensorProductIsTrie @v @w
-                 ( CompleteDualVBasis
-                 , (map snd (enumerate f) ++) )
-  decomposeLinMapWithin = dlm
-   where dlm :: ∀ w . SubBasis (DualVectorFromBasis v)
-                -> (DualVectorFromBasis v+>w)
-                -> Either (SubBasis (DualVectorFromBasis v), [w]->[w])
-                          ([w]->[w])
-         dlm CompleteDualVBasis (LinearMap f) = proveTensorProductIsTrie @v @w
-                 (Right (map snd (enumerate f) ++) )
-  recomposeSB = rsb
-   where rsb :: SubBasis (DualVectorFromBasis v)
-                -> [Scalar v]
-                -> (DualVectorFromBasis v, [Scalar v])
-         rsb CompleteDualVBasis cs = first recompose
-                   $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs
-  recomposeSBTensor = rsbt
-   where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar v)
-             => SubBasis (DualVectorFromBasis v) -> SubBasis w
-                -> [Scalar v]
-                -> (DualVectorFromBasis v⊗w, [Scalar v])
-         rsbt CompleteDualVBasis sbw ws = proveTensorProductIsTrie @v @w
-                 (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))
-                   $ zipConsumeWith' (\i cs' -> first (i,) $ recomposeSB sbw cs')
-                         (fst <$> enumerate (trie $ const ())) ws)
-  recomposeLinMap = rlm
-   where rlm :: ∀ w . SubBasis (DualVectorFromBasis v)
-                -> [w]
-                -> (DualVectorFromBasis v+>w, [w])
-         rlm CompleteDualVBasis ws = proveTensorProductIsTrie @v @w
-                 (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))
-                   $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)
-  recomposeContraLinMap = rclm
-   where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar v, Hask.Functor f)
-              => (f (Scalar w) -> w) -> f v
-                -> (DualVectorFromBasis v+>w)
-         rclm f vs = proveTensorProductIsTrie @v @w
-               (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))
-  recomposeContraLinMapTensor = rclm
-   where rclm :: ∀ u w f
-           . ( FiniteDimensional u, LinearSpace w
-             , Scalar u ~ Scalar v, Scalar w ~ Scalar v, Hask.Functor f
-             )
-              => (f (Scalar w) -> w) -> f (DualVectorFromBasis v+>DualVector u)
-                -> ((DualVectorFromBasis v⊗u)+>w)
-         rclm f vus = case dualSpaceWitness @u of
-           DualSpaceWitness -> proveTensorProductIsTrie @v @(DualVector u)
-                      (proveTensorProductIsTrie @v @(DualVector u⊗w)
-               (LinearMap $ trie
-                   (\i -> case recomposeContraLinMap @u @w @f f
-                              $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis v)) vus of
-                      LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))
-  uncanonicallyFromDual = LinearFunction DualVectorFromBasis
-  uncanonicallyToDual = LinearFunction getDualVectorFromBasis
-
-
-instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v
-               , Real (Scalar v), Scalar (Scalar v) ~ Scalar v
-               , HasTrie (Basis v), Ord (Basis v)
-               , Eq v, Eq (Basis v) )
-     => SemiInner (DualVectorFromBasis v) where
-  dualBasisCandidates = cartesianDualBasisCandidates
-          (enumerateSubBasis entireBasis)
-          (\v -> map (abs . realToFrac . decompose' v . fst)
-                  $ enumerate (trie $ const ()) )
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE PatternSynonyms            #-}
+
+module Math.LinearMap.Category.Instances.Deriving
+   ( makeLinearSpaceFromBasis, makeFiniteDimensionalFromBasis
+   , copyNewtypeInstances, pattern AbstractDualVector
+   -- * The instantiated classes
+   , AffineSpace(..), Semimanifold(..), PseudoAffine(..)
+   , TensorSpace(..), LinearSpace(..), FiniteDimensional(..), SemiInner(..)
+   -- * Internals
+   , BasisGeneratedSpace(..), LinearSpaceFromBasisDerivationConfig, def
+   ) where
+
+import Math.LinearMap.Category.Class
+import Math.LinearMap.Category.Instances
+import Math.VectorSpace.Docile
+
+import Data.VectorSpace
+import Data.AffineSpace
+import Data.Basis
+import qualified Data.Map as Map
+import Data.Tree (Forest)
+import Data.MemoTrie
+import Data.Hashable
+
+import Prelude ()
+import qualified Prelude as Hask
+
+import Control.Category.Constrained.Prelude
+import Control.Arrow.Constrained
+
+import Data.Coerce
+import Data.Type.Coercion
+import Data.Tagged
+import qualified Data.Kind as Kind
+import Data.Traversable (traverse)
+import Data.Default.Class
+
+import Math.Manifold.Core.PseudoAffine
+import Math.LinearMap.Asserted
+import Math.VectorSpace.ZeroDimensional
+import Data.VectorSpace.Free
+
+import GHC.Generics (Generic)
+
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax (Name(..), OccName(..)
+#if MIN_VERSION_template_haskell(2,17,0)
+           , Specificity(..)
+#endif
+           )
+import qualified Language.Haskell.TH.Datatype as D
+
+-- | Given a type @V@ that is already a 'VectorSpace' and 'HasBasis', generate
+--   the other class instances that are needed to use the type with this
+--   library.
+--
+--   Prerequisites: (these can often be derived automatically,
+--   using either the @newtype@ \/ @via@ strategy or generics \/ anyclass)
+--
+-- @
+-- instance 'AdditiveGroup' V
+--
+-- instance 'VectorSpace' V where
+--   type Scalar V = -- a simple number type, usually 'Double'
+--
+-- instance 'HasBasis' V where
+--   type Basis V = -- a type with an instance of 'HasTrie'
+-- @
+--
+--   Note that the 'Basis' does /not/ need to be orthonormal – in fact it
+--   is not necessary to have a scalar product (i.e. an 'InnerSpace' instance)
+--   at all.
+--
+--   The macro, invoked like
+-- @
+-- makeLinearSpaceFromBasis [t| V |]
+-- @
+--
+--   will then generate @V@-instances for the classes 'Semimanifold',
+--   'PseudoAffine', 'AffineSpace', 'TensorSpace' and 'LinearSpace'.
+--
+--   It also works on parameterised types, in that case you need to use
+--   universal-quantification syntax, e.g.
+--
+-- @
+-- makeLinearSpaceFromBasis [t| ∀ n . (KnownNat n) => V n |]
+-- @
+makeLinearSpaceFromBasis :: Q Type -> DecsQ
+makeLinearSpaceFromBasis v
+   = makeLinearSpaceFromBasis' def $ deQuantifyType v
+
+data LinearSpaceFromBasisDerivationConfig = LinearSpaceFromBasisDerivationConfig
+instance Default LinearSpaceFromBasisDerivationConfig where
+  def = LinearSpaceFromBasisDerivationConfig
+
+-- | More general version of 'makeLinearSpaceFromBasis', that can be used with
+--   parameterised types.
+makeLinearSpaceFromBasis' :: LinearSpaceFromBasisDerivationConfig
+                -> Q ([TyVarBndr
+#if MIN_VERSION_template_haskell(2,17,0)
+                        Specificity
+#endif
+                          ], Cxt, Type) -> DecsQ
+makeLinearSpaceFromBasis' _ cxtv = do
+ (cxt,v) <- do
+   (_, cxt', v') <- cxtv
+   return (pure cxt', pure v')
+ 
+ exts <- extsEnabled
+ if not $ all (`elem`exts) [TypeFamilies, ScopedTypeVariables, TypeApplications]
+   then reportError "This macro requires -XTypeFamilies, -XScopedTypeVariables and -XTypeApplications."
+   else pure ()
+ 
+ sequence
+  [ InstanceD Nothing <$> cxt <*> [t|Semimanifold $v|] <*> [d|
+         type instance Needle $v = $v
+#if !MIN_VERSION_manifolds_core(0,6,0)
+         type instance Interior $v = $v
+         $(varP 'toInterior) = pure
+         $(varP 'fromInterior) = id
+         $(varP 'translateP) = Tagged (^+^)
+         $(varP 'semimanifoldWitness) = SemimanifoldWitness BoundarylessWitness
+#endif
+         $(varP '(.+~^)) = (^+^)
+      |]
+  , InstanceD Nothing <$> cxt <*> [t|PseudoAffine $v|] <*> do
+      [d|
+         $(varP '(.-~!)) = (^-^)
+         $(varP '(.-~.)) = \p q -> pure (p^-^q)
+       |]
+  , InstanceD Nothing <$> cxt <*> [t|AffineSpace $v|] <*> [d|
+         type instance Diff $v = $v
+         $(varP '(.+^)) = (^+^)
+         $(varP '(.-.)) = (^-^)
+       |]
+  , InstanceD Nothing <$> cxt <*> [t|TensorSpace $v|] <*> [d|
+         type instance TensorProduct $v w = Basis $v :->: w
+         $(varP 'wellDefinedVector) = \v
+            -> if v==v then Just v else Nothing
+         $(varP 'wellDefinedTensor) = \(Tensor v)
+            -> fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v
+         $(varP 'zeroTensor) = Tensor . trie $ const zeroV
+         $(varP 'toFlatTensor) = LinearFunction $ Tensor . trie . decompose'
+         $(varP 'fromFlatTensor) = LinearFunction $ \(Tensor t)
+                 -> recompose $ enumerate t
+         $(varP 'scalarSpaceWitness) = ScalarSpaceWitness
+         $(varP 'linearManifoldWitness) = LinearManifoldWitness
+#if !MIN_VERSION_manifolds_core(0,6,0)
+                                 BoundarylessWitness
+#endif
+         $(varP 'addTensors) = \(Tensor v) (Tensor w)
+             -> Tensor $ (^+^) <$> v <*> w
+         $(varP 'subtractTensors) = \(Tensor v) (Tensor w)
+             -> Tensor $ (^-^) <$> v <*> w
+         $(varP 'tensorProduct) = bilinearFunction
+           $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w
+         $(varP 'transposeTensor) = LinearFunction $ \(Tensor t)
+              -> sumV [ (tensorProduct-+$>w)-+$>basisValue b
+                      | (b,w) <- enumerate t ]
+         $(varP 'fmapTensor) = bilinearFunction
+           $ \(LinearFunction f) (Tensor t)
+                -> Tensor $ fmap f t
+         $(varP 'fzipTensorWith) = bilinearFunction
+           $ \(LinearFunction f) (Tensor tv, Tensor tw)
+                -> Tensor $ liftA2 (curry f) tv tw
+         $(varP 'coerceFmapTensorProduct) = \_ Coercion
+           -> error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"
+       |]
+  , InstanceD Nothing <$> cxt <*> [t|BasisGeneratedSpace $v|] <*> do
+      [d|
+         $(varP 'proveTensorProductIsTrie) = \φ -> φ
+       |]
+  , InstanceD Nothing <$> cxt <*> [t|LinearSpace $v|] <*> [d|
+         type instance DualVector $v = DualVectorFromBasis $v
+         $(varP 'dualSpaceWitness) = case closedScalarWitness @(Scalar $v) of
+              ClosedScalarWitness -> DualSpaceWitness
+         $(varP 'linearId) = LinearMap . trie $ basisValue
+         $(varP 'tensorId) = tid
+             where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar $v)
+                     => ($v⊗w) +> ($v⊗w)
+                   tid = case dualSpaceWitness @w of
+                    DualSpaceWitness -> LinearMap . trie $ Tensor . \i
+                     -> getTensorProduct $
+                       (fmapTensor @(DualVector w)
+                           -+$>(LinearFunction $ \w -> Tensor . trie
+                                        $ (\j -> if i==j then w else zeroV)
+                                         :: $v⊗w))
+                        -+$> case linearId @w of
+                              LinearMap lw -> Tensor lw :: DualVector w⊗w
+         $(varP 'applyDualVector) = bilinearFunction
+              $ \(DualVectorFromBasis f) v
+                    -> sum [decompose' f i * vi | (i,vi) <- decompose v]
+         $(varP 'applyLinear) = bilinearFunction
+              $ \(LinearMap f) v
+                    -> sumV [vi *^ untrie f i | (i,vi) <- decompose v]
+         $(varP 'applyTensorFunctional) = atf
+             where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar $v)
+                    => Bilinear (DualVector ($v ⊗ u))
+                                   ($v ⊗ u) (Scalar $v)
+                   atf = case dualSpaceWitness @u of
+                    DualSpaceWitness -> bilinearFunction
+                     $ \(LinearMap f) (Tensor t)
+                       -> sum [ (applyDualVector-+$>fi)-+$>untrie t i
+                              | (i, fi) <- enumerate f ]
+         $(varP 'applyTensorLinMap) = atlm
+             where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w
+                                   , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v )
+                            => Bilinear (($v ⊗ u) +> w) ($v ⊗ u) w
+                   atlm = case dualSpaceWitness @u of
+                     DualSpaceWitness -> bilinearFunction
+                       $ \(LinearMap f) (Tensor t)
+                        -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))
+                                   -+$> untrie t i
+                                | (i, Tensor fi) <- enumerate f ]
+         $(varP 'useTupleLinearSpaceComponents) = \_ -> usingNonTupleTypeAsTupleError
+ 
+       |]
+  ]
+
+data FiniteDimensionalFromBasisDerivationConfig
+         = FiniteDimensionalFromBasisDerivationConfig
+instance Default FiniteDimensionalFromBasisDerivationConfig where
+  def = FiniteDimensionalFromBasisDerivationConfig
+
+-- | Like 'makeLinearSpaceFromBasis', but additionally generate instances for
+--   'FiniteDimensional' and 'SemiInner'.
+makeFiniteDimensionalFromBasis :: Q Type -> DecsQ
+makeFiniteDimensionalFromBasis v
+   = makeFiniteDimensionalFromBasis' def $ deQuantifyType v
+
+makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig
+              -> Q ([TyVarBndr
+#if MIN_VERSION_template_haskell(2,17,0)
+                        Specificity
+#endif
+                       ], Cxt, Type) -> DecsQ
+makeFiniteDimensionalFromBasis' _ cxtv = do
+ generalInsts <- makeLinearSpaceFromBasis' def cxtv
+ (cxt,v) <- do
+   (_, cxt', v') <- cxtv
+   return (pure cxt', pure v')
+ vtnameHash <- abs . hash . show <$> v
+ 
+ fdInsts <- sequence
+  [ InstanceD Nothing <$> cxt <*> [t|FiniteDimensional $v|] <*> do
+    
+    -- This is a hack. Ideally, @newName@ should generate globally unique names,
+    -- but it doesn't, so we append a hash of the vector space type.
+    -- Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/13054
+    subBasisCstr <- newName $ "CompleteBasis"++show vtnameHash
+
+    tySyns <- sequence [
+#if MIN_VERSION_template_haskell(2,15,0)
+       DataInstD [] Nothing
+          <$> (AppT (ConT ''SubBasis) <$> v)
+          <*> pure Nothing
+          <*> pure [NormalC subBasisCstr []]
+          <*> pure []
+#else
+       DataInstD [] ''SubBasis
+          <$> ((:[]) <$> v)
+          <*> pure Nothing
+          <*> pure [NormalC subBasisCstr []]
+          <*> pure []
+#endif
+     ]
+    methods <- [d|
+        $(varP 'entireBasis) = $(conE subBasisCstr)
+        $(varP 'enumerateSubBasis) =
+            \ $(conP subBasisCstr []) -> basisValue . fst <$> enumerate (trie $ const ())
+        $(varP 'tensorEquality)
+          = \(Tensor t) (Tensor t')  -> and [ti == untrie t' i | (i,ti) <- enumerate t]
+        $(varP 'decomposeLinMap) = dlm
+           where dlm :: ∀ w . ($v+>w)
+                       -> (SubBasis $v, [w]->[w])
+                 dlm (LinearMap f) = 
+                         ( $(conE subBasisCstr)
+                         , (map snd (enumerate f) ++) )
+        $(varP 'decomposeLinMapWithin) = dlm
+           where dlm :: ∀ w . SubBasis $v
+                        -> ($v+>w)
+                        -> Either (SubBasis $v, [w]->[w])
+                                  ([w]->[w])
+                 dlm $(conP subBasisCstr []) (LinearMap f) = 
+                         (Right (map snd (enumerate f) ++) )
+        $(varP 'recomposeSB) = rsb
+           where rsb :: SubBasis $v
+                        -> [Scalar $v]
+                        -> ($v, [Scalar $v])
+                 rsb $(conP subBasisCstr []) cs = first recompose
+                           $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs
+        $(varP 'recomposeSBTensor) = rsbt
+           where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar $v)
+                     => SubBasis $v -> SubBasis w
+                        -> [Scalar $v]
+                        -> ($v⊗w, [Scalar $v])
+                 rsbt $(conP subBasisCstr []) sbw ws = 
+                         (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))
+                           $ zipConsumeWith' (\i cs' -> first (\c->(i,c))
+                                                       $ recomposeSB sbw cs')
+                                 (fst <$> enumerate (trie $ const ())) ws)
+        $(varP 'recomposeLinMap) = rlm
+           where rlm :: ∀ w . SubBasis $v
+                        -> [w]
+                        -> ($v+>w, [w])
+                 rlm $(conP subBasisCstr []) ws = 
+                    (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))
+                      $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)
+        $(varP 'recomposeContraLinMap) = rclm
+           where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar $v, Hask.Functor f)
+                      => (f (Scalar w) -> w) -> f (DualVectorFromBasis $v)
+                        -> ($v+>w)
+                 rclm f vs = 
+                       (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))
+        $(varP 'recomposeContraLinMapTensor) = rclm
+           where rclm :: ∀ u w f
+                   . ( FiniteDimensional u, LinearSpace w
+                     , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v, Hask.Functor f
+                     )
+                      => (f (Scalar w) -> w) -> f ($v+>DualVector u)
+                        -> (($v⊗u)+>w)
+                 rclm f vus = case dualSpaceWitness @u of
+                   DualSpaceWitness -> 
+                              (
+                       (LinearMap $ trie
+                           (\i -> case recomposeContraLinMap @u @w @f f
+                                      $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis $v)) vus of
+                              LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))
+        $(varP 'uncanonicallyFromDual) = LinearFunction getDualVectorFromBasis
+        $(varP 'uncanonicallyToDual) = LinearFunction DualVectorFromBasis
+
+      |]
+    return $ tySyns ++ methods
+  , InstanceD Nothing <$> cxt <*> [t|SemiInner $v|] <*> do
+     [d|
+        $(varP 'dualBasisCandidates)
+           = cartesianDualBasisCandidates
+               (enumerateSubBasis CompleteDualVBasis)
+               (\v -> map (abs . realToFrac . decompose' v . fst)
+                       $ enumerate (trie $ const ()) )
+      |]
+  ]
+ return $ generalInsts ++ fdInsts
+
+
+deQuantifyType :: Q Type -> Q ([TyVarBndr
+#if MIN_VERSION_template_haskell(2,17,0)
+                                 Specificity
+#endif
+                                ], Cxt, Type)
+deQuantifyType t = do
+   t' <- t
+   return $ case t' of
+     ForallT tvbs cxt instT -> (tvbs, cxt, instT)
+     _ -> ([], [], t')
+
+
+newtype DualVectorFromBasis v = DualVectorFromBasis { getDualVectorFromBasis :: v }
+  deriving newtype (Eq, AdditiveGroup, VectorSpace, HasBasis)
+
+instance AdditiveGroup v => Semimanifold (DualVectorFromBasis v) where
+  type Needle (DualVectorFromBasis v) = DualVectorFromBasis v
+#if !MIN_VERSION_manifolds_core(0,6,0)
+  type Interior (DualVectorFromBasis v) = DualVectorFromBasis v
+  toInterior = pure
+  fromInterior = id
+  translateP = Tagged (^+^)
+  semimanifoldWitness = SemimanifoldWitness BoundarylessWitness
+#endif
+  (.+~^) = (^+^)
+
+instance AdditiveGroup v => AffineSpace (DualVectorFromBasis v) where
+  type Diff (DualVectorFromBasis v) = DualVectorFromBasis v
+  (.+^) = (^+^)
+  (.-.) = (^-^)
+
+instance AdditiveGroup v => PseudoAffine (DualVectorFromBasis v) where
+  (.-~!) = (^-^)
+  p.-~.q = pure (p^-^q)
+
+instance ∀ v . ( HasBasis v, Num' (Scalar v)
+               , Scalar (Scalar v) ~ Scalar v
+               , HasTrie (Basis v)
+               , Eq v )
+     => TensorSpace (DualVectorFromBasis v) where
+  type TensorProduct (DualVectorFromBasis v) w = Basis v :->: w
+  wellDefinedVector v
+   | v==v       = Just v
+   | otherwise  = Nothing
+  wellDefinedTensor (Tensor v)
+     = fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v
+  zeroTensor = Tensor . trie $ const zeroV
+  toFlatTensor = LinearFunction $ Tensor . trie . decompose'
+  fromFlatTensor = LinearFunction $ \(Tensor t)
+          -> recompose $ enumerate t
+  scalarSpaceWitness = ScalarSpaceWitness
+  linearManifoldWitness = LinearManifoldWitness
+#if !MIN_VERSION_manifolds_core(0,6,0)
+        BoundarylessWitness
+#endif
+  addTensors (Tensor v) (Tensor w) = Tensor $ (^+^) <$> v <*> w
+  subtractTensors (Tensor v) (Tensor w) = Tensor $ (^-^) <$> v <*> w
+  tensorProduct = bilinearFunction
+    $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w
+  transposeTensor = LinearFunction $ \(Tensor t)
+       -> sumV [ (tensorProduct-+$>w)-+$>basisValue b
+               | (b,w) <- enumerate t ]
+  fmapTensor = bilinearFunction
+    $ \(LinearFunction f) (Tensor t)
+         -> Tensor $ fmap f t
+  fzipTensorWith = bilinearFunction
+    $ \(LinearFunction f) (Tensor tv, Tensor tw)
+         -> Tensor $ liftA2 (curry f) tv tw
+  coerceFmapTensorProduct _ Coercion
+    = error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"
+
+
+-- | Do not manually instantiate this class. It is used internally
+--   by 'makeLinearSpaceFromBasis'.
+class ( HasBasis v, Num' (Scalar v)
+      , LinearSpace v, DualVector v ~ DualVectorFromBasis v)
+    => BasisGeneratedSpace v where
+  proveTensorProductIsTrie
+    :: ∀ w φ . (TensorProduct v w ~ (Basis v :->: w) => φ) -> φ
+
+instance ∀ v . ( BasisGeneratedSpace v
+               , Scalar (Scalar v) ~ Scalar v
+               , HasTrie (Basis v)
+               , Eq v, Eq (Basis v) )
+     => LinearSpace (DualVectorFromBasis v) where
+  type DualVector (DualVectorFromBasis v) = v
+  dualSpaceWitness = case closedScalarWitness @(Scalar v) of
+    ClosedScalarWitness -> DualSpaceWitness
+  linearId = proveTensorProductIsTrie @v @(DualVectorFromBasis v)
+     (LinearMap . trie $ DualVectorFromBasis . basisValue)
+  tensorId = tid
+   where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar v)
+           => (DualVectorFromBasis v⊗w) +> (DualVectorFromBasis v⊗w)
+         tid = proveTensorProductIsTrie @v @(DualVector w⊗(DualVectorFromBasis v⊗w))
+                    ( case dualSpaceWitness @w of
+          DualSpaceWitness -> LinearMap . trie $ Tensor . \i
+           -> getTensorProduct $
+             (fmapTensor @(DualVector w)
+                 -+$>(LinearFunction $ \w -> Tensor . trie
+                              $ (\j -> if i==j then w else zeroV)
+                               :: DualVectorFromBasis v⊗w))
+              -+$> case linearId @w of
+                    LinearMap lw -> Tensor lw :: DualVector w⊗w )
+  applyDualVector = proveTensorProductIsTrie @v @(DualVectorFromBasis v)
+     ( bilinearFunction $ \f (DualVectorFromBasis v)
+          -> sum [decompose' f i * vi | (i,vi) <- decompose v] )
+  applyLinear = ali
+   where ali :: ∀ w . (TensorSpace w, Scalar w~Scalar v)
+           => Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
+         ali = proveTensorProductIsTrie @v @w ( bilinearFunction
+            $ \(LinearMap f) (DualVectorFromBasis v)
+                -> sumV [vi *^ untrie f i | (i,vi) <- decompose v] )
+  applyTensorFunctional = atf
+   where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar v)
+          => Bilinear (DualVector (DualVectorFromBasis v ⊗ u))
+                         (DualVectorFromBasis v ⊗ u) (Scalar v)
+         atf = proveTensorProductIsTrie @v @(DualVector u) (case dualSpaceWitness @u of
+          DualSpaceWitness -> bilinearFunction
+           $ \(LinearMap f) (Tensor t)
+             -> sum [ (applyDualVector-+$>fi)-+$>untrie t i
+                    | (i, fi) <- enumerate f ]
+               )
+  applyTensorLinMap = atlm
+   where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w
+                         , Scalar u ~ Scalar v, Scalar w ~ Scalar v )
+                  => Bilinear ((DualVectorFromBasis v ⊗ u) +> w)
+                               (DualVectorFromBasis v ⊗ u) w
+         atlm = proveTensorProductIsTrie @v @(DualVector u⊗w) (
+          case dualSpaceWitness @u of
+           DualSpaceWitness -> bilinearFunction
+             $ \(LinearMap f) (Tensor t)
+              -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))
+                         -+$> untrie t i
+                      | (i, Tensor fi) <- enumerate f ]
+          )
+  useTupleLinearSpaceComponents _ = usingNonTupleTypeAsTupleError
+
+
+zipWith' :: (a -> b -> c) -> [a] -> [b] -> ([c], [b])
+zipWith' _ _ [] = ([], [])
+zipWith' _ [] ys = ([], ys)
+zipWith' f (x:xs) (y:ys) = first (f x y :) $ zipWith' f xs ys
+
+zipConsumeWith' :: (a -> [b] -> (c,[b])) -> [a] -> [b] -> ([c], [b])
+zipConsumeWith' _ _ [] = ([], [])
+zipConsumeWith' _ [] ys = ([], ys)
+zipConsumeWith' f (x:xs) ys
+    = case f x ys of
+       (z, ys') -> first (z :) $ zipConsumeWith' f xs ys'
+
+instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v
+               , Scalar (Scalar v) ~ Scalar v
+               , HasTrie (Basis v), Ord (Basis v)
+               , Eq v, Eq (Basis v) )
+     => FiniteDimensional (DualVectorFromBasis v) where
+  data SubBasis (DualVectorFromBasis v) = CompleteDualVBasis
+  entireBasis = CompleteDualVBasis
+  enumerateSubBasis CompleteDualVBasis
+      = basisValue . fst <$> enumerate (trie $ const ())
+  tensorEquality (Tensor t) (Tensor t')
+      = and [ti == untrie t' i | (i,ti) <- enumerate t]
+  decomposeLinMap = dlm
+   where dlm :: ∀ w . (DualVectorFromBasis v+>w)
+               -> (SubBasis (DualVectorFromBasis v), [w]->[w])
+         dlm (LinearMap f) = proveTensorProductIsTrie @v @w
+                 ( CompleteDualVBasis
+                 , (map snd (enumerate f) ++) )
+  decomposeLinMapWithin = dlm
+   where dlm :: ∀ w . SubBasis (DualVectorFromBasis v)
+                -> (DualVectorFromBasis v+>w)
+                -> Either (SubBasis (DualVectorFromBasis v), [w]->[w])
+                          ([w]->[w])
+         dlm CompleteDualVBasis (LinearMap f) = proveTensorProductIsTrie @v @w
+                 (Right (map snd (enumerate f) ++) )
+  recomposeSB = rsb
+   where rsb :: SubBasis (DualVectorFromBasis v)
+                -> [Scalar v]
+                -> (DualVectorFromBasis v, [Scalar v])
+         rsb CompleteDualVBasis cs = first recompose
+                   $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs
+  recomposeSBTensor = rsbt
+   where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar v)
+             => SubBasis (DualVectorFromBasis v) -> SubBasis w
+                -> [Scalar v]
+                -> (DualVectorFromBasis v⊗w, [Scalar v])
+         rsbt CompleteDualVBasis sbw ws = proveTensorProductIsTrie @v @w
+                 (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))
+                   $ zipConsumeWith' (\i cs' -> first (i,) $ recomposeSB sbw cs')
+                         (fst <$> enumerate (trie $ const ())) ws)
+  recomposeLinMap = rlm
+   where rlm :: ∀ w . SubBasis (DualVectorFromBasis v)
+                -> [w]
+                -> (DualVectorFromBasis v+>w, [w])
+         rlm CompleteDualVBasis ws = proveTensorProductIsTrie @v @w
+                 (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))
+                   $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)
+  recomposeContraLinMap = rclm
+   where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar v, Hask.Functor f)
+              => (f (Scalar w) -> w) -> f v
+                -> (DualVectorFromBasis v+>w)
+         rclm f vs = proveTensorProductIsTrie @v @w
+               (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))
+  recomposeContraLinMapTensor = rclm
+   where rclm :: ∀ u w f
+           . ( FiniteDimensional u, LinearSpace w
+             , Scalar u ~ Scalar v, Scalar w ~ Scalar v, Hask.Functor f
+             )
+              => (f (Scalar w) -> w) -> f (DualVectorFromBasis v+>DualVector u)
+                -> ((DualVectorFromBasis v⊗u)+>w)
+         rclm f vus = case dualSpaceWitness @u of
+           DualSpaceWitness -> proveTensorProductIsTrie @v @(DualVector u)
+                      (proveTensorProductIsTrie @v @(DualVector u⊗w)
+               (LinearMap $ trie
+                   (\i -> case recomposeContraLinMap @u @w @f f
+                              $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis v)) vus of
+                      LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))
+  uncanonicallyFromDual = LinearFunction DualVectorFromBasis
+  uncanonicallyToDual = LinearFunction getDualVectorFromBasis
+
+
+instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v
+               , Real (Scalar v), Scalar (Scalar v) ~ Scalar v
+               , HasTrie (Basis v), Ord (Basis v)
+               , Eq v, Eq (Basis v) )
+     => SemiInner (DualVectorFromBasis v) where
+  dualBasisCandidates = cartesianDualBasisCandidates
+          (enumerateSubBasis entireBasis)
+          (\v -> map (abs . realToFrac . decompose' v . fst)
+                  $ enumerate (trie $ const ()) )
+
+
+newtype AbstractDualVector a c
+           = AbstractDualVector_ { getConcreteDualVector :: DualVector c }
+deriving newtype instance (Eq (DualVector c)) => Eq (AbstractDualVector a c)
+
+class ( Coercible v (VectorSpaceImplementation v)
+      , AdditiveGroup (VectorSpaceImplementation v) )
+        => AbstractAdditiveGroup v where
+  type VectorSpaceImplementation v :: Kind.Type
+
+class (AbstractAdditiveGroup v, VectorSpace (VectorSpaceImplementation v))
+        => AbstractVectorSpace v where
+  scalarsSameInAbstraction
+    :: ( Scalar (VectorSpaceImplementation v) ~ Scalar v
+         => ρ ) -> ρ
+
+class ( AbstractVectorSpace v, TensorSpace (VectorSpaceImplementation v)
+#if !MIN_VERSION_manifolds_core(0,6,0)
+      , Semimanifold v, Interior v ~ v
+#endif
+      ) => AbstractTensorSpace v where
+  abstractTensorProductsCoercion
+    :: Coercion (TensorProduct v w)
+                (TensorProduct (VectorSpaceImplementation v) w)
+
+class ( AbstractTensorSpace v, LinearSpace (VectorSpaceImplementation v)
+      , DualVector v
+          ~ AbstractDualVector v (VectorSpaceImplementation v) )
+    => AbstractLinearSpace v
+
+scalarsSameInAbstractionAndDuals :: ∀ v ρ . AbstractLinearSpace v
+     => ( ( Scalar (VectorSpaceImplementation v) ~ Scalar v
+          , Scalar (DualVector v) ~ Scalar v
+          , Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v )
+         => ρ ) -> ρ
+scalarsSameInAbstractionAndDuals φ
+     = case dualSpaceWitness @(VectorSpaceImplementation v) of
+        DualSpaceWitness -> scalarsSameInAbstraction @v φ
+
+abstractDualVectorCoercion :: ∀ a
+   . Coercion (AbstractDualVector a (VectorSpaceImplementation a))
+              (DualVector (VectorSpaceImplementation a))
+abstractDualVectorCoercion = Coercion
+
+abstractTensorsCoercion :: ∀ a c w
+  . ( AbstractVectorSpace a, LinearSpace c
+    , c ~ VectorSpaceImplementation a, TensorSpace w )
+      => Coercion (AbstractDualVector a c⊗w) (DualVector c⊗w)
+abstractTensorsCoercion = Coercion
+
+abstractLinmapCoercion :: ∀ a c w
+  . ( AbstractLinearSpace a, LinearSpace c
+    , c ~ VectorSpaceImplementation a, TensorSpace w )
+      => Coercion (AbstractDualVector a c+>w) (DualVector c+>w)
+abstractLinmapCoercion = case ( dualSpaceWitness @c
+                              , abstractTensorProductsCoercion @a @w ) of
+   (DualSpaceWitness, Coercion) -> Coercion
+
+coerceLinearMapCodomain :: ∀ v w x . ( LinearSpace v, Coercible w x )
+         => (v+>w) -> (v+>x)
+coerceLinearMapCodomain = case dualSpaceWitness @v of
+ DualSpaceWitness -> \(LinearMap m)
+     -> LinearMap $ (coerceFmapTensorProduct ([]::[DualVector v])
+                            (Coercion :: Coercion w x) $ m)
+
+instance (Show (DualVector c)) => Show (AbstractDualVector a c) where
+  showsPrec p (AbstractDualVector_ φ) = showParen (p>10)
+       $ ("AbstractDualVector "++) . showsPrec 11 φ
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , AdditiveGroup (DualVector c) )
+     => AdditiveGroup (AbstractDualVector a c) where
+  zeroV = AbstractDualVector zeroV
+  (^+^) = coerce ((^+^) @(DualVector c))
+  negateV = coerce (negateV @(DualVector c))
+
+instance ∀ a c . (AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , AdditiveGroup (DualVector c))
+     => AffineSpace (AbstractDualVector a c) where
+  type Diff (AbstractDualVector a c) = AbstractDualVector a c
+  (.+^) = coerce ((^+^) @(DualVector c))
+  (.-.) = coerce ((^-^) @(DualVector c))
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , AdditiveGroup (DualVector c) )
+     => Semimanifold (AbstractDualVector a c) where
+  type Needle (AbstractDualVector a c) = AbstractDualVector a c
+  (.+~^) = (^+^)
+#if !MIN_VERSION_manifolds_core(0,6,0)
+  type instance Interior (AbstractDualVector a c) = AbstractDualVector a c
+  toInterior = pure
+  fromInterior = id
+  translateP = Tagged (^+^)
+  semimanifoldWitness = SemimanifoldWitness BoundarylessWitness
+#endif
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , AdditiveGroup (DualVector c) )
+     => PseudoAffine (AbstractDualVector a c) where
+  v.-~.w = pure (v^-^w)
+  (.-~!) = (^-^)
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , VectorSpace (DualVector c) )
+     => VectorSpace (AbstractDualVector a c) where
+  type Scalar (AbstractDualVector a c) = Scalar a
+  (*^) = scalarsSameInAbstractionAndDuals @a (coerce ((*^) @(DualVector c)))
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , TensorSpace (DualVector c) )
+     => TensorSpace (AbstractDualVector a c) where
+  type TensorProduct (AbstractDualVector a c) w
+          = TensorProduct (DualVector c) w
+  scalarSpaceWitness = scalarsSameInAbstractionAndDuals @a
+     (case scalarSpaceWitness @(DualVector c) of ScalarSpaceWitness -> ScalarSpaceWitness)
+  linearManifoldWitness = scalarsSameInAbstractionAndDuals @a
+     (case linearManifoldWitness @(DualVector c) of
+#if MIN_VERSION_manifolds_core(0,6,0)
+       LinearManifoldWitness -> LinearManifoldWitness
+#else
+       LinearManifoldWitness BoundarylessWitness
+          -> LinearManifoldWitness BoundarylessWitness
+#endif
+         )
+  zeroTensor = zt
+   where zt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => (AbstractDualVector a c ⊗ w)
+         zt = scalarsSameInAbstractionAndDuals @a
+                (coerce (zeroTensor @(DualVector c) @w))
+  addTensors = at
+   where at :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w)
+                                            -> (AbstractDualVector a c ⊗ w)
+         at = scalarsSameInAbstractionAndDuals @a
+                (coerce (addTensors @(DualVector c) @w))
+  subtractTensors = st
+   where st :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w)
+                                            -> (AbstractDualVector a c ⊗ w)
+         st = scalarsSameInAbstractionAndDuals @a
+                (coerce (subtractTensors @(DualVector c) @w))
+  negateTensor = nt
+   where nt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => (AbstractDualVector a c ⊗ w) -+> (AbstractDualVector a c ⊗ w)
+         nt = scalarsSameInAbstractionAndDuals @a
+                (coerce (negateTensor @(DualVector c) @w))
+  scaleTensor = st
+   where st :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => Bilinear (Scalar a) (AbstractDualVector a c ⊗ w)
+                                   (AbstractDualVector a c ⊗ w)
+         st = scalarsSameInAbstractionAndDuals @a
+                (coerce (scaleTensor @(DualVector c) @w))
+  toFlatTensor = scalarsSameInAbstractionAndDuals @a
+                    ( coerce (toFlatTensor @(DualVector c)) )
+  fromFlatTensor = scalarsSameInAbstractionAndDuals @a
+                    ( coerce (fromFlatTensor @(DualVector c)) )
+  tensorProduct = tp
+   where tp :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => Bilinear (AbstractDualVector a c) w
+                                   (AbstractDualVector a c ⊗ w)
+         tp = scalarsSameInAbstractionAndDuals @a
+                (coerce (tensorProduct @(DualVector c) @w))
+  wellDefinedVector (AbstractDualVector v) = AbstractDualVector <$> wellDefinedVector v
+  wellDefinedTensor = wdt
+   where wdt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
+            => (AbstractDualVector a c ⊗ w) -> Maybe (AbstractDualVector a c ⊗ w)
+         wdt = scalarsSameInAbstractionAndDuals @a
+                (coerce (wellDefinedTensor @(DualVector c) @w))
+  transposeTensor = scalarsSameInAbstractionAndDuals @a tt
+   where tt :: ∀ w . ( TensorSpace w, Scalar w ~ Scalar a
+                     , Scalar (DualVector c) ~ Scalar a )
+            => (AbstractDualVector a c ⊗ w) -+> (w ⊗ AbstractDualVector a c)
+         tt = case coerceFmapTensorProduct @w []
+                       (Coercion @(DualVector c) @(AbstractDualVector a c)) of
+             Coercion -> coerce (transposeTensor @(DualVector c) @w)
+  fmapTensor = ft
+   where ft :: ∀ w x . ( TensorSpace w, Scalar w ~ Scalar a
+                       , TensorSpace x, Scalar x ~ Scalar a )
+           => Bilinear (w-+>x) (AbstractDualVector a c ⊗ w) (AbstractDualVector a c ⊗ x) 
+         ft = scalarsSameInAbstractionAndDuals @a
+                 (coerce $ fmapTensor @(DualVector c) @w @x)
+  fzipTensorWith = ft
+   where ft :: ∀ u w x . ( TensorSpace w, Scalar w ~ Scalar a
+                         , TensorSpace u, Scalar u ~ Scalar a
+                         , TensorSpace x, Scalar x ~ Scalar a )
+           => Bilinear ((w,x)-+>u)
+                       (AbstractDualVector a c ⊗ w, AbstractDualVector a c ⊗ x)
+                       (AbstractDualVector a c ⊗ u) 
+         ft = scalarsSameInAbstractionAndDuals @a
+                 (coerce $ fzipTensorWith @(DualVector c) @u @w @x)
+  coerceFmapTensorProduct _ = coerceFmapTensorProduct ([]::[DualVector c])
+
+witnessAbstractDualVectorTensorSpacyness
+  :: ∀ a c r . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+               , LinearSpace a, LinearSpace c
+               , TensorSpace (DualVector c), Num (Scalar a) )
+    => (( TensorSpace (AbstractDualVector a c)
+        , LinearSpace (DualVector c)
+        , Scalar (DualVector c) ~ Scalar a )
+            => r) -> r
+witnessAbstractDualVectorTensorSpacyness φ = case dualSpaceWitness @c of
+   DualSpaceWitness -> scalarsSameInAbstraction @a φ
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , LinearSpace a, LinearSpace c
+                 , TensorSpace (DualVector c), Num (Scalar a) )
+     => LinearSpace (AbstractDualVector a c) where
+  type DualVector (AbstractDualVector a c) = a
+  dualSpaceWitness = case (dualSpaceWitness @c, scalarSpaceWitness @c) of
+    (DualSpaceWitness, ScalarSpaceWitness)
+        -> scalarsSameInAbstraction @a DualSpaceWitness
+  linearId = witnessAbstractDualVectorTensorSpacyness @a @c
+       (sym (abstractLinmapCoercion @a)
+           $ sampleLinearFunction @(DualVector c)
+           -+$> linearFunction AbstractDualVector)
+  tensorId = tid
+   where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar a)
+            => (AbstractDualVector a c ⊗ w) +> (AbstractDualVector a c ⊗ w) 
+         tid = case ( dualSpaceWitness @w, dualSpaceWitness @c ) of
+          (DualSpaceWitness, DualSpaceWitness)
+            -> witnessAbstractDualVectorTensorSpacyness @a (
+                let LinearMap ida = linearId :: (DualVector c ⊗ w) +> (DualVector c ⊗ w)
+                in LinearMap $ 
+                    sym (abstractTensorProductsCoercion @a
+                          @(DualVector w ⊗ (AbstractDualVector a c⊗w)) )
+                    . coerceFmapTensorProduct ([]::[c ⊗ DualVector w])
+                       (Coercion @(DualVector c ⊗ w) @(AbstractDualVector a c ⊗ w))
+                    $ ida )
+  applyDualVector = scalarsSameInAbstraction @a ( bilinearFunction
+     $ \v (AbstractDualVector d) -> (applyDualVector -+$> d)-+$>(coerce v::c) )
+  applyLinear = witnessAbstractDualVectorTensorSpacyness @a ( LinearFunction
+     $ \f -> (applyLinear -+$> abstractLinmapCoercion $ f) . LinearFunction coerce
+      )
+  applyTensorFunctional = atf
+   where atf :: ∀ u . ( LinearSpace u, Scalar u ~ Scalar a )
+                  => Bilinear (DualVector (AbstractDualVector a c⊗u))
+                                       (AbstractDualVector a c⊗u) (Scalar a)
+         atf = case (scalarSpaceWitness @a, dualSpaceWitness @u) of
+          (ScalarSpaceWitness, DualSpaceWitness)
+            -> witnessAbstractDualVectorTensorSpacyness @a (
+                LinearFunction $ \f
+                 -> (applyTensorFunctional @(DualVector c)
+                         -+$> abstractLinmapCoercion @a $ f)
+                      . LinearFunction (abstractTensorsCoercion @a $)
+              )
+  applyTensorLinMap = atlm
+   where atlm :: ∀ u w . ( LinearSpace u, Scalar u ~ Scalar a
+                         , TensorSpace w, Scalar w ~ Scalar a )
+                  => Bilinear ((AbstractDualVector a c⊗u)+>w)
+                                       (AbstractDualVector a c⊗u) w
+         atlm = case (dualSpaceWitness @c, dualSpaceWitness @u) of
+          (DualSpaceWitness, DualSpaceWitness)
+                      -> witnessAbstractDualVectorTensorSpacyness @a (
+             LinearFunction $ \(LinearMap f) ->
+                     let f' = LinearMap (abstractTensorProductsCoercion
+                                           @a @((Tensor (Scalar a) (DualVector u) w))
+                                          $ coerce f) :: (DualVector c⊗u)+>w
+                     in (applyTensorLinMap @(DualVector c)-+$>f')
+                              . LinearFunction (abstractTensorsCoercion @a $)
+           )
+  useTupleLinearSpaceComponents = \_ -> usingNonTupleTypeAsTupleError
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , FiniteDimensional a, FiniteDimensional c
+                 , TensorSpace (DualVector c), Eq (DualVector c), Num (Scalar a) )
+     => FiniteDimensional (AbstractDualVector a c) where
+  newtype SubBasis (AbstractDualVector a c) = AbstractDualVectorSubBasis {
+                        getAbstractDualVectorSubBasis :: SubBasis (DualVector c) }
+  dualFinitenessWitness = scalarsSameInAbstraction @a
+       ( case (scalarSpaceWitness @a, dualSpaceWitness @a) of
+        (ScalarSpaceWitness, DualSpaceWitness)
+            -> DualFinitenessWitness DualSpaceWitness )
+  entireBasis = case dualFinitenessWitness @c of
+    DualFinitenessWitness _ -> coerce (entireBasis @(DualVector c))
+  enumerateSubBasis = case dualFinitenessWitness @c of
+    DualFinitenessWitness _ 
+          -> coerce (enumerateSubBasis @(DualVector c))
+  decomposeLinMap = scalarsSameInAbstraction @a dclm
+   where dclm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)
+            => (AbstractDualVector a c +> w)
+                  -> (SubBasis (AbstractDualVector a c), DList w)
+         dclm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of
+          (DualFinitenessWitness DualSpaceWitness, Coercion)
+              -> coerce (decomposeLinMap @(DualVector c) @w)
+  decomposeLinMapWithin = scalarsSameInAbstraction @a dclm
+   where dclm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)
+            => SubBasis (AbstractDualVector a c) -> (AbstractDualVector a c +> w)
+                   -> Either (SubBasis (AbstractDualVector a c), DList w) (DList w)
+         dclm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of
+          (DualFinitenessWitness DualSpaceWitness, Coercion)
+              -> coerce (decomposeLinMapWithin @(DualVector c) @w)
+  recomposeSB = case dualFinitenessWitness @c of
+          DualFinitenessWitness DualSpaceWitness -> scalarsSameInAbstraction @a
+                                (coerce $ recomposeSB @(DualVector c))
+  recomposeSBTensor = scalarsSameInAbstraction @a rst
+   where rst :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar c)
+           => SubBasis (AbstractDualVector a c) -> SubBasis w -> [Scalar c]
+                  -> (AbstractDualVector a c ⊗ w, [Scalar c])
+         rst = case dualFinitenessWitness @c of
+          DualFinitenessWitness DualSpaceWitness
+                  -> coerce (recomposeSBTensor @(DualVector c) @w)
+  recomposeLinMap = scalarsSameInAbstraction @a rlm
+   where rlm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)
+           => SubBasis (AbstractDualVector a c)
+                 -> [w] -> (AbstractDualVector a c +> w, [w])
+         rlm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of
+          (DualFinitenessWitness DualSpaceWitness, Coercion)
+              -> coerce (recomposeLinMap @(DualVector c) @w)
+  recomposeContraLinMap = scalarsSameInAbstraction @a rclm
+   where rclm :: ∀ f w . (LinearSpace w, Scalar w ~ Scalar c, Hask.Functor f)
+           => (f (Scalar w) -> w) -> f a -> AbstractDualVector a c +> w
+         rclm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of
+          (DualFinitenessWitness DualSpaceWitness, Coercion) -> \f ->
+             (coerce $ recomposeContraLinMap @(DualVector c) @w @f) f
+               . fmap (coerce :: a -> c)
+  recomposeContraLinMapTensor = scalarsSameInAbstraction @a rclmt
+   where rclmt :: ∀ f w u . ( LinearSpace w, Scalar w ~ Scalar c
+                            , FiniteDimensional u, Scalar u ~ Scalar c
+                            , Hask.Functor f )
+           => (f (Scalar w) -> w) -> f (AbstractDualVector a c+>DualVector u)
+                   -> (AbstractDualVector a c⊗u) +> w
+         rclmt = scalarsSameInAbstraction @a (case dualSpaceWitness @u of
+           DualSpaceWitness ->
+                 case ( dualFinitenessWitness @c
+                      , abstractTensorProductsCoercion @a @(DualVector u)
+                      , abstractTensorProductsCoercion @a
+                          @(Tensor (Scalar a) (DualVector u) w) ) of
+            (DualFinitenessWitness DualSpaceWitness, Coercion, Coercion) -> \f ->
+              (coerce $ recomposeContraLinMapTensor @(DualVector c) @u @w @f) f
+                . fmap (coerce :: (AbstractDualVector a c+>DualVector u)
+                                    -> (DualVector c+>DualVector u))
+          )
+  uncanonicallyFromDual = case dualFinitenessWitness @c of
+    DualFinitenessWitness DualSpaceWitness
+        -> coerce (uncanonicallyFromDual @(DualVector c))
+  uncanonicallyToDual = case dualFinitenessWitness @c of
+    DualFinitenessWitness DualSpaceWitness
+        -> coerce (uncanonicallyToDual @(DualVector c))
+  tensorEquality = te
+   where te :: ∀ w . (TensorSpace w, Eq w, Scalar w ~ Scalar a)
+                => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w) -> Bool
+         te = case dualFinitenessWitness @c of
+           DualFinitenessWitness _ -> scalarsSameInAbstractionAndDuals @a
+                (coerce (tensorEquality @(DualVector c) @w))
+
+instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
+                 , SemiInner a, LinearSpace c, SemiInner (DualVector c)
+                 , TensorSpace (DualVector c), Eq (DualVector c), Num (Scalar a) )
+     => SemiInner (AbstractDualVector a c) where
+  dualBasisCandidates = case dualSpaceWitness @c of
+    DualSpaceWitness -> coerce (dualBasisCandidates @(DualVector c))
+  tensorDualBasisCandidates = scalarsSameInAbstraction @a tdbc
+   where tdbc :: ∀ w . (SemiInner w, Scalar w ~ Scalar c)
+            => [(Int, AbstractDualVector a c ⊗ w)]
+             -> Forest (Int, AbstractDualVector a c +> DualVector w)
+         tdbc = case (dualSpaceWitness @c, dualSpaceWitness @w) of
+           (DualSpaceWitness, DualSpaceWitness)
+               -> case abstractTensorProductsCoercion @a @(DualVector w) of
+             Coercion -> coerce (tensorDualBasisCandidates @(DualVector c) @w)
+  symTensorDualBasisCandidates = scalarsSameInAbstraction @a
+          ( case ( coerceFmapTensorProduct @c [] (Coercion @a @c)
+                          . abstractTensorProductsCoercion @a @a
+                 , coerceFmapTensorProduct @(DualVector c) []
+                      (Coercion @(AbstractDualVector a c) @(DualVector c))
+                 , dualSpaceWitness @c ) of
+             (Coercion, Coercion, DualSpaceWitness)
+               -> coerce (symTensorDualBasisCandidates @(DualVector c))
+          )
+
+ 
+
+pattern AbstractDualVector
+    :: AbstractLinearSpace v => DualVector (VectorSpaceImplementation v) -> DualVector v
+pattern AbstractDualVector φ = AbstractDualVector_ φ
+
+
+
+abstractVS_zeroV :: ∀ v .
+    (AbstractAdditiveGroup v)
+       => v
+abstractVS_zeroV = coerce (zeroV @(VectorSpaceImplementation v))
+
+abstractVS_addvs :: ∀ v .
+    (AbstractAdditiveGroup v)
+       => v -> v -> v
+abstractVS_addvs = coerce ((^+^) @(VectorSpaceImplementation v))
+
+abstractVS_subvs :: ∀ v .
+    (AbstractAdditiveGroup v)
+       => v -> v -> v
+abstractVS_subvs = coerce ((^-^) @(VectorSpaceImplementation v))
+
+abstractVS_negateV :: ∀ v .
+    (AbstractAdditiveGroup v)
+       => v -> v
+abstractVS_negateV = coerce (negateV @(VectorSpaceImplementation v))
+
+abstractVS_scalev :: ∀ v .
+    (AbstractVectorSpace v)
+       => Scalar v -> v -> v
+abstractVS_scalev = scalarsSameInAbstraction @v
+  ( coerce ((*^) @(VectorSpaceImplementation v)) )
+
+abstractVS_innerProd :: ∀ v .
+    (AbstractVectorSpace v, InnerSpace (VectorSpaceImplementation v))
+       => v -> v -> Scalar v
+abstractVS_innerProd = scalarsSameInAbstraction @v
+  ( coerce ((<.>) @(VectorSpaceImplementation v)) )
+
+abstractVS_scalarsSameInAbstraction :: ∀ v ρ .
+    ( AbstractVectorSpace v
+    , Scalar (VectorSpaceImplementation v) ~ Scalar v
+    )
+   => ( Scalar (VectorSpaceImplementation v) ~ Scalar v
+         => ρ ) -> ρ
+abstractVS_scalarsSameInAbstraction φ
+   = φ
+
+abstractVS_scalarSpaceWitness :: ∀ v .
+    (AbstractTensorSpace v)
+       => ScalarSpaceWitness v
+abstractVS_scalarSpaceWitness
+   = case scalarSpaceWitness @(VectorSpaceImplementation v) of
+      ScalarSpaceWitness -> scalarsSameInAbstraction @v ScalarSpaceWitness 
+
+abstractVS_linearManifoldWitness :: ∀ v .
+    ( AbstractTensorSpace v, AffineSpace v, Needle v ~ v, Diff v ~ v
+    )
+       => LinearManifoldWitness v
+abstractVS_linearManifoldWitness
+   = case linearManifoldWitness @(VectorSpaceImplementation v) of
+#if MIN_VERSION_manifolds_core(0,6,0)
+           LinearManifoldWitness -> LinearManifoldWitness
+#else
+           LinearManifoldWitness BoundarylessWitness
+                -> LinearManifoldWitness BoundarylessWitness
+#endif
+
+abstractVS_toFlatTensor :: ∀ v .
+    ( AbstractTensorSpace v
+    , Coercible (TensorProduct v (Scalar v))
+                (TensorProduct (VectorSpaceImplementation v)
+                               (Scalar (VectorSpaceImplementation v))) )
+       => v -+> (v ⊗ Scalar v)
+abstractVS_toFlatTensor = coerce (toFlatTensor @(VectorSpaceImplementation v))
+
+abstractVS_fromFlatTensor :: ∀ v .
+    ( AbstractTensorSpace v
+    , Coercible (TensorProduct v (Scalar v))
+                (TensorProduct (VectorSpaceImplementation v)
+                               (Scalar (VectorSpaceImplementation v))) )
+       => (v ⊗ Scalar v) -+> v
+abstractVS_fromFlatTensor = coerce (fromFlatTensor @(VectorSpaceImplementation v))
+
+abstractVS_zeroTensor :: ∀ v w
+       . ( AbstractTensorSpace v
+         , TensorSpace w, Scalar w ~ Scalar v
+         , Coercible (TensorProduct v w)
+                     (TensorProduct (VectorSpaceImplementation v) w) )
+           => (v ⊗ w)
+abstractVS_zeroTensor = scalarsSameInAbstraction @v
+  (coerce (zeroTensor @(VectorSpaceImplementation v) @w))
+
+abstractVS_addTensors :: ∀ v w
+       . ( AbstractTensorSpace v
+         , TensorSpace w, Scalar w ~ Scalar v
+         , Coercible (TensorProduct v w)
+                     (TensorProduct (VectorSpaceImplementation v) w) )
+           => (v ⊗ w) -> (v ⊗ w) -> (v ⊗ w)
+abstractVS_addTensors = scalarsSameInAbstraction @v
+  (coerce (addTensors @(VectorSpaceImplementation v) @w))
+
+abstractVS_subtractTensors :: ∀ v w
+       . ( AbstractTensorSpace v
+         , TensorSpace w, Scalar w ~ Scalar v
+         , Coercible (TensorProduct v w)
+                     (TensorProduct (VectorSpaceImplementation v) w) )
+           => (v ⊗ w) -> (v ⊗ w) -> (v ⊗ w)
+abstractVS_subtractTensors = scalarsSameInAbstraction @v
+  (coerce (subtractTensors @(VectorSpaceImplementation v) @w))
+
+abstractVS_scaleTensor :: ∀ v w
+       . ( AbstractTensorSpace v
+         , TensorSpace w, Scalar w ~ Scalar v
+         , Coercible (TensorProduct v w)
+                     (TensorProduct (VectorSpaceImplementation v) w) )
+           => Bilinear (Scalar v) (v ⊗ w) (v ⊗ w)
+abstractVS_scaleTensor = scalarsSameInAbstraction @v
+  (coerce (scaleTensor @(VectorSpaceImplementation v) @w))
+
+abstractVS_negateTensor :: ∀ v w
+       . ( AbstractTensorSpace v
+         , TensorSpace w, Scalar w ~ Scalar v
+         , Coercible (TensorProduct v w)
+                     (TensorProduct (VectorSpaceImplementation v) w) )
+           => (v ⊗ w) -+> (v ⊗ w)
+abstractVS_negateTensor = scalarsSameInAbstraction @v
+  (coerce (negateTensor @(VectorSpaceImplementation v) @w))
+
+abstractVS_wellDefinedVector :: ∀ v
+         . ( AbstractTensorSpace v
+           ) => v -> Maybe v
+abstractVS_wellDefinedVector = coerce (wellDefinedVector @(VectorSpaceImplementation v))
+
+abstractVS_wellDefinedTensor :: ∀ v w
+         . ( AbstractTensorSpace v
+           , TensorSpace w, Scalar w ~ Scalar v
+           ) => (v ⊗ w) -> Maybe (v ⊗ w)
+abstractVS_wellDefinedTensor
+    = scalarsSameInAbstraction @v
+        (case abstractTensorProductsCoercion @v @w of
+           Coercion -> coerce (wellDefinedTensor @(VectorSpaceImplementation v) @w))
+
+abstractVS_tensorProduct :: ∀ v w . ( AbstractTensorSpace v
+           , TensorSpace w, Scalar w ~ Scalar v
+           ) => Bilinear v w (v ⊗ w)
+abstractVS_tensorProduct = scalarsSameInAbstraction @v
+    ( case ( abstractTensorProductsCoercion @v @w ) of
+       Coercion -> coerce (tensorProduct @(VectorSpaceImplementation v) @w) )
+
+abstractVS_transposeTensor :: ∀ v w . ( AbstractTensorSpace v
+           , TensorSpace w, Scalar w ~ Scalar v
+           ) => (v ⊗ w) -+> (w ⊗ v)
+abstractVS_transposeTensor
+    = scalarsSameInAbstraction @v ( case
+           ( abstractTensorProductsCoercion @v @w
+           , coerceFmapTensorProduct @w []
+                (Coercion @(VectorSpaceImplementation v) @(v)) ) of
+   (Coercion, Coercion) -> scalarsSameInAbstraction @v
+      (coerce (transposeTensor @(VectorSpaceImplementation v) @w))
+  )
+
+abstractVS_fmapTensor :: ∀ v u w . ( AbstractTensorSpace v
+           , TensorSpace u, Scalar u ~ Scalar v
+           , TensorSpace w, Scalar w ~ Scalar v )
+                   => Bilinear (u -+> w) (v ⊗ u) (v ⊗ w)
+abstractVS_fmapTensor
+   = scalarsSameInAbstraction @v
+       ( case ( abstractTensorProductsCoercion @v @u
+              , abstractTensorProductsCoercion @v @w ) of
+           (Coercion, Coercion)
+              -> coerce (fmapTensor @(VectorSpaceImplementation v) @u @w) )
+
+abstractVS_fzipTensorsWith :: ∀ v u w x . ( AbstractTensorSpace v
+           , TensorSpace u, Scalar u ~ Scalar v
+           , TensorSpace w, Scalar w ~ Scalar v
+           , TensorSpace x, Scalar x ~ Scalar v )
+                   => Bilinear ((w, x) -+> u) (v ⊗ w, v ⊗ x) (v ⊗ u)
+abstractVS_fzipTensorsWith = scalarsSameInAbstraction @v
+       ( case ( abstractTensorProductsCoercion @v @u
+              , abstractTensorProductsCoercion @v @w
+              , abstractTensorProductsCoercion @v @x ) of
+           (Coercion, Coercion, Coercion)
+              -> coerce (fzipTensorWith @(VectorSpaceImplementation v) @u @w @x)
+        )
+
+abstractVS_coerceFmapTensorProduct :: ∀ v u w p .
+         ( AbstractTensorSpace v
+         ) => p v -> Coercion u w -> Coercion (TensorProduct v u) (TensorProduct v w)
+abstractVS_coerceFmapTensorProduct _ crc
+      = case ( abstractTensorProductsCoercion @v @u
+             , abstractTensorProductsCoercion @v @w
+             , coerceFmapTensorProduct @(VectorSpaceImplementation v) [] crc ) of
+          (Coercion, Coercion, Coercion) -> Coercion
+
+abstractVS_dualSpaceWitness :: ∀ v . (AbstractLinearSpace v
+        , LinearSpace v
+        , LinearSpace (VectorSpaceImplementation v))
+     => DualSpaceWitness v
+abstractVS_dualSpaceWitness
+      = scalarsSameInAbstraction @v
+  ( case dualSpaceWitness @(VectorSpaceImplementation v) of
+      DualSpaceWitness -> DualSpaceWitness
+   )
+
+abstractVS_linearId :: ∀ v . ( AbstractLinearSpace v
+           , LinearSpace (VectorSpaceImplementation v) )
+                   => v +> v
+abstractVS_linearId = case dualSpaceWitness @(VectorSpaceImplementation v) of
+ DualSpaceWitness -> case coerceFmapTensorProduct
+                             @(DualVector (VectorSpaceImplementation v)) []
+                             (Coercion @v @(VectorSpaceImplementation v)) of
+   Coercion -> coerce (linearId @(VectorSpaceImplementation v))
+
+abstractVS_tensorId :: ∀ v w . ( AbstractLinearSpace v
+           , LinearSpace (VectorSpaceImplementation v)
+           , LinearSpace w, Scalar w ~ Scalar v )
+                   => (v ⊗ w) +> (v ⊗ w) 
+abstractVS_tensorId = scalarsSameInAbstraction @v
+  (case (dualSpaceWitness @w, dualSpaceWitness @(VectorSpaceImplementation v)) of
+     (DualSpaceWitness, DualSpaceWitness)
+       -> case coerceFmapTensorProduct @(DualVector w) []
+                 $ Coercion @(TensorProduct (VectorSpaceImplementation v) w)
+                            @(VectorSpaceImplementation v ⊗ w)
+                  . abstractTensorProductsCoercion @v @w
+                  . Coercion @(v ⊗ w) @(TensorProduct v w) of
+         Coercion
+           -> case ( coerceFmapTensorProduct 
+                      @(DualVector (VectorSpaceImplementation v)) []
+                      (Coercion :: Coercion
+                          (Tensor (Scalar v) (DualVector w) (Tensor (Scalar v) v w))
+                          (Tensor (Scalar v)
+                                  (DualVector w)
+                                  (Tensor (Scalar v)
+                                          (VectorSpaceImplementation v) w)))
+                   ) of
+            Coercion
+               -> coerce (tensorId @(VectorSpaceImplementation v) @w)
+       )
+
+abstractVS_applyDualVector :: ∀ v . ( AbstractLinearSpace v
+           , LinearSpace (VectorSpaceImplementation v) )
+                   => Bilinear (DualVector v) v (Scalar v)
+abstractVS_applyDualVector = scalarsSameInAbstraction @v
+ ( case dualSpaceWitness @(VectorSpaceImplementation v) of
+    DualSpaceWitness -> coerce (applyDualVector @(VectorSpaceImplementation v)) )
+
+abstractVS_applyLinear :: ∀ v w . ( AbstractLinearSpace v
+           , LinearSpace (VectorSpaceImplementation v)
+           , TensorSpace w, Scalar w ~ Scalar v )
+                   => Bilinear (v +> w) v w
+abstractVS_applyLinear = scalarsSameInAbstraction @v
+ ( coerce (applyLinear @(VectorSpaceImplementation v) @w)
+ )
+
+abstractVS_applyTensorFunctional :: ∀ v u .
+       ( AbstractLinearSpace v
+       , LinearSpace (VectorSpaceImplementation v)
+       , LinearSpace u, Scalar u ~ Scalar v )
+           => Bilinear (DualVector (v⊗u)) (v⊗u) (Scalar v)
+abstractVS_applyTensorFunctional = scalarsSameInAbstraction @v
+ (case abstractTensorProductsCoercion @v @u of
+   Coercion -> coerce (applyTensorFunctional @(VectorSpaceImplementation v) @u))
+
+abstractVS_applyTensorLinMap :: ∀ v u w .
+       ( AbstractLinearSpace v
+       , LinearSpace (VectorSpaceImplementation v)
+       , LinearSpace u, Scalar u ~ Scalar v
+       , TensorSpace w, Scalar w ~ Scalar v )
+                         => Bilinear ((v⊗u)+>w) (v⊗u) w
+abstractVS_applyTensorLinMap = scalarsSameInAbstraction @v
+ ( case abstractTensorProductsCoercion @v @u of
+   Coercion -> coerce (applyTensorLinMap @(VectorSpaceImplementation v) @u @w) )
+
+abstractSubbasisCoercion :: ∀ v .
+       Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+     => Coercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+abstractSubbasisCoercion = Coercion
+
+precomposeCoercion :: Coercion a b -> Coercion (b -> c) (a -> c)
+precomposeCoercion Coercion = Coercion
+
+postcomposeCoercion :: Coercion b c -> Coercion (a -> b) (a -> c)
+postcomposeCoercion Coercion = Coercion
+
+firstCoercion :: Coercion a b -> Coercion (a,c) (b,c)
+firstCoercion Coercion = Coercion
+
+leftCoercion :: Coercion a b -> Coercion (Either a c) (Either b c)
+leftCoercion Coercion = Coercion
+
+abstractVS_dualFinitenessWitness :: ∀ v .
+       ( AbstractLinearSpace v, FiniteDimensional v
+       , FiniteDimensional (VectorSpaceImplementation v) )
+     => DualFinitenessWitness v
+abstractVS_dualFinitenessWitness = scalarsSameInAbstraction @v
+  (case dualFinitenessWitness @(VectorSpaceImplementation v) of
+     DualFinitenessWitness DualSpaceWitness
+        -> DualFinitenessWitness DualSpaceWitness
+    )
+
+abstractVS_entireBasis :: ∀ v .
+       ( AbstractLinearSpace v, FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )
+          => SubBasis v
+abstractVS_entireBasis = sym (abstractSubbasisCoercion @v)
+            $ entireBasis @(VectorSpaceImplementation v)
+
+abstractVS_enumerateSubBasis :: ∀ v .
+       ( AbstractLinearSpace v, FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )
+          => SubBasis v -> [v]
+abstractVS_enumerateSubBasis = precomposeCoercion (abstractSubbasisCoercion @v)
+    $ coerce (enumerateSubBasis @(VectorSpaceImplementation v))
+
+abstractVS_decomposeLinMap :: ∀ v w .
+       ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+       , LSpace w, Scalar w ~ Scalar v )
+                   => (v +> w) -> (SubBasis v, DList w)
+abstractVS_decomposeLinMap = scalarsSameInAbstraction @v
+   ( postcomposeCoercion (firstCoercion $ sym (abstractSubbasisCoercion @v))
+      $ case abstractTensorProductsCoercion @v @w of
+         Coercion -> ( coerce (decomposeLinMap @(VectorSpaceImplementation v) @w)
+                         :: (v +> w) -> ( SubBasis (VectorSpaceImplementation v)
+                                        , DList w ) )
+     )
+
+abstractVS_decomposeLinMapWithin :: ∀ v w . ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+       , LSpace w, Scalar w ~ Scalar v )
+   => SubBasis v -> (v +> w) -> Either (SubBasis v, DList w) (DList w)
+abstractVS_decomposeLinMapWithin = scalarsSameInAbstraction @v
+ ( precomposeCoercion (abstractSubbasisCoercion @v)
+    . postcomposeCoercion (postcomposeCoercion
+        . leftCoercion . firstCoercion $ sym (abstractSubbasisCoercion @v))
+      $ coerce (decomposeLinMapWithin @(VectorSpaceImplementation v) @w)
+  )
+
+abstractVS_recomposeSB :: ∀ v . ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )
+   => SubBasis v -> [Scalar v] -> (v, [Scalar v])
+abstractVS_recomposeSB = scalarsSameInAbstraction @v
+ ( precomposeCoercion (abstractSubbasisCoercion @v)
+  $ coerce (recomposeSB @(VectorSpaceImplementation v))
+  )
+
+abstractVS_recomposeSBTensor :: ∀ v w . ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+       , FiniteDimensional w, Scalar w ~ Scalar v )
+   => SubBasis v -> SubBasis w -> [Scalar v] -> (v ⊗ w, [Scalar v])
+abstractVS_recomposeSBTensor = scalarsSameInAbstraction @v
+ ( precomposeCoercion (abstractSubbasisCoercion @v)
+  $ case abstractTensorProductsCoercion @v @w of
+     Coercion -> coerce (recomposeSBTensor @(VectorSpaceImplementation v) @w)
+  )
+
+abstractVS_recomposeLinMap :: ∀ v w . ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+       , LSpace w, Scalar w ~ Scalar v )
+   => SubBasis v -> [w] -> (v +> w, [w])
+abstractVS_recomposeLinMap = scalarsSameInAbstraction @v
+ ( precomposeCoercion (abstractSubbasisCoercion @v)
+  $ coerce (recomposeLinMap @(VectorSpaceImplementation v) @w)
+  )
+
+abstractVS_recomposeContraLinMap :: ∀ v f w . ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+       , LinearSpace w, Scalar w ~ Scalar v
+       , Hask.Functor f )
+                  => (f (Scalar w) -> w) -> f (DualVector v) -> v +> w
+abstractVS_recomposeContraLinMap f = scalarsSameInAbstraction @v
+ ( coerce (recomposeContraLinMap @(VectorSpaceImplementation v) @w @f f)
+                . fmap getConcreteDualVector
+  )
+
+abstractVS_recomposeLinMapTensor :: ∀ v f w u . ( AbstractLinearSpace v
+       , FiniteDimensional (VectorSpaceImplementation v)
+       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
+       , LinearSpace w, Scalar w ~ Scalar v
+       , FiniteDimensional u, Scalar u ~ Scalar v
+       , Hask.Functor f )
+   => (f (Scalar w) -> w) -> f (v+>DualVector u) -> (v⊗u) +> w
+abstractVS_recomposeLinMapTensor f = scalarsSameInAbstraction @v
+ ( coerce (recomposeContraLinMapTensor @(VectorSpaceImplementation v) @u @w @f f)
+              . fmap (coerce :: (v+>DualVector u)
+                          -> (VectorSpaceImplementation v+>DualVector u))
+  )
+
+abstractVS_uncanonicallyFromDual :: ∀ v . ( AbstractLinearSpace v
+        , FiniteDimensional (VectorSpaceImplementation v) )
+   => DualVector v -+> v
+abstractVS_uncanonicallyFromDual = scalarsSameInAbstraction @v
+ ( case abstractDualVectorCoercion @v of
+            Coercion -> coerce (uncanonicallyFromDual @(VectorSpaceImplementation v))
+  )
+
+abstractVS_uncanonicallyToDual :: ∀ v . ( AbstractLinearSpace v
+        , FiniteDimensional (VectorSpaceImplementation v) )
+   => v -+> DualVector v
+abstractVS_uncanonicallyToDual = scalarsSameInAbstraction @v
+ ( case abstractDualVectorCoercion @v of
+            Coercion -> coerce (uncanonicallyToDual @(VectorSpaceImplementation v))
+  )
+
+abstractVS_tensorEquality :: ∀ v w . ( AbstractLinearSpace v
+        , FiniteDimensional (VectorSpaceImplementation v)
+        , TensorSpace w, Eq w, Scalar w ~ Scalar v )
+                       => (v ⊗ w) -> (v ⊗ w) -> Bool
+abstractVS_tensorEquality = scalarsSameInAbstraction @v
+ ( case abstractTensorProductsCoercion @v @w of
+    Coercion -> coerce (tensorEquality @(VectorSpaceImplementation v) @w)
+  )
+
+abstractVS_dualBasisCandidates :: ∀ v . ( AbstractLinearSpace v
+        , SemiInner (VectorSpaceImplementation v) )
+      => [(Int, v)] -> Forest (Int, DualVector v)
+abstractVS_dualBasisCandidates = scalarsSameInAbstraction @v
+ ( case abstractDualVectorCoercion @v of
+            Coercion -> coerce (dualBasisCandidates @(VectorSpaceImplementation v))
+  )
+
+abstractVS_tensorDualBasisCandidates :: ∀ v w . ( AbstractLinearSpace v
+        , LinearSpace v
+        , SemiInner (VectorSpaceImplementation v)
+        , SemiInner w, Scalar w ~ Scalar v)
+                    => [(Int, v ⊗ w)]
+                     -> Forest (Int, v +> DualVector w)
+abstractVS_tensorDualBasisCandidates = scalarsSameInAbstraction @v
+ ( case (dualSpaceWitness @v, dualSpaceWitness @w) of
+    (DualSpaceWitness, DualSpaceWitness)
+         -> case ( abstractDualVectorCoercion @v
+                 , abstractTensorProductsCoercion @v @(DualVector w)
+                 , abstractTensorProductsCoercion @v @w
+                 ) of
+       (Coercion, Coercion, Coercion)
+          -> coerce (tensorDualBasisCandidates @(VectorSpaceImplementation v) @w)
+  )
+
+abstractVS_symTensorDualBasisCandidates :: ∀ v . ( AbstractLinearSpace v
+         , LinearSpace v
+         , SemiInner (VectorSpaceImplementation v) )
+        => [(Int, SymmetricTensor (Scalar v) v)]
+              -> Forest (Int, SymmetricTensor (Scalar v) (DualVector v))
+abstractVS_symTensorDualBasisCandidates = scalarsSameInAbstraction @v
+ ( case ( dualSpaceWitness @v
+        , dualSpaceWitness @(VectorSpaceImplementation v)
+        , abstractDualVectorCoercion @v ) of
+    (DualSpaceWitness, DualSpaceWitness, crdv)
+       -> case ( abstractTensorProductsCoercion @v @v
+               , coerceFmapTensorProduct @(DualVector (VectorSpaceImplementation v)) []
+                   crdv
+               , coerceFmapTensorProduct @(VectorSpaceImplementation v) []
+                   crdv
+               , coerceFmapTensorProduct @(VectorSpaceImplementation v) []
+                   (Coercion @v @(VectorSpaceImplementation v))
+               ) of
+     (Coercion, Coercion, Coercion, Coercion)
+        -> coerce (symTensorDualBasisCandidates @(VectorSpaceImplementation v))
+  )
+
+-- | More powerful version of @deriving newtype@, specialised to the classes from
+--   this package (and of @manifolds-core@). The 'DualVector' space will be a separate
+--   type, even if the type you abstract over is self-dual.
+copyNewtypeInstances :: Q Type -> [Name] -> DecsQ
+copyNewtypeInstances cxtv classes = do
+
+ (tvbs, cxt, (a,c)) <- do
+   (tvbs', cxt', a') <- deQuantifyType cxtv
+   let extractImplementationType (AppT tc (VarT tvb)) atvbs
+              = extractImplementationType tc $ atvbs++[PlainTV tvb]
+       extractImplementationType (ConT aName) atvbs = do
+         D.reifyDatatype aName >>= \case
+          D.DatatypeInfo{ D.datatypeVariant = D.Newtype
+                        , D.datatypeVars = dttvbs
+                        , D.datatypeCons = [
+                           D.ConstructorInfo
+                              { D.constructorFields = [c''] } ]
+                        }
+             -> let replaceTVs :: [TyVarBndr] -> [TyVarBndr] -> Type -> Type
+                    replaceTVs [] [] = id
+                    replaceTVs (PlainTV infoTV:infoTVs) (PlainTV instTV:instTVs)
+                        = replaceTVs infoTVs instTVs . replaceTV infoTV instTV
+                    replaceTVs (KindedTV infoTV _:infoTVs) instTVs
+                        = replaceTVs (PlainTV infoTV:infoTVs) instTVs
+                    replaceTVs infoTVs (KindedTV instTV _:instTVs)
+                        = replaceTVs infoTVs (PlainTV instTV:instTVs)
+                    replaceTVs infoTVs instTVs
+                        = error $ "infoTVs = "++show infoTVs++", instTVs = "++show instTVs
+                    replaceTV :: Name -> Name -> Type -> Type
+                    replaceTV infoTV instTV (AppT tc (VarT tv))
+                     | tv==infoTV  = AppT (replaceTV infoTV instTV tc) (VarT instTV)
+                    replaceTV infoTV instTV (AppT tc ta)
+                           = AppT (replaceTV infoTV instTV tc)
+                                  (replaceTV infoTV instTV ta)
+                    replaceTV _ _ t@(TupleT _) = t
+                    replaceTV _ _ t@(ConT _) = t
+                    replaceTV _ _ t
+                        = error $ "Don't know how to substitute type variables in "
+                                    ++ show t
+                in return $ replaceTVs dttvbs atvbs c''
+          _ -> error $ show aName ++ " is not a newtype."
+       extractImplementationType a'' _
+           = error $ "Don't know how to handle type "++show a''
+                            ++" (specified: "++show a'++")"
+   c' <- extractImplementationType a' []
+   return (tvbs', pure cxt', (pure a', pure c'))
+ 
+ let allClasses =
+       [ ''AbstractAdditiveGroup | _<-[()], ''AdditiveGroup `elem` classes ]
+      ++ [ ''AbstractVectorSpace | _<-[()], ''VectorSpace `elem` classes ]
+      ++ [ ''AbstractTensorSpace | _<-[()], ''TensorSpace `elem` classes ]
+      ++ [ ''AbstractLinearSpace | _<-[()], ''LinearSpace `elem` classes ]
+      ++ classes
+
+ vtnameHash <- abs . hash . show <$> a
+
+ sequence [case dClass of
+     "AbstractAdditiveGroup" -> InstanceD Nothing <$> cxt <*>
+                          [t|AbstractAdditiveGroup $a|] <*> [d|
+         type instance VectorSpaceImplementation $a = $c
+      |]
+     "AdditiveGroup" -> InstanceD Nothing <$> cxt <*>
+                          [t|AdditiveGroup $a|] <*> [d|
+         $(varP 'zeroV) = abstractVS_zeroV
+         $(varP '(^+^)) = abstractVS_addvs
+         $(varP '(^-^)) = abstractVS_subvs
+         $(varP 'negateV) = abstractVS_negateV
+      |]
+     "AffineSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|AffineSpace $a|] <*> [d|
+         type instance Diff $a = $a
+         $(varP '(.-.)) = abstractVS_subvs
+         $(varP '(.+^)) = abstractVS_addvs
+      |]
+     "VectorSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|VectorSpace $a|] <*> [d|
+         type instance Scalar $a = Scalar ($c)
+         $(varP '(*^)) = abstractVS_scalev
+      |]
+     "AbstractVectorSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|AbstractVectorSpace $a|] <*> [d|
+         $(varP 'scalarsSameInAbstraction)
+            = abstractVS_scalarsSameInAbstraction @($a)
+      |]
+     "InnerSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|InnerSpace $a|] <*> [d|
+         $(varP '(<.>)) = abstractVS_innerProd
+      |]
+     "Semimanifold" -> InstanceD Nothing <$> cxt <*>
+                          [t|Semimanifold $a|] <*> [d|
+         type instance Needle $a = $a
+         $(varP '(.+~^)) = abstractVS_addvs
+#if !MIN_VERSION_manifolds_core(0,6,0)
+         type instance Interior $a = $a
+         $(varP 'toInterior) = pure
+         $(varP 'fromInterior) = id
+         $(varP 'translateP) = Tagged (^+^)
+         $(varP 'semimanifoldWitness) = SemimanifoldWitness BoundarylessWitness
+#endif
+      |]
+     "PseudoAffine" -> InstanceD Nothing <$> cxt <*>
+                          [t|PseudoAffine $a|] <*> [d|
+         $(varP '(.-~.)) = \p q -> Just (abstractVS_subvs p q)
+         $(varP '(.-~!)) = abstractVS_subvs
+      |]
+     "TensorSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|TensorSpace $a|] <*> [d|
+         type instance TensorProduct $a w = TensorProduct $c w
+         $(varP 'scalarSpaceWitness) = abstractVS_scalarSpaceWitness
+         $(varP 'linearManifoldWitness) = abstractVS_linearManifoldWitness
+         $(varP 'toFlatTensor) = abstractVS_toFlatTensor
+         $(varP 'fromFlatTensor) = abstractVS_fromFlatTensor
+         $(varP 'zeroTensor) = abstractVS_zeroTensor
+         $(varP 'addTensors) = abstractVS_addTensors
+         $(varP 'subtractTensors) = abstractVS_subtractTensors
+         $(varP 'scaleTensor) = abstractVS_scaleTensor
+         $(varP 'negateTensor) = abstractVS_negateTensor
+         $(varP 'wellDefinedVector) = abstractVS_wellDefinedVector
+         $(varP 'wellDefinedTensor) = abstractVS_wellDefinedTensor
+         $(varP 'tensorProduct) = abstractVS_tensorProduct
+         $(varP 'transposeTensor) = abstractVS_transposeTensor
+         $(varP 'fmapTensor) = abstractVS_fmapTensor
+         $(varP 'fzipTensorWith) = abstractVS_fzipTensorsWith
+         $(varP 'coerceFmapTensorProduct) = abstractVS_coerceFmapTensorProduct
+      |]
+     "AbstractTensorSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|AbstractTensorSpace $a|] <*> [d|
+         $(varP 'abstractTensorProductsCoercion)
+                  = Coercion
+      |]
+     "LinearSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|LinearSpace $a|] <*> [d|
+         type instance DualVector $a = AbstractDualVector $a $c
+         $(varP 'dualSpaceWitness) = abstractVS_dualSpaceWitness
+         $(varP 'linearId) = abstractVS_linearId
+         $(varP 'tensorId) = abstractVS_tensorId
+         $(varP 'applyDualVector) = abstractVS_applyDualVector
+         $(varP 'applyLinear) = abstractVS_applyLinear
+         $(varP 'applyTensorFunctional) = abstractVS_applyTensorFunctional
+         $(varP 'applyTensorLinMap) = abstractVS_applyTensorLinMap
+         $(varP 'useTupleLinearSpaceComponents) = \_ -> usingNonTupleTypeAsTupleError
+      |]
+     "AbstractLinearSpace" -> InstanceD Nothing <$> cxt <*>
+                          [t|AbstractLinearSpace $a|] <*> [d|
+      |]
+     "FiniteDimensional" -> InstanceD Nothing <$> cxt <*>
+                          [t|FiniteDimensional $a|] <*> do
+        subBasisCstr <- newName $ "SubBasis"++show vtnameHash
+        
+        tySyns <- sequence [
+#if MIN_VERSION_template_haskell(2,15,0)
+           NewtypeInstD [] (Just tvbs)
+              <$> (AppT (ConT ''SubBasis) <$> a)
+              <*> pure Nothing
+              <*> (NormalC subBasisCstr . pure .
+                          (Bang NoSourceUnpackedness NoSourceStrictness,)
+                     <$> [t| SubBasis $c |])
+              <*> pure []
+#else
+           NewtypeInstD [] ''SubBasis
+              <$> ((:[]) <$> a)
+              <*> pure Nothing
+              <*> (NormalC subBasisCstr . pure . 
+                          (Bang NoSourceUnpackedness NoSourceStrictness,)
+                     <$> [t| SubBasis $c |])
+              <*> pure []
+#endif
+         ]
+        methods <- [d|
+         $(varP 'dualFinitenessWitness) = abstractVS_dualFinitenessWitness
+         $(varP 'entireBasis) = abstractVS_entireBasis
+         $(varP 'enumerateSubBasis) = abstractVS_enumerateSubBasis
+         $(varP 'decomposeLinMap) = abstractVS_decomposeLinMap
+         $(varP 'decomposeLinMapWithin) = abstractVS_decomposeLinMapWithin
+         $(varP 'recomposeSB) = abstractVS_recomposeSB
+         $(varP 'recomposeSBTensor) = abstractVS_recomposeSBTensor
+         $(varP 'recomposeLinMap) = abstractVS_recomposeLinMap
+         $(varP 'recomposeContraLinMap) = abstractVS_recomposeContraLinMap
+         $(varP 'recomposeContraLinMapTensor) = abstractVS_recomposeLinMapTensor
+         $(varP 'uncanonicallyFromDual) = abstractVS_uncanonicallyFromDual
+         $(varP 'uncanonicallyToDual) = abstractVS_uncanonicallyToDual
+         $(varP 'tensorEquality) = abstractVS_tensorEquality
+          |]
+        return $ tySyns ++ methods
+     "SemiInner" -> InstanceD Nothing <$> cxt <*>
+                          [t|SemiInner $a|] <*> [d|
+          $(varP 'dualBasisCandidates) = abstractVS_dualBasisCandidates
+          $(varP 'tensorDualBasisCandidates) = abstractVS_tensorDualBasisCandidates
+          $(varP 'symTensorDualBasisCandidates) = abstractVS_symTensorDualBasisCandidates
+       |]
+     _ -> error $ "Unsupported class to derive newtype instance for: ‘"++dClass++"’"
+   | Name (OccName dClass) _ <- allClasses
+   ]
 
diff --git a/Math/VectorSpace/Docile.hs b/Math/VectorSpace/Docile.hs
--- a/Math/VectorSpace/Docile.hs
+++ b/Math/VectorSpace/Docile.hs
@@ -664,7 +664,7 @@
 deriving instance Show (SubBasis ℝ)
   
 instance ∀ u v . ( FiniteDimensional u, FiniteDimensional v
-                 , Scalar u ~ Scalar v, Scalar (DualVector u) ~ Scalar (DualVector v) )
+                 , Scalar u ~ Scalar v )
             => FiniteDimensional (u,v) where
   data SubBasis (u,v) = TupleBasis !(SubBasis u) !(SubBasis v)
   entireBasis = TupleBasis entireBasis entireBasis
@@ -929,31 +929,6 @@
                      -> LinearMap s (LinearMap s (DualVector v) v) w
          rcCLM (DualFinitenessWitness DualSpaceWitness) f
             = recomposeContraLinMap f
-  recomposeContraLinMapTensor = rcCLMT'
-   where rcCLMT' :: ∀ f u w . (Hask.Functor f, LinearSpace w, s~Scalar w
-                                            , FiniteDimensional u, s~Scalar u)
-                    => (f s->w) -> f (SymmetricTensor s v +> DualVector u)
-                                  -> (SymmetricTensor s v ⊗ u) +> w
-         rcCLMT' f tenss
-           = LinearMap . arr (fmap rassocTensor . rassocTensor . asTensor)
-                 . rcCLMT (dualFinitenessWitness, dualFinitenessWitness) f
-                      $ fmap getLinearMap tenss
-          where rcCLMT :: (DualFinitenessWitness v, DualFinitenessWitness u)
-                 -> (f s->w) -> f (Tensor s (DualVector v)
-                                            (Tensor s (DualVector v) (DualVector u)))
-                  -- -> LinearMap s (Tensor s (SymmetricTensor s v) u) w
-                  --  ∼ TensorProduct (LinearMap s (SymmetricTensor s v) (DualVector u)) w
-                  --  ⩵ TensorProduct (SymmetricTensor s (DualVector v)) (DualVector u ⊗ w)
-                  --  ⩵ Tensor s (DualVector v) (DualVector v ⊗ (DualVector u ⊗ w))
-                     -> LinearMap s (LinearMap s (DualVector v)
-                                                 (LinearMap s (DualVector v) u)) w
-                  --  ∼ Tensor s (Tensor s (DualVector v)
-                  --                       (DualVector v ⊗ DualVector u)) w
-                  --  ∼ Tensor s (DualVector v)
-                  --             (Tensor s (DualVector v ⊗ DualVector u) w)
-                rcCLMT ( DualFinitenessWitness DualSpaceWitness
-                       , DualFinitenessWitness DualSpaceWitness ) f
-                             = recomposeContraLinMap f
   uncanonicallyFromDual = case dualFinitenessWitness :: DualFinitenessWitness v of
      DualFinitenessWitness DualSpaceWitness -> LinearFunction
           $ \(SymTensor t) -> SymTensor $ arr fromLinearMap . uncanonicallyFromDual $ t
diff --git a/linearmap-category.cabal b/linearmap-category.cabal
--- a/linearmap-category.cabal
+++ b/linearmap-category.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                linearmap-category
-version:             0.4.2.0
+version:             0.4.3.0
 synopsis:            Native, complete, matrix-free linear algebra.
 description:         The term /numerical linear algebra/ is often used almost
                      synonymous with /matrix modifications/. However, what's interesting
@@ -61,7 +61,9 @@
                        semigroups, hashable,
                        data-default-class,
                        ieee754 >= 0.7 && < 0.9,
-                       call-stack, template-haskell >=2.12 && <2.18,
+                       call-stack,
+                       template-haskell >=2.12 && <2.18,
+                       th-abstraction >=0.4 && <0.5,
                        QuickCheck >=2.11 && <2.15
   -- hs-source-dirs:      
   default-language:    Haskell2010
diff --git a/test/tasty/test.hs b/test/tasty/test.hs
--- a/test/tasty/test.hs
+++ b/test/tasty/test.hs
@@ -36,7 +36,32 @@
 import qualified Test.QuickCheck as QC
 
 
+newtype ℝ⁴ = ℝ⁴ { getℝ⁴ :: V4 ℝ }
+ deriving (Eq, Show)
 
+copyNewtypeInstances [t| ℝ⁴ |]
+   [ ''AdditiveGroup, ''AffineSpace, ''VectorSpace
+   , ''Semimanifold, ''PseudoAffine
+   , ''TensorSpace, ''LinearSpace
+   , ''FiniteDimensional, ''SemiInner, ''InnerSpace ]
+
+newtype H¹ℝ⁴ a = H¹ℝ⁴ { getH¹ℝ⁴ :: ((a,a),(a,a)) }
+ deriving (Eq, Show)
+
+copyNewtypeInstances [t| ∀ a
+          . (RealFloat' a, FiniteDimensional a, SemiInner a) => H¹ℝ⁴ a |]
+   [ ''AdditiveGroup, ''AffineSpace, ''VectorSpace
+   , ''Semimanifold, ''PseudoAffine
+   , ''TensorSpace, ''LinearSpace
+   , ''FiniteDimensional, ''SemiInner ]
+
+derivative₄ :: H¹ℝ⁴ ℝ -> ℝ⁴
+derivative₄ (H¹ℝ⁴ ((w,x),(y,z))) = ℝ⁴ (V4 z w x y) ^-^ ℝ⁴ (V4 x y z w)
+
+instance InnerSpace (H¹ℝ⁴ ℝ) where
+  H¹ℝ⁴ v <.> H¹ℝ⁴ w = v<.>w + derivative₄ (H¹ℝ⁴ v)<.>derivative₄ (H¹ℝ⁴ w)
+
+
 newtype ℝ⁵ a = ℝ⁵ { getℝ⁵ :: [ℝ] }
  deriving (Eq, Show)
 
@@ -86,11 +111,11 @@
 
 makeFiniteDimensionalFromBasis [t| H¹ℝ⁵ |]
 
-derivative :: H¹ℝ⁵ -> ℝ⁵ Int
-derivative (H¹ℝ⁵ (ℝ⁵ (x₀:xs))) = ℝ⁵ (x₀:xs) ^-^ ℝ⁵ (xs++[x₀])
+derivative₅ :: H¹ℝ⁵ -> ℝ⁵ Int
+derivative₅ (H¹ℝ⁵ (ℝ⁵ (x₀:xs))) = ℝ⁵ (x₀:xs) ^-^ ℝ⁵ (xs++[x₀])
 
 instance InnerSpace H¹ℝ⁵ where
-  H¹ℝ⁵ v <.> H¹ℝ⁵ w = v<.>w + derivative (H¹ℝ⁵ v)<.>derivative (H¹ℝ⁵ w)
+  H¹ℝ⁵ v <.> H¹ℝ⁵ w = v<.>w + derivative₅ (H¹ℝ⁵ v)<.>derivative₅ (H¹ℝ⁵ w)
 
 instance Arbitrary (V4 ℝ) where
   arbitrary = V4<$>arbitrary<*>arbitrary<*>arbitrary<*>arbitrary
@@ -113,6 +138,19 @@
      $ \v -> (riesz-+$>coRiesz-+$>v) === (v :: ℝ⁵ Int)
     , testProperty "Riesz representation, non-orthonormal basis"
      $ \v -> (riesz-+$>coRiesz-+$>v) ≈≈≈ (v :: H¹ℝ⁵)
+    ]
+   , testGroup "Newtype-derived space"
+    [ testProperty "Addition"
+     $ \v w -> ℝ⁴ v^+^ℝ⁴ w === ℝ⁴ (v^+^w)
+    , testProperty "Riesz representation, orthonormal basis"
+     $ \v -> (riesz-+$>coRiesz-+$>ℝ⁴ v) === ℝ⁴ v
+    , testProperty "Riesz is trivial in orthonormal basis"
+     $ \v -> (riesz-+$>AbstractDualVector v) ≈≈≈ ℝ⁴ v
+    , testProperty "Riesz representation, non-orthonormal basis"
+     $ \v -> (riesz-+$>coRiesz-+$>H¹ℝ⁴ v) ≈≈≈ (H¹ℝ⁴ v :: H¹ℝ⁴ Double)
+    , testProperty "Riesz nontriviality in general case"
+     . QC.expectFailure
+     $ \v -> (riesz-+$>AbstractDualVector v) ≈≈≈ (H¹ℝ⁴ v :: H¹ℝ⁴ Double)
     ]
    ]