A simple example demonstrating the importance of fusion would be the following set of data types:

data X : Nat -> Nat -> Type where
  MkX : X 42 m

data Y : Nat -> Nat -> Type where
  MkY : Y n 1337

data Z : Type where
  MkZ : (n : Nat) -> (m : Nat) -> X n m -> Y n m -> Z

Currently, the derived generator for Z would turn out to be grossly inefficient. There are two possible orderings of argument generation for constructor MkZ: X[], Y[0, 1] and Y[], X[0, 1], and either one is impractical to use.

However, this specific case could be solved with even the simplest fusion algorithm that works only on non-recursive data types. It would result in the following type:

XY : Nat -> Nat -> Type where
  MkXMkY : XY 42 1337

Which can be efficiently generated.

Just for a record, when you have the following data type definitions (based on the comment above)

data X : Nat -> Nat -> Type where
  MkX : X 42 m
  MkX2 : X n m
  MkX3 : X 42 24

data Y : Nat -> Nat -> Type where
  MkY : Y n 1337

data Z : Type where
  MkZ : (n : Nat) -> (m : Nat) -> X n m -> Y n m -> Z

having available the following (effective) generators

genX : Fuel -> Gen MaybeEmpty (n ** m ** X n m)
genXm : Fuel -> (m : Nat) -> Gen MaybeEmpty (n ** X n m)
genXnm : Fuel -> (n, m : Nat) -> Gen MaybeEmpty (X n m)

genY : Fuel -> Gen MaybeEmpty (n ** m ** Y n m)
genYn : Fuel -> (n : Nat) -> Gen MaybeEmpty (m ** Y n m)
genYnm : Fuel -> (n, m : Nat) -> Gen MaybeEmpty (Y n m)

currently we derive generator for Z which is equivalent to the following variant (using simplicifaction hack):

genZ : Fuel -> Gen MaybeEmpty Z
genZ fl = do
  (n ** m ** x) <- genX fl
  y <- genYnm fl n m
  pure $ MkZ n m x y

or, alternatively, this one

genZ' : Fuel -> Gen MaybeEmpty Z
genZ' fl = do
  (n ** m ** y) <- genY fl
  x <- genXnm fl n m
  pure $ MkZ n m x y

or alternative of both is simplification-hack option is turned off. Notice, that technically derived code is not the same, but it is equivalent for this particular example.

If we tries to use most effective subgenerators for both X and Y, we would run into a chicken and egg problem:

genZ'' : Fuel -> Gen MaybeEmpty Z
genZ'' fl = do
  (m ** y) <- genYn fl ?generated_below
  (n ** x) <- genXm fl m
  pure $ MkZ n m x ?y's_n_does_not_unify

So, what we could do is to employ the fusion. For this particular case, we can see than in the MkZ when using X and Y types, only two free variables are used, n and m, thus we can derive a fused data type indexed by them:

data XY : (n : Nat) -> (m : Nat) -> Type where
  MkX_MkY : XY 42 1337
  MkX2_MkY : XY n 1337

It contains a cartesian product of all the constructors that match each other (i.e. where actual indices unify with each other).

Also, we can derive the splitting function

splitXY : XY n m -> (X n m, Y n m)
splitXY MkX_MkY        = (MkX {m=1337}     , MkY {n=42})
splitXY (MkX2_MkY {n}) = (MkX2 {n} {m=1337}, MkY {n})

Thus, we can call usual derivation for the fused type:

genXY : Fuel -> Gen MaybeEmpty (n ** m ** XY n m)

and derive the following generator for Z:

genZ_ultimate : Fuel -> Gen MaybeEmpty Z
genZ_ultimate fl = do
  (n ** m ** xy) <- genXY fl
  let (x, y) = splitXY xy
  pure $ MkZ n m x y