After tinkering with it a bit, I arrived at the following definition sketch:

data IVCCircuit a p i o = forall sp si it . IVCCircuit
  { ivcStep :: NoIVC a sp (si :*: it) sp si
  , ivcBoot :: NoIVC a (p :*: sp) (i :*: si) (o :*: si) (sp :*: (Infinite :.: it))
  }

data NoIVC a p i o q = NoIVC
  { noSystem :: [Constraint a i]
  , noRange :: Map a [SysVar i] -- no FoldVar's. Better to introduce a separate type
  , noWitness :: Map ByteString (CircuitWitness a p i)
  , noOutput :: o (Var a i)
  , noPayload :: forall w. isWitness a w => (p :*: i) w -> q w
  }

That is, all the folding in the circuit is performed with the ivcStep function. Operations outside of circuit are performed with the ivcBoot functions; this includes both preparation of inputs for the step function as well as post-processing of the results. Thanks to Haskell being lazy, witness computation would not get stuck as long as we preserve witnesses from the original circuit.

Also note that there should be no separate notion of "fold variables" in the end: once we compile to this form, results from folding are fed as input to the ivcBoot.

Functors describing the layout/payload of step function are hidden behind an existential because they cannot be known statically in advance. Most likely we would need some Haskell constraints on them, but I didn't explore it properly yet.

Makes sense and looks quite complicated at the same time :)

One thing that is definitely desired is for the step circuit's variables not to leak into the set of the enclosing circuit's variables.

The diagram for this circuit goes roughly like this: