diff --git a/brush-strokes/src/cusps/bench/Bench/Types.hs b/brush-strokes/src/cusps/bench/Bench/Types.hs
index 2971df6..87ee128 100644
--- a/brush-strokes/src/cusps/bench/Bench/Types.hs
+++ b/brush-strokes/src/cusps/bench/Bench/Types.hs
@@ -61,18 +61,18 @@ type ParamsCt nbParams
   = ( Show ( ℝ nbParams )
     , HasChainRule Double 2 ( ℝ nbParams )
     , HasChainRule 𝕀 3 ( 𝕀ℝ nbParams )
-    , Applicative ( D 2 ( ℝ nbParams ) )
-    , Applicative ( D 3 ( ℝ nbParams ) )
-    , Traversable ( D 2 ( ℝ nbParams ) )
-    , Traversable ( D 3 ( ℝ nbParams ) )
+    , Applicative ( D 2 nbParams )
+    , Applicative ( D 3 nbParams )
+    , Traversable ( D 2 nbParams )
+    , Traversable ( D 3 nbParams )
     , Representable Double ( ℝ nbParams )
     , Representable 𝕀 ( 𝕀ℝ nbParams )
     , Module Double ( T ( ℝ nbParams ) )
     , Module 𝕀 ( T ( 𝕀ℝ nbParams ) )
-    , Module ( D 2 ( ℝ nbParams ) Double ) ( D 2 ( ℝ nbParams ) ( ℝ 2 ) )
-    , Module ( D 3 ( ℝ nbParams ) 𝕀 ) ( D 3 ( ℝ nbParams ) ( 𝕀ℝ 2 ) )
-    , Transcendental ( D 2 ( ℝ nbParams ) Double )
-    , Transcendental ( D 3 ( ℝ nbParams ) 𝕀 )
+    , Module ( D 2 nbParams Double ) ( D 2 nbParams ( ℝ 2 ) )
+    , Module ( D 3 nbParams 𝕀 ) ( D 3 nbParams ( 𝕀ℝ 2 ) )
+    , Transcendental ( D 2 nbParams Double )
+    , Transcendental ( D 3 nbParams 𝕀 )
     )
 
 newtype Params nbParams = Params { getParams :: ( ℝ nbParams ) }
diff --git a/brush-strokes/src/cusps/inspect/Main.hs b/brush-strokes/src/cusps/inspect/Main.hs
index 5e0f265..152606b 100644
--- a/brush-strokes/src/cusps/inspect/Main.hs
+++ b/brush-strokes/src/cusps/inspect/Main.hs
@@ -75,10 +75,6 @@ data PointData params
 outlineFunction
   :: forall {t} (i :: t) brushParams
   .  ( Show brushParams
-     , D 1 ( I i 2 ) ~ D 1 ( ℝ 2 )
-     , D 2 ( I i 2 ) ~ D 2 ( ℝ 2 )
-     , D 3 ( I i 1 ) ~ D 3 ( ℝ 1 )
-     , D 3 ( I i 2 ) ~ D 3 ( ℝ 2 )
      , HasType ( ℝ 2 ) ( PointData brushParams )
      , Cross  ( I i Double ) ( T ( I i 2 ) )
      , Module ( I i Double ) ( T ( I i brushParams ) )
@@ -90,7 +86,6 @@ outlineFunction
      , HasChainRule ( I i Double ) 3 ( I i 1 )
      , HasChainRule ( I i Double ) 3 ( I i brushParams )
      , Traversable ( D 3 brushParams )
-     , Traversable ( D 3 ( I i brushParams ) )
      , HasBézier 3 i
      )
   => ( I i Double -> I i 1 )
@@ -263,9 +258,9 @@ instance HasBézier 3 AI where
 κ = 0.5519150244935105707435627227925
 
 circleSpline :: forall {t} (i :: t) k u v
-             .  Applicative ( D k ( I i u ) )
-             => ( Double -> Double -> D k ( I i u ) ( I i v ) )
-             -> D k ( I i u ) ( Spline 'Closed () ( I i v ) )
+             .  Applicative ( D k ( Dim u ) )
+             => ( Double -> Double -> D k ( Dim u ) ( I i v ) )
+             -> D k ( Dim u ) ( Spline 'Closed () ( I i v ) )
 circleSpline p = sequenceA $
   Spline { splineStart  = p 1 0
          , splineCurves = ClosedCurves crvs lastCrv }
diff --git a/brush-strokes/src/lib/Calligraphy/Brushes.hs b/brush-strokes/src/lib/Calligraphy/Brushes.hs
index 151ab70..fbaf1d5 100644
--- a/brush-strokes/src/lib/Calligraphy/Brushes.hs
+++ b/brush-strokes/src/lib/Calligraphy/Brushes.hs
@@ -64,14 +64,15 @@ data Brush nbBrushParams
 
 -- Some convenience type synonyms for brush types... a bit horrible
 type ParamsICt :: Nat -> k -> Nat -> Constraint
-type ParamsICt k i rec =
+type ParamsICt k i nbParams =
     ( Module
-       ( D k ( I i rec ) ( I i Double ) )
-       ( D k ( I i rec ) ( I i 2 ) )
+       ( D k nbParams ( I i Double ) )
+       ( D k nbParams ( I i 2 ) )
     , Module ( I i Double ) ( T ( I i Double ) )
-    , HasChainRule ( I i Double ) k ( I i rec )
-    , Representable ( I i Double ) ( I i rec )
-    , Applicative ( D k ( I i rec ) )
+    , HasChainRule ( I i Double ) k ( I i nbParams )
+    , Representable ( I i Double ) ( I i nbParams )
+    , Applicative ( D k nbParams )
+    , Dim ( I i nbParams ) ~ nbParams
     )
 
 {-# INLINEABLE circleBrush #-}
@@ -137,19 +138,19 @@ circleBrushFn :: forall {t} (i :: t) k nbParams
               -> C k ( I i nbParams ) ( Spline 'Closed () ( I i 2 ) )
 circleBrushFn _ mkI1 mkI2 =
   D \ params ->
-    let r :: D k ( I i nbParams ) ( I i Double )
+    let r :: D k nbParams ( I i Double )
         r = runD ( var @_ @k $ Fin 1 ) params
-        mkPt :: Double -> Double -> D k ( I i nbParams ) ( I i 2 )
+        mkPt :: Double -> Double -> D k nbParams ( I i 2 )
         mkPt x y
           =   ( r `scaledBy` x ) *^ e_x
           ^+^ ( r `scaledBy` y ) *^ e_y
     in circleSpline mkPt
   where
-    e_x, e_y :: D k ( I i nbParams ) ( I i 2 )
+    e_x, e_y :: D k nbParams ( I i 2 )
     e_x = pure $ mkI2 $ ℝ2 1 0
     e_y = pure $ mkI2 $ ℝ2 0 1
 
-    scaledBy :: D k ( I i nbParams ) ( I i Double ) -> Double -> D k ( I i nbParams ) ( I i Double )
+    scaledBy :: D k nbParams ( I i Double ) -> Double -> D k nbParams ( I i Double )
     scaledBy d x = fmap ( mkI1 x * ) d
 {-# INLINEABLE circleBrushFn #-}
 
@@ -160,25 +161,24 @@ ellipseBrushFn :: forall {t} (i :: t) k nbParams
                 => Proxy# i
                 -> ( Double -> I i Double )
                 -> ( I ℝ 2 -> I i 2 )
-
                 -> C k ( I i nbParams ) ( Spline 'Closed () ( I i 2 ) )
 ellipseBrushFn _ mkI1 mkI2 =
   D \ params ->
-    let a, b :: D k ( I i nbParams ) ( I i Double )
+    let a, b :: D k nbParams ( I i Double )
         a = runD ( var @_ @k $ Fin 1 ) params
         b = runD ( var @_ @k $ Fin 2 ) params
-        mkPt :: Double -> Double -> D k ( I i nbParams ) ( I i 2 )
+        mkPt :: Double -> Double -> D k nbParams ( I i 2 )
         mkPt x y
           = let !x' = a `scaledBy` x
                 !y' = b `scaledBy` y
             in x' *^ e_x ^+^ y' *^ e_y
     in circleSpline mkPt
   where
-    e_x, e_y :: D k ( I i nbParams ) ( I i 2 )
+    e_x, e_y :: D k nbParams ( I i 2 )
     e_x = pure $ mkI2 $ ℝ2 1 0
     e_y = pure $ mkI2 $ ℝ2 0 1
 
-    scaledBy :: D k ( I i nbParams ) ( I i Double ) -> Double -> D k ( I i nbParams ) ( I i Double )
+    scaledBy :: D k nbParams ( I i Double ) -> Double -> D k nbParams ( I i Double )
     scaledBy d x = fmap ( mkI1 x * ) d
 {-# INLINEABLE ellipseBrushFn #-}
 
@@ -212,10 +212,10 @@ tearDropBrushFn :: forall {t} (i :: t) k nbParams
                  -> C k ( I i nbParams ) ( Spline 'Closed () ( I i 2 ) )
 tearDropBrushFn _ mkI1 mkI2 =
   D \ params ->
-    let w, h :: D k ( I i nbParams ) ( I i Double )
+    let w, h :: D k nbParams ( I i Double )
         w = runD ( var @_ @k ( Fin 1 ) ) params
         h = runD ( var @_ @k ( Fin 2 ) ) params
-        mkPt :: Double -> Double -> D k ( I i nbParams ) ( I i 2 )
+        mkPt :: Double -> Double -> D k nbParams ( I i 2 )
         mkPt x y
           -- 1. translate the teardrop so that the centre of mass is at the origin
           -- 2. scale the teardrop so that it has the requested width/height
@@ -232,10 +232,10 @@ tearDropBrushFn _ mkI1 mkI2 =
                     ( mkPt -0.5 sqrt3_over_2 )
                     BackToStart () }
   where
-    e_x, e_y :: D k ( I i nbParams ) ( I i 2 )
+    e_x, e_y :: D k nbParams ( I i 2 )
     e_x = pure $ mkI2 $ ℝ2 1 0
     e_y = pure $ mkI2 $ ℝ2 0 1
 
-    scaledBy :: D k ( I i nbParams ) ( I i Double ) -> Double -> D k ( I i nbParams ) ( I i Double )
+    scaledBy :: D k nbParams ( I i Double ) -> Double -> D k nbParams ( I i Double )
     scaledBy d x = fmap ( mkI1 x * ) d
 {-# INLINEABLE tearDropBrushFn #-}
diff --git a/brush-strokes/src/lib/Math/Algebra/Dual.hs b/brush-strokes/src/lib/Math/Algebra/Dual.hs
index 6150f44..cde608b 100644
--- a/brush-strokes/src/lib/Math/Algebra/Dual.hs
+++ b/brush-strokes/src/lib/Math/Algebra/Dual.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes  #-}
+{-# LANGUAGE PolyKinds            #-}
 {-# LANGUAGE RebindableSyntax     #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE TemplateHaskell      #-}
@@ -7,7 +8,7 @@
 {-# OPTIONS_GHC -Wno-orphans -O2 #-}
 
 module Math.Algebra.Dual
-  ( C(..), D
+  ( C(..), D, Dim
   , HasChainRule(..), chainRule
   , uncurryD2, uncurryD3
   , linear, fun, var
@@ -45,8 +46,12 @@ import Math.Ring
 
 -- | @C n u v@ is the space of @C^k@-differentiable maps from @u@ to @v@.
 type C :: Nat -> Type -> Type -> Type
-newtype C k u v = D { runD :: u -> D k u v }
-deriving stock instance Functor ( D k u ) => Functor ( C k u )
+newtype C k u v = D { runD :: u -> D k ( Dim u ) v }
+deriving stock instance Functor ( D k ( Dim u ) ) => Functor ( C k u )
+
+type Dim :: k -> Nat
+type family Dim u
+type instance Dim ( ℝ n ) = n
 
 -- | @D k u v@ is the space of @k@-th order germs of functions from @u@ to @v@,
 -- represented by the algebra:
@@ -54,35 +59,35 @@ deriving stock instance Functor ( D k u ) => Functor ( C k u )
 -- \[ \mathbb{Z}[x_1, \ldots, x_n]/(x_1, \ldots, x_n)^{k+1} \otimes_\mathbb{Z} v \]
 --
 -- when @u@ is of dimension @n@.
-type D :: Nat -> Type -> Type -> Type
+type D :: Nat -> Nat -> Type -> Type
 type family D k u
 
-type instance D k ( ℝ 0 ) = D𝔸0
-type instance D 0 ( ℝ 1 ) = D𝔸0
-type instance D 0 ( ℝ 2 ) = D𝔸0
-type instance D 0 ( ℝ 3 ) = D𝔸0
-type instance D 0 ( ℝ 4 ) = D𝔸0
+type instance D k 0 = D𝔸0
+type instance D 0 1 = D𝔸0
+type instance D 0 2 = D𝔸0
+type instance D 0 3 = D𝔸0
+type instance D 0 4 = D𝔸0
 
-type instance D 1 ( ℝ 1 ) = D1𝔸1
-type instance D 1 ( ℝ 2 ) = D1𝔸2
-type instance D 1 ( ℝ 3 ) = D1𝔸3
-type instance D 1 ( ℝ 4 ) = D1𝔸4
+type instance D 1 1 = D1𝔸1
+type instance D 1 2 = D1𝔸2
+type instance D 1 3 = D1𝔸3
+type instance D 1 4 = D1𝔸4
 
-type instance D 2 ( ℝ 1 ) = D2𝔸1
-type instance D 2 ( ℝ 2 ) = D2𝔸2
-type instance D 2 ( ℝ 3 ) = D2𝔸3
-type instance D 2 ( ℝ 4 ) = D2𝔸4
+type instance D 2 1 = D2𝔸1
+type instance D 2 2 = D2𝔸2
+type instance D 2 3 = D2𝔸3
+type instance D 2 4 = D2𝔸4
 
-type instance D 3 ( ℝ 1 ) = D3𝔸1
-type instance D 3 ( ℝ 2 ) = D3𝔸2
-type instance D 3 ( ℝ 3 ) = D3𝔸3
-type instance D 3 ( ℝ 4 ) = D3𝔸4
+type instance D 3 1 = D3𝔸1
+type instance D 3 2 = D3𝔸2
+type instance D 3 3 = D3𝔸3
+type instance D 3 4 = D3𝔸4
 
 --------------------------------------------------------------------------------
 
 -- Weird instance needed in just one place;
 -- see use of chain in 'Math.Bezier.Stroke.brushStrokeData'.
-instance ( Applicative ( D k u ), Module r ( T v ) )
+instance ( Applicative ( D k ( Dim u ) ), Module r ( T v ) )
        => Module r ( T ( C k u v ) ) where
   origin = T $ D \ _ -> pure $ coerce $ origin @r @( T v )
   T ( D f ) ^+^ T ( D g ) = T $ D \ t -> liftA2 ( coerce $ (^+^) @r @( T v ) ) ( f t ) ( g t )
@@ -98,10 +103,10 @@ instance ( Applicative ( D k u ), Module r ( T v ) )
 -- with @D k v w@ in the middle, for any @r@-module @w@.
 class HasChainRule r k v where
   chain   :: Module r ( T w )
-          => D k ( ℝ 1 ) v -> D k v w -> D k ( ℝ 1 ) w
-  konst   :: AbelianGroup w => w -> D k v w
-  value   :: D k v w -> w
-  linearD :: Module r ( T w ) => ( v -> w ) -> v -> D k v w
+          => D k 1 v -> D k ( Dim v ) w -> D k 1 w
+  konst   :: AbelianGroup w => w -> D k ( Dim v ) w
+  value   :: D k ( Dim v ) w -> w
+  linearD :: Module r ( T w ) => ( v -> w ) -> v -> D k ( Dim v ) w
 
 linear :: forall k r v w
        .  ( HasChainRule r k v, Module r ( T w ) )
@@ -110,7 +115,7 @@ linear f = D \ x -> linearD @r @k @v @w f x
 
 chainRule :: forall r k u v w
           .  ( HasChainRule r k v, Module r ( T w )
-             , D k u ~ D k ( ℝ 1 ), HasChainRule r k u
+             , Dim u ~ 1, HasChainRule r k u
              )
           => C k u v -> C k v w -> C k u w
 chainRule ( D df ) ( D dg ) =
@@ -120,8 +125,8 @@ chainRule ( D df ) ( D dg ) =
         chain @r @k @v df_x ( dg $ value @r @k @u df_x )
 
 
-uncurryD2 :: D 2 a ~ D 2 ( ℝ 1 )
-          => D 2 ( ℝ 1 ) ( C 2 a b ) -> a -> D 2 ( ℝ 2 ) b
+uncurryD2 :: Dim a ~ 1
+          => D 2 1 ( C 2 a b ) -> a -> D 2 2 b
 uncurryD2 ( D21 ( D b_t0 ) ( T ( D dbdt_t0 ) ) ( T ( D d2bdt2_t0 ) ) ) s0 =
   let D21 b_t0s0 dbds_t0s0 d2bds2_t0s0 = b_t0 s0
       D21 dbdt_t0s0 d2bdtds_t0s0 _ = dbdt_t0 s0
@@ -131,8 +136,8 @@ uncurryD2 ( D21 ( D b_t0 ) ( T ( D dbdt_t0 ) ) ( T ( D d2bdt2_t0 ) ) ) s0 =
        ( T dbdt_t0s0 ) dbds_t0s0
        ( T d2bdt2_t0s0 ) d2bdtds_t0s0 d2bds2_t0s0
 
-uncurryD3 :: D 3 a ~ D 3 ( ℝ 1 )
-          => D 3 ( ℝ 1 ) ( C 3 a b ) -> a -> D 3 ( ℝ 2 ) b
+uncurryD3 :: Dim a ~ 1
+          => D 3 1 ( C 3 a b ) -> a -> D 3 2 b
 uncurryD3 ( D31 ( D b_t0 ) ( T ( D dbdt_t0 ) ) ( T ( D d2bdt2_t0 ) ) ( T ( D d3bdt3_t0 ) ) ) s0 =
   let D31 b_t0s0 dbds_t0s0 d2bds2_t0s0 d3bds3_t0s0 = b_t0 s0
       D31 dbdt_t0s0 d2bdtds_t0s0 d3bdtds2_t0s0 _ = dbdt_t0 s0
@@ -159,6 +164,7 @@ var i = D $ linearD @r @k @v ( `index` i )
 --------------------------------------------------------------------------------
 
 -- | Newtype for the module instance @Module r v => Module ( dr r ) ( dr v )@.
+type ApAp :: Type -> ( Type -> Type ) -> Type -> Type
 newtype ApAp r dr v = ApAp { unApAp :: dr v }
 
 instance ( Ring ( dr r ), Module r ( T v ), Applicative dr )
@@ -199,9 +205,9 @@ deriving via ApAp r D3𝔸4 v
 --------------------------------------------------------------------------------
 -- AbelianGroup instances
 
-newtype ApAp2 k u r = ApAp2 { unApAp2 :: D k u r }
+newtype ApAp2 k u r = ApAp2 { unApAp2 :: D k ( Dim u ) r }
 
-instance ( Applicative ( D k u )
+instance ( Applicative ( D k ( Dim u ) )
          , AbelianGroup r
          , HasChainRule Double k u
          ) => AbelianGroup ( ApAp2 k u r ) where
diff --git a/brush-strokes/src/lib/Math/Bezier/Stroke.hs b/brush-strokes/src/lib/Math/Bezier/Stroke.hs
index a7e0f20..0050081 100644
--- a/brush-strokes/src/lib/Math/Bezier/Stroke.hs
+++ b/brush-strokes/src/lib/Math/Bezier/Stroke.hs
@@ -62,7 +62,7 @@ import GHC.STRef
 import GHC.Generics
   ( Generic, Generic1, Generically(..) )
 import GHC.TypeNats
-  ( Nat, type (-) )
+  ( Nat )
 
 -- acts
 import Data.Act
@@ -213,7 +213,7 @@ data Cusp
   = Cusp
   { cuspParameters   :: !( ℝ 2 )
     -- ^ @(t,s)@ parameter values of the cusp
-  , cuspPathCoords   :: !( D 2 ( ℝ 1 ) ( ℝ 2 ) )
+  , cuspPathCoords   :: !( D 2 1 ( ℝ 2 ) )
     -- ^ path point coordinates and tangent
   , cuspStrokeCoords :: !( ℝ 2 )
     -- ^ brush stroke point coordinates
@@ -243,10 +243,11 @@ computeStrokeOutline ::
      , HasChainRule 𝕀 3 ( 𝕀ℝ nbUsedParams )
      , HasChainRule Double 2 ( ℝ nbBrushParams )
      , HasChainRule 𝕀 3 ( 𝕀ℝ nbBrushParams )
-     , Traversable ( D 2 ( ℝ nbBrushParams ) )
+     , Traversable ( D 2 nbBrushParams )
+     , Traversable ( D 3 nbBrushParams )
      , Representable Double ( ℝ nbUsedParams )
      , Representable 𝕀 ( 𝕀ℝ nbUsedParams )
-     , Module 𝕀 (T (𝕀ℝ nbUsedParams))
+     , Module 𝕀 (T ( 𝕀ℝ nbUsedParams ) )
 
      -- Debugging.
      , Show ptData, Show ( ℝ nbBrushParams )
@@ -526,8 +527,9 @@ outlineFunction
      , HasChainRule 𝕀 3 ( 𝕀ℝ nbUsedParams )
      , HasChainRule Double 2 ( ℝ nbBrushParams )
      , HasChainRule 𝕀 3 ( 𝕀ℝ nbBrushParams )
-     , Traversable ( D 2 ( ℝ nbBrushParams ) )
-     , Module 𝕀 (T (𝕀ℝ nbUsedParams))
+     , Traversable ( D 2 nbBrushParams )
+     , Traversable ( D 3 nbBrushParams )
+     , Module 𝕀 ( T ( 𝕀ℝ nbUsedParams ) )
 
      -- Computing AABBs
      , Representable Double ( ℝ nbUsedParams )
@@ -624,7 +626,6 @@ pathAndUsedParams :: forall k i (nbUsedParams :: Nat) arr crvData ptData
                   .  ( HasType ( ℝ 2 ) ptData
                      , HasBézier k i
                      , arr ~ C k
-                     , D k ( I i 1 ) ~ D k ( ℝ 1 )
                      , Module ( I i Double ) ( T ( I i 2 ) )
                      , Torsor ( T ( I i 2 ) ) ( I i 2 )
                      , Module ( I i Double ) ( T ( I i nbUsedParams ) )
@@ -955,7 +956,6 @@ withTangent tgt_wanted spline@( Spline { splineStart } )
 
 splineCurveFns :: forall k i
                .  ( HasBézier k i
-                  , D k ( I i 1 ) ~ D k ( ℝ 1 )
                   , Module ( I i Double ) ( T ( I i 2 ) )
                   , Torsor ( T ( I i 2 ) ) ( I i 2 ) )
                => ( I i 1 -> I i Double )
@@ -992,13 +992,11 @@ brushStrokeData :: forall {kd} (k :: Nat) (nbBrushParams :: Nat) (i :: kd) arr
                    , HasBézier k i, HasEnvelopeEquation k
                    , Differentiable k i nbBrushParams
                    , HasChainRule ( I i Double ) k ( I i 1 )
-                   , Applicative ( D k ( ℝ 1 ) )
+                   , Applicative ( D k 1 )
+                   , Dim ( I i 1 ) ~ 1
+                   , Dim ( I i nbBrushParams ) ~ nbBrushParams
+                   , Traversable ( D k nbBrushParams )
 
-                   , D ( k - 2 ) ( I i 2 ) ~ D ( k - 2 ) ( ℝ 2 )
-                   , D ( k - 1 ) ( I i 2 ) ~ D ( k - 1 ) ( ℝ 2 )
-                   , D k ( I i 1 ) ~ D k ( ℝ 1 )
-                   , D k ( I i 1 ) ~ D k ( ℝ 1 )
-                   , D k ( I i 2 ) ~ D k ( ℝ 2 )
                    , Transcendental ( I i Double )
                    , Module ( I i Double ) ( T ( I i 1 ) )
                    , Cross ( I i Double ) ( T ( I i 2 ) )
@@ -1020,24 +1018,24 @@ brushStrokeData :: forall {kd} (k :: Nat) (nbBrushParams :: Nat) (i :: kd) arr
 brushStrokeData co1 co2 path params brush mbBrushRotation =
   \ t ->
     let
-        dpath_t :: D k ( I i 1 ) ( I i 2 )
+        dpath_t :: D k 1 ( I i 2 )
         !dpath_t = runD path t
-        dparams_t :: D k ( I i 1 ) ( I i nbBrushParams )
+        dparams_t :: D k 1 ( I i nbBrushParams )
         !dparams_t = runD params t
-        dbrush_params :: D k ( I i nbBrushParams ) ( Spline Closed () ( I i 2 ) )
+        dbrush_params :: D k nbBrushParams ( Spline Closed () ( I i 2 ) )
         !dbrush_params = runD brush $ value @( I i Double ) @k @( I i 1 ) dparams_t
-        splines :: Seq ( D k ( I i nbBrushParams ) ( I i 1 `arr` I i 2 ) )
+        splines :: Seq ( D k nbBrushParams ( I i 1 `arr` I i 2 ) )
         !splines = getZipSeq $ traverse ( ZipSeq . splineCurveFns @k @i co2 ) dbrush_params
-        dbrushes_t :: Seq ( I i 1 -> D k ( I i 2 ) ( I i 2 ) )
+        dbrushes_t :: Seq ( I i 1 -> D k 2 ( I i 2 ) )
         !dbrushes_t = force $ fmap ( uncurryD @k . chain @( I i Double ) @k dparams_t ) splines
           -- This is the crucial use of the chain rule.
 
     in fmap ( mkStrokeDatum dpath_t dparams_t ) dbrushes_t
   where
 
-    mkStrokeDatum :: D k ( I i 1 ) ( I i 2 )
-                  -> D k ( I i 1 ) ( I i nbBrushParams )
-                  -> ( I i 1 -> D k ( I i 2 ) ( I i 2 ) )
+    mkStrokeDatum :: D k 1 ( I i 2 )
+                  -> D k 1 ( I i nbBrushParams )
+                  -> ( I i 1 -> D k 2 ( I i 2 ) )
                   -> ( I i 1 -> StrokeDatum k i )
     mkStrokeDatum dpath_t dparams_t dbrush_t s =
       let dbrush_t_s = dbrush_t s
diff --git a/brush-strokes/src/lib/Math/Bezier/Stroke/EnvelopeEquation.hs b/brush-strokes/src/lib/Math/Bezier/Stroke/EnvelopeEquation.hs
index 16b8f99..1eaca13 100644
--- a/brush-strokes/src/lib/Math/Bezier/Stroke/EnvelopeEquation.hs
+++ b/brush-strokes/src/lib/Math/Bezier/Stroke/EnvelopeEquation.hs
@@ -45,11 +45,11 @@ type StrokeDatum :: Nat -> k -> Type
 data StrokeDatum k i
   = StrokeDatum
   { -- | Path \( p(t) \).
-    dpath    :: D k ( I i 1 ) ( I i 2 )
+    dpath    :: D k 1 ( I i 2 )
     -- | Brush shape \( b(t, s) \).
-  , dbrush   :: D k ( I i 2 ) ( I i 2 )
+  , dbrush   :: D k 2 ( I i 2 )
     -- | (Optional) rotation angle \( \theta(t) \).
-  , mbRotation :: Maybe ( D k ( I i 1 ) ( I i Double ) )
+  , mbRotation :: Maybe ( D k 1 ( I i Double ) )
 
    -- Everything below is computed in terms of the first three fields.
 
@@ -58,19 +58,19 @@ data StrokeDatum k i
 
     -- | \( u(t,s) = R(-\theta(t)) \frac{\partial c}{\partial t} \),
     --   \( v(t,s) = R(-\theta(t)) \frac{\partial c}{\partial s} \)
-  , du, dv :: D ( k - 1 ) ( I i 2 ) ( I i 2 )
+  , du, dv :: D ( k - 1 ) 2 ( I i 2 )
 
     -- | Envelope function
     --
     -- \[ E(t_0,s_0) = \left ( \frac{\partial c}{\partial t} \times \frac{\partial c}{\partial s} \right )_{(t_0,s_0)}. \]
-  , ee       :: D ( k - 1 ) ( I i 2 ) ( I i 1 )
+  , ee       :: D ( k - 1 ) 2 ( I i 1 )
 
    -- \[ \frac{\partial E}{\partial s} \frac{\mathrm{d} c}{\mathrm{d} t}, \]
    --
    -- where \( \frac{\mathrm{d} c}{\mathrm{d} t} \)
    --
    -- denotes a total derivative.
-  , 𝛿E𝛿sdcdt :: D ( k - 2 ) ( I i 2 ) ( T ( I i 2 ) )
+  , 𝛿E𝛿sdcdt :: D ( k - 2 ) 2 ( T ( I i 2 ) )
   }
 
 deriving stock instance Show ( StrokeDatum 2 ℝ )
@@ -85,7 +85,6 @@ class HasBézier k i where
   line :: forall ( n :: Nat )
        .  ( Module Double ( T ( ℝ n ) ), Torsor ( T ( ℝ n ) ) ( ℝ n )
           , Module ( I i Double ) ( T ( I i n ) ), Torsor ( T ( I i n ) ) ( I i n )
-          , D k ( I i 1 ) ~ D k ( ℝ 1 )
           )
        => ( I i 1 -> I i Double )
        -> Segment ( I i n ) -> C k ( I i 1 ) ( I i n )
@@ -96,7 +95,6 @@ class HasBézier k i where
              , Module ( I i Double ) ( T ( I i n ) ), Torsor ( T ( I i n ) ) ( I i n )
              , Representable Double ( ℝ n )
              , Representable 𝕀 ( 𝕀ℝ n )
-             , D k ( I i 1 ) ~ D k ( ℝ 1 )
              )
           => ( I i 1 -> I i Double )
           -> Quadratic.Bezier ( I i n ) -> C k ( I i 1 ) ( I i n )
@@ -107,7 +105,6 @@ class HasBézier k i where
              , Module ( I i Double ) ( T ( I i n ) ), Torsor ( T ( I i n ) ) ( I i n )
              , Representable Double ( ℝ n )
              , Representable 𝕀 ( 𝕀ℝ n )
-             , D k ( I i 1 ) ~ D k ( ℝ 1 )
              )
           => ( I i 1 -> I i Double )
           -> Cubic.Bezier ( I i n ) -> C k ( I i 1 ) ( I i n )
@@ -115,8 +112,8 @@ class HasBézier k i where
 type HasEnvelopeEquation :: Nat -> Constraint
 class HasEnvelopeEquation k where
 
-  uncurryD :: D k a ~ D k ( ℝ 1 )
-           => D k ( ℝ 1 ) ( C k a b ) -> a -> D k ( ℝ 2 ) b
+  uncurryD :: Dim a ~ 1
+           => D k 1 ( C k a b ) -> a -> D k 2 b
 
   -- | The envelope function
   --
@@ -130,11 +127,7 @@ class HasEnvelopeEquation k where
   --
   -- denotes a total derivative.
   envelopeEquation :: forall i
-                   .  ( D ( k - 2 ) ( I i 2 ) ~ D ( k - 2 ) ( ℝ 2 )
-                      , D ( k - 1 ) ( I i 2 ) ~ D ( k - 1 ) ( ℝ 2 )
-                      , D k ( I i 2 ) ~ D k ( ℝ 2 )
-                      , D k ( I i 1 ) ~ D k ( ℝ 1 )
-                      , Module ( I i Double ) ( T ( I i 1 ) )
+                   .  ( Module ( I i Double ) ( T ( I i 1 ) )
                       , Cross ( I i Double ) ( T ( I i 2 ) )
                       , Transcendental ( I i Double )
                       , Representable ( I i Double ) ( I i 2 )
@@ -142,9 +135,9 @@ class HasEnvelopeEquation k where
                       )
                    => Proxy i
                    -> ( I i Double -> I i 1 )
-                   -> D k ( I i 1 ) ( I i 2 )
-                   -> D k ( I i 2 ) ( I i 2 )
-                   -> Maybe ( D k ( I i 1 ) ( I i Double ) )
+                   -> D k 1 ( I i 2 )
+                   -> D k 2 ( I i 2 )
+                   -> Maybe ( D k 1 ( I i Double ) )
                    -> StrokeDatum k i
 
 instance HasBézier 2 ℝ where
diff --git a/brush-strokes/src/lib/Math/Differentiable.hs b/brush-strokes/src/lib/Math/Differentiable.hs
index b6c102a..8c2c489 100644
--- a/brush-strokes/src/lib/Math/Differentiable.hs
+++ b/brush-strokes/src/lib/Math/Differentiable.hs
@@ -37,12 +37,12 @@ type Differentiable :: Nat -> k -> Nat -> Constraint
 class
   ( Module ( I i Double ) ( T ( I i u ) )
   , HasChainRule ( I i Double ) k ( I i u )
-  , Traversable ( D k ( I i u ) )
+  , Traversable ( D k u )
   ) => Differentiable k i u
 instance
   ( Module ( I i Double ) ( T ( I i u ) )
   , HasChainRule ( I i Double ) k ( I i u )
-  , Traversable ( D k ( I i u ) )
+  , Traversable ( D k u )
   ) => Differentiable k i u
 
 type DiffInterp :: Nat -> k -> Nat -> Constraint
@@ -50,10 +50,10 @@ class
   ( Differentiable k i u
   , Interpolatable ( I i Double ) ( I i u )
   , Module ( I i Double ) ( T ( I i Double ) )
-  , Module ( D k ( I i u ) ( I i Double ) )
-           ( D k ( I i u ) ( I i 2 ) )
-  , Transcendental ( D k ( I i u ) ( I i Double ) )
-  , Applicative ( D k ( I i u ) )
+  , Module ( D k u ( I i Double ) )
+           ( D k u ( I i 2 ) )
+  , Transcendental ( D k u ( I i Double ) )
+  , Applicative ( D k u )
   , Representable ( I i Double ) ( I i u )
   , RepDim ( I i u ) ~ RepDim u
   ) => DiffInterp k i u
@@ -61,10 +61,10 @@ instance
   ( Differentiable k i u
   , Interpolatable ( I i Double ) ( I i u )
   , Module ( I i Double ) ( T ( I i Double ) )
-  , Module ( D k ( I i u ) ( I i Double ) )
-           ( D k ( I i u ) ( I i 2 ) )
-  , Transcendental ( D k ( I i u ) ( I i Double ) )
-  , Applicative ( D k ( I i u ) )
+  , Module ( D k u ( I i Double ) )
+           ( D k u ( I i 2 ) )
+  , Transcendental ( D k u ( I i Double ) )
+  , Applicative ( D k u )
   , Representable ( I i Double ) ( I i u )
   , RepDim ( I i u ) ~ RepDim u
   ) => DiffInterp k i u
diff --git a/brush-strokes/src/lib/Math/Interval.hs b/brush-strokes/src/lib/Math/Interval.hs
index 203497e..46a587c 100644
--- a/brush-strokes/src/lib/Math/Interval.hs
+++ b/brush-strokes/src/lib/Math/Interval.hs
@@ -58,8 +58,7 @@ import Math.Ring
 --------------------------------------------------------------------------------
 -- Interval arithmetic.
 
-type instance D k 𝕀 = D k Double
-type instance D k ( 𝕀ℝ n ) = D k ( ℝ n )
+type instance Dim ( 𝕀ℝ n ) = n
 
 -- | Turn a non-decreasing function into a function on intervals.
 nonDecreasing :: forall n m
diff --git a/brush-strokes/src/lib/Math/Root/Isolation.hs b/brush-strokes/src/lib/Math/Root/Isolation.hs
index 51a9c76..6b62eec 100644
--- a/brush-strokes/src/lib/Math/Root/Isolation.hs
+++ b/brush-strokes/src/lib/Math/Root/Isolation.hs
@@ -188,7 +188,7 @@ isolateRootsIn
   .  BoxCt n d
   => RootIsolationOptions n d
       -- ^ configuration (which algorithms to use, and with what parameters)
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
       -- ^ equations to solve
   -> Box n
       -- ^ initial search domain
@@ -271,7 +271,7 @@ doStrategy
   .  RootIsolationAlgorithmWithOptions n d
   -> [ ( RootIsolationStep, Box n ) ]
   -> BoxHistory n
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
   -> Box n
   -> Writer ( DoneBoxes n )
             ( RootIsolationStep, [ Box n ] )
diff --git a/brush-strokes/src/lib/Math/Root/Isolation/Bisection.hs b/brush-strokes/src/lib/Math/Root/Isolation/Bisection.hs
index de4bc67..2bb3550 100644
--- a/brush-strokes/src/lib/Math/Root/Isolation/Bisection.hs
+++ b/brush-strokes/src/lib/Math/Root/Isolation/Bisection.hs
@@ -74,7 +74,7 @@ instance BoxCt n d => RootIsolationAlgorithm Bisection n d where
         :: RootIsolationAlgorithmOptions Bisection 2 3
         -> [ ( RootIsolationStep, Box 2 ) ]
         -> BoxHistory 2
-        -> ( 𝕀ℝ 2 -> D 1 ( 𝕀ℝ 2 ) ( 𝕀ℝ 3 ) )
+        -> ( 𝕀ℝ 2 -> D 1 2 ( 𝕀ℝ 3 ) )
         -> Box 2
         -> Writer ( DoneBoxes 2 ) ( StepDescription Bisection, [ Box 2 ] ) #-}
     -- NB: including this to be safe. The specialiser seems to sometimes
@@ -92,7 +92,7 @@ data BisectionOptions n d =
     --
     -- NB: only return 'False' if non-existence of solutions is guaranteed
     -- (otherwise, the root isolation algorithm might not be consistent).
-    canHaveSols :: !( ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) ) -> Box n -> Bool )
+    canHaveSols :: !( ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) ) -> Box n -> Bool )
     -- | Heuristic to choose which coordinate dimension to bisect.
     --
     -- It's only a fallback, as we prefer to bisect along coordinate dimensions
@@ -104,7 +104,7 @@ data BisectionOptions n d =
 type BisectionCoordPicker n d
   =  [ ( RootIsolationStep, Box n ) ]
   -> BoxHistory n
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
   -> forall r. ( NE.NonEmpty ( Fin n, r ) -> ( r, String ) )
 
 -- | Default options for the bisection method.
diff --git a/brush-strokes/src/lib/Math/Root/Isolation/Core.hs b/brush-strokes/src/lib/Math/Root/Isolation/Core.hs
index 16d5195..c750b99 100644
--- a/brush-strokes/src/lib/Math/Root/Isolation/Core.hs
+++ b/brush-strokes/src/lib/Math/Root/Isolation/Core.hs
@@ -98,9 +98,9 @@ type BoxCt n d =
   , Eq ( ℝ n )
   , Representable Double ( ℝ n )
   , Representable 𝕀 ( 𝕀ℝ n )
-  , MonomialBasis ( D 1 ( ℝ n ) )
-  , Deg ( D 1 ( ℝ n ) ) ~ 1
-  , Vars ( D 1 ( ℝ n ) ) ~ n
+  , MonomialBasis ( D 1 n )
+  , Deg ( D 1 n ) ~ 1
+  , Vars ( D 1 n ) ~ n
   , Module Double ( T ( ℝ n ) )
   , Module 𝕀 ( T ( 𝕀ℝ n ) )
   , NFData ( ℝ n )
@@ -181,7 +181,7 @@ class ( Typeable ty, Show ( StepDescription ty ), BoxCt n d )
         -- ^ history of the current round
     -> BoxHistory n
         -- ^ previous rounds history
-    -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+    -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
       -- ^ equations
     -> Box n
        -- ^ box
diff --git a/brush-strokes/src/lib/Math/Root/Isolation/Narrowing.hs b/brush-strokes/src/lib/Math/Root/Isolation/Narrowing.hs
index 5611e47..f2bd778 100644
--- a/brush-strokes/src/lib/Math/Root/Isolation/Narrowing.hs
+++ b/brush-strokes/src/lib/Math/Root/Isolation/Narrowing.hs
@@ -75,7 +75,7 @@ instance BoxCt n d => RootIsolationAlgorithm Box1 n d where
         :: RootIsolationAlgorithmOptions Box1 2 3
         -> [ ( RootIsolationStep, Box 2 ) ]
         -> BoxHistory 2
-        -> ( 𝕀ℝ 2 -> D 1 ( 𝕀ℝ 2 ) ( 𝕀ℝ 3 ) )
+        -> ( 𝕀ℝ 2 -> D 1 2 ( 𝕀ℝ 3 ) )
         -> Box 2
         -> Writer ( DoneBoxes 2 ) ( StepDescription Box1, [ Box 2 ] ) #-}
     -- NB: including this to be safe. The specialiser seems to sometimes
@@ -93,7 +93,7 @@ instance BoxCt n d => RootIsolationAlgorithm Box2 n d where
         :: RootIsolationAlgorithmOptions Box2 2 3
         -> [ ( RootIsolationStep, Box 2 ) ]
         -> BoxHistory 2
-        -> ( 𝕀ℝ 2 -> D 1 ( 𝕀ℝ 2 ) ( 𝕀ℝ 3 ) )
+        -> ( 𝕀ℝ 2 -> D 1 2 ( 𝕀ℝ 3 ) )
         -> Box 2
         -> Writer ( DoneBoxes 2 ) ( StepDescription Box2, [ Box 2 ] ) #-}
     -- NB: including this to be safe. The specialiser seems to sometimes
@@ -159,14 +159,14 @@ makeBox1Consistent
   :: ( KnownNat n
      , Representable Double ( ℝ n )
      , Representable 𝕀 ( 𝕀ℝ n )
-     , MonomialBasis ( D 1 ( ℝ n ) )
-     , Deg ( D 1 ( ℝ n ) ) ~ 1
-     , Vars ( D 1 ( ℝ n ) ) ~ n
+     , MonomialBasis ( D 1 n )
+     , Deg ( D 1 n ) ~ 1
+     , Vars ( D 1 n ) ~ n
      , Representable Double ( ℝ d )
      , Representable 𝕀 ( 𝕀ℝ d )
      )
   => Box1Options n d
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
   -> 𝕀ℝ n -> [ 𝕀ℝ n ]
 makeBox1Consistent box1Options eqs x =
   ( `State.evalState` False ) $
@@ -180,14 +180,14 @@ makeBox2Consistent
   .  ( KnownNat n
      , Representable Double ( ℝ n )
      , Representable 𝕀 ( 𝕀ℝ n )
-     , MonomialBasis ( D 1 ( ℝ n ) )
-     , Deg ( D 1 ( ℝ n ) ) ~ 1
-     , Vars ( D 1 ( ℝ n ) ) ~ n
+     , MonomialBasis ( D 1 n )
+     , Deg ( D 1 n ) ~ 1
+     , Vars ( D 1 n ) ~ n
      , Representable Double ( ℝ d )
      , Representable 𝕀 ( 𝕀ℝ d )
      )
   => Box2Options n d
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
   -> 𝕀ℝ n -> 𝕀ℝ n
 makeBox2Consistent (Box2Options box1Options ε_eq λMin) eqs x0
   = ( `State.evalState` False ) $ doLoop 0.25 x0
@@ -261,14 +261,14 @@ allNarrowingOperators
   .  ( KnownNat n
      , Representable Double ( ℝ n )
      , Representable 𝕀 ( 𝕀ℝ n )
-     , MonomialBasis ( D 1 ( ℝ n ) )
-     , Deg ( D 1 ( ℝ n ) ) ~ 1
-     , Vars ( D 1 ( ℝ n ) ) ~ n
+     , MonomialBasis ( D 1 n )
+     , Deg ( D 1 n ) ~ 1
+     , Vars ( D 1 n ) ~ n
      , Representable Double ( ℝ d )
      , Representable 𝕀 ( 𝕀ℝ d )
      )
   => Box1Options n d
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
   -> [ 𝕀ℝ n -> State Bool [ 𝕀ℝ n ] ]
 allNarrowingOperators ( Box1Options ε_eq ε_bis coordsToNarrow eqsToUse narrowingMethod ) eqs =
   [ \ cand ->
diff --git a/brush-strokes/src/lib/Math/Root/Isolation/Newton.hs b/brush-strokes/src/lib/Math/Root/Isolation/Newton.hs
index b14501a..215bb70 100644
--- a/brush-strokes/src/lib/Math/Root/Isolation/Newton.hs
+++ b/brush-strokes/src/lib/Math/Root/Isolation/Newton.hs
@@ -63,7 +63,7 @@ instance BoxCt n d => RootIsolationAlgorithm Newton n d where
         :: RootIsolationAlgorithmOptions Newton 2 3
         -> [ ( RootIsolationStep, Box 2 ) ]
         -> BoxHistory 2
-        -> ( 𝕀ℝ 2 -> D 1 ( 𝕀ℝ 2 ) ( 𝕀ℝ 3 ) )
+        -> ( 𝕀ℝ 2 -> D 1 2 ( 𝕀ℝ 3 ) )
         -> Box 2
         -> Writer ( DoneBoxes 2 ) ( StepDescription Newton, [ Box 2 ] ) #-}
     -- NB: including this to be safe. The specialiser seems to sometimes
@@ -100,7 +100,7 @@ intervalNewton
   :: forall n d
   .  BoxCt n d
   => NewtonOptions n d
-  -> ( 𝕀ℝ n -> D 1 ( 𝕀ℝ n ) ( 𝕀ℝ d ) )
+  -> ( 𝕀ℝ n -> D 1 n ( 𝕀ℝ d ) )
       -- ^ equations
   -> 𝕀ℝ n
      -- ^ box