I dislike this a lot but imo it's better than forcing 3 <= n constraint on the user.

Why not make it so that you create different circuits for different values of n? i.e.

stretchResetAsync clk en sn@SNat rst = rstOut
 where
  rstOut = case snatToInteger sn of
    0 -> rst
    1 -> unsafeToReset (delay clk en isActiveHigh (unsafeFromReset rst))
    _ -> unsafeToReset (if isActiveHigh then fmap (/=maxBound) counter else fmap (==maxBound) counter)

  counter :: Signal dom (Index n)
  counter = register clk rst en 0 (fmap (satSucc SatBound) counter)

  isActiveHigh = case resetPolarity @dom of { SActiveHigh -> True; _ -> False }

I explicitly left out the resetSynchronizer because the incoming reset should already be synchronously deasserted for the counter to work properly.

You need the reset synchronizer to stop the glitches as indicated by the comment in #3115 (comment)

I thought only one FF is enough though since there should be Recovery and Removal timing checks from the counter output FFs to the reset input. But I'm not 100% sure.

My reasoning for not being 100% sure is that the recovery and removal check only apply to the de-assertion path so timing closure will not ensure any glitch assertion will be safe with respect to recovery and removal checks.

In the linked comment you write assertion, but what you are describing is a glitch deassertion of the outgoing reset. Just FYI; I wondered if you got them mixed up.

You just need a simple register on the output to stop the glitching. So in that case rstOut would be something along the lines of:

case snatToInteger sn of
  0 -> rst
  1 -> unsafeToReset (register clk rst en isActiveHigh (pure (not isActiveHigh))
  _ -> unsafeToReset (register clk rst en isActiveHigh (if isActiveHigh then fmap (/=maxBound) counter else fmap (==maxBound) counter)

And even if the outer flop does go meta-stable because CLR/SET port is asserted later on the outer flop than the CLR/SET ports of the counter flops, the circuit will recover, because eventually the assertion will arrive at the CLR/SET port of the outer flop.

Also, if you want to use the standard dual FF reset synchronizer, that's fine by me. The only thing I care about is that stretchReset has a simple semantics. If I want the to stretch the deassertion of the reset by 1 cycle, it should just stretch the deassertion by 1 cycle, regardless of whether I have synchronous or asynchronous resets.

I think it's important that you can configure it precisely, to control the order in which stuff comes out of reset, but the ability to stretch by very small amounts seems less important (not sure, just can't think of a case where that'd matter much). So if it can't stretch by just 1 or 2 cycles, I think that'd be fine, but if you say n it should really mean n.

Yes indeed! I now am convinced that this is safe. I was thinking of a possibility where the rst source -> sync FF would be much slower than rst source -> counter FF -> comb logic -> sync FF could induce meta stability. But that's just a standard case with async resets and does not introduce problems since eventually everything will reset. I realized it when I drew it out.

I will update the code and doc. Thank you for the discussion!

This is solved now. Pleas re-review.